[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
p q : Substructure L M
h : ↑p = ↑q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
q : Substructure L M
carrier✝ : Set M
fun_mem✝ : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f carrier✝
h : ↑{ carrier := carrier✝, fun_mem := fun_mem✝ } = ↑q
⊢ { carrier := carrier✝, fun_mem := fun_mem✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
carrier✝¹ : Set M
fun_mem✝¹ : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f carrier✝¹
carrier✝ : Set M
fun_mem✝ : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f carrier✝
h : ↑{ carrier := carrier✝¹, fun_mem := fun_mem✝¹ } = ↑{ carrier := carrier✝, fun_mem := fun_mem✝ }
⊢ { carrier := carrier✝¹, fun_mem := fun_mem✝¹ } = { carrier := carrier✝, fun_mem := fun_mem✝ }
[PROOFSTEP]
congr
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
α : Type u_3
t : Term L α
xs : α → M
h : ∀ (a : α), xs a ∈ S
⊢ realize xs t ∈ S
[PROOFSTEP]
induction' t with a n f ts ih
[GOAL]
case var
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
a : α
⊢ realize xs (var a) ∈ S
[PROOFSTEP]
exact h a
[GOAL]
case func
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
n : ℕ
f : Functions L n
ts : Fin n → Term L α
ih : ∀ (a : Fin n), realize xs (ts a) ∈ S
⊢ realize xs (func f ts) ∈ S
[PROOFSTEP]
exact Substructure.fun_mem _ _ _ ih
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set (Substructure L M)
n : ℕ
f : Functions L n
⊢ ∀ (s_1 : Set M), (s_1 ∈ Set.range fun t => ⋂ (_ : t ∈ s), ↑t) → ClosedUnder f s_1
[PROOFSTEP]
rintro _ ⟨t, rfl⟩
[GOAL]
case intro
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set (Substructure L M)
n : ℕ
f : Functions L n
t : Substructure L M
⊢ ClosedUnder f ((fun t => ⋂ (_ : t ∈ s), ↑t) t)
[PROOFSTEP]
by_cases h : t ∈ s
[GOAL]
case pos
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set (Substructure L M)
n : ℕ
f : Functions L n
t : Substructure L M
h : t ∈ s
⊢ ClosedUnder f ((fun t => ⋂ (_ : t ∈ s), ↑t) t)
[PROOFSTEP]
simpa [h] using t.fun_mem f
[GOAL]
case neg
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set (Substructure L M)
n : ℕ
f : Functions L n
t : Substructure L M
h : ¬t ∈ s
⊢ ClosedUnder f ((fun t => ⋂ (_ : t ∈ s), ↑t) t)
[PROOFSTEP]
simp [h]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
ι : Sort u_3
S : ι → Substructure L M
x : M
⊢ x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i
[PROOFSTEP]
simp only [iInf, mem_sInf, Set.forall_range_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
ι : Sort u_3
S : ι → Substructure L M
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
[PROOFSTEP]
simp only [iInf, coe_sInf, Set.biInter_range]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ ↑(LowerAdjoint.toFun (closure L) s) = range (Term.realize Subtype.val)
[PROOFSTEP]
let S : L.Substructure M :=
  ⟨range (Term.realize (L := L) ((↑) : s → M)), fun {n} f x hx =>
    by
    simp only [mem_range] at *
    refine' ⟨func f fun i => Classical.choose (hx i), _⟩
    simp only [Term.realize, fun i => Classical.choose_spec (hx i)]⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)
⊢ funMap f x ∈ range (Term.realize Subtype.val)
[PROOFSTEP]
simp only [mem_range] at *
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), ∃ y, Term.realize Subtype.val y = x i
⊢ ∃ y, Term.realize Subtype.val y = funMap f x
[PROOFSTEP]
refine' ⟨func f fun i => Classical.choose (hx i), _⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), ∃ y, Term.realize Subtype.val y = x i
⊢ Term.realize Subtype.val (func f fun i => Classical.choose (_ : ∃ y, Term.realize Subtype.val y = x i)) = funMap f x
[PROOFSTEP]
simp only [Term.realize, fun i => Classical.choose_spec (hx i)]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
⊢ ↑(LowerAdjoint.toFun (closure L) s) = range (Term.realize Subtype.val)
[PROOFSTEP]
change _ = (S : Set M)
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
⊢ ↑(LowerAdjoint.toFun (closure L) s) = ↑S
[PROOFSTEP]
rw [← SetLike.ext'_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
⊢ LowerAdjoint.toFun (closure L) s = S
[PROOFSTEP]
refine' closure_eq_of_le (fun x hx => ⟨var ⟨x, hx⟩, rfl⟩) (le_sInf fun S' hS' => _)
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
S' : Substructure L M
hS' : S' ∈ {S | s ⊆ ↑S}
⊢ S ≤ S'
[PROOFSTEP]
rintro _ ⟨t, rfl⟩
[GOAL]
case intro
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L M :=
  { carrier := range (Term.realize Subtype.val),
    fun_mem :=
      (_ :
        ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
          (∀ (i : Fin n), x i ∈ range (Term.realize Subtype.val)) → funMap f x ∈ range (Term.realize Subtype.val)) }
S' : Substructure L M
hS' : S' ∈ {S | s ⊆ ↑S}
t : Term L { x // x ∈ s }
⊢ Term.realize Subtype.val t ∈ S'
[PROOFSTEP]
exact t.realize_mem _ fun i => hS' i.2
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Small.{u, w} ↑s
⊢ Small.{u, w} { x // x ∈ LowerAdjoint.toFun (closure L) s }
[PROOFSTEP]
rw [← SetLike.coe_sort_coe, Substructure.coe_closure_eq_range_term_realize]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Small.{u, w} ↑s
⊢ Small.{u, w} ↑(range (Term.realize Subtype.val))
[PROOFSTEP]
exact small_range _
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
x : M
⊢ x ∈ LowerAdjoint.toFun (closure L) s ↔ ∃ t, Term.realize Subtype.val t = x
[PROOFSTEP]
rw [← SetLike.mem_coe, coe_closure_eq_range_term_realize, mem_range]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift #{ x // x ∈ LowerAdjoint.toFun (closure L) s } ≤ #(Term L ↑s)
[PROOFSTEP]
rw [← SetLike.coe_sort_coe, coe_closure_eq_range_term_realize]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift #↑(range (Term.realize Subtype.val)) ≤ #(Term L ↑s)
[PROOFSTEP]
rw [← Cardinal.lift_id'.{w, max u w} #(L.Term s)]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift #↑(range (Term.realize Subtype.val)) ≤ lift #(Term L ↑s)
[PROOFSTEP]
exact Cardinal.mk_range_le_lift
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift #{ x // x ∈ LowerAdjoint.toFun (closure L) s } ≤ max ℵ₀ (lift #↑s + lift #((i : ℕ) × Functions L i))
[PROOFSTEP]
rw [← lift_umax]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift #{ x // x ∈ LowerAdjoint.toFun (closure L) s } ≤ max ℵ₀ (lift #↑s + lift #((i : ℕ) × Functions L i))
[PROOFSTEP]
refine' lift_card_closure_le_card_term.trans (Term.card_le.trans _)
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ max ℵ₀ #(↑s ⊕ (i : ℕ) × Functions L i) ≤ max ℵ₀ (lift #↑s + lift #((i : ℕ) × Functions L i))
[PROOFSTEP]
rw [mk_sum, lift_umax.{w, u}]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Countable ((l : ℕ) × Functions L l)
h : Set.Countable s
⊢ Countable { x // x ∈ LowerAdjoint.toFun (closure L) s }
[PROOFSTEP]
haveI : Countable s := h.to_subtype
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Countable ((l : ℕ) × Functions L l)
h : Set.Countable s
this : Countable ↑s
⊢ Countable { x // x ∈ LowerAdjoint.toFun (closure L) s }
[PROOFSTEP]
rw [← mk_le_aleph0_iff, ← lift_le_aleph0]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Countable ((l : ℕ) × Functions L l)
h : Set.Countable s
this : Countable ↑s
⊢ lift #{ x // x ∈ LowerAdjoint.toFun (closure L) s } ≤ ℵ₀
[PROOFSTEP]
exact lift_card_closure_le_card_term.trans mk_le_aleph0
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ : Set M
p : M → Prop
x : M
s : Set M
hs : LowerAdjoint.toFun (closure L) s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f (setOf p)
⊢ p x
[PROOFSTEP]
have : ∀ x ∈ closure L s, p x := fun x hx => closure_induction hx Hs fun {n} => Hfun
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ : Set M
p : M → Prop
x : M
s : Set M
hs : LowerAdjoint.toFun (closure L) s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f (setOf p)
this : ∀ (x : M), x ∈ LowerAdjoint.toFun (closure L) s → p x
⊢ p x
[PROOFSTEP]
simpa [hs] using this x
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ Small.{u, w} { x // x ∈ ⊥ }
[PROOFSTEP]
rw [← closure_empty]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ Small.{u, w} { x // x ∈ LowerAdjoint.toFun (closure L) ∅ }
[PROOFSTEP]
haveI : Small.{u} (∅ : Set M) := small_subsingleton _
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
this : Small.{u, w} ↑∅
⊢ Small.{u, w} { x // x ∈ LowerAdjoint.toFun (closure L) ∅ }
[PROOFSTEP]
exact Substructure.small_closure
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
φ : M →[L] N
S : Substructure L N
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑φ ⁻¹' ↑S
⊢ funMap f x ∈ ↑φ ⁻¹' ↑S
[PROOFSTEP]
rw [mem_preimage, φ.map_fun]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
φ : M →[L] N
S : Substructure L N
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑φ ⁻¹' ↑S
⊢ funMap f (↑φ ∘ x) ∈ ↑S
[PROOFSTEP]
exact S.fun_mem f (φ ∘ x) hx
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
S : Substructure L P
⊢ ∀ (x : P), x ∈ comap (Hom.id L P) S ↔ x ∈ S
[PROOFSTEP]
simp
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
φ : M →[L] N
S : Substructure L M
n : ℕ
f : Functions L n
x : Fin n → N
hx : ∀ (i : Fin n), x i ∈ ↑φ '' ↑S
⊢ (fun a => ↑φ a) (funMap f fun i => Classical.choose (_ : x i ∈ ↑φ '' ↑S)) = funMap f x
[PROOFSTEP]
simp only [Hom.map_fun, SetLike.mem_coe]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
φ : M →[L] N
S : Substructure L M
n : ℕ
f : Functions L n
x : Fin n → N
hx : ∀ (i : Fin n), x i ∈ ↑φ '' ↑S
⊢ funMap f (↑φ ∘ fun i => Classical.choose (_ : ∃ x_1, (fun x_2 => x_2 ∈ S ∧ ↑φ x_2 = x i) x_1)) = funMap f x
[PROOFSTEP]
exact congr rfl (funext fun i => (Classical.choose_spec (hx i)).2)
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
ι : Type u_3
f : M →[L] N
hf : Function.Injective ↑f
S : Substructure L M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S
[PROOFSTEP]
simp [mem_comap, mem_map, hf.eq_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ : Substructure L M
s : Set M
ι : Type u_3
f : M →[L] N
hf : Function.Surjective ↑f
S : Substructure L N
x : N
h : x ∈ S
y : M
hy : ↑f y = x
⊢ y ∈ comap f S ∧ ↑f y = x
[PROOFSTEP]
simp [hy, h]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
m : { x // x ∈ ⊤ }
⊢ (fun m => { val := m, property := (_ : m ∈ ⊤) }) (↑(subtype ⊤) m) = m
[PROOFSTEP]
simp
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ s : Set M
p : (x : M) → x ∈ LowerAdjoint.toFun (closure L) s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(LowerAdjoint.toFun (closure L) s))
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f {x | ∃ hx, p x hx}
x : M
hx : x ∈ LowerAdjoint.toFun (closure L) s
⊢ p x hx
[PROOFSTEP]
refine' Exists.elim _ fun (hx : x ∈ closure L s) (hc : p x hx) => hc
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ s : Set M
p : (x : M) → x ∈ LowerAdjoint.toFun (closure L) s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x (_ : x ∈ ↑(LowerAdjoint.toFun (closure L) s))
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f {x | ∃ hx, p x hx}
x : M
hx : x ∈ LowerAdjoint.toFun (closure L) s
⊢ ∃ x_1, p x x_1
[PROOFSTEP]
exact closure_induction hx (fun x hx => ⟨subset_closure hx, Hs x hx⟩) @Hfun
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
S✝ : Substructure L M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
S : Substructure L' M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑S
⊢ funMap f x ∈ ↑S
[PROOFSTEP]
have h := S.fun_mem (φ.onFunction f) x hx
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
S✝ : Substructure L M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
S : Substructure L' M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑S
h : funMap (onFunction φ f) x ∈ ↑S
⊢ funMap f x ∈ ↑S
[PROOFSTEP]
simp only [LHom.map_onFunction, Substructure.mem_carrier] at h
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
S✝ : Substructure L M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
S : Substructure L' M
n : ℕ
f : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ ↑S
h : funMap f x ∈ S
⊢ funMap f x ∈ ↑S
[PROOFSTEP]
exact h
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
S✝ : Substructure L M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
S T : Substructure L' M
h :
  (fun S =>
        { carrier := ↑S,
          fun_mem := (_ : ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), (∀ (i : Fin n), x i ∈ ↑S) → funMap f x ∈ S) })
      S =
    (fun S =>
        { carrier := ↑S,
          fun_mem := (_ : ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), (∀ (i : Fin n), x i ∈ ↑S) → funMap f x ∈ S) })
      T
⊢ S = T
[PROOFSTEP]
simp only [SetLike.coe_set_eq, Substructure.mk.injEq] at h
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
S✝ : Substructure L M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
S T : Substructure L' M
h : S = T
⊢ S = T
[PROOFSTEP]
exact h
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
A : Set M
h : A ⊆ ↑S
n : ℕ
f : Functions (L[[↑A]]) n
⊢ ClosedUnder f ↑S
[PROOFSTEP]
cases' f with f f
[GOAL]
case inl
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
A : Set M
h : A ⊆ ↑S
n : ℕ
f : Functions L n
⊢ ClosedUnder (Sum.inl f) ↑S
[PROOFSTEP]
exact S.fun_mem f
[GOAL]
case inr
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
A : Set M
h : A ⊆ ↑S
n : ℕ
f : Functions (constantsOn ↑A) n
⊢ ClosedUnder (Sum.inr f) ↑S
[PROOFSTEP]
cases n
[GOAL]
case inr.zero
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
A : Set M
h : A ⊆ ↑S
f : Functions (constantsOn ↑A) Nat.zero
⊢ ClosedUnder (Sum.inr f) ↑S
[PROOFSTEP]
exact fun _ _ => h f.2
[GOAL]
case inr.succ
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
A : Set M
h : A ⊆ ↑S
n✝ : ℕ
f : Functions (constantsOn ↑A) (Nat.succ n✝)
⊢ ClosedUnder (Sum.inr f) ↑S
[PROOFSTEP]
exact isEmptyElim f
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ ↑(LHom.substructureReduct (lhomWithConstants L ↑A)) (withConstants S h) = S
[PROOFSTEP]
ext
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
x✝ : M
⊢ x✝ ∈ ↑(LHom.substructureReduct (lhomWithConstants L ↑A)) (withConstants S h) ↔ x✝ ∈ S
[PROOFSTEP]
simp
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ A ⊆ ↑(LowerAdjoint.toFun (closure (L[[↑A]])) s)
[PROOFSTEP]
intro a ha
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
a : M
ha : a ∈ A
⊢ a ∈ ↑(LowerAdjoint.toFun (closure (L[[↑A]])) s)
[PROOFSTEP]
simp only [SetLike.mem_coe]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
a : M
ha : a ∈ A
⊢ a ∈ LowerAdjoint.toFun (closure (L[[↑A]])) s
[PROOFSTEP]
let a' : L[[A]].Constants := Sum.inr ⟨a, ha⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
a : M
ha : a ∈ A
a' : Language.Constants (L[[↑A]]) := Sum.inr { val := a, property := ha }
⊢ a ∈ LowerAdjoint.toFun (closure (L[[↑A]])) s
[PROOFSTEP]
exact constants_mem a'
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ LowerAdjoint.toFun (closure (L[[↑A]])) s =
    withConstants (LowerAdjoint.toFun (closure L) (A ∪ s)) (_ : A ⊆ ↑(LowerAdjoint.toFun (closure L) (A ∪ s)))
[PROOFSTEP]
refine' closure_eq_of_le ((A.subset_union_right s).trans subset_closure) _
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ withConstants (LowerAdjoint.toFun (closure L) (A ∪ s)) (_ : A ⊆ ↑(LowerAdjoint.toFun (closure L) (A ∪ s))) ≤
    LowerAdjoint.toFun (closure (L[[↑A]])) s
[PROOFSTEP]
rw [← (L.lhomWithConstants A).substructureReduct.le_iff_le]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ ↑(LHom.substructureReduct (lhomWithConstants L ↑A))
      (withConstants (LowerAdjoint.toFun (closure L) (A ∪ s)) (_ : A ⊆ ↑(LowerAdjoint.toFun (closure L) (A ∪ s)))) ≤
    ↑(LHom.substructureReduct (lhomWithConstants L ↑A)) (LowerAdjoint.toFun (closure (L[[↑A]])) s)
[PROOFSTEP]
simp only [subset_closure, reduct_withConstants, closure_le, LHom.coe_substructureReduct, Set.union_subset_iff,
  and_true_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ A ⊆ ↑(LowerAdjoint.toFun (closure (L[[↑A]])) s)
[PROOFSTEP]
exact subset_closure_withConstants
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
p : Substructure L N
f✝ : M →[L] N
h : ∀ (c : M), ↑f✝ c ∈ p
n : ℕ
f : Functions L n
x : Fin n → M
⊢ (fun c => { val := ↑f✝ c, property := (_ : ↑f✝ c ∈ p) }) (funMap f x) =
    funMap f ((fun c => { val := ↑f✝ c, property := (_ : ↑f✝ c ∈ p) }) ∘ x)
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
⊢ range f = Substructure.map f ⊤
[PROOFSTEP]
ext
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
x✝ : N
⊢ x✝ ∈ range f ↔ x✝ ∈ Substructure.map f ⊤
[PROOFSTEP]
simp
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
⊢ range f = ⊤ ↔ Function.Surjective ↑f
[PROOFSTEP]
rw [SetLike.ext'_iff, range_coe, coe_top, Set.range_iff_surjective]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M →[L] N
p : Substructure L N
⊢ range f ≤ p ↔ comap f p = ⊤
[PROOFSTEP]
rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
⊢ funMap fn x ∈ {x | ↑f x = ↑g x}
[PROOFSTEP]
have h : f ∘ x = g ∘ x := by
  ext
  repeat' rw [Function.comp_apply]
  apply hx
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
⊢ ↑f ∘ x = ↑g ∘ x
[PROOFSTEP]
ext
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
x✝ : Fin n
⊢ (↑f ∘ x) x✝ = (↑g ∘ x) x✝
[PROOFSTEP]
repeat' rw [Function.comp_apply]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
x✝ : Fin n
⊢ (↑f ∘ x) x✝ = (↑g ∘ x) x✝
[PROOFSTEP]
rw [Function.comp_apply]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
x✝ : Fin n
⊢ ↑f (x x✝) = (↑g ∘ x) x✝
[PROOFSTEP]
rw [Function.comp_apply]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
x✝ : Fin n
⊢ ↑f (x x✝) = ↑g (x x✝)
[PROOFSTEP]
rw [Function.comp_apply]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
x✝ : Fin n
⊢ ↑f (x x✝) = ↑g (x x✝)
[PROOFSTEP]
apply hx
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f g : M →[L] N
n : ℕ
fn : Functions L n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | ↑f x = ↑g x}
h : ↑f ∘ x = ↑g ∘ x
⊢ funMap fn x ∈ {x | ↑f x = ↑g x}
[PROOFSTEP]
simp [h]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
p : Substructure L N
f : M ↪[L] N
h : ∀ (c : M), ↑f c ∈ p
n : ℕ
r : Relations L n
x : Fin n → M
⊢ RelMap r
      ({ toFun := ↑(Hom.codRestrict p (toHom f) h),
            inj' :=
              (_ :
                ∀ (a b : M), ↑(Hom.codRestrict p (toHom f) h) a = ↑(Hom.codRestrict p (toHom f) h) b → a = b) }.toFun ∘
        x) ↔
    RelMap r x
[PROOFSTEP]
simp only
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
p : Substructure L N
f : M ↪[L] N
h : ∀ (c : M), ↑f c ∈ p
n : ℕ
r : Relations L n
x : Fin n → M
⊢ RelMap r (↑(Hom.codRestrict p (toHom f) h) ∘ x) ↔ RelMap r x
[PROOFSTEP]
rw [← p.subtype.map_rel]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
p : Substructure L N
f : M ↪[L] N
h : ∀ (c : M), ↑f c ∈ p
n : ℕ
r : Relations L n
x : Fin n → M
⊢ RelMap r (↑(subtype p) ∘ ↑(Hom.codRestrict p (toHom f) h) ∘ x) ↔ RelMap r x
[PROOFSTEP]
change RelMap r (Hom.comp p.subtype.toHom (f.toHom.codRestrict p h) ∘ x) ↔ _
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
p : Substructure L N
f : M ↪[L] N
h : ∀ (c : M), ↑f c ∈ p
n : ℕ
r : Relations L n
x : Fin n → M
⊢ RelMap r (↑(Hom.comp (toHom (subtype p)) (Hom.codRestrict p (toHom f) h)) ∘ x) ↔ RelMap r x
[PROOFSTEP]
rw [Hom.subtype_comp_codRestrict, ← f.map_rel]
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
p : Substructure L N
f : M ↪[L] N
h : ∀ (c : M), ↑f c ∈ p
n : ℕ
r : Relations L n
x : Fin n → M
⊢ RelMap r (↑(toHom f) ∘ x) ↔ RelMap r (↑f ∘ x)
[PROOFSTEP]
rfl
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f✝ : M ↪[L] N
s : Substructure L M
n : ℕ
f : Functions L n
x : Fin n → { x // x ∈ s }
⊢ Equiv.toFun
      {
        toFun :=
          ↑(codRestrict (Substructure.map (toHom f✝) s) (domRestrict f✝ s)
              (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f✝ s) x ∈ Substructure.map (toHom f✝) s)),
        invFun := fun n =>
          { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s),
            property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s) ∈ ↑s) },
        left_inv :=
          (_ :
            ∀ (x : { x // x ∈ s }),
              (fun n =>
                    { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s),
                      property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s) ∈ ↑s) })
                  (↑(codRestrict (Substructure.map (toHom f✝) s) (domRestrict f✝ s)
                        (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f✝ s) x ∈ Substructure.map (toHom f✝) s))
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : { x // x ∈ Substructure.map (toHom f✝) s }),
              ↑(codRestrict (Substructure.map (toHom f✝) s) (domRestrict f✝ s)
                      (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f✝ s) x ∈ Substructure.map (toHom f✝) s))
                  ((fun n =>
                      { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s),
                        property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s) ∈ ↑s) })
                    x) =
                x) }
      (funMap f x) =
    funMap f
      ({
            toFun :=
              ↑(codRestrict (Substructure.map (toHom f✝) s) (domRestrict f✝ s)
                  (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f✝ s) x ∈ Substructure.map (toHom f✝) s)),
            invFun := fun n =>
              { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s),
                property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s) ∈ ↑s) },
            left_inv :=
              (_ :
                ∀ (x : { x // x ∈ s }),
                  (fun n =>
                        { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s),
                          property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s) ∈ ↑s) })
                      (↑(codRestrict (Substructure.map (toHom f✝) s) (domRestrict f✝ s)
                            (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f✝ s) x ∈ Substructure.map (toHom f✝) s))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : { x // x ∈ Substructure.map (toHom f✝) s }),
                  ↑(codRestrict (Substructure.map (toHom f✝) s) (domRestrict f✝ s)
                          (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f✝ s) x ∈ Substructure.map (toHom f✝) s))
                      ((fun n =>
                          { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s),
                            property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f✝) s) ∈ ↑s) })
                        x) =
                    x) }.toFun ∘
        x)
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ↪[L] N
s : Substructure L M
n : ℕ
R : Relations L n
x : Fin n → { x // x ∈ s }
⊢ RelMap R
      ({
            toFun :=
              ↑(codRestrict (Substructure.map (toHom f) s) (domRestrict f s)
                  (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f s) x ∈ Substructure.map (toHom f) s)),
            invFun := fun n =>
              { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f) s),
                property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f) s) ∈ ↑s) },
            left_inv :=
              (_ :
                ∀ (x : { x // x ∈ s }),
                  (fun n =>
                        { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f) s),
                          property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f) s) ∈ ↑s) })
                      (↑(codRestrict (Substructure.map (toHom f) s) (domRestrict f s)
                            (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f s) x ∈ Substructure.map (toHom f) s))
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : { x // x ∈ Substructure.map (toHom f) s }),
                  ↑(codRestrict (Substructure.map (toHom f) s) (domRestrict f s)
                          (_ : ∀ (x : { x // x ∈ s }), ↑(domRestrict f s) x ∈ Substructure.map (toHom f) s))
                      ((fun n =>
                          { val := Classical.choose (_ : ↑n ∈ Substructure.map (toHom f) s),
                            property := (_ : Classical.choose (_ : ↑n ∈ Substructure.map (toHom f) s) ∈ ↑s) })
                        x) =
                    x) }.toFun ∘
        x) ↔
    RelMap R x
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f✝ : M ↪[L] N
n : ℕ
f : Functions L n
x : Fin n → M
⊢ Equiv.toFun
      { toFun := ↑(codRestrict (Hom.range (toHom f✝)) f✝ (_ : ∀ (x : M), ↑(toHom f✝) x ∈ Hom.range (toHom f✝))),
        invFun := fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f✝)),
        left_inv :=
          (_ :
            ∀ (m : M),
              (fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f✝)))
                  (↑(codRestrict (Hom.range (toHom f✝)) f✝ (_ : ∀ (x : M), ↑(toHom f✝) x ∈ Hom.range (toHom f✝))) m) =
                m),
        right_inv :=
          (_ :
            ∀ (x : { x // x ∈ Hom.range (toHom f✝) }),
              ↑(codRestrict (Hom.range (toHom f✝)) f✝ (_ : ∀ (x : M), ↑(toHom f✝) x ∈ Hom.range (toHom f✝)))
                  ((fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f✝))) x) =
                x) }
      (funMap f x) =
    funMap f
      ({ toFun := ↑(codRestrict (Hom.range (toHom f✝)) f✝ (_ : ∀ (x : M), ↑(toHom f✝) x ∈ Hom.range (toHom f✝))),
            invFun := fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f✝)),
            left_inv :=
              (_ :
                ∀ (m : M),
                  (fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f✝)))
                      (↑(codRestrict (Hom.range (toHom f✝)) f✝ (_ : ∀ (x : M), ↑(toHom f✝) x ∈ Hom.range (toHom f✝)))
                        m) =
                    m),
            right_inv :=
              (_ :
                ∀ (x : { x // x ∈ Hom.range (toHom f✝) }),
                  ↑(codRestrict (Hom.range (toHom f✝)) f✝ (_ : ∀ (x : M), ↑(toHom f✝) x ∈ Hom.range (toHom f✝)))
                      ((fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f✝))) x) =
                    x) }.toFun ∘
        x)
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ↪[L] N
n : ℕ
R : Relations L n
x : Fin n → M
⊢ RelMap R
      ({ toFun := ↑(codRestrict (Hom.range (toHom f)) f (_ : ∀ (x : M), ↑(toHom f) x ∈ Hom.range (toHom f))),
            invFun := fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f)),
            left_inv :=
              (_ :
                ∀ (m : M),
                  (fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f)))
                      (↑(codRestrict (Hom.range (toHom f)) f (_ : ∀ (x : M), ↑(toHom f) x ∈ Hom.range (toHom f))) m) =
                    m),
            right_inv :=
              (_ :
                ∀ (x : { x // x ∈ Hom.range (toHom f) }),
                  ↑(codRestrict (Hom.range (toHom f)) f (_ : ∀ (x : M), ↑(toHom f) x ∈ Hom.range (toHom f)))
                      ((fun n => Classical.choose (_ : ↑n ∈ Hom.range (toHom f))) x) =
                    x) }.toFun ∘
        x) ↔
    RelMap R x
