mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
this : Fintype.card σ = s.card
⊢ Multiset.map (fun i ↦ Polynomial.X + Polynomial.C (X i)) univ.val =
    Multiset.map (fun r ↦ Polynomial.X + Polynomial.C r) s

Tactic:
s,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
this : Fintype.card σ = s.card
⊢ Multiset.map (fun i ↦ Polynomial.X + Polynomial.C (X i)) univ.val =
    Multiset.map (fun r ↦ Polynomial.X + Polynomial.C r) (Multiset.map (fun i ↦ X i) univ.val)
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case e'_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
h : k ≤ s.card
this : Fintype.card σ = s.card
e_2✝ : AddMonoidAlgebra.semiring = AddMonoidAlgebra.commSemiring.toSemiring
⊢ Multiset.map (fun i ↦ Polynomial.X + Polynomial.C (X i)) univ.val =
    Multiset.map (fun r ↦ Polynomial.X + Polynomial.C r) s

Tactic:
s,

Goal state after:
case e'_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
h : k ≤ s.card
this : Fintype.card σ = s.card
e_2✝ : AddMonoidAlgebra.semiring = AddMonoidAlgebra.commSemiring.toSemiring
⊢ Multiset.map (fun i ↦ Polynomial.X + Polynomial.C (X i)) univ.val =
    Multiset.map (fun r ↦ Polynomial.X + Polynomial.C r) (Multiset.map (fun i ↦ X i) univ.val)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
φ : k →+* ℂ
⊢ K →+* ℂ

Tactic:
letI := φ.toAlgebra

Goal state after:
K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
φ : k →+* ℂ
this : Algebra k ℂ := φ.toAlgebra
⊢ K →+* ℂ
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
⊢ Fintype.card ↑(p.rootSet ℂ) = p.natDegree

Tactic:
simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]

Goal state after:
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
⊢ (p.aroots ℂ).toFinset.card = p.natDegree
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case mp.refine_2
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
hk' : 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1
⊢ mkRat (↑k * a.num - m) (k * a.den) ∈ ratLt y

