harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
lemma differentiableAt_comp_neg {a : 𝕜} :
    DifferentiableAt 𝕜 (fun x ↦ f (-x)) a ↔ DifferentiableAt 𝕜 f (-a)

Proof state:
case h.e'_11.h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (-x)) a
x✝ : 𝕜
⊢ f x✝ = ((fun x => f (-x)) ∘ Neg.neg) x✝

Tactic:
simp only [Function.comp_apply, neg_neg]

Result:
no goals

Proof state:
case h.e'_11
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (-x)) a
⊢ f = (fun x => f (-x)) ∘ Neg.neg

Tactic:
ext

Result:
case h.e'_11.h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (-x)) a
x✝ : 𝕜
⊢ f x✝ = ((fun x => f (-x)) ∘ Neg.neg) x✝

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
⊢ DifferentiableAt 𝕜 (fun x => f (-x)) a ↔ DifferentiableAt 𝕜 f (-a)

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H.comp a differentiable_neg.differentiableAt⟩

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (-x)) a
⊢ DifferentiableAt 𝕜 f (-a)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (-x)) a
⊢ DifferentiableAt 𝕜 f (-a)

Tactic:
convert ((neg_neg a).symm ▸ H).comp (-a) differentiable_neg.differentiableAt

Result:
case h.e'_11
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (-x)) a
⊢ f = (fun x => f (-x)) ∘ Neg.neg
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eval_basis_self (hvs : Set.InjOn v s) (hi : i ∈ s) :
    (Lagrange.basis s v i).eval (v i) = 1

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∏ j ∈ s.erase i, eval (v i) (basisDivisor (v i) (v j)) = 1

Tactic:
refine prod_eq_one fun j H => ?_

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ eval (v i) (basisDivisor (v i) (v j)) = 1

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) (Lagrange.basis s v i) = 1

Tactic:
rw [Lagrange.basis, eval_prod]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∏ j ∈ s.erase i, eval (v i) (basisDivisor (v i) (v j)) = 1

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ eval (v i) (basisDivisor (v i) (v j)) = 1

Tactic:
rw [eval_basisDivisor_left_of_ne]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ v i ≠ v j

Proof state:
case intro
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
hij : j ≠ i
hj : j ∈ s
⊢ v i ≠ v j

Tactic:
exact mt (hvs hi hj) hij.symm

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ v i ≠ v j

Tactic:
rcases mem_erase.mp H with ⟨hij, hj⟩

Result:
case intro
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
hij : j ≠ i
hj : j ∈ s
⊢ v i ≠ v j
-- Mathlib/Algebra/Group/AddChar.lean
lemma compAddMonoidHom_injective_right (ψ : AddChar B M) (hψ : Injective ψ) :
    Injective fun f : A →+ B ↦ ψ.compAddMonoidHom f

Proof state:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
ψ : AddChar B M
hψ : Injective ⇑ψ
f g : A →+ B
h : (fun f => ψ.compAddMonoidHom f) f = (fun f => ψ.compAddMonoidHom f) g
⊢ f = g

Tactic:
rw [DFunLike.ext'_iff] at h ⊢

Result:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
ψ : AddChar B M
hψ : Injective ⇑ψ
f g : A →+ B
h : ⇑((fun f => ψ.compAddMonoidHom f) f) = ⇑((fun f => ψ.compAddMonoidHom f) g)
⊢ ⇑f = ⇑g

Proof state:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
ψ : AddChar B M
hψ : Injective ⇑ψ
f g : A →+ B
h : ⇑((fun f => ψ.compAddMonoidHom f) f) = ⇑((fun f => ψ.compAddMonoidHom f) g)
⊢ ⇑f = ⇑g

Tactic:
exact hψ.comp_left h

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
ψ : AddChar B M
hψ : Injective ⇑ψ
⊢ Injective fun f => ψ.compAddMonoidHom f

Tactic:
rintro f g h

Result:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
ψ : AddChar B M
hψ : Injective ⇑ψ
f g : A →+ B
h : (fun f => ψ.compAddMonoidHom f) f = (fun f => ψ.compAddMonoidHom f) g
⊢ f = g
-- Mathlib/Analysis/Polynomial/CauchyBound.lean
@[simp]
lemma cauchyBound_X_add_C (x : K) : cauchyBound (X + C x) = ‖x‖₊ + 1

Proof state:
K : Type u_1
inst✝ : NormedDivisionRing K
x : K
⊢ (X + C x).cauchyBound = ‖x‖₊ + 1

Tactic:
simp [cauchyBound]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem Perm.extendDomain_apply_not_subtype {b : β'} (h : ¬p b) : e.extendDomain f b = b

Proof state:
α' : Type u_9
β' : Type u_10
e : Perm α'
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
b : β'
h : ¬p b
⊢ (e.extendDomain f) b = b

Tactic:
simp [Perm.extendDomain, h]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_le_of_le_one_left [SMulPosMono α β] (hb : 0 ≤ b) (h : a ≤ 1) : a • b ≤ b

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Monoid α
inst✝⁴ : Zero β
inst✝³ : MulAction α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
hb : 0 ≤ b
h : a ≤ 1
⊢ a • b ≤ b

Tactic:
simpa only [one_smul] using smul_le_smul_of_nonneg_right h hb

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
lemma sumAlgEquiv_comp_rename_inl :
    (sumAlgEquiv R S₁ S₂).toAlgHom.comp (rename Sum.inl) =
      MvPolynomial.mapAlgHom (Algebra.ofId _ _)

Proof state:
case hf.a.a
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
i : S₁
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ (((↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inl)) (X i))) =
    coeff m✝ (coeff m✝¹ ((mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R))) (X i)))

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
⊢ (↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inl) = mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R))

Tactic:
ext i

Result:
case hf.a.a
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
i : S₁
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ (((↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inl)) (X i))) =
    coeff m✝ (coeff m✝¹ ((mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R))) (X i)))
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_neg_left {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    o.oangle (-x) y = o.oangle x y + π

Proof state:
case convert_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.kahler x) y ≠ 0

Tactic:
exact o.kahler_ne_zero hx hy

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑((-o.kahler x) y).arg = ↑((o.kahler x) y).arg + ↑π

Tactic:
convert Complex.arg_neg_coe_angle _

Result:
case convert_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.kahler x) y ≠ 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ o.oangle (-x) y = o.oangle x y + ↑π

Tactic:
simp only [oangle, map_neg]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑((-o.kahler x) y).arg = ↑((o.kahler x) y).arg + ↑π
-- Mathlib/Algebra/FreeAlgebra.lean
theorem ι_injective [Nontrivial R] : Function.Injective (ι R : X → FreeAlgebra R X) :=
  fun x y hoxy ↦
  by_contradiction <| by
    classical exact fun hxy : x ≠ y ↦
        let f : FreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
        have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
        have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
        have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
        one_ne_zero <| hfy1.symm.trans hfy0

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x y : X
hoxy : ι R x = ι R y
⊢ ¬x = y → False

Tactic:
classical exact fun hxy : x ≠ y ↦
    let f : FreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
    have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
    have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
    have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
    one_ne_zero <| hfy1.symm.trans hfy0

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x y : X
hoxy : ι R x = ι R y
⊢ ¬x = y → False

Tactic:
exact fun hxy : x ≠ y ↦
let f : FreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
one_ne_zero <| hfy1.symm.trans hfy0

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem deriv_id_of_nfp_id (h : nfp f = id) : deriv f = id :=
  ((isNormal_deriv _).eq_iff_zero_and_succ IsNormal.refl).2 (by simp [h])

Proof state:
f : Ordinal.{u} → Ordinal.{u}
h : nfp f = id
⊢ deriv f 0 = id 0 ∧ ∀ (a : Ordinal.{u}), deriv f a = id a → deriv f (succ a) = id (succ a)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Control/Fold.lean
theorem toList_map (f : α → β) (xs : t α) : toList (f <$> xs) = f <$> toList xs

