harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean
theorem homothety_neg_one_apply (c p : P₁) : homothety c (-1 : R') p = pointReflection R' c p

Proof state:
P₁ : Type u_2
V₁ : Type u_6
inst✝³ : AddCommGroup V₁
inst✝² : AffineSpace V₁ P₁
R' : Type u_10
inst✝¹ : CommRing R'
inst✝ : Module R' V₁
c p : P₁
⊢ (homothety c (-1)) p = (pointReflection R' c) p

Tactic:
simp [homothety_apply, Equiv.pointReflection_apply]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem sSup_image' {s : Set β} {f : β → α} : sSup (f '' s) = ⨆ a : s, f a

Proof state:
α : Type u_1
β : Type u_2
inst✝ : SupSet α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ a, f ↑a

Tactic:
rw [iSup, image_eq_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SizeOf.lean
theorem Bool.sizeOf_eq_one (b : Bool) : sizeOf b = 1

Proof state:
b : Bool
⊢ sizeOf b = 1

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblX_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy : P y * Q z ≠ W.negY Q * P z) :
    W.dblX P / W.dblZ P = W.toAffine.addX (P x / P z) (Q x / Q z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.dblX P / W.dblZ P =
    (toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
rw [dblX_eq hP hPz, dblZ, toAffine_slope_of_eq hP hQ hPz hQz hx hy, ← (X_eq_iff hPz hQz).mp hx,
  toAffine_addX_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hPz hQz hx hy]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/Stalks.lean
theorem congr_point {X Y : PresheafedSpace.{_, _, v} C}
    (α : X ⟶ Y) (x x' : X) (h : x = x') :
    α.stalkMap x ≫ eqToHom (show X.presheaf.stalk x = X.presheaf.stalk x' by rw [h]) =
      eqToHom (show Y.presheaf.stalk (α.base x) =
        Y.presheaf.stalk (α.base x') by rw [h]) ≫ α.stalkMap x'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ Hom.stalkMap α x ≫ eqToHom ⋯ = eqToHom ⋯ ≫ Hom.stalkMap α x'

Tactic:
rw [stalkMap.congr α α rfl x x' h]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ Y.presheaf.stalk ((ConcreteCategory.hom α.base) x) = Y.presheaf.stalk ((ConcreteCategory.hom α.base) x')

Tactic:
rw [h]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ X.presheaf.stalk x = X.presheaf.stalk x'

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem cons_transpose (v : n' → α) (A : Matrix (Fin m) n' α) :
    (of (vecCons v A))ᵀ = of fun i => vecCons (v i) (Aᵀ i)

Proof state:
case a
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ (of (vecCons v A))ᵀ i j = of (fun i => vecCons (v i) (Aᵀ i)) i j

Tactic:
refine Fin.cases ?_ ?_ j <;> simp

Result:
no goals

Proof state:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
⊢ (of (vecCons v A))ᵀ = of fun i => vecCons (v i) (Aᵀ i)

Tactic:
ext i j

Result:
case a
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ (of (vecCons v A))ᵀ i j = of (fun i => vecCons (v i) (Aᵀ i)) i j
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem isNat_rpow_neg {a b : ℝ} {nb ne : ℕ}
    (pb : IsInt b (Int.negOfNat nb)) (pe' : IsNat (a ^ (Int.negOfNat nb)) ne) :
    IsNat (a ^ b) ne

Proof state:
a b : ℝ
nb ne : ℕ
pb : IsInt b (Int.negOfNat nb)
pe' : IsNat (a ^ Int.negOfNat nb) ne
⊢ IsNat (a ^ b) ne

Tactic:
rwa [pb.out, Real.rpow_intCast]

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Basic.lean
theorem vsub_right_cancel {p₁ p₂ p : P} (h : p -ᵥ p₁ = p -ᵥ p₂) : p₁ = p₂

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
h : p -ᵥ p₁ = p -ᵥ p₂
⊢ (p -ᵥ p₂) +ᵥ p₁ = (p -ᵥ p₂) +ᵥ p₂

Tactic:
rw [vsub_vadd, ← h, vsub_vadd]

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
h : p -ᵥ p₁ = p -ᵥ p₂
⊢ p₁ = p₂

Tactic:
refine vadd_left_cancel (p -ᵥ p₂) ?_

Result:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ p : P
h : p -ᵥ p₁ = p -ᵥ p₂
⊢ (p -ᵥ p₂) +ᵥ p₁ = (p -ᵥ p₂) +ᵥ p₂
-- Mathlib/CategoryTheory/GradedObject.lean
lemma hasMap_of_iso (e : X ≅ Y) (p: I → J) [HasMap X p] : HasMap Y p := fun j => by
  have α : Discrete.functor (X.mapObjFun p j) ≅ Discrete.functor (Y.mapObjFun p j) :=
    Discrete.natIso (fun ⟨i, _⟩ => (GradedObject.eval i).mapIso e)
  exact hasColimitOfIso α.symm

Proof state:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝¹ : Category.{u_5, u_4} C
X Y : GradedObject I C
e : X ≅ Y
p : I → J
inst✝ : X.HasMap p
j : J
⊢ HasCoproduct (Y.mapObjFun p j)

Tactic:
have α : Discrete.functor (X.mapObjFun p j) ≅ Discrete.functor (Y.mapObjFun p j) :=
  Discrete.natIso (fun ⟨i, _⟩ => (GradedObject.eval i).mapIso e)

Result:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝¹ : Category.{u_5, u_4} C
X Y : GradedObject I C
e : X ≅ Y
p : I → J
inst✝ : X.HasMap p
j : J
α : Discrete.functor (X.mapObjFun p j) ≅ Discrete.functor (Y.mapObjFun p j)
⊢ HasCoproduct (Y.mapObjFun p j)

Proof state:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝¹ : Category.{u_5, u_4} C
X Y : GradedObject I C
e : X ≅ Y
p : I → J
inst✝ : X.HasMap p
j : J
α : Discrete.functor (X.mapObjFun p j) ≅ Discrete.functor (Y.mapObjFun p j)
⊢ HasCoproduct (Y.mapObjFun p j)

Tactic:
exact hasColimitOfIso α.symm

Result:
no goals
-- Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
@[simp]
lemma hasCardinalLT_aleph0_iff (X : Type u) :
    HasCardinalLT X Cardinal.aleph0.{v} ↔ Finite X

Proof state:
X : Type u
⊢ HasCardinalLT X Cardinal.aleph0 ↔ Finite X

Tactic:
simpa [HasCardinalLT] using Cardinal.mk_lt_aleph0_iff

Result:
no goals
-- Mathlib/Probability/Kernel/Integral.lean
theorem integral_const {μ : Measure β} : ∫ x, f x ∂const α μ a = ∫ x, f x ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
μ : Measure β
⊢ ∫ (x : β), f x ∂(const α μ) a = ∫ (x : β), f x ∂μ

Tactic:
rw [const_apply]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
@[simp] lemma mpullback_id {V : Π (x : M), TangentSpace I x} : mpullback I I id V = V

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
V : (x : M) → TangentSpace I x
⊢ mpullback I I _root_.id V = V

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
V : (x : M) → TangentSpace I x
x : M
⊢ mpullback I I _root_.id V x = V x

Proof state:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
V : (x : M) → TangentSpace I x
x : M
⊢ mpullback I I _root_.id V x = V x

Tactic:
simp [mpullback]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem snd : IsBoundedLinearMap 𝕜 fun x : E × F => x.2

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E × F
⊢ ‖(LinearMap.snd 𝕜 E F) x‖ ≤ 1 * ‖x‖

Tactic:
rw [one_mul]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E × F
⊢ ‖(LinearMap.snd 𝕜 E F) x‖ ≤ ‖x‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E × F
⊢ ‖(LinearMap.snd 𝕜 E F) x‖ ≤ ‖x‖

Tactic:
exact le_max_right _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ IsBoundedLinearMap 𝕜 fun x => x.2

Tactic:
refine (LinearMap.snd 𝕜 E F).isLinear.with_bound 1 fun x => ?_

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E × F
⊢ ‖(LinearMap.snd 𝕜 E F) x‖ ≤ 1 * ‖x‖
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma exists_ne_zero_of_expect_ne_zero (h : 𝔼 i ∈ s, f i ≠ 0) : ∃ i ∈ s, f i ≠ 0

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
h : 𝔼 i ∈ s, f i ≠ 0
⊢ ∃ i ∈ s, f i ≠ 0

Tactic:
contrapose! h

Result:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
h : ∀ i ∈ s, f i = 0
⊢ 𝔼 i ∈ s, f i = 0

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
h : ∀ i ∈ s, f i = 0
⊢ 𝔼 i ∈ s, f i = 0

Tactic:
exact expect_eq_zero h

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_eq_one_iff_eq_inv' : a * b = 1 ↔ b = a⁻¹

Proof state:
G : Type u_3
inst✝ : Group G
a b : G
⊢ a * b = 1 ↔ b = a⁻¹

Tactic:
rw [mul_eq_one_iff_inv_eq, eq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
theorem cancel_natIso_inv_right_assoc {W X X' : D} {Y : C} (f : W ⟶ X) (g : X ⟶ G.obj Y)
    (f' : W ⟶ X') (g' : X' ⟶ G.obj Y) :
    f ≫ g ≫ α.inv.app Y = f' ≫ g' ≫ α.inv.app Y ↔ f ≫ g = f' ≫ g'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
W X X' : D
Y : C
f : W ⟶ X
g : X ⟶ G.obj Y
f' : W ⟶ X'
g' : X' ⟶ G.obj Y
⊢ f ≫ g ≫ α.inv.app Y = f' ≫ g' ≫ α.inv.app Y ↔ f ≫ g = f' ≫ g'

Tactic:
simp only [← Category.assoc, cancel_mono, refl]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod_isoCoprod_hom {X Y : C} [HasBinaryBiproduct X Y] :
    (biprod.isoCoprod X Y).hom = biprod.desc coprod.inl coprod.inr

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (biprod.isoCoprod X Y).hom = biprod.desc coprod.inl coprod.inr

Tactic:
ext <;> simp [← Iso.eq_comp_inv]

Result:
no goals
-- Mathlib/RingTheory/Localization/Submodule.lean
theorem coeSubmodule_bot : coeSubmodule S (⊥ : Ideal R) = ⊥

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ coeSubmodule S ⊥ = ⊥

Tactic:
rw [coeSubmodule, Submodule.map_bot]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToHom_trans {X Y Z : C} (p : X = Y) (q : Y = Z) :
    eqToHom p ≫ eqToHom q = eqToHom (p.trans q)

Proof state:
case refl.refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ eqToHom p ≫ eqToHom q = eqToHom ⋯

Tactic:
cases p

Result:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X = Z
⊢ eqToHom ⋯ ≫ eqToHom q = eqToHom ⋯

Proof state:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X = Z
⊢ eqToHom ⋯ ≫ eqToHom q = eqToHom ⋯

Tactic:
cases q

Result:
case refl.refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯
-- Mathlib/Algebra/Polynomial/Degree/Support.lean
theorem nonempty_support_iff : p.support.Nonempty ↔ p ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.support.Nonempty ↔ p ≠ 0

Tactic:
rw [Ne, nonempty_iff_ne_empty, Ne, ← support_eq_empty]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem filter_false (l : List α) :
    filter (fun _ => false) l = []

Proof state:
α : Type u
l : List α
⊢ filter (fun x => false) l = []

Tactic:
induction l <;> simp [*, filter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.countP_eq (p : α → Bool) {l₁ l₂ : List α} (s : l₁ ~ l₂) :
    countP p l₁ = countP p l₂

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ ~ l₂
⊢ (List.filter p l₁).length = (List.filter p l₂).length

Tactic:
exact (s.filter _).length_eq

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ ~ l₂
⊢ countP p l₁ = countP p l₂

Tactic:
simp only [countP_eq_length_filter]

Result:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ ~ l₂
⊢ (List.filter p l₁).length = (List.filter p l₂).length
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem map.id (x : FreeGroup α) : map id x = x

Proof state:
α : Type u
x : FreeGroup α
⊢ (map _root_.id) x = x

Tactic:
rcases x with ⟨L⟩

Result:
case mk
α : Type u
x : FreeGroup α
L : List (α × Bool)
⊢ (map _root_.id) (Quot.mk Red.Step L) = Quot.mk Red.Step L

Proof state:
case mk
α : Type u
x : FreeGroup α
L : List (α × Bool)
⊢ (map _root_.id) (Quot.mk Red.Step L) = Quot.mk Red.Step L

Tactic:
simp [List.map_id']

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma hasFPowerSeriesWithinAt_pi_iff :
    HasFPowerSeriesWithinAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) s e ↔
      ∀ i, HasFPowerSeriesWithinAt (f i) (p i) s e

Proof state:
case intro
𝕜 : 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
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
i : ι
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e r
⊢ HasFPowerSeriesWithinAt (f i) (p i) s e

Tactic:
exact ⟨r, (hasFPowerSeriesWithinOnBall_pi_iff hr.r_pos).1 hr i⟩

Result:
no goals

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
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e

Tactic:
refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩

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
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
h : HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e
i : ι
⊢ HasFPowerSeriesWithinAt (f i) (p i) s 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
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
h : HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e
i : ι
⊢ HasFPowerSeriesWithinAt (f i) (p i) s e

Tactic:
obtain ⟨r, hr⟩ := h

Result:
case intro
𝕜 : 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
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
i : ι
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e r
⊢ HasFPowerSeriesWithinAt (f i) (p i) s e
-- Mathlib/Data/Complex/Basic.lean
theorem mul_I_im (z : ℂ) : (z * I).im = z.re

Proof state:
z : ℂ
⊢ (z * I).im = z.re

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
theorem hasEigenvector_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0)
    (hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) :
    HasEigenvector (T : E →ₗ[𝕜] E) (↑(T.rayleighQuotient x₀)) x₀

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ ↑T x₀ = ↑(T.rayleighQuotient x₀) • x₀

Tactic:
exact hT.eq_smul_self_of_isLocalExtrOn hextr

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ HasEigenvector (↑T) (↑(T.rayleighQuotient x₀)) x₀

Tactic:
refine ⟨?_, hx₀⟩

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ x₀ ∈ (genEigenspace ↑T ↑(T.rayleighQuotient x₀)) 1

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ x₀ ∈ (genEigenspace ↑T ↑(T.rayleighQuotient x₀)) 1

Tactic:
rw [Module.End.mem_eigenspace_iff]

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ ↑T x₀ = ↑(T.rayleighQuotient x₀) • x₀
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_false_right : ∀(c t : Bool), cond c t false = ( c && t)

Proof state:
⊢ ∀ (c t : Bool), (bif c then t else false) = (c && t)

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem toNat_of_nonneg {a : Int} (h : 0 ≤ a) : (toNat a : Int) = a

Proof state:
a : Int
h : 0 ≤ a
⊢ ↑a.toNat = a

Tactic:
rw [toNat_eq_max, Int.max_eq_left h]

Result:
no goals
-- Mathlib/Algebra/Lie/Classical.lean
theorem pd_inv [Fintype l] [Invertible (2 : R)] : PD l R * ⅟ (2 : R) • (PD l R)ᵀ = 1

Proof state:
l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ fromBlocks (1 * ⅟2 • 1ᵀ + -1 * ⅟2 • (-1)ᵀ) (1 * ⅟2 • 1ᵀ + -1 * ⅟2 • 1ᵀ) (1 * ⅟2 • 1ᵀ + 1 * ⅟2 • (-1)ᵀ)
      (1 * ⅟2 • 1ᵀ + 1 * ⅟2 • 1ᵀ) =
    1

Tactic:
simp

Result:
no goals

Proof state:
l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ PD l R * ⅟2 • (PD l R)ᵀ = 1

Tactic:
rw [PD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_smul,
  Matrix.fromBlocks_multiply]

Result:
l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ fromBlocks (1 * ⅟2 • 1ᵀ + -1 * ⅟2 • (-1)ᵀ) (1 * ⅟2 • 1ᵀ + -1 * ⅟2 • 1ᵀ) (1 * ⅟2 • 1ᵀ + 1 * ⅟2 • (-1)ᵀ)
      (1 * ⅟2 • 1ᵀ + 1 * ⅟2 • 1ᵀ) =
    1
-- Mathlib/CategoryTheory/Equivalence.lean
theorem unitInv_app_inverse (e : C ≌ D) (Y : D) :
    e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.inverse.map (e.counit.app Y) = e.unitInv.app (e.inverse.obj Y)

Tactic:
erw [← Iso.hom_comp_eq_id (e.unitIso.app _), unit_inverse_comp]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ 𝟙 (e.inverse.obj Y) = 𝟙 ((𝟭 C).obj (e.inverse.obj Y))

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y)

Tactic:
symm

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.inverse.map (e.counit.app Y) = e.unitInv.app (e.inverse.obj Y)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ 𝟙 (e.inverse.obj Y) = 𝟙 ((𝟭 C).obj (e.inverse.obj Y))

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem strongInduction_eq {p : Finset α → Sort*} (H : ∀ s, (∀ t ⊂ s, p t) → p s)
    (s : Finset α) : strongInduction H s = H s fun t _ => strongInduction H t

Proof state:
α : Type u_1
p : Finset α → Sort u_4
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
s : Finset α
⊢ strongInduction H s = H s fun t x => strongInduction H t

Tactic:
rw [strongInduction]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_im_le_pi (x : ℂ) : (log x).im ≤ π

Proof state:
x : ℂ
⊢ (log x).im ≤ π

Tactic:
simp only [log_im, arg_le_pi]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_preimage_inter_eq (x : M) :
    (extChartAt I x).symm ⁻¹' (s ∩ t) ∩ range I =
      (extChartAt I x).symm ⁻¹' s ∩ range I ∩ (extChartAt I x).symm ⁻¹' t

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s t : Set M
inst✝ : ChartedSpace H M
x : M
⊢ ↑(extChartAt I x).symm ⁻¹' (s ∩ t) ∩ range ↑I = ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' t

Tactic:
mfld_set_tac

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem hasProd_subtype_iff_mulIndicator {s : Set β} :
    HasProd (f ∘ (↑) : s → α) a ↔ HasProd (s.mulIndicator f) a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set β
⊢ HasProd (f ∘ Subtype.val) a ↔ HasProd (s.mulIndicator f) a

Tactic:
rw [← Set.mulIndicator_range_comp, Subtype.range_coe,
  hasProd_subtype_iff_of_mulSupport_subset Set.mulSupport_mulIndicator_subset]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four (x y : E) :
    re ⟪x, y⟫ = (‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖ - (‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖)) / 4

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫_𝕜 = (‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4

Tactic:
rw [@norm_add_mul_self 𝕜, @norm_sub_mul_self 𝕜]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖ - (‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖)) / 4
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
lemma image_symm (e : α ≃ᵐ β) (s : Set β) : e.symm '' s = e ⁻¹' s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
⊢ ⇑e.symm '' s = ⇑e ⁻¹' s

Tactic:
rw [← symm_symm e, preimage_symm, symm_symm]

Result:
no goals