harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffOn_iff_of_subset_source' {x : M} {y : M'} (hs : s ⊆ (extChartAt I x).source)
    (h2s : MapsTo f s (extChartAt I' y).source) :
    ContMDiffOn I I' n f s ↔
        ContDiffOn 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (extChartAt I x '' s)

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
x : M
y : M'
hs : s ⊆ (extChartAt I x).source
h2s : MapsTo f s (extChartAt I' y).source
⊢ ContMDiffOn I I' n f s ↔ ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s)

Tactic:
rw [extChartAt_source] at hs h2s

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
x : M
y : M'
hs : s ⊆ (chartAt H x).source
h2s : MapsTo f s (chartAt H' y).source
⊢ ContMDiffOn I I' n f s ↔ ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s)

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
x : M
y : M'
hs : s ⊆ (chartAt H x).source
h2s : MapsTo f s (chartAt H' y).source
⊢ ContMDiffOn I I' n f s ↔ ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s)

Tactic:
exact contMDiffOn_iff_of_mem_maximalAtlas' (chart_mem_maximalAtlas x)
  (chart_mem_maximalAtlas y) hs h2s

Result:
no goals
-- Mathlib/Topology/Homotopy/HomotopyGroup.lean
theorem insertAt_boundary (i : N) {t₀ : I} {t}
    (H : (t₀ = 0 ∨ t₀ = 1) ∨ t ∈ boundary { j // j ≠ i }) : insertAt i ⟨t₀, t⟩ ∈ boundary N

Proof state:
case inr.intro
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N

Tactic:
use j

Result:
case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (insertAt i) (t₀, t) ↑j = 0 ∨ (insertAt i) (t₀, t) ↑j = 1

Proof state:
case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (insertAt i) (t₀, t) ↑j = 0 ∨ (insertAt i) (t₀, t) ↑j = 1

Tactic:
rwa [funSplitAt_symm_apply, dif_neg j.prop, Subtype.coe_eta]

Result:
no goals

Proof state:
case inl
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N

Tactic:
use i

Result:
case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (insertAt i) (t₀, t) i = 0 ∨ (insertAt i) (t₀, t) i = 1

Proof state:
case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (insertAt i) (t₀, t) i = 0 ∨ (insertAt i) (t₀, t) i = 1

Tactic:
rwa [funSplitAt_symm_apply, dif_pos rfl]

Result:
no goals

Proof state:
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : (t₀ = 0 ∨ t₀ = 1) ∨ t ∈ boundary { j // j ≠ i }
⊢ (insertAt i) (t₀, t) ∈ boundary N

Tactic:
obtain H | ⟨j, H⟩ := H

Result:
case inl
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N

case inr.intro
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd'_zero_add (a : A) :
    shiftFunctorAdd' C 0 a a (zero_add a) = (Functor.leftUnitor _).symm ≪≫
    isoWhiskerRight (shiftFunctorZero C A).symm (shiftFunctor C a)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
⊢ shiftFunctorAdd' C 0 a a ⋯ =
    (shiftFunctor C a).leftUnitor.symm ≪≫ isoWhiskerRight (shiftFunctorZero C A).symm (shiftFunctor C a)

Tactic:
ext X

Result:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd' C 0 a a ⋯).hom.app X =
    ((shiftFunctor C a).leftUnitor.symm ≪≫ isoWhiskerRight (shiftFunctorZero C A).symm (shiftFunctor C a)).hom.app X

Proof state:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ eqToHom ⋯ ≫ (shiftFunctorAdd C 0 a).hom.app X =
    eqToHom ⋯ ≫ (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) (𝟙_ (Discrete A)) { as := a }).app X

Tactic:
rfl

Result:
no goals

Proof state:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd' C 0 a a ⋯).hom.app X =
    ((shiftFunctor C a).leftUnitor.symm ≪≫ isoWhiskerRight (shiftFunctorZero C A).symm (shiftFunctor C a)).hom.app X

Tactic:
dsimp [shiftFunctorAdd', shiftFunctorZero, shiftFunctor]

Result:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (eqToHom ⋯).app X ≫ (shiftFunctorAdd C 0 a).hom.app X =
    𝟙 (((shiftMonoidalFunctor C A).obj { as := a }).obj X) ≫
      ((shiftMonoidalFunctor C A).obj { as := a }).map ((Functor.LaxMonoidal.ε (shiftMonoidalFunctor C A)).app X)

Proof state:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (eqToHom ⋯).app X ≫ (shiftFunctorAdd C 0 a).hom.app X =
    𝟙 (((shiftMonoidalFunctor C A).obj { as := a }).obj X) ≫
      ((shiftMonoidalFunctor C A).obj { as := a }).map ((Functor.LaxMonoidal.ε (shiftMonoidalFunctor C A)).app X)

Tactic:
simp only [eqToHom_app, obj_ε_app, Discrete.addMonoidal_leftUnitor, eqToIso.inv,
  eqToHom_map, Category.id_comp]

Result:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ eqToHom ⋯ ≫ (shiftFunctorAdd C 0 a).hom.app X =
    eqToHom ⋯ ≫ (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) (𝟙_ (Discrete A)) { as := a }).app X
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatMap_append (xs ys : List α) (f : α → List β) :
    (xs ++ ys).flatMap f = xs.flatMap f ++ ys.flatMap f

Proof state:
case cons
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : flatMap f (tail✝ ++ ys) = flatMap f tail✝ ++ flatMap f ys
⊢ flatMap f (head✝ :: tail✝ ++ ys) = flatMap f (head✝ :: tail✝) ++ flatMap f ys

Tactic:
simp_all [flatMap_cons, append_assoc]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
xs ys : List α
f : α → List β
⊢ flatMap f (xs ++ ys) = flatMap f xs ++ flatMap f ys

Tactic:
induction xs

Result:
case nil
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
⊢ flatMap f ([] ++ ys) = flatMap f [] ++ flatMap f ys

case cons
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : flatMap f (tail✝ ++ ys) = flatMap f tail✝ ++ flatMap f ys
⊢ flatMap f (head✝ :: tail✝ ++ ys) = flatMap f (head✝ :: tail✝) ++ flatMap f ys

Proof state:
case nil
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
⊢ flatMap f ([] ++ ys) = flatMap f [] ++ flatMap f ys

Tactic:
rfl

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
⊢ flatMap f ([] ++ ys) = flatMap f [] ++ flatMap f ys

case cons
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : flatMap f (tail✝ ++ ys) = flatMap f tail✝ ++ flatMap f ys
⊢ flatMap f (head✝ :: tail✝ ++ ys) = flatMap f (head✝ :: tail✝) ++ flatMap f ys

Tactic:
{rfl}

Result:
case cons
α : Type u_1
β : Type u_2
ys : List α
f : α → List β
head✝ : α
tail✝ : List α
tail_ih✝ : flatMap f (tail✝ ++ ys) = flatMap f tail✝ ++ flatMap f ys
⊢ flatMap f (head✝ :: tail✝ ++ ys) = flatMap f (head✝ :: tail✝) ++ flatMap f ys
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_univ (e : X ≃ᵢ Y) : dimH (univ : Set X) = dimH (univ : Set Y)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
e : X ≃ᵢ Y
⊢ dimH univ = dimH univ

Tactic:
rw [← e.dimH_preimage univ, preimage_univ]

Result:
no goals
-- Mathlib/Algebra/Homology/Localization.lean
lemma HomologicalComplex.homologyFunctor_inverts_quasiIso (i : ι) :
    (quasiIso C c).IsInvertedBy (homologyFunctor C c i) := fun _ _ _ hf => by
  rw [mem_quasiIso_iff] at hf
  dsimp
  infer_instance

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
inst✝ : CategoryWithHomology C
i : ι
x✝² x✝¹ : HomologicalComplex C c
x✝ : x✝² ⟶ x✝¹
hf : quasiIso C c x✝
⊢ IsIso ((homologyFunctor C c i).map x✝)

Tactic:
rw [mem_quasiIso_iff] at hf

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
inst✝ : CategoryWithHomology C
i : ι
x✝² x✝¹ : HomologicalComplex C c
x✝ : x✝² ⟶ x✝¹
hf : QuasiIso x✝
⊢ IsIso ((homologyFunctor C c i).map x✝)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
inst✝ : CategoryWithHomology C
i : ι
x✝² x✝¹ : HomologicalComplex C c
x✝ : x✝² ⟶ x✝¹
hf : QuasiIso x✝
⊢ IsIso (homologyMap x✝ i)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
inst✝ : CategoryWithHomology C
i : ι
x✝² x✝¹ : HomologicalComplex C c
x✝ : x✝² ⟶ x✝¹
hf : QuasiIso x✝
⊢ IsIso ((homologyFunctor C c i).map x✝)

Tactic:
dsimp

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
inst✝ : CategoryWithHomology C
i : ι
x✝² x✝¹ : HomologicalComplex C c
x✝ : x✝² ⟶ x✝¹
hf : QuasiIso x✝
⊢ IsIso (homologyMap x✝ i)
-- Mathlib/ModelTheory/Quotients.lean
theorem relMap_quotient_mk' {n : ℕ} (r : L.Relations n) (x : Fin n → M) :
    (RelMap r fun i => (⟦x i⟧ : Quotient s)) ↔ @RelMap _ _ ps.toStructure _ r x

Proof state:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ (RelMap r fun i => ⟦x i⟧) ↔ RelMap r x

Tactic:
change
  Quotient.lift (@RelMap L M ps.toStructure n r) Prestructure.rel_equiv (Quotient.finChoice _) ↔
    _

Result:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ Quotient.lift (RelMap r) ⋯ (Quotient.finChoice fun i => ⟦x i⟧) ↔ RelMap r x

Proof state:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ Quotient.lift (RelMap r) ⋯ (Quotient.finChoice fun i => ⟦x i⟧) ↔ RelMap r x

Tactic:
rw [Quotient.finChoice_eq, Quotient.lift_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α}
    (hl : DistinctKeys l) (h : Perm l l') : getValue? a l = getValue? a l'

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((_ : α) × β)
a : α
hl : DistinctKeys l
h : l.Perm l'
⊢ getValue? a l = getValue? a l'

Tactic:
simp only [getValue?_eq_getEntry?, getEntry?_of_perm hl h]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Ultra.lean
lemma isNonarchimedean_norm {R} [SeminormedAddCommGroup R] [IsUltrametricDist R] :
    IsNonarchimedean (‖·‖ : R → ℝ)

Proof state:
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
⊢ IsNonarchimedean fun x => ‖x‖

Tactic:
intro x y

Result:
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x => ‖x‖) (x + y) ≤ (fun x => ‖x‖) x ⊔ (fun x => ‖x‖) y

Proof state:
case h.e'_4
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x => ‖x‖) x ⊔ (fun x => ‖x‖) y = dist 0 x ⊔ dist x (x + y)

Tactic:
congr <;> simp [SeminormedAddGroup.dist_eq]

Result:
no goals

Proof state:
case h.e'_3
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x => ‖x‖) (x + y) = dist 0 (x + y)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x => ‖x‖) (x + y) ≤ (fun x => ‖x‖) x ⊔ (fun x => ‖x‖) y

Tactic:
convert dist_triangle_max 0 x (x + y) using 1

Result:
case h.e'_3
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x => ‖x‖) (x + y) = dist 0 (x + y)

case h.e'_4
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x => ‖x‖) x ⊔ (fun x => ‖x‖) y = dist 0 x ⊔ dist x (x + y)
-- Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean
theorem dist_smul_Lp (c : Mᵈᵐᵃ) (f g : Lp E p μ) : dist (c • f) (c • g) = dist f g

Proof state:
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
f g : ↥(Lp E p μ)
⊢ dist (c • f) (c • g) = dist f g

Tactic:
simp only [dist, ← smul_Lp_sub, norm_smul_Lp]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negY_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.negY P / P z ^ 3 = W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3)

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negY P / P z ^ 3 = (toAffine W).negY (P x / P z ^ 2) (P y / P z ^ 3)

Tactic:
linear_combination (norm := (rw [negY, Affine.negY]; ring1))
  -W.a₁ * P x / P z ^ 2 * div_self hPz - W.a₃ * div_self (pow_ne_zero 3 hPz)

Result:
no goals

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negY P / P z ^ 3 + (-W.a₁ * P x / P z ^ 2 * 1 + W.a₃ * (P z ^ 3 / P z ^ 3)) -
      ((toAffine W).negY (P x / P z ^ 2) (P y / P z ^ 3) + (-W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * 1)) =
    0

Tactic:
rw [negY, Affine.negY]

Result:
case a.a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (-P y - W.a₁ * P x * P z - W.a₃ * P z ^ 3) / P z ^ 3 + (-W.a₁ * P x / P z ^ 2 * 1 + W.a₃ * (P z ^ 3 / P z ^ 3)) -
      (-(P y / P z ^ 3) - (toAffine W).a₁ * (P x / P z ^ 2) - (toAffine W).a₃ +
        (-W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * 1)) =
    0

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (-P y - W.a₁ * P x * P z - W.a₃ * P z ^ 3) / P z ^ 3 + (-W.a₁ * P x / P z ^ 2 * 1 + W.a₃ * (P z ^ 3 / P z ^ 3)) -
      (-(P y / P z ^ 3) - (toAffine W).a₁ * (P x / P z ^ 2) - (toAffine W).a₃ +
        (-W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * 1)) =
    0

Tactic:
ring1

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_eval {R} [CommSemiring R] (r : R) (f : R[X]) (s : R) :
    (taylor r f).eval s = f.eval (s + r)

Proof state:
R : Type u_2
inst✝ : CommSemiring R
r : R
f : R[X]
s : R
⊢ eval s ((taylor r) f) = eval (s + r) f

Tactic:
simp only [taylor_apply, eval_comp, eval_C, eval_X, eval_add]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem convs'Aux_succ_some {s : Stream'.Seq (Pair K)} {p : Pair K} (h : s.head = some p)
    (n : ℕ) : convs'Aux s (n + 1) = p.a / (p.b + convs'Aux s.tail n)