Proof state:
α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β
xs : t α
⊢ toList (f <$> xs) = f <$> toList xs

Tactic:
simp only [toList_spec, Free.map_eq_map, foldMap_hom, foldMap_map, FreeMonoid.ofList_toList,
  FreeMonoid.map_of, Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k

Proof state:
case zero
m k : Nat
⊢ 0 = 0 + 0 * k

Tactic:
rw [Nat.zero_mul]

Result:
no goals

Proof state:
case succ
m k n : Nat
ih : n * (m + k) = n * m + n * k
⊢ (n + 1) * (m + k) = (n + 1) * m + (n + 1) * k

Tactic:
simp [succ_mul, ih]

Result:
case succ
m k n : Nat
ih : n * (m + k) = n * m + n * k
⊢ n * m + n * k + (m + k) = n * m + m + (n * k + k)

Proof state:
case succ.h
m k n : Nat
ih : n * (m + k) = n * m + n * k
⊢ n * k + (m + k) = m + (n * k + k)

Tactic:
apply Nat.add_left_comm

Result:
no goals

Proof state:
case succ
m k n : Nat
ih : n * (m + k) = n * m + n * k
⊢ n * m + n * k + (m + k) = n * m + m + (n * k + k)

Tactic:
rw [Nat.add_assoc, Nat.add_assoc (n*m)]

Result:
case succ
m k n : Nat
ih : n * (m + k) = n * m + n * k
⊢ n * m + (n * k + (m + k)) = n * m + (m + (n * k + k))

Proof state:
n m k : Nat
⊢ n * (m + k) = n * m + n * k

Tactic:
induction n with
| zero      => repeat rw [Nat.zero_mul]
| succ n ih => simp [succ_mul, ih]; rw [Nat.add_assoc, Nat.add_assoc (n*m)]; apply congrArg; apply Nat.add_left_comm

Result:
no goals

Proof state:
case succ
m k n : Nat
ih : n * (m + k) = n * m + n * k
⊢ n * m + (n * k + (m + k)) = n * m + (m + (n * k + k))

Tactic:
apply congrArg

Result:
case succ.h
m k n : Nat
ih : n * (m + k) = n * m + n * k
⊢ n * k + (m + k) = m + (n * k + k)

Proof state:
case zero
m k : Nat
⊢ 0 * (m + k) = 0 * m + 0 * k

Tactic:
repeat rw [Nat.zero_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem mapComp_eq {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) :
    map (f ≫ g) = (map g) ⋙ (map f)

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ autoParam
    (∀ (X_1 Y_1 : Under Z) (f_1 : X_1 ⟶ Y_1), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map g ⋙ map f).map f_1 ≫ eqToHom ⋯)
    _auto✝

Tactic:
intro U V k

Result:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Under Z
k : U ⟶ V
⊢ (map (f ≫ g)).map k = eqToHom ⋯ ≫ (map g ⋙ map f).map k ≫ eqToHom ⋯

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Under Z
k : U ⟶ V
⊢ (map (f ≫ g)).map k = eqToHom ⋯ ≫ (map g ⋙ map f).map k ≫ eqToHom ⋯

Tactic:
ext

Result:
case h_map.h
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Under Z
k : U ⟶ V
⊢ ((map (f ≫ g)).map k).right = (eqToHom ⋯ ≫ (map g ⋙ map f).map k ≫ eqToHom ⋯).right

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (X_1 : Under Z), (map (f ≫ g)).obj X_1 = (map g ⋙ map f).obj X_1

Tactic:
simp [Under.map, Comma.mapLeft]

Result:
no goals

Proof state:
case h_map.h
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Under Z
k : U ⟶ V
⊢ ((map (f ≫ g)).map k).right = (eqToHom ⋯ ≫ (map g ⋙ map f).map k ≫ eqToHom ⋯).right

Tactic:
simp

Result:
no goals

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ map (f ≫ g) = map g ⋙ map f

Tactic:
fapply Functor.ext

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (X_1 : Under Z), (map (f ≫ g)).obj X_1 = (map g ⋙ map f).obj X_1

case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ autoParam
    (∀ (X_1 Y_1 : Under Z) (f_1 : X_1 ⟶ Y_1), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map g ⋙ map f).map f_1 ≫ eqToHom ⋯)
    _auto✝
-- Mathlib/Algebra/Vertex/HVertexOperator.lean
theorem coeff_inj : Function.Injective (coeff : HVertexOperator Γ R V W → Γ → (V →ₗ[R] W))

Proof state:
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
a₁✝ a₂✝ : HVertexOperator Γ R V W
h : a₁✝.coeff = a₂✝.coeff
⊢ a₁✝ = a₂✝

Tactic:
ext v n

Result:
case h.h.h
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
a₁✝ a₂✝ : HVertexOperator Γ R V W
h : a₁✝.coeff = a₂✝.coeff
v : V
n : Γ
⊢ ((of R).symm (a₁✝ v)).coeff n = ((of R).symm (a₂✝ v)).coeff n

Proof state:
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
⊢ Function.Injective coeff

Tactic:
intro _ _ h

Result:
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
a₁✝ a₂✝ : HVertexOperator Γ R V W
h : a₁✝.coeff = a₂✝.coeff
⊢ a₁✝ = a₂✝

Proof state:
case h.h.h
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
a₁✝ a₂✝ : HVertexOperator Γ R V W
h : a₁✝.coeff = a₂✝.coeff
v : V
n : Γ
⊢ ((of R).symm (a₁✝ v)).coeff n = ((of R).symm (a₂✝ v)).coeff n

Tactic:
exact congrFun (congrArg DFunLike.coe (congrFun h n)) v

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem toSubmodule_bot : (⊥ : NonUnitalSubalgebra R A).toSubmodule = ⊥

Proof state:
case h
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x✝ : A
⊢ x✝ ∈ ⊥.toSubmodule ↔ x✝ ∈ ⊥

Tactic:
simp only [mem_bot, NonUnitalSubalgebra.mem_toSubmodule, Submodule.mem_bot]

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ ⊥.toSubmodule = ⊥

Tactic:
ext

Result:
case h
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x✝ : A
⊢ x✝ ∈ ⊥.toSubmodule ↔ x✝ ∈ ⊥
-- Mathlib/Topology/Filter.lean
theorem tendsto_nhds {la : Filter α} {lb : Filter β} {f : α → Filter β} :
    Tendsto f la (𝓝 lb) ↔ ∀ s ∈ lb, ∀ᶠ a in la, s ∈ f a

Proof state:
α : Type u_2
β : Type u_3
la : Filter α
lb : Filter β
f : α → Filter β
⊢ Tendsto f la (𝓝 lb) ↔ ∀ s ∈ lb, ∀ᶠ (a : α) in la, s ∈ f a

Tactic:
simp only [nhds_eq', tendsto_lift', mem_setOf_eq]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem isPreconnected_setOf_wSameSide (s : AffineSubspace ℝ P) (x : P) :
    IsPreconnected { y | s.WSameSide x y }

Proof state:
case inr
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
⊢ IsPreconnected {y | s.WSameSide x y}

Tactic:
exact (isConnected_setOf_wSameSide x h).isPreconnected

Result:
no goals

Proof state:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | False}

Tactic:
exact isPreconnected_empty

Result:
no goals

Proof state:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | s.WSameSide x y}

Tactic:
simp only [h, not_wSameSide_bot]

Result:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | False}

Proof state:
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
⊢ IsPreconnected {y | s.WSameSide x y}

Tactic:
rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)

Result:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : ↑s = ∅
⊢ IsPreconnected {y | s.WSameSide x y}

case inr
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s).Nonempty
⊢ IsPreconnected {y | s.WSameSide x y}

Proof state:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : ↑s = ∅
⊢ IsPreconnected {y | s.WSameSide x y}

Tactic:
rw [coe_eq_bot_iff] at h

Result:
case inl
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
⊢ IsPreconnected {y | s.WSameSide x y}
-- Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
lemma map_mul_map_inv (g : GL n R) : map f g * map f g⁻¹ = 1

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (map f) g * (map f) g⁻¹ = 1

Tactic:
simp only [map_inv, mul_inv_cancel]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
/-- **Stirling's Formula**, formulated in terms of `Asymptotics.IsEquivalent`. -/
lemma factorial_isEquivalent_stirling :
    (fun n ↦ n ! : ℕ → ℝ) ~[atTop] fun n ↦ Real.sqrt (2 * n * π) * (n / exp 1) ^ n

Proof state:
case refine_2

⊢ Tendsto ((fun n => ↑n !) / fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n) atTop (𝓝 1)

Tactic:
have : sqrt π ≠ 0 := by positivity

Result:
case refine_2
this : √π ≠ 0
⊢ Tendsto ((fun n => ↑n !) / fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n) atTop (𝓝 1)

Proof state:
case refine_2
this : √π ≠ 0
⊢ Tendsto ((fun n => ↑n !) / fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n) atTop (𝓝 (√π / √π))

Tactic:
convert tendsto_stirlingSeq_sqrt_pi.div tendsto_const_nhds this using 1

Result:
case h.e'_3
this : √π ≠ 0
⊢ ((fun n => ↑n !) / fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n) = stirlingSeq / fun x => √π

Proof state:
⊢ (fun n => ↑n !) ~[atTop] fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n

Tactic:
refine Asymptotics.isEquivalent_of_tendsto_one ?_ ?_

Result:
case refine_1

⊢ ∀ᶠ (x : ℕ) in atTop, √(2 * ↑x * π) * (↑x / rexp 1) ^ x = 0 → ↑x ! = 0

case refine_2

⊢ Tendsto ((fun n => ↑n !) / fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n) atTop (𝓝 1)

Proof state:
case h.e'_3.h
this : √π ≠ 0
n : ℕ
⊢ ((fun n => ↑n !) / fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n) n = (stirlingSeq / fun x => √π) n

Tactic:
field_simp [stirlingSeq, mul_right_comm]

Result:
no goals

Proof state:
case h.e'_3
this : √π ≠ 0
⊢ ((fun n => ↑n !) / fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n) = stirlingSeq / fun x => √π

Tactic:
ext n

Result:
case h.e'_3.h
this : √π ≠ 0
n : ℕ
⊢ ((fun n => ↑n !) / fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n) n = (stirlingSeq / fun x => √π) n

Proof state:
n : ℕ
hn : n ≠ 0
h : √(2 * ↑n * π) * (↑n / rexp 1) ^ n = 0
⊢ ¬√(2 * ↑n * π) * (↑n / rexp 1) ^ n = 0

Tactic:
positivity

Result:
no goals

Proof state:
⊢ √π ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case refine_1

⊢ ∀ᶠ (x : ℕ) in atTop, √(2 * ↑x * π) * (↑x / rexp 1) ^ x = 0 → ↑x ! = 0

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn h

Result:
case h
n : ℕ
hn : n ≠ 0
h : √(2 * ↑n * π) * (↑n / rexp 1) ^ n = 0
⊢ ↑n ! = 0

Proof state:
case refine_2
this : √π ≠ 0
⊢ Tendsto ((fun n => ↑n !) / fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n) atTop (𝓝 1)

Tactic:
nth_rewrite 2 [← div_self this]

Result:
case refine_2
this : √π ≠ 0
⊢ Tendsto ((fun n => ↑n !) / fun n => √(2 * ↑n * π) * (↑n / rexp 1) ^ n) atTop (𝓝 (√π / √π))

Proof state:
case h
n : ℕ
hn : n ≠ 0
h : √(2 * ↑n * π) * (↑n / rexp 1) ^ n = 0
⊢ ↑n ! = 0

Tactic:
exact absurd h (by positivity)

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem isClosedMap_mk : IsClosedMap (mk : X → SeparationQuotient X) :=
  isInducing_mk.isClosedMap <| by rw [range_mk]; exact isClosed_univ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed univ

Tactic:
exact isClosed_univ

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed (Set.range mk)

Tactic:
rw [range_mk]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed univ