[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : sSupHomClass F α β
f : F
g : ι → α
⊢ ↑f (⨆ (i : ι), g i) = ⨆ (i : ι), ↑f (g i)
[PROOFSTEP]
simp [iSup, ← Set.range_comp, Function.comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : sSupHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ ↑f (⨆ (i : ι) (j : κ i), g i j) = ⨆ (i : ι) (j : κ i), ↑f (g i j)
[PROOFSTEP]
simp_rw [map_iSup]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : InfSet α
inst✝¹ : InfSet β
inst✝ : sInfHomClass F α β
f : F
g : ι → α
⊢ ↑f (⨅ (i : ι), g i) = ⨅ (i : ι), ↑f (g i)
[PROOFSTEP]
simp [iInf, ← Set.range_comp, Function.comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : InfSet α
inst✝¹ : InfSet β
inst✝ : sInfHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ ↑f (⨅ (i : ι) (j : κ i), g i j) = ⨅ (i : ι) (j : κ i), ↑f (g i j)
[PROOFSTEP]
simp_rw [map_iInf]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
src✝ : sSupHomClass F α β := inst✝
f : F
a b : α
⊢ ↑f (a ⊔ b) = ↑f a ⊔ ↑f b
[PROOFSTEP]
rw [← sSup_pair, map_sSup]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
src✝ : sSupHomClass F α β := inst✝
f : F
a b : α
⊢ sSup (↑f '' {a, b}) = ↑f a ⊔ ↑f b
[PROOFSTEP]
simp only [Set.image_pair, sSup_insert, sSup_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
src✝ : sSupHomClass F α β := inst✝
f : F
⊢ ↑f ⊥ = ⊥
[PROOFSTEP]
rw [← sSup_empty, map_sSup, Set.image_empty]
  -- Porting note: rw [sSup_empty] does not work, but exact sSup_empty does?
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
src✝ : sSupHomClass F α β := inst✝
f : F
⊢ sSup ∅ = ⊥
[PROOFSTEP]
exact sSup_empty
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sInfHomClass F α β
src✝ : sInfHomClass F α β := inst✝
f : F
a b : α
⊢ ↑f (a ⊓ b) = ↑f a ⊓ ↑f b
[PROOFSTEP]
rw [← sInf_pair, map_sInf, Set.image_pair]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sInfHomClass F α β
src✝ : sInfHomClass F α β := inst✝
f : F
a b : α
⊢ sInf {↑f a, ↑f b} = ↑f a ⊓ ↑f b
[PROOFSTEP]
simp only [Set.image_pair, sInf_insert, sInf_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sInfHomClass F α β
src✝ : sInfHomClass F α β := inst✝
f : F
⊢ ↑f ⊤ = ⊤
[PROOFSTEP]
rw [← sInf_empty, map_sInf, Set.image_empty]
  -- Porting note: rw [sInf_empty] does not work, but exact sInf_empty does?
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sInfHomClass F α β
src✝ : sInfHomClass F α β := inst✝
f : F
⊢ sInf ∅ = ⊤
[PROOFSTEP]
exact sInf_empty
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : OrderIsoClass F α β
src✝ : OrderHomClass F α β :=
  let_fun this := inferInstance;
  this
f : F
s : Set α
c : (fun x => β) (sSup s)
⊢ ↑f (sSup s) ≤ c ↔ sSup (↑f '' s) ≤ c
[PROOFSTEP]
simp only [← le_map_inv_iff, sSup_le_iff, Set.ball_image_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : OrderIsoClass F α β
src✝ : OrderHomClass F α β :=
  let_fun this := inferInstance;
  this
f : F
s : Set α
c : (fun x => β) (sInf s)
⊢ c ≤ ↑f (sInf s) ↔ c ≤ sInf (↑f '' s)
[PROOFSTEP]
simp only [← map_inv_le_iff, le_sInf_iff, Set.ball_image_iff]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f g : sSupHom α β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
g : sSupHom α β
toFun✝ : α → β
map_sSup'✝ : ∀ (s : Set α), toFun✝ (sSup s) = sSup (toFun✝ '' s)
h : { toFun := toFun✝, map_sSup' := map_sSup'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_sSup' := map_sSup'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
toFun✝¹ : α → β
map_sSup'✝¹ : ∀ (s : Set α), toFun✝¹ (sSup s) = sSup (toFun✝¹ '' s)
toFun✝ : α → β
map_sSup'✝ : ∀ (s : Set α), toFun✝ (sSup s) = sSup (toFun✝ '' s)
h : { toFun := toFun✝¹, map_sSup' := map_sSup'✝¹ }.toFun = { toFun := toFun✝, map_sSup' := map_sSup'✝ }.toFun
⊢ { toFun := toFun✝¹, map_sSup' := map_sSup'✝¹ } = { toFun := toFun✝, map_sSup' := map_sSup'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
s : Set α
⊢ id (sSup s) = sSup (id '' s)
[PROOFSTEP]
rw [id, Set.image_id]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
⊢ (↑f ∘ ↑g) (sSup s) = sSup (↑f ∘ ↑g '' s)
[PROOFSTEP]
rw [comp_apply, map_sSup, map_sSup, Set.image_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
⊢ sSup ((fun x => ↑f (↑g x)) '' s) = sSup (↑f ∘ ↑g '' s)
[PROOFSTEP]
simp only [Function.comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
g : sSupHom β γ
f₁ f₂ : sSupHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : SupSet α
x✝ : CompleteLattice β
s : Set α
⊢ (fun x => ⊥) (sSup s) = sSup ((fun x => ⊥) '' s)
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : SupSet α
x✝ : CompleteLattice β
⊢ (fun x => ⊥) (sSup ∅) = sSup ((fun x => ⊥) '' ∅)
[PROOFSTEP]
rw [Set.image_empty, sSup_empty]
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : SupSet α
x✝ : CompleteLattice β
s : Set α
hs : Set.Nonempty s
⊢ (fun x => ⊥) (sSup s) = sSup ((fun x => ⊥) '' s)
[PROOFSTEP]
rw [hs.image_const, sSup_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
f g : sInfHom α β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
g : sInfHom α β
toFun✝ : α → β
map_sInf'✝ : ∀ (s : Set α), toFun✝ (sInf s) = sInf (toFun✝ '' s)
h : { toFun := toFun✝, map_sInf' := map_sInf'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_sInf' := map_sInf'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
toFun✝¹ : α → β
map_sInf'✝¹ : ∀ (s : Set α), toFun✝¹ (sInf s) = sInf (toFun✝¹ '' s)
toFun✝ : α → β
map_sInf'✝ : ∀ (s : Set α), toFun✝ (sInf s) = sInf (toFun✝ '' s)
h : { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ }.toFun = { toFun := toFun✝, map_sInf' := map_sInf'✝ }.toFun
⊢ { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ } = { toFun := toFun✝, map_sInf' := map_sInf'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
s : Set α
⊢ id (sInf s) = sInf (id '' s)
[PROOFSTEP]
rw [id, Set.image_id]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
f : sInfHom β γ
g : sInfHom α β
s : Set α
⊢ (↑f ∘ ↑g) (sInf s) = sInf (↑f ∘ ↑g '' s)
[PROOFSTEP]
rw [comp_apply, map_sInf, map_sInf, Set.image_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
f : sInfHom β γ
g : sInfHom α β
s : Set α
⊢ sInf ((fun x => ↑f (↑g x)) '' s) = sInf (↑f ∘ ↑g '' s)
[PROOFSTEP]
simp only [Function.comp]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : InfSet α
inst✝² : InfSet β
inst✝¹ : InfSet γ
inst✝ : InfSet δ
g : sInfHom β γ
f₁ f₂ : sInfHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : InfSet α
inst✝ : CompleteLattice β
s : Set α
⊢ (fun x => ⊤) (sInf s) = sInf ((fun x => ⊤) '' s)
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : InfSet α
inst✝ : CompleteLattice β
⊢ (fun x => ⊤) (sInf ∅) = sInf ((fun x => ⊤) '' ∅)
[PROOFSTEP]
rw [Set.image_empty, sInf_empty]
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : InfSet α
inst✝ : CompleteLattice β
s : Set α
hs : Set.Nonempty s
⊢ (fun x => ⊤) (sInf s) = sInf ((fun x => ⊤) '' s)
[PROOFSTEP]
rw [hs.image_const, sInf_singleton]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
f g : FrameHom α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
[GOAL]
case mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
g : FrameHom α β
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
map_top'✝ : InfHom.toFun { toFun := toFun✝, map_inf' := map_inf'✝ } ⊤ = ⊤
map_sSup'✝ :
  ∀ (s : Set α),
    InfHom.toFun { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ }.toInfHom (sSup s) =
      sSup ({ toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ }.toInfHom.toFun '' s)
h :
  (fun f => f.toFun)
      { toInfTopHom := { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ },
        map_sSup' := map_sSup'✝ } =
    (fun f => f.toFun) g
⊢ { toInfTopHom := { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ },
      map_sSup' := map_sSup'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
toFun✝¹ : α → β
map_inf'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊓ b) = toFun✝¹ a ⊓ toFun✝¹ b
map_top'✝¹ : InfHom.toFun { toFun := toFun✝¹, map_inf' := map_inf'✝¹ } ⊤ = ⊤
map_sSup'✝¹ :
  ∀ (s : Set α),
    InfHom.toFun { toInfHom := { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }, map_top' := map_top'✝¹ }.toInfHom
        (sSup s) =
      sSup ({ toInfHom := { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }, map_top' := map_top'✝¹ }.toInfHom.toFun '' s)
toFun✝ : α → β
map_inf'✝ : ∀ (a b : α), toFun✝ (a ⊓ b) = toFun✝ a ⊓ toFun✝ b
map_top'✝ : InfHom.toFun { toFun := toFun✝, map_inf' := map_inf'✝ } ⊤ = ⊤
map_sSup'✝ :
  ∀ (s : Set α),
    InfHom.toFun { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ }.toInfHom (sSup s) =
      sSup ({ toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ }.toInfHom.toFun '' s)
h :
  (fun f => f.toFun)
      { toInfTopHom := { toInfHom := { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }, map_top' := map_top'✝¹ },
        map_sSup' := map_sSup'✝¹ } =
    (fun f => f.toFun)
      { toInfTopHom := { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ },
        map_sSup' := map_sSup'✝ }
⊢ { toInfTopHom := { toInfHom := { toFun := toFun✝¹, map_inf' := map_inf'✝¹ }, map_top' := map_top'✝¹ },
      map_sSup' := map_sSup'✝¹ } =
    { toInfTopHom := { toInfHom := { toFun := toFun✝, map_inf' := map_inf'✝ }, map_top' := map_top'✝ },
      map_sSup' := map_sSup'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
g : FrameHom β γ
f₁ f₂ : FrameHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
f g : CompleteLatticeHom α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
g : CompleteLatticeHom α β
toFun✝ : α → β
map_sInf'✝ : ∀ (s : Set α), toFun✝ (sInf s) = sInf (toFun✝ '' s)
map_sSup'✝ :
  ∀ (s : Set α),
    sInfHom.toFun { toFun := toFun✝, map_sInf' := map_sInf'✝ } (sSup s) =
      sSup ({ toFun := toFun✝, map_sInf' := map_sInf'✝ }.toFun '' s)
h :
  (fun f => f.toFun) { tosInfHom := { toFun := toFun✝, map_sInf' := map_sInf'✝ }, map_sSup' := map_sSup'✝ } =
    (fun f => f.toFun) g
⊢ { tosInfHom := { toFun := toFun✝, map_sInf' := map_sInf'✝ }, map_sSup' := map_sSup'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
toFun✝¹ : α → β
map_sInf'✝¹ : ∀ (s : Set α), toFun✝¹ (sInf s) = sInf (toFun✝¹ '' s)
map_sSup'✝¹ :
  ∀ (s : Set α),
    sInfHom.toFun { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ } (sSup s) =
      sSup ({ toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ }.toFun '' s)
toFun✝ : α → β
map_sInf'✝ : ∀ (s : Set α), toFun✝ (sInf s) = sInf (toFun✝ '' s)
map_sSup'✝ :
  ∀ (s : Set α),
    sInfHom.toFun { toFun := toFun✝, map_sInf' := map_sInf'✝ } (sSup s) =
      sSup ({ toFun := toFun✝, map_sInf' := map_sInf'✝ }.toFun '' s)
h :
  (fun f => f.toFun) { tosInfHom := { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ }, map_sSup' := map_sSup'✝¹ } =
    (fun f => f.toFun) { tosInfHom := { toFun := toFun✝, map_sInf' := map_sInf'✝ }, map_sSup' := map_sSup'✝ }
⊢ { tosInfHom := { toFun := toFun✝¹, map_sInf' := map_sInf'✝¹ }, map_sSup' := map_sSup'✝¹ } =
    { tosInfHom := { toFun := toFun✝, map_sInf' := map_sInf'✝ }, map_sSup' := map_sSup'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
g : CompleteLatticeHom β γ
f₁ f₂ : CompleteLatticeHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set β)
⊢ ⋂ (t : Set β) (_ : t ∈ s), f ⁻¹' t = sInf (preimage f '' s)
[PROOFSTEP]
simp only [Set.sInf_eq_sInter, Set.sInter_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set β)
⊢ ⋃ (t : Set β) (_ : t ∈ s), (fun x => f x) ⁻¹' t =
    sSup
      ({ toFun := preimage f, map_sInf' := (_ : ∀ (s : Set (Set β)), f ⁻¹' ⋂₀ s = sInf (preimage f '' s)) }.toFun '' s)
[PROOFSTEP]
simp only [Set.sSup_eq_sUnion, Set.sUnion_image]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
⊢ f '' sSup s = sSup (image f '' s)
[PROOFSTEP]
ext b
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
b : β
⊢ b ∈ f '' sSup s ↔ b ∈ sSup (image f '' s)
[PROOFSTEP]
simp only [sSup_eq_sUnion, mem_image, mem_sUnion, exists_prop, sUnion_image, mem_iUnion]
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
b : β
⊢ (∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = b) ↔ ∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = b
[PROOFSTEP]
constructor
[GOAL]
case h.mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
b : β
⊢ (∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = b) → ∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = b
[PROOFSTEP]
rintro ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
a : α
t : Set α
ht₁ : t ∈ s
ht₂ : a ∈ t
⊢ ∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = f a
[PROOFSTEP]
exact ⟨t, ht₁, a, ht₂, rfl⟩
[GOAL]
case h.mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
b : β
⊢ (∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = b) → ∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = b
[PROOFSTEP]
rintro ⟨t, ht₁, a, ht₂, rfl⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
f : α → β
s : Set (Set α)
t : Set α
ht₁ : t ∈ s
a : α
ht₂ : a ∈ t
⊢ ∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = f a
[PROOFSTEP]
exact ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
e : α ≃ β
s : Set α
⊢ (fun s => ↑e.symm '' s) ((fun s => ↑e '' s) s) = s
[PROOFSTEP]
simp only [← image_comp, Equiv.symm_comp_self, id.def, image_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
e : α ≃ β
s : Set β
⊢ (fun s => ↑e '' s) ((fun s => ↑e.symm '' s) s) = s
[PROOFSTEP]
simp only [← image_comp, Equiv.self_comp_symm, id.def, image_id']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
e : α ≃ β
a✝ b✝ : Set α
h :
  ↑{ toFun := fun s => ↑e '' s, invFun := fun s => ↑e.symm '' s,
          left_inv := (_ : ∀ (s : Set α), ↑e.symm '' (fun s => ↑e '' s) s = s),
          right_inv := (_ : ∀ (s : Set β), ↑e '' (fun s => ↑e.symm '' s) s = s) }
      a✝ ≤
    ↑{ toFun := fun s => ↑e '' s, invFun := fun s => ↑e.symm '' s,
          left_inv := (_ : ∀ (s : Set α), ↑e.symm '' (fun s => ↑e '' s) s = s),
          right_inv := (_ : ∀ (s : Set β), ↑e '' (fun s => ↑e.symm '' s) s = s) }
      b✝
⊢ a✝ ≤ b✝
[PROOFSTEP]
simpa using @monotone_image _ _ e.symm _ _ h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : CompleteLattice α
x : α × α
s : Set (α × α)
⊢ (fun x => x.fst ⊔ x.snd) (sSup s) = sSup ((fun x => x.fst ⊔ x.snd) '' s)
[PROOFSTEP]
simp_rw [Prod.fst_sSup, Prod.snd_sSup, sSup_image, iSup_sup_eq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝ : CompleteLattice α
x : α × α
s : Set (α × α)
⊢ (fun x => x.fst ⊓ x.snd) (sInf s) = sInf ((fun x => x.fst ⊓ x.snd) '' s)
[PROOFSTEP]
simp_rw [Prod.fst_sInf, Prod.snd_sInf, sInf_image, iInf_inf_eq]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
⊢ map id = id
[PROOFSTEP]
ext ⟨f⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g h : α → β
x✝ : Germ l β
f : α → β
⊢ map id (Quot.mk Setoid.r f) = id (Quot.mk Setoid.r f)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h : α → β
op : β → γ → δ
f f' : α → β
Hf✝ : Setoid.r f f'
g g' : α → γ
Hg✝ : Setoid.r g g'
x : α
Hf : f x = f' x
Hg : g x = g' x
⊢ (fun f g x => op (f x) (g x)) f g x = (fun f g x => op (f x) (g x)) f' g' x
[PROOFSTEP]
simp only [Hf, Hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
f✝ : Germ l β
f : α → β
⊢ 1 • ↑f = ↑f
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
f✝ : Germ l β
f : α → β
⊢ 1 • f =ᶠ[l] f
[PROOFSTEP]
simp only [one_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
f✝ : Germ l β
f : α → β
⊢ f =ᶠ[l] f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁ c₂ : M
f✝ : Germ l β
f : α → β
⊢ (c₁ * c₂) • ↑f = c₁ • c₂ • ↑f
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁ c₂ : M
f✝ : Germ l β
f : α → β
⊢ (c₁ * c₂) • f =ᶠ[l] c₁ • c₂ • f
[PROOFSTEP]
simp only [mul_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁ c₂ : M
f✝ : Germ l β
f : α → β
⊢ c₁ • c₂ • f =ᶠ[l] c₁ • c₂ • f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
f✝ : Germ l β
f : α → β
⊢ 1 • ↑f = ↑f
[PROOFSTEP]
simp only [← coe_one, ← coe_smul', one_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁✝ c₂✝ : Germ l M
f✝ : Germ l β
c₁ c₂ : α → M
f : α → β
⊢ (↑c₁ * ↑c₂) • ↑f = ↑c₁ • ↑c₂ • ↑f
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁✝ c₂✝ : Germ l M
f✝ : Germ l β
c₁ c₂ : α → M
f : α → β
⊢ (c₁ * c₂) • f =ᶠ[l] c₁ • c₂ • f
[PROOFSTEP]
simp only [mul_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝¹ : Monoid M
inst✝ : MulAction M β
c₁✝ c₂✝ : Germ l M
f✝ : Germ l β
c₁ c₂ : α → M
f : α → β
⊢ c₁ • c₂ • f =ᶠ[l] c₁ • c₂ • f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
⊢ c • 0 = 0
[PROOFSTEP]
simp only [← coe_zero, ← coe_smul, smul_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
f✝ g✝ : Germ l N
f g : α → N
⊢ c • (↑f + ↑g) = c • ↑f + c • ↑g
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
f✝ g✝ : Germ l N
f g : α → N
⊢ c • (f + g) =ᶠ[l] c • f + c • g
[PROOFSTEP]
simp only [smul_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
f✝ g✝ : Germ l N
f g : α → N
⊢ c • f + c • g =ᶠ[l] c • f + c • g
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : Germ l M
c : α → M
⊢ ↑c • 0 = 0
[PROOFSTEP]
simp only [← coe_zero, ← coe_smul', smul_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : Germ l M
f✝ g✝ : Germ l N
c : α → M
f g : α → N
⊢ ↑c • (↑f + ↑g) = ↑c • ↑f + ↑c • ↑g
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : Germ l M
f✝ g✝ : Germ l N
c : α → M
f g : α → N
⊢ c • (f + g) =ᶠ[l] c • f + c • g
[PROOFSTEP]
simp only [smul_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : Germ l M
f✝ g✝ : Germ l N
c : α → M
f g : α → N
⊢ c • f + c • g =ᶠ[l] c • f + c • g
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁ c₂ : R
f✝ : Germ l M
f : α → M
⊢ (c₁ + c₂) • ↑f = c₁ • ↑f + c₂ • ↑f
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁ c₂ : R
f✝ : Germ l M
f : α → M
⊢ (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f
[PROOFSTEP]
simp only [add_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁ c₂ : R
f✝ : Germ l M
f : α → M
⊢ c₁ • f + c₂ • f =ᶠ[l] c₁ • f + c₂ • f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f✝ : Germ l M
f : α → M
⊢ 0 • ↑f = 0
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f✝ : Germ l M
f : α → M
⊢ 0 • f =ᶠ[l] 0
[PROOFSTEP]
simp only [zero_smul, coe_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f✝ : Germ l M
f : α → M
⊢ 0 =ᶠ[l] 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁✝ c₂✝ : Germ l R
f✝ : Germ l M
c₁ c₂ : α → R
f : α → M
⊢ (↑c₁ + ↑c₂) • ↑f = ↑c₁ • ↑f + ↑c₂ • ↑f
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁✝ c₂✝ : Germ l R
f✝ : Germ l M
c₁ c₂ : α → R
f : α → M
⊢ (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f
[PROOFSTEP]
simp only [add_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c₁✝ c₂✝ : Germ l R
f✝ : Germ l M
c₁ c₂ : α → R
f : α → M
⊢ c₁ • f + c₂ • f =ᶠ[l] c₁ • f + c₂ • f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f✝ : Germ l M
f : α → M
⊢ 0 • ↑f = 0
[PROOFSTEP]
simp only [← coe_zero, ← coe_smul', zero_smul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : Germ l β
f g : α → β
h : f ≤ᶠ[l] g
⊢ ∃ c, ↑g = ↑f * c
[PROOFSTEP]
classical
choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx
refine ⟨ofFun <| fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
filter_upwards [h] with x hx
rw [dif_pos hx, hc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : Germ l β
f g : α → β
h : f ≤ᶠ[l] g
⊢ ∃ c, ↑g = ↑f * c
[PROOFSTEP]
choose c hc using fun x (hx : f x ≤ g x) ↦ exists_mul_of_le hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : Germ l β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → f x ≤ g x → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
⊢ ∃ c, ↑g = ↑f * c
[PROOFSTEP]
refine ⟨ofFun <| fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : Germ l β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → f x ≤ g x → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
⊢ g =ᶠ[l] (fun f g x => (fun x x_1 => x * x_1) (f x) (g x)) f fun x => if hx : f x ≤ g x then c x hx else f x
[PROOFSTEP]
filter_upwards [h] with x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x✝ y : Germ l β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → f x ≤ g x → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
x : α
hx : f x ≤ g x
⊢ g x = f x * if hx : f x ≤ g x then c x hx else f x
[PROOFSTEP]
rw [dif_pos hx, hc]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
F : Type u_5
inst✝ : RelHomClass F r s
f : F
a : α
⊢ Acc s (↑f a) → Acc r a
[PROOFSTEP]
generalize h : f a = b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
F : Type u_5
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : ↑f a = b
⊢ Acc s b → Acc r a
[PROOFSTEP]
intro ac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
F : Type u_5
inst✝ : RelHomClass F r s
f : F
a : α
b : β
h : ↑f a = b
ac : Acc s b
⊢ Acc r a
[PROOFSTEP]
induction' ac with _ H IH generalizing a
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
F : Type u_5
inst✝ : RelHomClass F r s
f : F
a✝ : α
b : β
h✝ : ↑f a✝ = b
x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), ↑f a = y → Acc r a
a : α
h : ↑f a = x✝
⊢ Acc r a
[PROOFSTEP]
subst h
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
F : Type u_5
inst✝ : RelHomClass F r s
f : F
a✝ : α
b : β
h : ↑f a✝ = b
a : α
H : ∀ (y : β), s y (↑f a) → Acc s y
IH : ∀ (y : β), s y (↑f a) → ∀ (a : α), ↑f a = y → Acc r a
⊢ Acc r a
[PROOFSTEP]
exact ⟨_, fun a' h => IH (f a') (map_rel f h) _ rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f g : r →r s
h : (fun o => o.toFun) f = (fun o => o.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
g : r →r s
toFun✝ : α → β
map_rel'✝ : ∀ {a b : α}, r a b → s (toFun✝ a) (toFun✝ b)
h : (fun o => o.toFun) { toFun := toFun✝, map_rel' := map_rel'✝ } = (fun o => o.toFun) g
⊢ { toFun := toFun✝, map_rel' := map_rel'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
toFun✝¹ : α → β
map_rel'✝¹ : ∀ {a b : α}, r a b → s (toFun✝¹ a) (toFun✝¹ b)
toFun✝ : α → β
map_rel'✝ : ∀ {a b : α}, r a b → s (toFun✝ a) (toFun✝ b)
h :
  (fun o => o.toFun) { toFun := toFun✝¹, map_rel' := map_rel'✝¹ } =
    (fun o => o.toFun) { toFun := toFun✝, map_rel' := map_rel'✝ }
⊢ { toFun := toFun✝¹, map_rel' := map_rel'✝¹ } = { toFun := toFun✝, map_rel' := map_rel'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
⊢ Injective f
[PROOFSTEP]
intro x y hxy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
⊢ x = y
[PROOFSTEP]
rcases trichotomous_of r x y with (h | h | h)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
⊢ x = y
[PROOFSTEP]
have := hf h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f x) (f y)
⊢ x = y
[PROOFSTEP]
rw [hxy] at this
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f y) (f y)
⊢ x = y
[PROOFSTEP]
exfalso
[GOAL]
case inl.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
this : s (f y) (f y)
⊢ False
[PROOFSTEP]
exact irrefl_of s (f y) this
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : x = y
⊢ x = y
[PROOFSTEP]
exact h
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
⊢ x = y
[PROOFSTEP]
have := hf h
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f x)
⊢ x = y
[PROOFSTEP]
rw [hxy] at this
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f y)
⊢ x = y
[PROOFSTEP]
exfalso
[GOAL]
case inr.inr.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsIrrefl β s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
this : s (f y) (f y)
⊢ False
[PROOFSTEP]
exact irrefl_of s (f y) this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
⊢ WellFounded r → WellFounded s
[PROOFSTEP]
refine RelHomClass.wellFounded (RelHom.mk ?_ ?_ : s →r r)
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
⊢ β → α
[PROOFSTEP]
exact Classical.choose hf.hasRightInverse
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
⊢ ∀ {a b : β}, s a b → r (Classical.choose (_ : HasRightInverse f) a) (Classical.choose (_ : HasRightInverse f) b)
[PROOFSTEP]
intro a b h
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ r (Classical.choose (_ : HasRightInverse f) a) (Classical.choose (_ : HasRightInverse f) b)
[PROOFSTEP]
apply o.2
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ s (f (Classical.choose (_ : HasRightInverse f) a)) (f (Classical.choose (_ : HasRightInverse f) b))
[PROOFSTEP]
convert h
[GOAL]
case h.e'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) a) = a
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) b) = b
[PROOFSTEP]
iterate 2 apply Classical.choose_spec hf.hasRightInverse
[GOAL]
case h.e'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) a) = a
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) b) = b
[PROOFSTEP]
apply Classical.choose_spec hf.hasRightInverse
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) b) = b
[PROOFSTEP]
apply Classical.choose_spec hf.hasRightInverse
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f g : r ↪r s
h : (fun x => x.toFun) f = (fun x => x.toFun) g
⊢ f = g
[PROOFSTEP]
rcases f with ⟨⟨⟩⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
g : r ↪r s
toFun✝ : α → β
inj'✝ : Injective toFun✝
map_rel_iff'✝ : ∀ {a b : α}, s (↑{ toFun := toFun✝, inj' := inj'✝ } a) (↑{ toFun := toFun✝, inj' := inj'✝ } b) ↔ r a b
h :
  (fun x => x.toFun) { toEmbedding := { toFun := toFun✝, inj' := inj'✝ }, map_rel_iff' := map_rel_iff'✝ } =
    (fun x => x.toFun) g
⊢ { toEmbedding := { toFun := toFun✝, inj' := inj'✝ }, map_rel_iff' := map_rel_iff'✝ } = g
[PROOFSTEP]
rcases g with ⟨⟨⟩⟩
[GOAL]
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
toFun✝¹ : α → β
inj'✝¹ : Injective toFun✝¹
map_rel_iff'✝¹ :
  ∀ {a b : α}, s (↑{ toFun := toFun✝¹, inj' := inj'✝¹ } a) (↑{ toFun := toFun✝¹, inj' := inj'✝¹ } b) ↔ r a b
toFun✝ : α → β
inj'✝ : Injective toFun✝
map_rel_iff'✝ : ∀ {a b : α}, s (↑{ toFun := toFun✝, inj' := inj'✝ } a) (↑{ toFun := toFun✝, inj' := inj'✝ } b) ↔ r a b
h :
  (fun x => x.toFun) { toEmbedding := { toFun := toFun✝¹, inj' := inj'✝¹ }, map_rel_iff' := map_rel_iff'✝¹ } =
    (fun x => x.toFun) { toEmbedding := { toFun := toFun✝, inj' := inj'✝ }, map_rel_iff' := map_rel_iff'✝ }
⊢ { toEmbedding := { toFun := toFun✝¹, inj' := inj'✝¹ }, map_rel_iff' := map_rel_iff'✝¹ } =
    { toEmbedding := { toFun := toFun✝, inj' := inj'✝ }, map_rel_iff' := map_rel_iff'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : s ↪r t
⊢ ∀ {a b : α},
    t (↑(Embedding.trans f.toEmbedding g.toEmbedding) a) (↑(Embedding.trans f.toEmbedding g.toEmbedding) b) ↔ r a b
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
⊢ r = ↑f ⁻¹'o s
[PROOFSTEP]
ext a b
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a b : α
⊢ r a b ↔ (↑f ⁻¹'o s) a b
[PROOFSTEP]
exact f.map_rel_iff.symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a : α
⊢ Acc s (↑f a) → Acc r a
[PROOFSTEP]
generalize h : f a = b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a : α
b : β
h : ↑f a = b
⊢ Acc s b → Acc r a
[PROOFSTEP]
intro ac
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a : α
b : β
h : ↑f a = b
ac : Acc s b
⊢ Acc r a
[PROOFSTEP]
induction' ac with _ H IH generalizing a
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a✝ : α
b : β
h✝ : ↑f a✝ = b
x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), ↑f a = y → Acc r a
a : α
h : ↑f a = x✝
⊢ Acc r a
[PROOFSTEP]
subst h
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
a✝ : α
b : β
h : ↑f a✝ = b
a : α
H : ∀ (y : β), s y (↑f a) → Acc s y
IH : ∀ (y : β), s y (↑f a) → ∀ (a : α), ↑f a = y → Acc r a
⊢ Acc r a
[PROOFSTEP]
exact ⟨_, fun a' h => IH (f a') (f.map_rel_iff.2 h) _ rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ ∀ {a b : Quotient inst✝}, r (↑(Embedding.quotientOut α) a) (↑(Embedding.quotientOut α) b) ↔ Quotient.lift₂ r H a b
[PROOFSTEP]
refine' @fun x y => Quotient.inductionOn₂ x y fun a b => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
x y : Quotient inst✝
a b : α
⊢ r (↑(Embedding.quotientOut α) (Quotient.mk inst✝ a)) (↑(Embedding.quotientOut α) (Quotient.mk inst✝ b)) ↔
    Quotient.lift₂ r H (Quotient.mk inst✝ a) (Quotient.mk inst✝ b)
[PROOFSTEP]
apply iff_iff_eq.2 (H _ _ _ _ _ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
x y : Quotient inst✝
a b : α
⊢ ↑(Embedding.quotientOut α) (Quotient.mk inst✝ a) ≈ a
[PROOFSTEP]
apply Quotient.mk_out
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
x y : Quotient inst✝
a b : α
⊢ ↑(Embedding.quotientOut α) (Quotient.mk inst✝ b) ≈ b
[PROOFSTEP]
apply Quotient.mk_out
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a) ↔ Acc r a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a) → Acc r a
[PROOFSTEP]
exact RelHomClass.acc (Quotient.mkRelHom H) a
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc r a → Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a)
[PROOFSTEP]
intro ac
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
ac : Acc r a
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a)
[PROOFSTEP]
induction' ac with _ _ IH
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ y)
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ x✝)
[PROOFSTEP]
refine' ⟨_, fun q h => _⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ y)
q : Quotient inst✝
h : Quotient.lift₂ r H q (Quotient.mk inst✝ x✝)
⊢ Acc (Quotient.lift₂ r H) q
[PROOFSTEP]
obtain ⟨a', rfl⟩ := q.exists_rep
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ y)
a' : α
h : Quotient.lift₂ r H (Quotient.mk inst✝ a') (Quotient.mk inst✝ x✝)
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a')
[PROOFSTEP]
exact IH a' h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) ↔ WellFounded r
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) → WellFounded r
[PROOFSTEP]
exact RelHomClass.wellFounded (Quotient.mkRelHom H)
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded r → WellFounded (Quotient.lift₂ r H)
[PROOFSTEP]
refine' fun wf => ⟨fun q => _⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
wf : WellFounded r
q : Quotient inst✝
⊢ Acc (Quotient.lift₂ r H) q
[PROOFSTEP]
obtain ⟨a, rfl⟩ := q.exists_rep
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
wf : WellFounded r
a : α
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a)
[PROOFSTEP]
exact acc_lift₂_iff.2 (wf.apply a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
⊢ r ↪r s
[PROOFSTEP]
haveI := @IsAsymm.isIrrefl β s _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
⊢ r ↪r s
[PROOFSTEP]
refine' ⟨⟨f, fun a b e => _⟩, @fun a b => ⟨fun h => _, H _ _⟩⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
e : f a = f b
⊢ a = b
[PROOFSTEP]
refine' ((@trichotomous _ r _ a b).resolve_left _).resolve_right _
[GOAL]
case refine'_1.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
e : f a = f b
⊢ ¬r a b
[PROOFSTEP]
exact fun h => @irrefl _ s _ _ (by simpa [e] using H _ _ h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
e : f a = f b
h : r a b
⊢ s (?m.45031 h) (?m.45031 h)
[PROOFSTEP]
simpa [e] using H _ _ h
[GOAL]
case refine'_1.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
e : f a = f b
⊢ ¬r b a
[PROOFSTEP]
exact fun h => @irrefl _ s _ _ (by simpa [e] using H _ _ h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
e : f a = f b
h : r b a
⊢ s (?m.45243 h) (?m.45243 h)
[PROOFSTEP]
simpa [e] using H _ _ h
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
h :
  s (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } a)
    (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } b)
⊢ r a b
[PROOFSTEP]
refine' (@trichotomous _ r _ a b).resolve_right (Or.rec (fun e => _) fun h' => _)
[GOAL]
case refine'_2.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
h :
  s (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } a)
    (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } b)
e : a = b
⊢ False
[PROOFSTEP]
subst e
[GOAL]
case refine'_2.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a : α
h :
  s (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } a)
    (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } a)
⊢ False
[PROOFSTEP]
exact irrefl _ h
[GOAL]
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : IsTrichotomous α r
inst✝ : IsAsymm β s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : IsIrrefl β s
a b : α
h :
  s (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } a)
    (↑{ toFun := f, inj' := (_ : ∀ (a b : α), f a = f b → a = b) } b)
h' : r b a
⊢ False
[PROOFSTEP]
exact asymm (H _ _ h') h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α ⊕ γ},
    Sum.LiftRel s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } a)
        (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } b) ↔
      Sum.LiftRel r t a b
[PROOFSTEP]
rintro (a | b) (c | d)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a c : α
⊢ Sum.LiftRel s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl a))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl c)) ↔
    Sum.LiftRel r t (Sum.inl a) (Sum.inl c)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a : α
d : γ
⊢ Sum.LiftRel s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl a))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr d)) ↔
    Sum.LiftRel r t (Sum.inl a) (Sum.inr d)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b : γ
c : α
⊢ Sum.LiftRel s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr b))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl c)) ↔
    Sum.LiftRel r t (Sum.inr b) (Sum.inl c)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b d : γ
⊢ Sum.LiftRel s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr b))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr d)) ↔
    Sum.LiftRel r t (Sum.inr b) (Sum.inr d)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α ⊕ γ},
    Sum.Lex s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } a)
        (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } b) ↔
      Sum.Lex r t a b
[PROOFSTEP]
rintro (a | b) (c | d)
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a c : α
⊢ Sum.Lex s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl a))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl c)) ↔
    Sum.Lex r t (Sum.inl a) (Sum.inl c)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
a : α
d : γ
⊢ Sum.Lex s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl a))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr d)) ↔
    Sum.Lex r t (Sum.inl a) (Sum.inr d)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b : γ
c : α
⊢ Sum.Lex s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr b))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inl c)) ↔
    Sum.Lex r t (Sum.inr b) (Sum.inl c)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
b d : γ
⊢ Sum.Lex s u (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr b))
      (↑{ toFun := Sum.map ↑f ↑g, inj' := (_ : Injective (Sum.map ↑f ↑g)) } (Sum.inr d)) ↔
    Sum.Lex r t (Sum.inr b) (Sum.inr d)
[PROOFSTEP]
simp [f.map_rel_iff, g.map_rel_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
s : β → β → Prop
a : α
h : ¬r a a
⊢ ∀ {a_1 b : β},
    Prod.Lex r s (↑{ toFun := Prod.mk a, inj' := (_ : Injective (Prod.mk a)) } a_1)
        (↑{ toFun := Prod.mk a, inj' := (_ : Injective (Prod.mk a)) } b) ↔
      s a_1 b
[PROOFSTEP]
simp [Prod.lex_def, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
b : β
h : ¬s b b
⊢ ∀ {a b_1 : α},
    Prod.Lex r s (↑{ toFun := fun a => (a, b), inj' := (_ : Injective fun a => (a, b)) } a)
        (↑{ toFun := fun a => (a, b), inj' := (_ : Injective fun a => (a, b)) } b_1) ↔
      r a b_1
[PROOFSTEP]
simp [Prod.lex_def, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ↪r s
g : t ↪r u
⊢ ∀ {a b : α × γ},
    Prod.Lex s u (↑{ toFun := Prod.map ↑f ↑g, inj' := (_ : Injective (Prod.map ↑f ↑g)) } a)
        (↑{ toFun := Prod.map ↑f ↑g, inj' := (_ : Injective (Prod.map ↑f ↑g)) } b) ↔
      Prod.Lex r t a b
[PROOFSTEP]
simp [Prod.lex_def, f.map_rel_iff, g.map_rel_iff, f.inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
e₁ : α ≃ β
o₁ : ∀ {a b : α}, s (↑e₁ a) (↑e₁ b) ↔ r a b
e₂ : α ≃ β
map_rel_iff'✝ : ∀ {a b : α}, s (↑e₂ a) (↑e₂ b) ↔ r a b
h : { toEquiv := e₁, map_rel_iff' := o₁ }.toEquiv = { toEquiv := e₂, map_rel_iff' := map_rel_iff'✝ }.toEquiv
⊢ { toEquiv := e₁, map_rel_iff' := o₁ } = { toEquiv := e₂, map_rel_iff' := map_rel_iff'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : r ≃r s
a b : β
⊢ r (↑f.symm a) (↑f.symm b) ↔ s a b
[PROOFSTEP]
erw [← f.map_rel_iff, f.1.apply_symm_apply, f.1.apply_symm_apply]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α β : Type u
r : α → α → Prop
s : β → β → Prop
h₁ : α = β
h₂ : HEq r s
a b : α
⊢ s (↑(Equiv.cast h₁) a) (↑(Equiv.cast h₁) b) ↔ r a b
[PROOFSTEP]
subst h₁
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α : Type u
r : α → α → Prop
a b : α
s : α → α → Prop
h₂ : HEq r s
⊢ s (↑(Equiv.cast (_ : α = α)) a) (↑(Equiv.cast (_ : α = α)) b) ↔ r a b
[PROOFSTEP]
rw [eq_of_heq h₂]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α : Type u
r : α → α → Prop
a b : α
s : α → α → Prop
h₂ : HEq r s
⊢ s (↑(Equiv.cast (_ : α = α)) a) (↑(Equiv.cast (_ : α = α)) b) ↔ s a b
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
u : δ → δ → Prop
α β γ : Type u
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
h₁ : α = β
h₁' : β = γ
h₂ : HEq r s
h₂' : HEq s t
x : α
⊢ ↑(RelIso.trans (RelIso.cast h₁ h₂) (RelIso.cast h₁' h₂')) x = ↑(RelIso.cast (_ : α = γ) (_ : HEq r t)) x
[PROOFSTEP]
subst h₁
[GOAL]
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
r✝ : α✝ → α✝ → Prop
s✝ : β → β → Prop
t✝ : γ✝ → γ✝ → Prop
u : δ → δ → Prop
α γ : Type u
r : α → α → Prop
t : γ → γ → Prop
x : α
s : α → α → Prop
h₁' : α = γ
h₂ : HEq r s
h₂' : HEq s t
⊢ ↑(RelIso.trans (RelIso.cast (_ : α = α) h₂) (RelIso.cast h₁' h₂')) x = ↑(RelIso.cast (_ : α = γ) (_ : HEq r t)) x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
e : r ≃r s
x : α
y : β
⊢ r x (↑(RelIso.symm e) y) ↔ s (↑e x) y
[PROOFSTEP]
rw [← e.map_rel_iff, e.apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
e : r ≃r s
x : β
y : α
⊢ r (↑(RelIso.symm e) x) y ↔ s x (↑e y)
[PROOFSTEP]
rw [← e.map_rel_iff, e.apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r s₁
e₂ : r₂ ≃r s₂
a b : α₁ ⊕ α₂
⊢ Sum.Lex s₁ s₂ (↑(Equiv.sumCongr e₁.toEquiv e₂.toEquiv) a) (↑(Equiv.sumCongr e₁.toEquiv e₂.toEquiv) b) ↔
    Sum.Lex r₁ r₂ a b
[PROOFSTEP]
cases' e₁ with f hf
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₂ : r₂ ≃r s₂
a b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
⊢ Sum.Lex s₁ s₂ (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv e₂.toEquiv) a)
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv e₂.toEquiv) b) ↔
    Sum.Lex r₁ r₂ a b
[PROOFSTEP]
cases' e₂ with g hg
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
a b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv) a)
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ a b
[PROOFSTEP]
cases a
[GOAL]
case mk.mk.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
val✝ : α₁
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inl val✝))
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝) b
[PROOFSTEP]
cases b
[GOAL]
case mk.mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
b : α₁ ⊕ α₂
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
val✝ : α₂
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inr val✝))
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv) b) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝) b
[PROOFSTEP]
cases b
[GOAL]
case mk.mk.inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
val✝¹ val✝ : α₁
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inl val✝¹))
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inl val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [hf, hg]
[GOAL]
case mk.mk.inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
val✝¹ : α₁
val✝ : α₂
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inl val✝¹))
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inr val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [hf, hg]
[GOAL]
case mk.mk.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
val✝¹ : α₂
val✝ : α₁
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inr val✝¹))
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inl val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp [hf, hg]
[GOAL]
case mk.mk.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.80676
α₂ : Type ?u.80684
β₁ : Type ?u.80677
β₂ : Type ?u.80685
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
f : α₁ ≃ β₁
hf : ∀ {a b : α₁}, s₁ (↑f a) (↑f b) ↔ r₁ a b
g : α₂ ≃ β₂
hg : ∀ {a b : α₂}, s₂ (↑g a) (↑g b) ↔ r₂ a b
val✝¹ val✝ : α₂
⊢ Sum.Lex s₁ s₂
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inr val✝¹))
      (↑(Equiv.sumCongr { toEquiv := f, map_rel_iff' := hf }.toEquiv { toEquiv := g, map_rel_iff' := hg }.toEquiv)
        (Sum.inr val✝)) ↔
    Sum.Lex r₁ r₂ (Sum.inr val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp [hf, hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.82669
α₂ : Type ?u.82677
β₁ : Type ?u.82670
β₂ : Type ?u.82678
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r s₁
e₂ : r₂ ≃r s₂
⊢ ∀ {a b : α₁ × α₂},
    Prod.Lex s₁ s₂ (↑(Equiv.prodCongr e₁.toEquiv e₂.toEquiv) a) (↑(Equiv.prodCongr e₁.toEquiv e₂.toEquiv) b) ↔
      Prod.Lex r₁ r₂ a b
[PROOFSTEP]
simp [Prod.lex_def, e₁.map_rel_iff, e₂.map_rel_iff, e₁.injective.eq_iff]