Proof state:
K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
p : Pair K
h : s.head = some p
n : ℕ
⊢ convs'Aux s (n + 1) = p.a / (p.b + convs'Aux s.tail n)

Tactic:
simp [convs'Aux, h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae
    (hab : IntervalIntegrable f volume a b) (hmeas_a : StronglyMeasurableAtFilter f la')
    (hmeas_b : StronglyMeasurableAtFilter f lb') (ha_lim : Tendsto f (la' ⊓ ae volume) (𝓝 ca))
    (hb_lim : Tendsto f (lb' ⊓ ae volume) (𝓝 cb)) (hua : Tendsto ua lt la) (hva : Tendsto va lt la)
    (hub : Tendsto ub lt lb) (hvb : Tendsto vb lt lb) :
    (fun t =>
        ((∫ x in va t..vb t, f x) - ∫ x in ua t..ub t, f x) -
          ((vb t - ub t) • cb - (va t - ua t) • ca)) =o[lt]
      fun t => ‖va t - ua t‖ + ‖vb t - ub t‖

Proof state:
ι : Type u_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ℝ → E
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
a b : ℝ
ua ub va vb : ι → ℝ
inst✝¹ : FTCFilter a la la'
inst✝ : FTCFilter b lb lb'
hab : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f la' volume
hmeas_b : StronglyMeasurableAtFilter f lb' volume
ha_lim : Tendsto f (la' ⊓ ae volume) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae volume) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
⊢ (fun t =>
      ((∫ (x : ℝ) in va t..vb t, f x) - ∫ (x : ℝ) in ua t..ub t, f x) -
        ((vb t - ub t) • cb - (va t - ua t) • ca)) =o[lt]
    fun t => ‖va t - ua t‖ + ‖vb t - ub t‖

Tactic:
simpa [integral_const]
  using measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hab hmeas_a hmeas_b
    ha_lim hb_lim hua hva hub hvb

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
theorem hasStrictDerivAt_log_of_pos (hx : 0 < x) : HasStrictDerivAt log x⁻¹ x

Proof state:
x : ℝ
hx : 0 < x
this : HasStrictDerivAt log (rexp (log x))⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x

Tactic:
rwa [exp_log hx] at this

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x

Tactic:
have : HasStrictDerivAt log (exp <| log x)⁻¹ x :=
  (hasStrictDerivAt_exp <| log x).of_local_left_inverse (continuousAt_log hx.ne')
      (ne_of_gt <| exp_pos _) <|
    Eventually.mono (lt_mem_nhds hx) @exp_log

Result:
x : ℝ
hx : 0 < x
this : HasStrictDerivAt log (rexp (log x))⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_push_of_neg (l) (pa : ¬p a) : countP p (l.push a) = countP p l

Proof state:
α : Type u_1
p : α → Bool
a : α
l : Array α
pa : ¬p a = true
⊢ countP p (l.push a) = countP p l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
a : α
pa : ¬p a = true
l : List α
⊢ countP p ({ toList := l }.push a) = countP p { toList := l }

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
pa : ¬p a = true
l : List α
⊢ countP p ({ toList := l }.push a) = countP p { toList := l }

Tactic:
simp_all

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_rightAngleRotation_left (x y : E) :
    o.kahler (J x) y = -Complex.I * o.kahler x y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑((o.areaForm x) y) + -↑(inner x y) * Complex.I = -Complex.I * (↑(inner x y) + ↑((o.areaForm x) y) * Complex.I)

Tactic:
linear_combination ω x y * Complex.I_sq

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.kahler (o.rightAngleRotation x)) y = -Complex.I * (o.kahler x) y

Tactic:
simp only [o.areaForm_rightAngleRotation_left, o.inner_rightAngleRotation_left,
  o.kahler_apply_apply, Complex.ofReal_neg, Complex.real_smul]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑((o.areaForm x) y) + -↑(inner x y) * Complex.I = -Complex.I * (↑(inner x y) + ↑((o.areaForm x) y) * Complex.I)
-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem mul_assoc_flip :
    (M.X ◁ M.mul) ≫ M.mul = (α_ M.X M.X M.X).inv ≫ (M.mul ▷ M.X) ≫ M.mul

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M : Mon_ C
⊢ M.X ◁ M.mul ≫ M.mul = (α_ M.X M.X M.X).inv ≫ M.mul ▷ M.X ≫ M.mul

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive] lemma prod_eq_one (hl : ∀ x ∈ l, x = 1) : l.prod = 1

Proof state:
M : Type u_4
inst✝ : Monoid M
l : List M
hl : ∀ (x : M), x ∈ l → x = 1
⊢ l.prod = 1

Tactic:
induction l with
| nil => rfl
| cons i l hil =>
  rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
    hl _ (mem_cons_self i l), one_mul]

Result:
no goals

Proof state:
case cons
M : Type u_4
inst✝ : Monoid M
l✝ : List M
i : M
l : List M
hil : (∀ (x : M), x ∈ l → x = 1) → l.prod = 1
hl : ∀ (x : M), x ∈ i :: l → x = 1
⊢ (i :: l).prod = 1

Tactic:
rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
  hl _ (mem_cons_self i l), one_mul]

Result:
no goals

Proof state:
case nil
M : Type u_4
inst✝ : Monoid M
l : List M
hl : ∀ (x : M), x ∈ [] → x = 1
⊢ [].prod = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem oreDiv_one_smul (r : M) (x : X[S⁻¹]) : (r /ₒ (1 : S)) • x = r • x

Proof state:
case c
M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
r' : X
s : ↥S
⊢ (r /ₒ 1) • (r' /ₒ s) = r • (r' /ₒ s)

Tactic:
rw [smul_oreDiv, oreDiv_smul_oreDiv, mul_one, smul_eq_mul, mul_one]

Result:
no goals

Proof state:
M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
x : OreLocalization S X
⊢ (r /ₒ 1) • x = r • x

Tactic:
induction' x using OreLocalization.ind with r' s

Result:
case c
M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
r' : X
s : ↥S
⊢ (r /ₒ 1) • (r' /ₒ s) = r • (r' /ₒ s)
-- Mathlib/Data/List/Sublists.lean
theorem length_sublists (l : List α) : length (sublists l) = 2 ^ length l

Proof state:
α : Type u
l : List α
⊢ l.sublists.length = 2 ^ l.length

Tactic:
simp only [sublists_eq_sublists', length_map, length_sublists', length_reverse]

Result:
no goals