internlm/Lean-Github huggingface dataset:
Theorem: Profinite.effectiveEpiFamily_tfae
Proof state before:
case tfae_2_to_3.intro.w.mk.w
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget Profinite).obj (∐ fun b => X b)
q : (fun x => (forget Profinite).obj (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
a : α
x✝ : (forget Profinite).obj (X a)
⊢ ↑(π a) x✝ = ↑((finiteCoproduct.cocone X).ι.app { as := a } ≫ finiteCoproduct.desc X π) x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Profinite.effectiveEpiFamily_tfae
Proof state before:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget Profinite).obj (∐ fun b => X b)
q : (fun x => (forget Profinite).obj (finiteCoproduct X)) t := ↑i.hom t
⊢ t = ↑(i.hom ≫ i.inv) t
Tactic:
simp only [i.hom_inv_id]
Proof state after:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget Profinite).obj (∐ fun b => X b)
q : (fun x => (forget Profinite).obj (finiteCoproduct X)) t := ↑i.hom t
⊢ t = ↑(𝟙 (∐ X)) t
Theorem: Profinite.effectiveEpiFamily_tfae
Proof state before:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget Profinite).obj (∐ fun b => X b)
q : (fun x => (forget Profinite).obj (finiteCoproduct X)) t := ↑i.hom t
⊢ t = ↑(𝟙 (∐ X)) t
Tactic:
rfl
Proof state after:
no goals
Theorem: Profinite.effectiveEpiFamily_tfae
Proof state before:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget Profinite).obj (∐ fun b => X b)
q : (fun x => (forget Profinite).obj (finiteCoproduct X)) t := ↑i.hom t
this✝ : t = ↑i.inv (↑i.hom t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ ↑(π q.fst) q.snd = ↑(i.inv ≫ Sigma.desc π) (↑i.hom t)
Tactic:
rw [this]
Proof state after:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget Profinite).obj (∐ fun b => X b)
q : (fun x => (forget Profinite).obj (finiteCoproduct X)) t := ↑i.hom t
this✝ : t = ↑i.inv (↑i.hom t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ ↑(π q.fst) q.snd = ↑(finiteCoproduct.desc X π) (↑i.hom t)
Theorem: Profinite.effectiveEpiFamily_tfae
Proof state before:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : (forget Profinite).obj (∐ fun b => X b)
q : (fun x => (forget Profinite).obj (finiteCoproduct X)) t := ↑i.hom t
this✝ : t = ↑i.inv (↑i.hom t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ ↑(π q.fst) q.snd = ↑(finiteCoproduct.desc X π) (↑i.hom t)
Tactic:
rfl
Proof state after:
no goals
Theorem: Profinite.effectiveEpiFamily_tfae
Proof state before:
case tfae_3_to_1
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_2_to_3 : Epi (Sigma.desc π) → ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ (∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b) → EffectiveEpiFamily X π
Tactic:
apply effectiveEpiFamily_of_jointly_surjective
Proof state after:
no goals
Theorem: equiv_reflects_mono
Proof state before:
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
⊢ Mono f
Tactic:
constructor
Proof state after:
case right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Theorem: equiv_reflects_mono
Proof state before:
case right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Tactic:
intros W φ ψ h
Proof state after:
case right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ φ = ψ
Theorem: equiv_reflects_mono
Proof state before:
case right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ φ = ψ
Tactic:
apply e.functor.map_injective
Proof state after:
case right_cancellation.a
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ e.functor.map φ = e.functor.map ψ
Theorem: equiv_reflects_mono
Proof state before:
case right_cancellation.a
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ e.functor.map φ = e.functor.map ψ
Tactic:
apply hef.1
Proof state after:
case right_cancellation.a.a
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ e.functor.map φ ≫ e.functor.map f = e.functor.map ψ ≫ e.functor.map f
Theorem: equiv_reflects_mono
Proof state before:
case right_cancellation.a.a
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ e.functor.map φ ≫ e.functor.map f = e.functor.map ψ ≫ e.functor.map f
Tactic:
rw [← Functor.map_comp, ← Functor.map_comp, h]
Proof state after:
no goals
Theorem: equiv_preserves_mono
Proof state before:
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
⊢ Mono (e.functor.map f)
Tactic:
constructor
Proof state after:
case right_cancellation
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
⊢ ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
Theorem: equiv_preserves_mono
Proof state before:
case right_cancellation
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
⊢ ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
Tactic:
intros W φ ψ h
Proof state after:
case right_cancellation
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ φ = ψ
Theorem: equiv_preserves_mono
Proof state before:
case right_cancellation
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ φ = ψ
Tactic:
apply Functor.map_injective e.inverse
Proof state after:
case right_cancellation.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ e.inverse.map φ = e.inverse.map ψ
Theorem: equiv_preserves_mono
Proof state before:
case right_cancellation.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ e.inverse.map φ = e.inverse.map ψ
Tactic:
apply Mono.right_cancellation (f := (Equivalence.unitInv e).app X)
Proof state after:
case right_cancellation.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ e.inverse.map φ ≫ (Equivalence.unitInv e).app X = e.inverse.map ψ ≫ (Equivalence.unitInv e).app X
Theorem: equiv_preserves_mono
Proof state before:
case right_cancellation.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ e.inverse.map φ ≫ (Equivalence.unitInv e).app X = e.inverse.map ψ ≫ (Equivalence.unitInv e).app X
Tactic:
apply Mono.right_cancellation (f := f)
Proof state after:
case right_cancellation.a.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ (e.inverse.map φ ≫ (Equivalence.unitInv e).app X) ≫ f = (e.inverse.map ψ ≫ (Equivalence.unitInv e).app X) ≫ f
Theorem: equiv_preserves_mono
Proof state before:
case right_cancellation.a.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ (e.inverse.map φ ≫ (Equivalence.unitInv e).app X) ≫ f = (e.inverse.map ψ ≫ (Equivalence.unitInv e).app X) ≫ f
Tactic:
apply e.functor.map_injective
Proof state after:
case right_cancellation.a.a.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ e.functor.map ((e.inverse.map φ ≫ (Equivalence.unitInv e).app X) ≫ f) =
    e.functor.map ((e.inverse.map ψ ≫ (Equivalence.unitInv e).app X) ≫ f)
Theorem: equiv_preserves_mono
Proof state before:
case right_cancellation.a.a.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ e.functor.map ((e.inverse.map φ ≫ (Equivalence.unitInv e).app X) ≫ f) =
    e.functor.map ((e.inverse.map ψ ≫ (Equivalence.unitInv e).app X) ≫ f)
Tactic:
simp only [Functor.map_comp]
Proof state after:
case right_cancellation.a.a.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ (e.functor.map (e.inverse.map φ) ≫ e.functor.map ((Equivalence.unitInv e).app X)) ≫ e.functor.map f =
    (e.functor.map (e.inverse.map ψ) ≫ e.functor.map ((Equivalence.unitInv e).app X)) ≫ e.functor.map f
Theorem: equiv_preserves_mono
Proof state before:
case right_cancellation.a.a.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ (e.functor.map (e.inverse.map φ) ≫ e.functor.map ((Equivalence.unitInv e).app X)) ≫ e.functor.map f =
    (e.functor.map (e.inverse.map ψ) ≫ e.functor.map ((Equivalence.unitInv e).app X)) ≫ e.functor.map f
Tactic:
simpa
Proof state after:
no goals
Theorem: Multiset.inf_eq_top
Proof state before:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
m : Multiset α
⊢ m.inf = ⊤ ↔ ∀ a ∈ m, a = ⊤
Tactic:
rw [le_antisymm_iff]
Proof state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
m : Multiset α
⊢ m.inf ≤ ⊤ ∧ ⊤ ≤ m.inf ↔ ∀ a ∈ m, a = ⊤
Theorem: Multiset.inf_eq_top
Proof state before:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
m : Multiset α
⊢ m.inf ≤ ⊤ ∧ ⊤ ≤ m.inf ↔ ∀ a ∈ m, a = ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: MinHeap.head?_ne_top
Proof state before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
h : ¬isEmpty c = true
⊢ head? c ≠ ⊤
Tactic:
intro hc
Proof state after:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
h : ¬isEmpty c = true
hc : head? c = ⊤
⊢ False
Theorem: MinHeap.head?_ne_top
Proof state before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
h : ¬isEmpty c = true
hc : head? c = ⊤
⊢ False
Tactic:
have := hc ▸ (head?_mem_toMultiset_map c h)
Proof state after:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
h : ¬isEmpty c = true
hc : head? c = ⊤
this : ⊤ ∈ Multiset.map WithTop.some (toMultiset c)
⊢ False
Theorem: MinHeap.head?_ne_top
Proof state before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
h : ¬isEmpty c = true
hc : head? c = ⊤
this : ⊤ ∈ Multiset.map WithTop.some (toMultiset c)
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: MinHeap.head_def
Proof state before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
h : ¬isEmpty c = true
⊢ ↑(head c h) = ↑((head? c).untop ⋯)
Tactic:
simpa using MinHeap.coe_head_eq_head? c h
Proof state after:
no goals
Theorem: MinHeap.head_mem_toMultiset
Proof state before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
h : ¬isEmpty c = true
⊢ head c h ∈ toMultiset c
Tactic:
obtain ⟨x, hx₁, hx₂⟩ := Multiset.mem_map.mp (head?_mem_toMultiset_map c h)
Proof state after:
case intro.intro
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
h : ¬isEmpty c = true
x : α
hx₁ : x ∈ toMultiset c
hx₂ : ↑x = head? c
⊢ head c h ∈ toMultiset c
Theorem: MinHeap.head_mem_toMultiset
Proof state before:
case intro.intro
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
h : ¬isEmpty c = true
x : α
hx₁ : x ∈ toMultiset c
hx₂ : ↑x = head? c
⊢ head c h ∈ toMultiset c
Tactic:
simp [hx₁, ← hx₂]
Proof state after:
no goals
Theorem: MinHeap.head_mem
Proof state before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
h : ¬isEmpty c = true
⊢ head c h ∈ c
Tactic:
exact mem_toMultiset.mp (head_mem_toMultiset c h)
Proof state after:
no goals
Theorem: MinHeap.head_le
Proof state before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
x : α
hx : x ∈ c
⊢ head c ⋯ ≤ x
Tactic:
simpa [WithTop.untop_le_iff] using head?_le c x hx
Proof state after:
no goals
Theorem: MinHeap.coe_eq_head?_of_forall_le
Proof state before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ∀ y ∈ c, p y → y ≠ x → x < y
⊢ ↑x = head? c
Tactic:
contrapose! h
Proof state after:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ↑x ≠ head? c
⊢ ∃ y ∈ c, p y ∧ y ≠ x ∧ ¬x < y
Theorem: MinHeap.coe_eq_head?_of_forall_le
Proof state before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ↑x ≠ head? c
⊢ ∃ y ∈ c, p y ∧ y ≠ x ∧ ¬x < y
Tactic:
exact ⟨head c (ToMultiset.not_isEmpty_of_mem hx), MinHeap.head_mem _ _, pc, by intro h'; simp [← h'] at h,
  fun h' ↦ (h'.trans_le (head_le c _ hx)).ne rfl⟩
Proof state after:
no goals
Theorem: MinHeap.coe_eq_head?_of_forall_le
Proof state before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ↑x ≠ head? c
⊢ head c ⋯ ≠ x
Tactic:
intro h'
Proof state after:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ↑x ≠ head? c
h' : head c ⋯ = x
⊢ False
Theorem: MinHeap.coe_eq_head?_of_forall_le
Proof state before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ↑x ≠ head? c
h' : head c ⋯ = x
⊢ False
Tactic:
simp [← h'] at h
Proof state after:
no goals
Theorem: MinHeap.eq_head_of_forall_le
Proof state before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ∀ y ∈ c, p y → y ≠ x → x < y
⊢ x = head c hc
Tactic:
apply WithTop.coe_injective
Proof state after:
case a
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ∀ y ∈ c, p y → y ≠ x → x < y
⊢ ↑x = ↑(head c hc)
Theorem: MinHeap.eq_head_of_forall_le
Proof state before:
case a
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ∀ y ∈ c, p y → y ≠ x → x < y
⊢ ↑x = ↑(head c hc)
Tactic:
simpa using coe_eq_head?_of_forall_le c p hc pc x hx h
Proof state after:
no goals
Theorem: MinHeap.head?_def
Proof state before:
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
⊢ head? c = (Multiset.map WithTop.some (toMultiset c)).inf
Tactic:
by_cases hc : isEmpty c
Proof state after:
case pos
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : isEmpty c = true
⊢ head? c = (Multiset.map WithTop.some (toMultiset c)).inf

case neg
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
⊢ head? c = (Multiset.map WithTop.some (toMultiset c)).inf
Theorem: MinHeap.head?_def
Proof state before:
case pos
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : isEmpty c = true
⊢ head? c = (Multiset.map WithTop.some (toMultiset c)).inf
Tactic:
simp [head?_eq_top c hc, hc]
Proof state after:
no goals
Theorem: MinHeap.head?_def
Proof state before:
case neg
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
⊢ head? c = (Multiset.map WithTop.some (toMultiset c)).inf
Tactic:
apply le_antisymm
Proof state after:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
⊢ head? c ≤ (Multiset.map WithTop.some (toMultiset c)).inf

case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
⊢ (Multiset.map WithTop.some (toMultiset c)).inf ≤ head? c
Theorem: MinHeap.head?_def
Proof state before:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
⊢ head? c ≤ (Multiset.map WithTop.some (toMultiset c)).inf
Tactic:
have := head?_le c
Proof state after:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
this : ∀ x ∈ c, head? c ≤ ↑x
⊢ head? c ≤ (Multiset.map WithTop.some (toMultiset c)).inf
Theorem: MinHeap.head?_def
Proof state before:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
this : ∀ x ∈ c, head? c ≤ ↑x
⊢ head? c ≤ (Multiset.map WithTop.some (toMultiset c)).inf
Tactic:
aesop
Proof state after:
no goals
Theorem: MinHeap.head?_def
Proof state before:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
⊢ (Multiset.map WithTop.some (toMultiset c)).inf ≤ head? c
Tactic:
have := head?_mem_toMultiset_map c hc
Proof state after:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
this : head? c ∈ Multiset.map WithTop.some (toMultiset c)
⊢ (Multiset.map WithTop.some (toMultiset c)).inf ≤ head? c
Theorem: MinHeap.head?_def
Proof state before:
case neg.a
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
this : head? c ∈ Multiset.map WithTop.some (toMultiset c)
⊢ (Multiset.map WithTop.some (toMultiset c)).inf ≤ head? c
Tactic:
apply Multiset.inf_le
Proof state after:
case neg.a.h
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
this : head? c ∈ Multiset.map WithTop.some (toMultiset c)
⊢ head? c ∈ Multiset.map WithTop.some (toMultiset c)
Theorem: MinHeap.head?_def
Proof state before:
case neg.a.h
C : Type u_1
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : MinHeap C α
c : C
hc : ¬isEmpty c = true
this : head? c ∈ Multiset.map WithTop.some (toMultiset c)
⊢ head? c ∈ Multiset.map WithTop.some (toMultiset c)
Tactic:
aesop
Proof state after:
no goals
Theorem: isEmpty_eq_decide_size
Proof state before:
C : Type u_1
α : Type ?u.565
inst✝ : Size C
c : C
⊢ isEmpty c = decide (size c = 0)
Tactic:
simp only [← isEmpty_iff_size_eq_zero, Bool.decide_coe]
Proof state after:
no goals
Theorem: isEmpty_eq_size_beq_zero
Proof state before:
C : Type u_1
α : Type ?u.736
inst✝ : Size C
c : C
⊢ isEmpty c = (size c == 0)
Tactic:
rw [isEmpty_eq_decide_size]
Proof state after:
C : Type u_1
α : Type ?u.736
inst✝ : Size C
c : C
⊢ decide (size c = 0) = (size c == 0)
Theorem: isEmpty_eq_size_beq_zero
Proof state before:
C : Type u_1
α : Type ?u.736
inst✝ : Size C
c : C
⊢ decide (size c = 0) = (size c == 0)
Tactic:
cases size c <;> rfl
Proof state after:
no goals
Theorem: List.head?_isSome
Proof state before:
C : Type u_1
α : Type u_2
l : List α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).head?.isSome = true ↔ head✝ :: tail✝ ≠ []
Tactic:
simp
Proof state after:
no goals
Theorem: List.tail?_isSome
Proof state before:
C : Type u_1
α : Type u_2
l : List α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).tail?.isSome = true ↔ head✝ :: tail✝ ≠ []
Tactic:
simp
Proof state after:
no goals
Theorem: List.isEmpty_eq_decide_eq_nil
Proof state before:
C : Type u_1
α : Type u_2
l : List α
⊢ l.isEmpty = decide (l = [])
Tactic:
cases l <;> simp [isEmpty]
Proof state after:
no goals
Theorem: List.isEmpty_eq_decide_length
Proof state before:
C : Type u_1
α : Type u_2
l : List α
⊢ l.isEmpty = decide (l.length = 0)
Tactic:
cases l <;> simp [isEmpty]
Proof state after:
no goals
Theorem: List.isEmpty_reverse
Proof state before:
C : Type u_1
α : Type u_2
l : List α
⊢ l.reverse.isEmpty = l.isEmpty
Tactic:
rw [isEmpty_eq_decide_eq_nil, isEmpty_eq_decide_eq_nil]
Proof state after:
C : Type u_1
α : Type u_2
l : List α
⊢ decide (l.reverse = []) = decide (l = [])