[PROOFSTEP]
aesop
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ≃[L] N
⊢ Hom.range (toHom f) = ⊤
[PROOFSTEP]
ext n
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ≃[L] N
n : N
⊢ n ∈ Hom.range (toHom f) ↔ n ∈ ⊤
[PROOFSTEP]
simp only [Hom.mem_range, coe_toHom, Substructure.mem_top, iff_true_iff]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
f : M ≃[L] N
n : N
⊢ ∃ y, ↑f y = n
[PROOFSTEP]
exact ⟨f.symm n, apply_symm_apply _ _⟩
[GOAL]
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
⊢ Hom.range (Embedding.toHom (subtype S)) = S
[PROOFSTEP]
ext x
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
x : M
⊢ x ∈ Hom.range (Embedding.toHom (subtype S)) ↔ x ∈ S
[PROOFSTEP]
simp only [Hom.mem_range, Embedding.coe_toHom, coeSubtype]
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
x : M
⊢ (∃ y, ↑y = x) ↔ x ∈ S
[PROOFSTEP]
refine' ⟨_, fun h => ⟨⟨x, h⟩, rfl⟩⟩
[GOAL]
case h
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
x : M
⊢ (∃ y, ↑y = x) → x ∈ S
[PROOFSTEP]
rintro ⟨⟨y, hy⟩, rfl⟩
[GOAL]
case h.intro.mk
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S✝ S : Substructure L M
y : M
hy : y ∈ S
⊢ ↑{ val := y, property := hy } ∈ S
[PROOFSTEP]
exact hy