Tactic:
have : k • a.num • 1 - k • a.den • y < m • 1 :=
        lt_of_lt_of_le (lt_add_of_pos_left _ zero_lt_one) (by simpa using hk'.trans hm1)

Goal state after:
case mp.refine_2
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
hk' : 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1
this : k • a.num • 1 - k • a.den • y < m • 1
⊢ mkRat (↑k * a.num - m) (k * a.den) ∈ ratLt y
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: case neg.inl
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
b : ValueGroupWithZero R
H : 0 < b
H' : 1 b ≤ 1 0
⊢ IsNontrivial R

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
this : u < e
⊢ (coeff (u, snd✝).1) x * (coeff (u, snd✝).2) φ = 0

Tactic:
simp only [he u this, zero_mul, map_zero]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d u snd✝ : σ →₀ ℕ
he : ∀ y < u, (coeff y) x = (coeff y) 0
huv : (u, snd✝) ∈ antidiagonal u
a✝ : (u, snd✝) ≠ (u, 0)
⊢ False

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsLeft R
x : MvPowerSeries σ R
hx : φ * x = 0
d fst✝ u : σ →₀ ℕ
he : ∀ y < u, (coeff y) x = (coeff y) 0
huv : (fst✝, u) ∈ antidiagonal u
a✝ : (fst✝, u) ≠ (0, u)
⊢ False

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬constantCoeff (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
rw [MvPowerSeries.inv_eq_iff_mul_eq_one h]

Goal state after:
case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬constantCoeff (φ * ψ) = 0
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: R : Type u_1
k : Type u_2
inst✝ : Field k
u : k⟦X⟧ˣ
⊢ (↑u).Unit_of_divided_by_X_pow_order⁻¹ = u⁻¹

Tactic:
set u₀ := u.1 with hu

Goal state after:
R : Type u_1
k : Type u_2
inst✝ : Field k
u : k⟦X⟧ˣ
u₀ : k⟦X⟧ := ↑u
hu : u₀ = ↑u
⊢ u₀.Unit_of_divided_by_X_pow_order⁻¹ = u⁻¹
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
⊢ (ofJ j).j = j

pp: case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
⊢ (ofJ j).j = j

Tactic:
· have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)
      have := Fact.mk h2.isUnit
      simp_rw [h1728, ofJ_1728_of_two_ne_zero h2, ofJ1728_j]

Goal state after:
case neg
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : ¬j = 1728
⊢ (ofJ j).j = j
Module: Mathlib.AlgebraicGeometry.Geometrically.Connected

Goal state before:
pp: X S : Scheme
f : X ⟶ S
⊢ GeometricallyConnected f ↔ ∀ (s : ↥S), GeometricallyConnected (Scheme.Hom.fiberToSpecResidueField f s)

Tactic:
by
  simp only [eq_geometrically, ← geometrically_iff_forall_fiberToSpecResidueField]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) = (ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
W : C
f : W ⟶ Z
x✝ : (E.sieve₁ g₁ g₂).arrows f
T : E.I₁ i₁ i₂
u : W ⟶ E.Y T
h₁ : f ≫ g₁ = u ≫ E.p₁ T
h₂ : f ≫ g₂ = u ≫ E.p₂ T
⊢ (ConcreteCategory.hom (F.map f.op)) ((ConcreteCategory.hom (F.map g₁.op)) (x i₁)) =
    (ConcreteCategory.hom (F.map f.op)) ((ConcreteCategory.hom (F.map g₂.op)) (x i₂))

Tactic:
rw [← comp_apply, ← Functor.map_comp, ← op_comp, h₁]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h : E.IsStronglySeparatedFor F
x : (i : E.I₀) → F.obj (op (E.X i))
hc :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
    (ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) = (ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)
i₁ i₂ : E.I₀
Z : C
g₁ : Z ⟶ E.X i₁
g₂ : Z ⟶ E.X i₂
heq : g₁ ≫ E.f i₁ = g₂ ≫ E.f i₂
W : C
f : W ⟶ Z
x✝ : (E.sieve₁ g₁ g₂).arrows f
T : E.I₁ i₁ i₂
u : W ⟶ E.Y T
h₁ : f ≫ g₁ = u ≫ E.p₁ T
h₂ : f ≫ g₂ = u ≫ E.p₂ T
⊢ (ConcreteCategory.hom (F.map (u ≫ E.p₁ T).op)) (x i₁) =
    (ConcreteCategory.hom (F.map f.op)) ((ConcreteCategory.hom (F.map g₂.op)) (x i₂))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialY / P z ^ 2 = Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY

Tactic:
linear_combination (norm := (rw [eval_polynomialY, Affine.evalEval_polynomialY]; ring1))
    2 * P y / P z * div_self hPz + W.a₁ * P x / P z * div_self hPz
      + W.a₃ * div_self (pow_ne_zero 2 hPz)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
i j : α
a : Equalizer.Presieve.Arrows.FirstObj F X
hi : ¬i = j
⊢ (ConcreteCategory.hom (F.map (pullback.fst (c.inj i) (c.inj j)).op))
      ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) i)) a) =
    (ConcreteCategory.hom (F.map (pullback.snd (c.inj i) (c.inj j)).op))
      ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) j)) a)

Tactic:
· have := preservesTerminal_of_isSheaf_for_empty F hF hI
    apply_fun (F.mapIso ((hd hi).isoPullback).op ≪≫ F.mapIso (terminalIsoIsTerminal
      (terminalOpOfInitial initialIsInitial)).symm ≪≫ (PreservesTerminal.iso F)).hom using
      injective_of_mono _
    ext ⟨i⟩
    exact i.elim

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : ¬Q z = 0
⊢ toAffine W (W.add P Q) = toAffine W Q

Tactic:
· rw [add_of_Z_eq_zero_left hP.left hPz hQz,
        toAffine_smul _ <| ((isUnit_Y_of_Z_eq_zero hP hPz).pow 2).mul <| Ne.isUnit hQz]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (W'⁄B).Nonsingular (⇑f ∘ P) ↔ (W'⁄A).Nonsingular P

Tactic:
rw [← RingHom.coe_coe, ← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : W.Point
⊢ (-P).toAffineLift = -P.toAffineLift

Tactic:
by
  rcases P with @⟨⟨_⟩, hP⟩
  exact toAffine_neg hP

Goal state after:
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: case localizationAwayPreserves
⊢ LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

pp: case ofLocalizationSpanTarget
⊢ OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

pp: case ofLocalizationSpan
⊢ OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

pp: case StableUnderCompositionWithLocalizationAwayTarget
⊢ StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
· exact isStableUnderBaseChange.localizationPreserves.away

Goal state after:
case ofLocalizationSpanTarget
⊢ OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

case ofLocalizationSpan
⊢ OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

case StableUnderCompositionWithLocalizationAwayTarget
⊢ StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
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.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) = -(eval P) W.polynomialX / P z / (P y - W.negY P)

Tactic:
by
  simp only [X_eq_iff hPz hQz, ne_eq, Y_eq_iff' hPz hQz] at hx hy
  rw [Affine.slope_of_Y_ne hx <| negY_of_Z_ne_zero hQz ▸ hy, ← negY_of_Z_ne_zero hPz]
  simp [field, eval_polynomialX]

Goal state after:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case refine_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
⊢ ∀ (x y : L),
    (↑{ toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯ }).toFun (x + y) =
      (↑{ toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯ }).toFun x +
        (↑{ toFun := fun x ↦ (g x) (IntermediateField.AdjoinSimple.gen K x), map_one' := ⋯, map_mul' := ⋯ }).toFun y

Tactic:
intro x y
    obtain ⟨α, hx, hy⟩ := H x y
    simp only [← hg₃ _ _ hx, ← hg₃ _ _ hy, ← map_add, ← hg₃ _ _ (add_mem hx hy)]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq 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
⊢ ((eval P) W.polynomialX ^ 2 - W.a₁ * (eval P) W.polynomialX * P z * (P y - W.negY P) -
              W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
            2 * P x * P z * (P y - W.negY P) ^ 2) *
          (P y - W.negY P) /
        P z /
      (P z * (P y - W.negY P) ^ 3) =
    W.toAffine.addX (P x / P z) (Q x / Q z) (-(eval P) W.polynomialX / P z / (P y - W.negY P))

Tactic:
← (X_eq_iff hPz hQz).mp hx,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq 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
⊢ ((eval P) W.polynomialX ^ 2 - W.a₁ * (eval P) W.polynomialX * P z * (P y - W.negY P) -
              W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
            2 * P x * P z * (P y - W.negY P) ^ 2) *
          (P y - W.negY P) /
        P z /
      (P z * (P y - W.negY P) ^ 3) =
    W.toAffine.addX (P x / P z) (P x / P z) (-(eval P) W.polynomialX / P z / (P y - W.negY P))
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x y : AdicCompletion I R
⊢ ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) (x + y)) ∘ₗ of I M =
    ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) x) ∘ₗ of I M +
      ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) y) ∘ₗ of I M

Tactic:
apply LinearMap.ext
        simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
y : K
x : M
⊢ s 0 = 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
y : K
x x✝ y✝ : M
hx✝ : x✝ ∈ Submodule.span R (Set.range (v ∘ a))
hy✝ : y✝ ∈ Submodule.span R (Set.range (v ∘ a))
a✝¹ : s x✝ = 0
a✝ : s y✝ = 0
⊢ s (x✝ + y✝) = 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
y : K
x x✝ y✝ : M
hx✝ : x✝ ∈ Submodule.span R (Set.range (v ∘ a))
hy✝ : y✝ ∈ Submodule.span R (Set.range (v ∘ a))
a✝¹ : s x✝ = 0
a✝ : s y✝ = 0
⊢ s (x✝ + y✝) = 0

Tactic:
| add =>

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: case smul
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
y : K
x : M
a✝¹ : R
x✝ : M
hx✝ : x✝ ∈ Submodule.span R (Set.range (v ∘ a))
a✝ : s x✝ = 0
⊢ s (a✝¹ • x✝) = 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
i j : σ
⊢ P.basisDeriv i j = (aeval P.val) ((pderiv (P.map j)) (P.relation i))

Tactic:
classical
  simp [basisDeriv]

Goal state after:
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : PreSubmersivePresentation R S ι σ
x : ↥P.ker
⊢ (∀ (x_1 : σ), (aeval P.val) ((pderiv (P.map x_1)) ↑x) = 0 x_1) ↔ ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0

Tactic:
Pi.zero_apply

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq 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
⊢ (-(eval P) W.polynomialX *
            ((eval P) W.polynomialX ^ 2 - W.a₁ * (eval P) W.polynomialX * P z * (P y - W.negY P) -
                  W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
                2 * P x * P z * (P y - W.negY P) ^ 2 -
              P x * P z * (P y - W.negY P) ^ 2) +
          P y * P z ^ 2 * (P y - W.negY P) ^ 3) /
        P z ^ 2 /
      (P z * (P y - W.negY P) ^ 3) =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z) (-(eval P) W.polynomialX / P z / (P y - W.negY P))

Tactic:
← (X_eq_iff hPz hQz).mp hx,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq 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
⊢ (-(eval P) W.polynomialX *
            ((eval P) W.polynomialX ^ 2 - W.a₁ * (eval P) W.polynomialX * P z * (P y - W.negY P) -
                  W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
                2 * P x * P z * (P y - W.negY P) ^ 2 -
              P x * P z * (P y - W.negY P) ^ 2) +
          P y * P z ^ 2 * (P y - W.negY P) ^ 3) /
        P z ^ 2 /
      (P z * (P y - W.negY P) ^ 3) =
    W.toAffine.negAddY (P x / P z) (P x / P z) (P y / P z) (-(eval P) W.polynomialX / P z / (P y - W.negY P))
Module: Mathlib.RingTheory.Extension.Cotangent.Free

Goal state before:
pp: case hker
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_3
σ : Type u_4
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
hm : Submodule.span S (Set.range fun i ↦ (D R S) (P.val (v i))) = ⊤
hk : Disjoint P.toExtension.toKaehler.ker (Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
inst✝ : Subsingleton (H1Cotangent R S)
f : P.toExtension.Cotangent →ₗ[S] ι →₀ S := ⋯
g : (ι →₀ S) →ₗ[S] Ω[S⁄R] := ⋯
hfg : Function.Exact ⇑f ⇑g
⊢ Disjoint g.ker (Submodule.span S (Set.range fun x ↦ Finsupp.single (v x) 1))

Tactic:
simp only [disjoint_iff, g]
    apply Submodule.map_injective_of_injective (f := P.cotangentSpaceBasis.repr.symm.toLinearMap)
      P.cotangentSpaceBasis.repr.symm.injective
    rw [Submodule.map_inf P.cotangentSpaceBasis.repr.symm.toLinearMap
        P.cotangentSpaceBasis.repr.symm.injective, Submodule.map_span, ← Set.range_comp,
        Function.comp_def, LinearMap.ker_comp, Submodule.map_comap_eq_of_surjective]
    · simpa [← disjoint_iff]
    · exact P.cotangentSpaceBasis.repr.symm.surjective

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_3
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S fun k ↦ (D R S) (P.val (v k))
⊢ ∀ x ∈ P.toExtension.toKaehler.ker ⊓ Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)), x = 0

Tactic:
intro x ⟨hx, hxs⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_3
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S fun k ↦ (D R S) (P.val (v k))
x : P.toExtension.CotangentSpace
hx : x ∈ ↑P.toExtension.toKaehler.ker
hxs : x ∈ ↑(Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
⊢ x = 0
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ IsStandardSmoothOfRelativeDimension n (algebraMap R S) ↔ Algebra.IsStandardSmoothOfRelativeDimension n R S

Tactic:
rw [RingHom.IsStandardSmoothOfRelativeDimension, toAlgebra_algebraMap]

Goal state after: