harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma analyticAt_pi_iff :
    AnalyticAt 𝕜 (fun x ↦ (f · x)) e ↔ ∀ i, AnalyticAt 𝕜 (f i) e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
⊢ AnalyticAt 𝕜 (fun x x_1 => f x_1 x) e ↔ ∀ (i : ι), AnalyticAt 𝕜 (f i) e

Tactic:
simp_rw [← analyticWithinAt_univ]

Result:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
⊢ AnalyticWithinAt 𝕜 (fun x x_1 => f x_1 x) Set.univ e ↔ ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) Set.univ e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
⊢ AnalyticWithinAt 𝕜 (fun x x_1 => f x_1 x) Set.univ e ↔ ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) Set.univ e

Tactic:
exact analyticWithinAt_pi_iff

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach
  | ⟨a, h⟩ => by
    have := mem_map.1 (by rw [attach_map_subtype_val]; exact h)
    rcases this with ⟨⟨_, _⟩, m, rfl⟩
    exact m

Proof state:
α : Type u_1
l : List α
a : α
h : a ∈ l
⊢ ?m.9194 ∈ map ?m.9195 ?m.9196

Tactic:
rw [attach_map_subtype_val]

Result:
α : Type u_1
l : List α
a : α
h : a ∈ l
⊢ ?m.9194 ∈ ?m.9209

α : Type u_1
l : List α
a : α
h : a ∈ l
⊢ List ?m.9207

α : Type u_1
l : List α
a : α
h : a ∈ l
⊢ Type ?u.9206

Proof state:
case intro.mk.intro
α : Type u_1
l : List α
val✝ : α
property✝ : val✝ ∈ l
m : ⟨val✝, property✝⟩ ∈ l.attach
h : ⟨val✝, property✝⟩.val ∈ l
⊢ ⟨⟨val✝, property✝⟩.val, h⟩ ∈ l.attach

Tactic:
exact m

Result:
no goals

Proof state:
α : Type u_1
l : List α
a : α
h : a ∈ l
⊢ ⟨a, h⟩ ∈ l.attach

Tactic:
have := mem_map.1 (by rw [attach_map_subtype_val]; exact h)

Result:
α : Type u_1
l : List α
a : α
h : a ∈ l
this : ∃ a_1, a_1 ∈ l.attach ∧ a_1.val = a
⊢ ⟨a, h⟩ ∈ l.attach

Proof state:
α : Type u_1
l : List α
a : α
h : a ∈ l
this : ∃ a_1, a_1 ∈ l.attach ∧ a_1.val = a
⊢ ⟨a, h⟩ ∈ l.attach

Tactic:
rcases this with ⟨⟨_, _⟩, m, rfl⟩

Result:
case intro.mk.intro
α : Type u_1
l : List α
val✝ : α
property✝ : val✝ ∈ l
m : ⟨val✝, property✝⟩ ∈ l.attach
h : ⟨val✝, property✝⟩.val ∈ l
⊢ ⟨⟨val✝, property✝⟩.val, h⟩ ∈ l.attach

Proof state:
α : Type u_1
l : List α
a : α
h : a ∈ l
⊢ ?m.9194 ∈ ?m.9209

α : Type u_1
l : List α
a : α
h : a ∈ l
⊢ List ?m.9207

α : Type u_1
l : List α
a : α
h : a ∈ l
⊢ Type ?u.9206

Tactic:
exact h

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma OrthogonalIdempotents.map (he : OrthogonalIdempotents e) :
    OrthogonalIdempotents (f ∘ e)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
⊢ OrthogonalIdempotents (⇑f ∘ e)

Tactic:
simp [iff_mul_eq, he.mul_eq, ← map_mul f, apply_ite f]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
⊢ OrthogonalIdempotents (⇑f ∘ e)

Tactic:
classical
simp [iff_mul_eq, he.mul_eq, ← map_mul f, apply_ite f]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem le_sSup {A : C} (s : Set (Subobject A)) (f) (hf : f ∈ s) : f ≤ sSup s

Proof state:
case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f ⟶ underlying.obj (sSup s)

Tactic:
refine eqToHom ?_ ≫ Sigma.ι _ ⟨equivShrink (Subobject A) f, by simpa [Set.mem_image] using hf⟩
  ≫ factorThruImage _ ≫ (underlyingIso _).inv

Result:
case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f = underlying.obj ((equivShrink (Subobject A)).symm ↑⟨(equivShrink (Subobject A)) f, ⋯⟩)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ (equivShrink (Subobject A)) f ∈ ⇑(equivShrink (Subobject A)) '' s

Tactic:
simpa [Set.mem_image] using hf

Result:
no goals

Proof state:
case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f = underlying.obj ((equivShrink (Subobject A)).symm ↑⟨(equivShrink (Subobject A)) f, ⋯⟩)

Tactic:
exact (congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _).symm)

Result:
no goals

Proof state:
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ (eqToHom ⋯ ≫
        Sigma.ι (fun j => underlying.obj ((equivShrink (Subobject A)).symm ↑j)) ⟨(equivShrink (Subobject A)) f, ⋯⟩ ≫
          factorThruImage (smallCoproductDesc s) ≫ (underlyingIso (image.ι (smallCoproductDesc s))).inv) ≫
      (sSup s).arrow =
    f.arrow

Tactic:
simp [sSup, smallCoproductDesc]

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ f ≤ sSup s

Tactic:
fapply le_of_comm

Result:
case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f ⟶ underlying.obj (sSup s)

case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ ?f ≫ (sSup s).arrow = f.arrow
-- Mathlib/Order/Partition/Finpartition.lean
theorem parts_eq_empty_iff : P.parts = ∅ ↔ a = ⊥

Proof state:
case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ ∅.sup id = ⊥

Tactic:
exact Finset.sup_empty

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ P.parts.sup id = ⊥

Tactic:
rw [h]

Result:
case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ ∅.sup id = ⊥

Proof state:
case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts.sup id = ⊥
b : α
hb : b ∈ P.parts
⊢ ⊥ ∈ P.parts

Tactic:
rwa [← le_bot_iff.1 ((le_sup hb).trans h.le)]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ a = ⊥

Tactic:
simp_rw [← P.sup_parts]

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ P.parts.sup id = ⊥

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
⊢ P.parts = ∅ ↔ P.parts.sup id = ⊥

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ eq_empty_iff_forall_not_mem.2 fun b hb ↦ P.not_bot_mem ?_⟩

Result:
case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts = ∅
⊢ P.parts.sup id = ⊥

case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : P.parts.sup id = ⊥
b : α
hb : b ∈ P.parts
⊢ ⊥ ∈ P.parts
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem epi_fst_of_factor_thru_epi_mono_factorization (g₁ : Y ⟶ W) [Epi g₁] (g₂ : W ⟶ Z) [Mono g₂]
    (hg : g₁ ≫ g₂ = g) (f' : X ⟶ W) (hf : f' ≫ g₂ = f) (t : PullbackCone f g) (ht : IsLimit t) :
    Epi t.fst

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g₁ : Y ⟶ W
inst✝¹ : Epi g₁
g₂ : W ⟶ Z
inst✝ : Mono g₂
hg : g₁ ≫ g₂ = g
f' : X ⟶ W
hf : f' ≫ g₂ = f
t : PullbackCone f g
ht : IsLimit t
⊢ Epi t.fst

Tactic:
apply epi_fst_of_isLimit _ _ (PullbackCone.isLimitOfFactors f g g₂ f' g₁ hf hg t ht)

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem orElse_eq_some (o o' : Option α) (x : α) :
    (o <|> o') = some x ↔ o = some x ∨ o = none ∧ o' = some x

Proof state:
α : Type u_1
o o' : Option α
x : α
⊢ (o <|> o') = some x ↔ o = some x ∨ o = none ∧ o' = some x

Tactic:
cases o

Result:
case none
α : Type u_1
o' : Option α
x : α
⊢ (none <|> o') = some x ↔ none = some x ∨ none = none ∧ o' = some x

case some
α : Type u_1
o' : Option α
x val✝ : α
⊢ (some val✝ <|> o') = some x ↔ some val✝ = some x ∨ some val✝ = none ∧ o' = some x

Proof state:
case none
α : Type u_1
o' : Option α
x : α
⊢ (none <|> o') = some x ↔ none = some x ∨ none = none ∧ o' = some x

Tactic:
simp only [true_and, false_or, eq_self_iff_true, none_orElse, reduceCtorEq]

Result:
no goals

Proof state:
case some
α : Type u_1
o' : Option α
x val✝ : α
⊢ (some val✝ <|> o') = some x ↔ some val✝ = some x ∨ some val✝ = none ∧ o' = some x

Tactic:
simp only [some_orElse, or_false, false_and, reduceCtorEq]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Reduced.lean
theorem isReduced_ofLocalizationMaximal : OfLocalizationMaximal fun R _ => IsReduced R

Proof state:
case eq_zero.h
R : Type u_1
inst✝ : CommRing R
x : R
hx : IsNilpotent x
J : Ideal R
hJ : J.IsMaximal
h : IsReduced (Localization.AtPrime J)
⊢ (algebraMap R (Localization.AtPrime J)) x = 0

Tactic:
exact (hx.map <| algebraMap R <| Localization.AtPrime J).eq_zero

Result:
no goals

Proof state:
case eq_zero
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x => IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
⊢ ∀ (x : R), IsNilpotent x → x = 0

Tactic:
intro x hx

Result:
case eq_zero
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x => IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
⊢ x = 0

Proof state:
⊢ OfLocalizationMaximal fun R x => IsReduced R

Tactic:
introv R h

Result:
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x => IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
⊢ IsReduced R

Proof state:
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x => IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
⊢ IsReduced R

Tactic:
constructor

Result:
case eq_zero
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x => IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
⊢ ∀ (x : R), IsNilpotent x → x = 0

Proof state:
case eq_zero.h
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x => IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
J : Ideal R
hJ : J.IsMaximal
⊢ (algebraMap R (Localization.AtPrime J)) x = 0

Tactic:
specialize h J hJ

Result:
case eq_zero.h
R : Type u_1
inst✝ : CommRing R
x : R
hx : IsNilpotent x
J : Ideal R
hJ : J.IsMaximal
h : IsReduced (Localization.AtPrime J)
⊢ (algebraMap R (Localization.AtPrime J)) x = 0

Proof state:
case eq_zero
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x => IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
⊢ x = 0

Tactic:
apply eq_zero_of_localization

Result:
case eq_zero.h
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x => IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
⊢ ∀ (J : Ideal R) (x_1 : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) x = 0

Proof state:
case eq_zero.h
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x => IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
⊢ ∀ (J : Ideal R) (x_1 : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) x = 0

Tactic:
intro J hJ

Result:
case eq_zero.h
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x => IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
J : Ideal R
hJ : J.IsMaximal
⊢ (algebraMap R (Localization.AtPrime J)) x = 0
-- Mathlib/LinearAlgebra/Reflection.lean
lemma preReflection_apply :
    preReflection x f y = y - (f y) • x

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
y : M
⊢ (preReflection x f) y = y - f y • x

Tactic:
simp [preReflection]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem hom_ext {A : Type*} [Semiring A] [Algebra R A] {f g : TensorAlgebra R M →ₐ[R] A}
    (w : f.toLinearMap.comp (ι R) = g.toLinearMap.comp (ι R)) : f = g

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : TensorAlgebra R M →ₐ[R] A
w : (lift R).symm f = (lift R).symm g
⊢ f = g

Tactic:
exact (lift R).symm.injective w

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : TensorAlgebra R M →ₐ[R] A
w : f.toLinearMap ∘ₗ ι R = g.toLinearMap ∘ₗ ι R
⊢ f = g

Tactic:
rw [← lift_symm_apply, ← lift_symm_apply] at w

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : TensorAlgebra R M →ₐ[R] A
w : (lift R).symm f = (lift R).symm g
⊢ f = g
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_dvd_opow (a : Ordinal) {b c : Ordinal} (h : b ≤ c) : a ^ b ∣ a ^ c :=
  ⟨a ^ (c - b), by rw [← opow_add, Ordinal.add_sub_cancel_of_le h]⟩

Proof state:
a b c : Ordinal.{u_1}
h : b ≤ c
⊢ a ^ c = a ^ b * a ^ (c - b)

Tactic:
rw [← opow_add, Ordinal.add_sub_cancel_of_le h]

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem Reduced.eq_empty_of_mem_range
    (hφ : ∀ i, Injective (φ i)) {w : Word G} (hw : Reduced φ w)
    (h : ofCoprodI w.prod ∈ (base φ).range) : w = .empty

Proof state:
case intro.intro.intro.intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
⊢ w = Word.empty

Tactic:
suffices w'.toWord = .empty by
  simp [this, @eq_comm _ []] at hw'map
  ext
  simp [hw'map]

Result:
case intro.intro.intro.intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
⊢ w'.toWord = Word.empty

Proof state:
case intro.intro.intro.intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : (base φ) h = ofCoprodI w.prod
⊢ w = Word.empty

Tactic:
have : (NormalWord.prod (d := d) ⟨.empty, h, by simp⟩) = base φ h := by
  simp [NormalWord.prod]

Result:
case intro.intro.intro.intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : (base φ) h = ofCoprodI w.prod
this : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
⊢ w = Word.empty

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
h : ofCoprodI w.prod ∈ (base φ).range
⊢ w = Word.empty

Tactic:
rcases transversal_nonempty φ hφ with ⟨d⟩

Result:
case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
h : ofCoprodI w.prod ∈ (base φ).range
d : Transversal φ
⊢ w = Word.empty
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem P_corec (i : X) (n : ℕ) : Agree (sCorec f i n) (sCorec f i (succ n))

Proof state:
case succ.mk.a
F : PFunctor.{u}
X : Type w
f : X → ↑F X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i n.succ)
i✝ : X
y : F.A
g : F.B y → X
i : F.B (f i✝).fst
⊢ Agree (sCorec f ((f i✝).snd i) n) (sCorec f ((f i✝).snd i) (n + 1))

Tactic:
apply n_ih

Result:
no goals

Proof state:
case succ
F : PFunctor.{u}
X : Type w
f : X → ↑F X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i n.succ)
i : X
⊢ Agree (sCorec f i (n + 1)) (sCorec f i (n + 1).succ)

Tactic:
obtain ⟨y, g⟩ := f i

Result:
case succ.mk
F : PFunctor.{u}
X : Type w
f : X → ↑F X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i n.succ)
i : X
y : F.A
g : F.B y → X
⊢ Agree (sCorec f i (n + 1)) (sCorec f i (n + 1).succ)

Proof state:
case zero
F : PFunctor.{u}
X : Type w
f : X → ↑F X
i : X
⊢ Agree (sCorec f i 0) (sCorec f i (succ 0))

case succ
F : PFunctor.{u}
X : Type w
f : X → ↑F X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i n.succ)
i : X
⊢ Agree (sCorec f i (n + 1)) (sCorec f i (n + 1).succ)

Tactic:
constructor

Result:
case succ
F : PFunctor.{u}
X : Type w
f : X → ↑F X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i n.succ)
i : X
⊢ Agree (sCorec f i (n + 1)) (sCorec f i (n + 1).succ)

Proof state:
case succ.mk.a
F : PFunctor.{u}
X : Type w
f : X → ↑F X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i n.succ)
i : X
y : F.A
g : F.B y → X
⊢ ∀ (i_1 : F.B (f i).fst), Agree (sCorec f ((f i).snd i_1) n) (sCorec f ((f i).snd i_1) (n + 1))

Tactic:
introv

Result:
case succ.mk.a
F : PFunctor.{u}
X : Type w
f : X → ↑F X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i n.succ)
i✝ : X
y : F.A
g : F.B y → X
i : F.B (f i✝).fst
⊢ Agree (sCorec f ((f i✝).snd i) n) (sCorec f ((f i✝).snd i) (n + 1))

Proof state:
F : PFunctor.{u}
X : Type w
f : X → ↑F X
i : X
n : ℕ
⊢ Agree (sCorec f i n) (sCorec f i n.succ)

Tactic:
induction' n with n n_ih generalizing i

Result:
case zero
F : PFunctor.{u}
X : Type w
f : X → ↑F X
i : X
⊢ Agree (sCorec f i 0) (sCorec f i (succ 0))

case succ
F : PFunctor.{u}
X : Type w
f : X → ↑F X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i n.succ)
i : X
⊢ Agree (sCorec f i (n + 1)) (sCorec f i (n + 1).succ)

Proof state:
case succ.mk
F : PFunctor.{u}
X : Type w
f : X → ↑F X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i n.succ)
i : X
y : F.A
g : F.B y → X
⊢ Agree (sCorec f i (n + 1)) (sCorec f i (n + 1).succ)

Tactic:
constructor

Result:
case succ.mk.a
F : PFunctor.{u}
X : Type w
f : X → ↑F X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i n.succ)
i : X
y : F.A
g : F.B y → X
⊢ ∀ (i_1 : F.B (f i).fst), Agree (sCorec f ((f i).snd i_1) n) (sCorec f ((f i).snd i_1) (n + 1))
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_erase_lt_of_one_lt {γ : Type*} [DecidableEq α] [CommMonoid γ] [Preorder γ]
    [MulLeftStrictMono γ] {s : Finset α} {d : α} (hd : d ∈ s) {f : α → γ}
    (hdf : 1 < f d) : ∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m

Proof state:
α : Type u_3
γ : Type u_6
inst✝³ : DecidableEq α
inst✝² : CommMonoid γ
inst✝¹ : Preorder γ
inst✝ : MulLeftStrictMono γ
s : Finset α
d : α
hd : d ∈ s
f : α → γ
hdf : 1 < f d
⊢ ∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m

Tactic:
conv in ∏ m ∈ s, f m => rw [← Finset.insert_erase hd]

Result:
α : Type u_3
γ : Type u_6
inst✝³ : DecidableEq α
inst✝² : CommMonoid γ
inst✝¹ : Preorder γ
inst✝ : MulLeftStrictMono γ
s : Finset α
d : α
hd : d ∈ s
f : α → γ
hdf : 1 < f d
⊢ ∏ m ∈ s.erase d, f m < ∏ m ∈ insert d (s.erase d), f m

Proof state:
α : Type u_3
γ : Type u_6
inst✝³ : DecidableEq α
inst✝² : CommMonoid γ
inst✝¹ : Preorder γ
inst✝ : MulLeftStrictMono γ
s : Finset α
d : α
hd : d ∈ s
f : α → γ
hdf : 1 < f d
⊢ ∏ m ∈ s.erase d, f m < ∏ m ∈ insert d (s.erase d), f m

Tactic:
rw [Finset.prod_insert (Finset.not_mem_erase d s)]

Result:
α : Type u_3
γ : Type u_6
inst✝³ : DecidableEq α
inst✝² : CommMonoid γ
inst✝¹ : Preorder γ
inst✝ : MulLeftStrictMono γ
s : Finset α
d : α
hd : d ∈ s
f : α → γ
hdf : 1 < f d
⊢ ∏ m ∈ s.erase d, f m < f d * ∏ x ∈ s.erase d, f x

Proof state:
α : Type u_3
γ : Type u_6
inst✝³ : DecidableEq α
inst✝² : CommMonoid γ
inst✝¹ : Preorder γ
inst✝ : MulLeftStrictMono γ
s : Finset α
d : α
hd : d ∈ s
f : α → γ
hdf : 1 < f d
⊢ ∏ m ∈ s.erase d, f m < f d * ∏ x ∈ s.erase d, f x

Tactic:
exact lt_mul_of_one_lt_left' _ hdf

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_of_not_mem_closure (hx : x ∉ closure s) :
    ContinuousWithinAt f s x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : x ∉ closure s
⊢ ContinuousWithinAt f s x

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ ContinuousWithinAt f s x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ Tendsto f ⊥ (𝓝 (f x))

Tactic:
exact tendsto_bot

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ ContinuousWithinAt f s x

Tactic:
rw [ContinuousWithinAt, hx]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ Tendsto f ⊥ (𝓝 (f x))