confusion in using rw

Stream: new members

[Chengyan Hu]

I'm trying to prove this example in problem sheet.
I hope to use rw[sym_sup] only on the right hand side of h2, to exchange a\inf b and a, however it really seems what I'm doing is wrong and I have no idea.
image.png

[Ruben Van de Velde]

I suggest you share a #mwe

[Chengyan Hu]

Sincerely apologize for that! I just hoped to share what lean said as well. Here it is:
import Mathlib.Tactic
variable (L : Type) [Lattice L]

theorem sym_sup (a b:L): a⊔b=b⊔a := by

apply le_antisymm

· exact sup_le le_sup_right le_sup_left

· exact sup_le le_sup_right le_sup_left

theorem sym_inf (a b:L): a⊓b=b⊓a := by

apply le_antisymm

· exact le_inf inf_le_right inf_le_left

· exact le_inf inf_le_right inf_le_left

example (L : Type) [Lattice L] :

(∀ a b c : L, a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)) ↔ ∀ a b c : L, a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c := by

constructor

· rintro h1 a b c

have h2:=h1

specialize h2 (a⊓b) a c

rw [← sym_sup (a⊓b) a] at h2

[Chengyan Hu]

import Mathlib.Tactic
variable (L : Type) [Lattice L]

theorem sym_sup (a b:L): a⊔b=b⊔a := by

apply le_antisymm

· exact sup_le le_sup_right le_sup_left

· exact sup_le le_sup_right le_sup_left

theorem sym_inf (a b:L): a⊓b=b⊓a := by

apply le_antisymm

· exact le_inf inf_le_right inf_le_left

· exact le_inf inf_le_right inf_le_left

example (L : Type) [Lattice L] :

(∀ a b c : L, a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)) ↔ ∀ a b c : L, a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c := by

constructor

· rintro h1 a b c

have h2:=h1

specialize h2 (a⊓b) a c

rw [← sym_sup (a⊓b) a] at h2

[Bjørn Kjos-Hanssen]

Looks like you have to give L as another input to sym_sup. So like this:

import Mathlib.Tactic
variable (L : Type) [Lattice L]

theorem sym_sup (a b:L): a⊔b=b⊔a := by
  apply le_antisymm
  · exact sup_le le_sup_right le_sup_left
  · exact sup_le le_sup_right le_sup_left

theorem sym_inf (a b:L): a⊓b=b⊓a := by
  apply le_antisymm
  · exact le_inf inf_le_right inf_le_left
  · exact le_inf inf_le_right inf_le_left

example (L : Type) [Lattice L] :
(∀ a b c : L, a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)) ↔ ∀ a b c : L, a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c := by
  constructor
  · rintro h1 a b c
    have h2:=h1
    specialize h2 (a⊓b) a c
    have := sym_sup L (a ⊓ b) a
    rw [this] at h2
    sorry

[Philippe Duchon]

The standard thing would be to make L an implicit parameter, by having {L : Type} in the Variable declaration; this makes it implicit in sym_sup and sym_inf.

[Kevin Buzzard]

@Chengyan Hu check out the part of the course notes about brackets to understand the difference between (L : Type) and {L : Type}. And checkout out #backticks for how to post code on Zulip (but it looks like you already figured it out).

[Chengyan Hu]

Ahhh, I see! Thank you so much!