[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
hSup : ∀ (s : Set α), (∀ (a : α), a ∈ s → p a) → p (sSup s)
⊢ p (↑lfp f)
[PROOFSTEP]
set s := {a | a ≤ lfp f ∧ p a}
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
hSup : ∀ (s : Set α), (∀ (a : α), a ∈ s → p a) → p (sSup s)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
⊢ p (↑lfp f)
[PROOFSTEP]
specialize hSup s fun a => And.right
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
⊢ p (↑lfp f)
[PROOFSTEP]
suffices : sSup s = lfp f
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
this : sSup s = ↑lfp f
⊢ p (↑lfp f)
case this
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
⊢ sSup s = ↑lfp f
[PROOFSTEP]
exact this ▸ hSup
[GOAL]
case this
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
⊢ sSup s = ↑lfp f
[PROOFSTEP]
have h : sSup s ≤ lfp f := sSup_le fun b => And.left
[GOAL]
case this
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ ↑lfp f
⊢ sSup s = ↑lfp f
[PROOFSTEP]
have hmem : f (sSup s) ∈ s := ⟨f.map_le_lfp h, step _ hSup h⟩
[GOAL]
case this
α : Type u
β : Type v
γ : Type w
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ ↑lfp f → p (↑f a)
s : Set α := {a | a ≤ ↑lfp f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ ↑lfp f
hmem : ↑f (sSup s) ∈ s
⊢ sSup s = ↑lfp f
[PROOFSTEP]
exact h.antisymm (f.lfp_le <| le_sSup hmem)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : β →o α
g : α →o β
h : α →o α →o α
⊢ ↑lfp (comp lfp h) = ↑lfp (onDiag h)
[PROOFSTEP]
let a := lfp (lfp.comp h)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : β →o α
g : α →o β
h : α →o α →o α
a : α := ↑lfp (comp lfp h)
⊢ ↑lfp (comp lfp h) = ↑lfp (onDiag h)
[PROOFSTEP]
refine' (lfp_le _ _).antisymm (lfp_le _ (Eq.le _))
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : β →o α
g : α →o β
h : α →o α →o α
a : α := ↑lfp (comp lfp h)
⊢ ↑(comp lfp h) (↑lfp (onDiag h)) ≤ ↑lfp (onDiag h)
[PROOFSTEP]
exact lfp_le _ h.onDiag.map_lfp.le
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : β →o α
g : α →o β
h : α →o α →o α
a : α := ↑lfp (comp lfp h)
⊢ ↑(onDiag h) (↑lfp (comp lfp h)) = ↑lfp (comp lfp h)
[PROOFSTEP]
have ha : (lfp ∘ h) a = a := (lfp.comp h).map_lfp
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : β →o α
g : α →o β
h : α →o α →o α
a : α := ↑lfp (comp lfp h)
ha : (↑lfp ∘ ↑h) a = a
⊢ ↑(onDiag h) (↑lfp (comp lfp h)) = ↑lfp (comp lfp h)
[PROOFSTEP]
calc
  h a a = h a (lfp (h a)) := congr_arg (h a) ha.symm
  _ = lfp (h a) := (h a).map_lfp
  _ = a := ha


[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Sup α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c
[PROOFSTEP]
show a ⊔ c = c
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Sup α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ a ⊔ c = c
[PROOFSTEP]
rw [← hbc, ← sup_assoc, hab]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Sup α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
hab : a ≤ b
hba : b ≤ a
⊢ a = b
[PROOFSTEP]
rwa [← hba, sup_comm]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Sup α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
⊢ a ⊔ (a ⊔ b) = a ⊔ b
[PROOFSTEP]
rw [← sup_assoc, sup_idem]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Sup α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b : α
⊢ b ⊔ (a ⊔ b) = a ⊔ b
[PROOFSTEP]
rw [sup_comm, sup_assoc, sup_idem]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Sup α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hac : a ≤ c
hbc : b ≤ c
⊢ a ⊔ b ≤ c
[PROOFSTEP]
show (a ⊔ b) ⊔ c = c
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Sup α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hac : a ≤ c
hbc : b ≤ c
⊢ a ⊔ b ⊔ c = c
[PROOFSTEP]
rwa [sup_assoc, hbc]
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ⊔ b ≤ a ∧ a ≤ a ⊔ b ↔ b ≤ a
[PROOFSTEP]
simp [le_rfl]
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ⊔ b ≤ b ∧ b ≤ a ⊔ b ↔ a ≤ b
[PROOFSTEP]
simp [le_rfl]
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ≤ b ↔ ∃ c, b = a ⊔ c
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ≤ b → ∃ c, b = a ⊔ c
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
h : a ≤ b
⊢ ∃ c, b = a ⊔ c
[PROOFSTEP]
exact ⟨b, (sup_eq_right.mpr h).symm⟩
[GOAL]
case mpr
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ (∃ c, b = a ⊔ c) → a ≤ b
[PROOFSTEP]
rintro ⟨c, rfl : _ = _ ⊔ _⟩
[GOAL]
case mpr.intro
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a c✝ d c : α
⊢ a ≤ a ⊔ c
[PROOFSTEP]
exact le_sup_left
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ⊔ a = a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ⊔ b = b ⊔ a
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ⊔ b ≤ b ⊔ a
[PROOFSTEP]
simp
[GOAL]
case a
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ b ⊔ a ≤ a ⊔ b
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d x : α
⊢ a ⊔ b ⊔ c ≤ x ↔ a ⊔ (b ⊔ c) ≤ x
[PROOFSTEP]
simp only [sup_le_iff]
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d x : α
⊢ (a ≤ x ∧ b ≤ x) ∧ c ≤ x ↔ a ≤ x ∧ b ≤ x ∧ c ≤ x
[PROOFSTEP]
rw [and_assoc]
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a✝ b✝ c✝ d a b c : α
⊢ a ⊔ b ⊔ c = c ⊔ b ⊔ a
[PROOFSTEP]
rw [sup_comm, @sup_comm _ _ a, sup_assoc]
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ⊔ (a ⊔ b) = a ⊔ b
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a b c d : α
⊢ a ⊔ b ⊔ b = a ⊔ b
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a✝ b✝ c✝ d a b c : α
⊢ a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)
[PROOFSTEP]
rw [← sup_assoc, ← sup_assoc, @sup_comm α _ a]
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a✝ b✝ c✝ d a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ b
[PROOFSTEP]
rw [sup_assoc, sup_assoc, @sup_comm _ _ b]
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a✝ b✝ c✝ d✝ a b c d : α
⊢ a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
[PROOFSTEP]
rw [sup_assoc, sup_left_comm b, ← sup_assoc]
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a✝ b✝ c✝ d a b c : α
⊢ a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)
[PROOFSTEP]
rw [sup_sup_sup_comm, sup_idem]
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeSup α
a✝ b✝ c✝ d a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)
[PROOFSTEP]
rw [sup_sup_sup_comm, sup_idem]
[GOAL]
α✝ : Type u
β : Type v
inst✝ : SemilatticeSup α✝
a b c✝ d : α✝
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ⊔ y ≤ c
[PROOFSTEP]
simp only [sup_le_iff]
[GOAL]
α✝ : Type u
β : Type v
inst✝ : SemilatticeSup α✝
a b c✝ d : α✝
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
[PROOFSTEP]
rw [← H, @sup_le_iff α A, H, H]
[GOAL]
α✝ : Type u
β : Type v
inst✝ : SemilatticeSup α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
[PROOFSTEP]
have ss : A.toSup = B.toSup := by ext; apply SemilatticeSup.ext_sup H
[GOAL]
α✝ : Type u
β : Type v
inst✝ : SemilatticeSup α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ toSup = toSup
[PROOFSTEP]
ext
[GOAL]
case sup.h.h
α✝ : Type u
β : Type v
inst✝ : SemilatticeSup α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝¹ x✝ : α
⊢ x✝¹ ⊔ x✝ = x✝¹ ⊔ x✝
[PROOFSTEP]
apply SemilatticeSup.ext_sup H
[GOAL]
α✝ : Type u
β : Type v
inst✝ : SemilatticeSup α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toSup = toSup
⊢ A = B
[PROOFSTEP]
cases A
[GOAL]
case mk
α✝ : Type u
β : Type v
inst✝ : SemilatticeSup α✝
a b c d : α✝
α : Type u_1
B : SemilatticeSup α
toSup✝ : Sup α
toPartialOrder✝ : PartialOrder α
le_sup_left✝ : ∀ (a b : α), a ≤ a ⊔ b
le_sup_right✝ : ∀ (a b : α), b ≤ a ⊔ b
sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toSup = toSup
⊢ mk le_sup_left✝ le_sup_right✝ sup_le✝ = B
[PROOFSTEP]
cases B
[GOAL]
case mk.mk
α✝ : Type u
β : Type v
inst✝ : SemilatticeSup α✝
a b c d : α✝
α : Type u_1
toSup✝¹ : Sup α
toPartialOrder✝¹ : PartialOrder α
le_sup_left✝¹ : ∀ (a b : α), a ≤ a ⊔ b
le_sup_right✝¹ : ∀ (a b : α), b ≤ a ⊔ b
sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
toSup✝ : Sup α
toPartialOrder✝ : PartialOrder α
le_sup_left✝ : ∀ (a b : α), a ≤ a ⊔ b
le_sup_right✝ : ∀ (a b : α), b ≤ a ⊔ b
sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toSup = toSup
⊢ mk le_sup_left✝¹ le_sup_right✝¹ sup_le✝¹ = mk le_sup_left✝ le_sup_right✝ sup_le✝
[PROOFSTEP]
cases PartialOrder.ext H
[GOAL]
case mk.mk.refl
α✝ : Type u
β : Type v
inst✝ : SemilatticeSup α✝
a b c d : α✝
α : Type u_1
toSup✝¹ : Sup α
toPartialOrder✝ : PartialOrder α
le_sup_left✝¹ : ∀ (a b : α), a ≤ a ⊔ b
le_sup_right✝¹ : ∀ (a b : α), b ≤ a ⊔ b
sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
toSup✝ : Sup α
le_sup_left✝ : ∀ (a b : α), a ≤ a ⊔ b
le_sup_right✝ : ∀ (a b : α), b ≤ a ⊔ b
sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toSup = toSup
⊢ mk le_sup_left✝¹ le_sup_right✝¹ sup_le✝¹ = mk le_sup_left✝ le_sup_right✝ sup_le✝
[PROOFSTEP]
congr
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeInf α
a b c d : α
⊢ a ⊓ b ≤ a ∧ a ≤ a ⊓ b ↔ a ≤ b
[PROOFSTEP]
simp [le_rfl]
[GOAL]
α : Type u
β : Type v
inst✝ : SemilatticeInf α
a b c d : α
⊢ a ⊓ b ≤ b ∧ b ≤ a ⊓ b ↔ b ≤ a
[PROOFSTEP]
simp [le_rfl]
[GOAL]
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c✝ d : α✝
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ c ≤ x ⊓ y ↔ c ≤ x ⊓ y
[PROOFSTEP]
simp only [le_inf_iff]
[GOAL]
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c✝ d : α✝
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ c ≤ x ⊓ y ↔ c ≤ x ∧ c ≤ y
[PROOFSTEP]
rw [← H, @le_inf_iff α A, H, H]
[GOAL]
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
[PROOFSTEP]
have ss : A.toInf = B.toInf := by ext; apply SemilatticeInf.ext_inf H
[GOAL]
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ toInf = toInf
[PROOFSTEP]
ext
[GOAL]
case inf.h.h
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝¹ x✝ : α
⊢ x✝¹ ⊓ x✝ = x✝¹ ⊓ x✝
[PROOFSTEP]
apply SemilatticeInf.ext_inf H
[GOAL]
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toInf = toInf
⊢ A = B
[PROOFSTEP]
cases A
[GOAL]
case mk
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
B : SemilatticeInf α
toInf✝ : Inf α
toPartialOrder✝ : PartialOrder α
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toInf = toInf
⊢ mk inf_le_left✝ inf_le_right✝ le_inf✝ = B
[PROOFSTEP]
cases B
[GOAL]
case mk.mk
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
toInf✝¹ : Inf α
toPartialOrder✝¹ : PartialOrder α
inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
toInf✝ : Inf α
toPartialOrder✝ : PartialOrder α
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toInf = toInf
⊢ mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
[PROOFSTEP]
cases PartialOrder.ext H
[GOAL]
case mk.mk.refl
α✝ : Type u
β : Type v
inst✝ : SemilatticeInf α✝
a b c d : α✝
α : Type u_1
toInf✝¹ : Inf α
toPartialOrder✝ : PartialOrder α
inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
toInf✝ : Inf α
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
ss : toInf = toInf
⊢ mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
[PROOFSTEP]
congr
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Inf α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
⊢ SemilatticeInf α
[PROOFSTEP]
haveI : SemilatticeSup αᵒᵈ := SemilatticeSup.mk' inf_comm inf_assoc inf_idem
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Inf α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
this : SemilatticeSup αᵒᵈ
⊢ SemilatticeInf α
[PROOFSTEP]
haveI i := OrderDual.semilatticeInf αᵒᵈ
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Inf α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
this : SemilatticeSup αᵒᵈ
i : SemilatticeInf αᵒᵈᵒᵈ
⊢ SemilatticeInf α
[PROOFSTEP]
exact i
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Sup α
inst✝ : Inf α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : a ⊔ b = b
⊢ b ⊓ a = a
[PROOFSTEP]
rw [← h, inf_comm, inf_sup_self]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Sup α
inst✝ : Inf α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : b ⊓ a = a
⊢ a ⊔ b = b
[PROOFSTEP]
rw [← h, sup_comm, sup_inf_self]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Sup α
inst✝ : Inf α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
b : α
⊢ b ⊔ b = b ⊔ b ⊓ (b ⊔ b)
[PROOFSTEP]
rw [inf_sup_self]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Sup α
inst✝ : Inf α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
b : α
⊢ b ⊔ b ⊓ (b ⊔ b) = b
[PROOFSTEP]
rw [sup_inf_self]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Sup α
inst✝ : Inf α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
b : α
⊢ b ⊓ b = b ⊓ (b ⊔ b ⊓ b)
[PROOFSTEP]
rw [sup_inf_self]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Sup α
inst✝ : Inf α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
b : α
⊢ b ⊓ (b ⊔ b ⊓ b) = b
[PROOFSTEP]
rw [inf_sup_self]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Sup α
inst✝ : Inf α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : SemilatticeSup.toPartialOrder = SemilatticeInf.toPartialOrder
a b : α
⊢ a ⊓ b ≤ a
[PROOFSTEP]
rw [partial_order_eq]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Sup α
inst✝ : Inf α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : SemilatticeSup.toPartialOrder = SemilatticeInf.toPartialOrder
a b : α
⊢ a ⊓ b ≤ a
[PROOFSTEP]
apply inf_le_left
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Sup α
inst✝ : Inf α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : SemilatticeSup.toPartialOrder = SemilatticeInf.toPartialOrder
a b : α
⊢ a ⊓ b ≤ b
[PROOFSTEP]
rw [partial_order_eq]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Sup α
inst✝ : Inf α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : SemilatticeSup.toPartialOrder = SemilatticeInf.toPartialOrder
a b : α
⊢ a ⊓ b ≤ b
[PROOFSTEP]
apply inf_le_right
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Sup α
inst✝ : Inf α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : SemilatticeSup.toPartialOrder = SemilatticeInf.toPartialOrder
a b c : α
⊢ a ≤ b → a ≤ c → a ≤ b ⊓ c
[PROOFSTEP]
rw [partial_order_eq]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Sup α
inst✝ : Inf α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : SemilatticeSup.toPartialOrder = SemilatticeInf.toPartialOrder
a b c : α
⊢ a ≤ b → a ≤ c → a ≤ b ⊓ c
[PROOFSTEP]
apply le_inf
[GOAL]
α : Type u
β : Type v
inst✝ : Lattice α
a b c d : α
⊢ a ⊔ b ≤ a ⊓ b ↔ a = b
[PROOFSTEP]
simp [le_antisymm_iff, and_comm]
[GOAL]
α : Type u
β : Type v
inst✝ : Lattice α
a b c d : α
⊢ a ⊓ b = a ⊔ b ↔ a = b
[PROOFSTEP]
rw [← inf_le_sup.ge_iff_eq, sup_le_inf]
[GOAL]
α : Type u
β : Type v
inst✝ : Lattice α
a b c d : α
⊢ a ⊓ b < a ⊔ b ↔ a ≠ b
[PROOFSTEP]
rw [inf_le_sup.lt_iff_ne, Ne.def, inf_eq_sup]
[GOAL]
α : Type u
β : Type v
inst✝ : Lattice α
a b c d : α
⊢ a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c
[PROOFSTEP]
refine' ⟨fun h ↦ _, _⟩
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : Lattice α
a b c d : α
h : a ⊓ b = c ∧ a ⊔ b = c
⊢ a = c ∧ b = c
case refine'_2 α : Type u β : Type v inst✝ : Lattice α a b c d : α ⊢ a = c ∧ b = c → a ⊓ b = c ∧ a ⊔ b = c
[PROOFSTEP]
{ obtain rfl := sup_eq_inf.1 (h.2.trans h.1.symm)
  simpa using h
}
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : Lattice α
a b c d : α
h : a ⊓ b = c ∧ a ⊔ b = c
⊢ a = c ∧ b = c
[PROOFSTEP]
obtain rfl := sup_eq_inf.1 (h.2.trans h.1.symm)
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : Lattice α
a c d : α
h : a ⊓ a = c ∧ a ⊔ a = c
⊢ a = c ∧ a = c
[PROOFSTEP]
simpa using h
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : Lattice α
a b c d : α
⊢ a = c ∧ b = c → a ⊓ b = c ∧ a ⊔ b = c
[PROOFSTEP]
{ rintro ⟨rfl, rfl⟩
  exact ⟨inf_idem, sup_idem⟩
}
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : Lattice α
a b c d : α
⊢ a = c ∧ b = c → a ⊓ b = c ∧ a ⊔ b = c
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case refine'_2.intro
α : Type u
β : Type v
inst✝ : Lattice α
b d : α
⊢ b ⊓ b = b ∧ b ⊔ b = b
[PROOFSTEP]
exact ⟨inf_idem, sup_idem⟩
[GOAL]
α : Type u
β : Type v
inst✝ : Lattice α
a b c d : α
⊢ a ⊓ (a ⊔ b) = a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝ : Lattice α
a b c d : α
⊢ a ⊔ a ⊓ b = a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝ : Lattice α
a b c d : α
⊢ a ⊔ b = b ↔ a ⊓ b = a
[PROOFSTEP]
rw [sup_eq_right, ← inf_eq_left]
[GOAL]
α✝ : Type u
β : Type v
inst✝ : Lattice α✝
a b c d : α✝
α : Type u_1
A B : Lattice α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
[PROOFSTEP]
cases A
[GOAL]
case mk
α✝ : Type u
β : Type v
inst✝ : Lattice α✝
a b c d : α✝
α : Type u_1
B : Lattice α
toSemilatticeSup✝ : SemilatticeSup α
toInf✝ : Inf α
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ mk inf_le_left✝ inf_le_right✝ le_inf✝ = B
[PROOFSTEP]
cases B
[GOAL]
case mk.mk
α✝ : Type u
β : Type v
inst✝ : Lattice α✝
a b c d : α✝
α : Type u_1
toSemilatticeSup✝¹ : SemilatticeSup α
toInf✝¹ : Inf α
inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
toSemilatticeSup✝ : SemilatticeSup α
toInf✝ : Inf α
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
[PROOFSTEP]
cases SemilatticeSup.ext H
[GOAL]
case mk.mk.refl
α✝ : Type u
β : Type v
inst✝ : Lattice α✝
a b c d : α✝
α : Type u_1
toSemilatticeSup✝ : SemilatticeSup α
toInf✝¹ : Inf α
inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
toInf✝ : Inf α
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
[PROOFSTEP]
cases SemilatticeInf.ext H
[GOAL]
case mk.mk.refl.refl
α✝ : Type u
β : Type v
inst✝ : Lattice α✝
a b c d : α✝
α : Type u_1
toSemilatticeSup✝ : SemilatticeSup α
toInf✝ : Inf α
inf_le_left✝¹ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝¹ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝¹ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
inf_le_left✝ : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right✝ : ∀ (a b : α), a ⊓ b ≤ b
le_inf✝ : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ mk inf_le_left✝¹ inf_le_right✝¹ le_inf✝¹ = mk inf_le_left✝ inf_le_right✝ le_inf✝
[PROOFSTEP]
congr
[GOAL]
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
⊢ y ⊓ z ⊔ x = (y ⊔ x) ⊓ (z ⊔ x)
[PROOFSTEP]
simp only [sup_inf_left, fun y : α => @sup_comm α _ y x, eq_self_iff_true]
[GOAL]
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
⊢ x ⊓ (y ⊔ z) = x ⊓ (x ⊔ z) ⊓ (y ⊔ z)
[PROOFSTEP]
rw [inf_sup_self]
[GOAL]
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
⊢ x ⊓ (x ⊔ z) ⊓ (y ⊔ z) = x ⊓ (x ⊓ y ⊔ z)
[PROOFSTEP]
simp only [inf_assoc, sup_inf_right, eq_self_iff_true]
[GOAL]
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
⊢ x ⊓ (x ⊓ y ⊔ z) = (x ⊔ x ⊓ y) ⊓ (x ⊓ y ⊔ z)
[PROOFSTEP]
rw [sup_inf_self]
[GOAL]
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
⊢ (x ⊔ x ⊓ y) ⊓ (x ⊓ y ⊔ z) = (x ⊓ y ⊔ x) ⊓ (x ⊓ y ⊔ z)
[PROOFSTEP]
rw [sup_comm]
[GOAL]
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
⊢ (x ⊓ y ⊔ x) ⊓ (x ⊓ y ⊔ z) = x ⊓ y ⊔ x ⊓ z
[PROOFSTEP]
rw [sup_inf_left]
[GOAL]
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
⊢ (y ⊔ z) ⊓ x = y ⊓ x ⊔ z ⊓ x
[PROOFSTEP]
simp only [inf_sup_left, fun y : α => @inf_comm α _ y x, eq_self_iff_true]
[GOAL]
α : Type u
β : Type v
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ y ⊓ z ⊔ x = (y ⊔ x) ⊓ (x ⊔ z)
[PROOFSTEP]
rw [sup_inf_right, @sup_comm _ _ x]
[GOAL]
α : Type u
β : Type v
inst✝ : LinearOrder α
a✝ b✝ c d a b : α
p : α → Prop
ha : p a
hb : p b
h : a ≤ b
⊢ p (a ⊔ b)
[PROOFSTEP]
rwa [sup_eq_right.2 h]
[GOAL]
α : Type u
β : Type v
inst✝ : LinearOrder α
a✝ b✝ c d a b : α
p : α → Prop
ha : p a
hb : p b
h : b ≤ a
⊢ p (a ⊔ b)
[PROOFSTEP]
rwa [sup_eq_left.2 h]
[GOAL]
α : Type u
β : Type v
inst✝ : LinearOrder α
a b c d : α
⊢ a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c
[PROOFSTEP]
exact
  ⟨fun h => (le_total c b).imp (fun bc => by rwa [sup_eq_left.2 bc] at h ) (fun bc => by rwa [sup_eq_right.2 bc] at h ),
    fun h => h.elim le_sup_of_le_left le_sup_of_le_right⟩
[GOAL]
α : Type u
β : Type v
inst✝ : LinearOrder α
a b c d : α
h : a ≤ b ⊔ c
bc : c ≤ b
⊢ a ≤ b
[PROOFSTEP]
rwa [sup_eq_left.2 bc] at h
[GOAL]
α : Type u
β : Type v
inst✝ : LinearOrder α
a b c d : α
h : a ≤ b ⊔ c
bc : b ≤ c
⊢ a ≤ c
[PROOFSTEP]
rwa [sup_eq_right.2 bc] at h
[GOAL]
α : Type u
β : Type v
inst✝ : LinearOrder α
a b c d : α
⊢ a < b ⊔ c ↔ a < b ∨ a < c
[PROOFSTEP]
exact
  ⟨fun h => (le_total c b).imp (fun bc => by rwa [sup_eq_left.2 bc] at h ) (fun bc => by rwa [sup_eq_right.2 bc] at h ),
    fun h => h.elim lt_sup_of_lt_left lt_sup_of_lt_right⟩
[GOAL]
α : Type u
β : Type v
inst✝ : LinearOrder α
a b c d : α
h : a < b ⊔ c
bc : c ≤ b
⊢ a < b
[PROOFSTEP]
rwa [sup_eq_left.2 bc] at h
[GOAL]
α : Type u
β : Type v
inst✝ : LinearOrder α
a b c d : α
h : a < b ⊔ c
bc : b ≤ c
⊢ a < c
[PROOFSTEP]
rwa [sup_eq_right.2 bc] at h
[GOAL]
α : Type u
β : Type v
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
⊢ (fun x x_1 => x ⊔ x_1) = maxDefault
[PROOFSTEP]
ext x y
[GOAL]
case h.h
α : Type u
β : Type v
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
⊢ x ⊔ y = maxDefault x y
[PROOFSTEP]
unfold maxDefault
[GOAL]
case h.h
α : Type u
β : Type v
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
⊢ x ⊔ y = if x ≤ y then y else x
[PROOFSTEP]
split_ifs with h'
[GOAL]
case pos
α : Type u
β : Type v
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
h' : x ≤ y
⊢ x ⊔ y = y
case neg
α : Type u
β : Type v
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
h' : ¬x ≤ y
⊢ x ⊔ y = x
[PROOFSTEP]
exacts [sup_of_le_right h', sup_of_le_left $ (total_of (· ≤ ·) x y).resolve_left h']
[GOAL]
α : Type u
β : Type v
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
⊢ (fun x x_1 => x ⊓ x_1) = minDefault
[PROOFSTEP]
ext x y
[GOAL]
case h.h
α : Type u
β : Type v
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
⊢ x ⊓ y = minDefault x y
[PROOFSTEP]
unfold minDefault
[GOAL]
case h.h
α : Type u
β : Type v
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
⊢ x ⊓ y = if x ≤ y then x else y
[PROOFSTEP]
split_ifs with h'
[GOAL]
case pos
α : Type u
β : Type v
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
h' : x ≤ y
⊢ x ⊓ y = x
case neg
α : Type u
β : Type v
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
x y : α
h' : ¬x ≤ y
⊢ x ⊓ y = y
[PROOFSTEP]
exacts [inf_of_le_left h', inf_of_le_right $ (total_of (· ≤ ·) x y).resolve_left h']
[GOAL]
α✝ : Type u
β : Type v
α : Type u
inst✝⁴ : Lattice α
inst✝³ : DecidableEq α
inst✝² : DecidableRel fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
src✝ : Lattice α := inst✝⁴
⊢ ∀ (a b : α), min a b = if a ≤ b then a else b
[PROOFSTEP]
exact congr_fun₂ inf_eq_minDefault
[GOAL]
α✝ : Type u
β : Type v
α : Type u
inst✝⁴ : Lattice α
inst✝³ : DecidableEq α
inst✝² : DecidableRel fun x x_1 => x ≤ x_1
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
src✝ : Lattice α := inst✝⁴
⊢ ∀ (a b : α), max a b = if a ≤ b then b else a
[PROOFSTEP]
exact congr_fun₂ sup_eq_maxDefault
[GOAL]
α : Type u
β : Type v
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
⊢ update f i (a ⊔ b) j = (update f i a ⊔ update f i b) j
[PROOFSTEP]
obtain rfl | hji := eq_or_ne j i
[GOAL]
case inl
α : Type u
β : Type v
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
j : ι
a b : π j
⊢ update f j (a ⊔ b) j = (update f j a ⊔ update f j b) j
[PROOFSTEP]
simp [update_noteq, *]
[GOAL]
case inr
α : Type u
β : Type v
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
hji : j ≠ i
⊢ update f i (a ⊔ b) j = (update f i a ⊔ update f i b) j
[PROOFSTEP]
simp [update_noteq, *]
[GOAL]
α : Type u
β : Type v
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeInf (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
⊢ update f i (a ⊓ b) j = (update f i a ⊓ update f i b) j
[PROOFSTEP]
obtain rfl | hji := eq_or_ne j i
[GOAL]
case inl
α : Type u
β : Type v
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeInf (π i)
f : (i : ι) → π i
j : ι
a b : π j
⊢ update f j (a ⊓ b) j = (update f j a ⊓ update f j b) j
[PROOFSTEP]
simp [update_noteq, *]
[GOAL]
case inr
α : Type u
β : Type v
ι : Type u_1
π : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → SemilatticeInf (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
hji : j ≠ i
⊢ update f i (a ⊓ b) j = (update f i a ⊓ update f i b) j
[PROOFSTEP]
simp [update_noteq, *]
[GOAL]
α : Type u
β : Type v
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α → β
h : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
x y : α
hxy : x ≤ y
⊢ f x ⊓ f y = f x
[PROOFSTEP]
rw [← h, inf_eq_left.2 hxy]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ f (x ⊔ y) = f x ⊔ f y
[PROOFSTEP]
simp only [h, hf h, sup_of_le_right]
[GOAL]
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
f : α → β
hf : Monotone f
x y : α
h : y ≤ x
⊢ f (x ⊔ y) = f x ⊔ f y
[PROOFSTEP]
simp only [h, hf h, sup_of_le_left]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b : α
⊢ a ≤ a ⊔ b
[PROOFSTEP]
change f a ≤ f (a ⊔ b)
[GOAL]
α : Type u
β : Type v
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b : α
⊢ f a ≤ f (a ⊔ b)
[PROOFSTEP]
rw [map_sup]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b : α
⊢ f a ≤ f a ⊔ f b
[PROOFSTEP]
exact le_sup_left
[GOAL]
α : Type u
β : Type v
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b : α
⊢ b ≤ a ⊔ b
[PROOFSTEP]
change f b ≤ f (a ⊔ b)
[GOAL]
α : Type u
β : Type v
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b : α
⊢ f b ≤ f (a ⊔ b)
[PROOFSTEP]
rw [map_sup]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b : α
⊢ f b ≤ f a ⊔ f b
[PROOFSTEP]
exact le_sup_right
[GOAL]
α : Type u
β : Type v
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b c : α
ha : a ≤ c
hb : b ≤ c
⊢ a ⊔ b ≤ c
[PROOFSTEP]
change f (a ⊔ b) ≤ f c
[GOAL]
α : Type u
β : Type v
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b c : α
ha : a ≤ c
hb : b ≤ c
⊢ f (a ⊔ b) ≤ f c
[PROOFSTEP]
rw [map_sup]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Sup α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b c : α
ha : a ≤ c
hb : b ≤ c
⊢ f a ⊔ f b ≤ f c
[PROOFSTEP]
exact sup_le ha hb
[GOAL]
α : Type u
β : Type v
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f : α → β
hf_inj : Injective f
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b : α
⊢ a ⊓ b ≤ a
[PROOFSTEP]
change f (a ⊓ b) ≤ f a
[GOAL]
α : Type u
β : Type v
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f : α → β
hf_inj : Injective f
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b : α
⊢ f (a ⊓ b) ≤ f a
[PROOFSTEP]
rw [map_inf]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f : α → β
hf_inj : Injective f
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b : α
⊢ f a ⊓ f b ≤ f a
[PROOFSTEP]
exact inf_le_left
[GOAL]
α : Type u
β : Type v
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f : α → β
hf_inj : Injective f
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b : α
⊢ a ⊓ b ≤ b
[PROOFSTEP]
change f (a ⊓ b) ≤ f b
[GOAL]
α : Type u
β : Type v
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f : α → β
hf_inj : Injective f
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b : α
⊢ f (a ⊓ b) ≤ f b
[PROOFSTEP]
rw [map_inf]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f : α → β
hf_inj : Injective f
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b : α
⊢ f a ⊓ f b ≤ f b
[PROOFSTEP]
exact inf_le_right
[GOAL]
α : Type u
β : Type v
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f : α → β
hf_inj : Injective f
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b c : α
ha : a ≤ b
hb : a ≤ c
⊢ a ≤ b ⊓ c
[PROOFSTEP]
change f a ≤ f (b ⊓ c)
[GOAL]
α : Type u
β : Type v
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f : α → β
hf_inj : Injective f
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b c : α
ha : a ≤ b
hb : a ≤ c
⊢ f a ≤ f (b ⊓ c)
[PROOFSTEP]
rw [map_inf]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Inf α
inst✝ : SemilatticeInf β
f : α → β
hf_inj : Injective f
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
src✝ : PartialOrder α := PartialOrder.lift f hf_inj
a b c : α
ha : a ≤ b
hb : a ≤ c
⊢ f a ≤ f b ⊓ f c
[PROOFSTEP]
exact le_inf ha hb
[GOAL]
α : Type u
β : Type v
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : DistribLattice β
f : α → β
hf_inj : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
src✝ : Lattice α := Injective.lattice f hf_inj map_sup map_inf
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
[PROOFSTEP]
change f ((a ⊔ b) ⊓ (a ⊔ c)) ≤ f (a ⊔ b ⊓ c)
[GOAL]
α : Type u
β : Type v
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : DistribLattice β
f : α → β
hf_inj : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
src✝ : Lattice α := Injective.lattice f hf_inj map_sup map_inf
a b c : α
⊢ f ((a ⊔ b) ⊓ (a ⊔ c)) ≤ f (a ⊔ b ⊓ c)
[PROOFSTEP]
rw [map_inf, map_sup, map_sup, map_sup, map_inf]
[GOAL]
α : Type u
β : Type v
inst✝² : Sup α
inst✝¹ : Inf α
inst✝ : DistribLattice β
f : α → β
hf_inj : Injective f
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
src✝ : Lattice α := Injective.lattice f hf_inj map_sup map_inf
a b c : α
⊢ (f a ⊔ f b) ⊓ (f a ⊔ f c) ≤ f a ⊔ f b ⊓ f c
[PROOFSTEP]
exact le_sup_inf


[GOAL]
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
n : ℕ
inst✝ : GradeMinOrder (Fin n) α
a : Fin n
h : IsMin a
⊢ IsMin ↑a
[PROOFSTEP]
cases n
[GOAL]
case zero
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : GradeMinOrder (Fin zero) α
a : Fin zero
h : IsMin a
⊢ IsMin ↑a
[PROOFSTEP]
exact a.elim0
[GOAL]
case succ
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
n✝ : ℕ
inst✝ : GradeMinOrder (Fin (succ n✝)) α
a : Fin (succ n✝)
h : IsMin a
⊢ IsMin ↑a
[PROOFSTEP]
rw [h.eq_bot, Fin.bot_eq_zero]
[GOAL]
case succ
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
n✝ : ℕ
inst✝ : GradeMinOrder (Fin (succ n✝)) α
a : Fin (succ n✝)
h : IsMin a
⊢ IsMin ↑0
[PROOFSTEP]
exact isMin_bot


[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsRefl α r
inst✝ : IsAntisymm α r
a b : α
⊢ a = b → r a b ∧ r b a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsRefl α r
inst✝ : IsAntisymm α r
a : α
⊢ r a a ∧ r a a
[PROOFSTEP]
exact ⟨refl _, refl _⟩
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsTrichotomous α r
a b : α
⊢ Function.swap r a b ∨ a = b ∨ Function.swap r b a
[PROOFSTEP]
simpa [Function.swap, or_comm, or_left_comm] using trichotomous_of r a b
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝¹ : IsIrrefl α r
inst✝ : Subsingleton α
⊢ ∀ (a b : α), r a b = EmptyRelation a b
[PROOFSTEP]
simpa using not_rel_of_subsingleton r
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
⊢ ¬r b a → r b c → r a c
[PROOFSTEP]
intro h₁ h₂
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : ¬r b a
h₂ : r b c
⊢ r a c
[PROOFSTEP]
rcases trichotomous_of r a b with (h₃ | rfl | h₃)
[GOAL]
case inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r a b
⊢ r a c
case inr.inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a c : α
h₁ : ¬r a a
h₂ : r a c
⊢ r a c
case inr.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c
[PROOFSTEP]
exacts [_root_.trans h₃ h₂, h₂, absurd h₃ h₁]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
⊢ r a b → ¬r c b → r a c
[PROOFSTEP]
intro h₁ h₂
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : r a b
h₂ : ¬r c b
⊢ r a c
[PROOFSTEP]
rcases trichotomous_of r b c with (h₃ | rfl | h₃)
[GOAL]
case inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r b c
⊢ r a c
case inr.inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b : α
h₁ : r a b
h₂ : ¬r b b
⊢ r a b
case inr.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c
[PROOFSTEP]
exacts [_root_.trans h₁ h₃, h₁, absurd h₃ h₂]
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : x < y
e : y = x
⊢ False
[PROOFSTEP]
rw [e] at h
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : x < x
e : y = x
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsOrderConnected α r
a b c : α
h₁ : ¬r a b
h₂ : ¬r b c
⊢ ¬(r a b ∨ r b c)
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
α✝ : Type u
β : Type v
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
α : Type ?u.14854
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ IsTrichotomous α r
[PROOFSTEP]
infer_instance
  -- see Note [lower instance priority]
[GOAL]
α✝ : Type u
β : Type v
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
α : Type ?u.14937
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ IsTrans α r
[PROOFSTEP]
infer_instance
  -- see Note [lower instance priority]
[GOAL]
α✝ : Type u
β : Type v
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
α : Type ?u.15023
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ IsIrrefl α r
[PROOFSTEP]
infer_instance
  -- see Note [lower instance priority]
[GOAL]
α✝ : Type u
β : Type v
r✝ : α✝ → α✝ → Prop
s : β → β → Prop
α : Type ?u.15135
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ IsAsymm α r
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
a b c : α × β
h₁ : Prod.Lex r s a b
h₂ : Prod.Lex r s b c
⊢ Prod.Lex r s a c
[PROOFSTEP]
cases' h₁ with a₁ a₂ b₁ b₂ ab a₁ b₁ b₂ ab
[GOAL]
case left
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : α × β
a₁ : α
a₂ : β
b₁ : α
b₂ : β
ab : r a₁ b₁
h₂ : Prod.Lex r s (b₁, b₂) c
⊢ Prod.Lex r s (a₁, a₂) c
[PROOFSTEP]
cases' h₂ with _ _ c₁ c₂ bc _ _ c₂ bc
[GOAL]
case right
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : α × β
a₁ : α
b₁ b₂ : β
ab : s b₁ b₂
h₂ : Prod.Lex r s (a₁, b₂) c
⊢ Prod.Lex r s (a₁, b₁) c
[PROOFSTEP]
cases' h₂ with _ _ c₁ c₂ bc _ _ c₂ bc
[GOAL]
case left.left
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
a₁ : α
a₂ : β
b₁ : α
b₂ : β
ab : r a₁ b₁
c₁ : α
c₂ : β
bc : r b₁ c₁
⊢ Prod.Lex r s (a₁, a₂) (c₁, c₂)
case left.right
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
a₁ : α
a₂ : β
b₁ : α
b₂ : β
ab : r a₁ b₁
c₂ : β
bc : s b₂ c₂
⊢ Prod.Lex r s (a₁, a₂) (b₁, c₂)
case right.left
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
a₁ : α
b₁ b₂ : β
ab : s b₁ b₂
c₁ : α
c₂ : β
bc : r a₁ c₁
⊢ Prod.Lex r s (a₁, b₁) (c₁, c₂)
case right.right
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
a₁ : α
b₁ b₂ : β
ab : s b₁ b₂
c₂ : β
bc : s b₂ c₂
⊢ Prod.Lex r s (a₁, b₁) (a₁, c₂)
[PROOFSTEP]
exacts [.left _ _ (_root_.trans ab bc), .left _ _ ab, .left _ _ bc, .right _ (_root_.trans ab bc)]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
refine @Subrelation.wf (α × β) (Prod.Lex (· < ·) (· < ·)) (· < ·) ?_ IsWellFounded.wf
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
⊢ Subrelation (fun x x_1 => x < x_1) (Prod.Lex (fun x x_1 => x < x_1) fun x x_1 => x < x_1)
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ w
[GOAL]
case mk.mk
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
w : (a₁, b₁) < (a₂, b₂)
⊢ Prod.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
simp only [Prod.mk_lt_mk] at w
[GOAL]
case mk.mk
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
w : a₁ < a₂ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₂ ∧ b₁ < b₂
⊢ Prod.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
rcases eq_or_ne a₁ a₂ with rfl | ha
[GOAL]
case mk.mk.inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ b₂ : β
w : a₁ < a₁ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₁ ∧ b₁ < b₂
⊢ Prod.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (a₁, b₁) (a₁, b₂)
[PROOFSTEP]
right
[GOAL]
case mk.mk.inl.h
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ b₂ : β
w : a₁ < a₁ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₁ ∧ b₁ < b₂
⊢ b₁ < b₂
[PROOFSTEP]
simpa using w
[GOAL]
case mk.mk.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
w : a₁ < a₂ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₂ ∧ b₁ < b₂
ha : a₁ ≠ a₂
⊢ Prod.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
left
[GOAL]
case mk.mk.inr.h
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
w : a₁ < a₂ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₂ ∧ b₁ < b₂
ha : a₁ ≠ a₂
⊢ a₁ < a₂
[PROOFSTEP]
rcases w with ⟨a_lt, _⟩ | ⟨a_le, _⟩
[GOAL]
case mk.mk.inr.h.inl.intro
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
ha : a₁ ≠ a₂
a_lt : a₁ < a₂
right✝ : b₁ ≤ b₂
⊢ a₁ < a₂
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.inr.h.inr.intro
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : PartialOrder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
ha : a₁ ≠ a₂
a_le : a₁ ≤ a₂
right✝ : b₁ < b₂
⊢ a₁ < a₂
[PROOFSTEP]
exact Ne.lt_of_le ha a_le
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s✝ : β → β → Prop
r : α → α → Prop
s : Set α
⊢ ¬Bounded r s ↔ Unbounded r s
[PROOFSTEP]
simp only [Bounded, Unbounded, not_forall, not_exists, exists_prop, not_and, not_not]
[GOAL]
α : Type u
β : Type v
r✝ : α → α → Prop
s✝ : β → β → Prop
r : α → α → Prop
s : Set α
⊢ ¬Unbounded r s ↔ Bounded r s
[PROOFSTEP]
rw [not_iff_comm, not_bounded_iff]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : HasSubset α
a b c : α
hab : a = b
hbc : b ⊆ c
⊢ a ⊆ c
[PROOFSTEP]
rwa [hab]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : HasSubset α
a b c : α
hab : a ⊆ b
hbc : b = c
⊢ a ⊆ c
[PROOFSTEP]
rwa [← hbc]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : HasSSubset α
a b c : α
hab : a = b
hbc : b ⊂ c
⊢ a ⊂ c
[PROOFSTEP]
rwa [hab]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : HasSSubset α
a b c : α
hab : a ⊂ b
hbc : b = c
⊢ a ⊂ c
[PROOFSTEP]
rwa [← hbc]
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : LinearOrder α
⊢ IsOrderConnected α fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : LinearOrder α
⊢ IsIncompTrans α fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : LinearOrder α
⊢ IsStrictWeakOrder α fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance