mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
r : F[X]
hr : Irreducible r
⊢ P r

Tactic:
by_cases hr' : natDegree r = 0

Goal state after:
case pos
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
r : F[X]
hr : Irreducible r
hr' : r.natDegree = 0
⊢ P r

case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
r : F[X]
hr : Irreducible r
hr' : ¬r.natDegree = 0
⊢ P r
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (map ?m.101 x).prod

pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ ∀ x_1 ∈ x, Function.const R (-1) x_1 * x_1 = ?m.101 x_1

pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ R → R

Tactic:
Function.comp_apply

Goal state after:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (map Neg.neg x).prod = (map ?m.101 x).prod

R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ ∀ x_1 ∈ x, Function.const R (-1) x_1 * x_1 = ?m.101 x_1

R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ R → R
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) ∘ fun i ↦ X i) univ.val

Tactic:
Function.comp_apply

Goal state after:
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) ∘ fun i ↦ X i) univ.val

Tactic:
Function.comp_apply

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case pos
p : ℚ[X]
hp : p = 0
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card

Tactic:
have : IsEmpty (p.rootSet ℂ) := by rw [hp, rootSet_zero]; infer_instance

Goal state after:
case pos
p : ℚ[X]
hp : p = 0
this : IsEmpty ↑(p.rootSet ℂ)
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: case mp
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
⊢ IsRankLeOne R → MulArchimedean (ValueGroupWithZero R)

Tactic:
rintro ⟨⟨f, hf⟩⟩

Goal state after:
case mp
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
f : ValueGroupWithZero R →*₀ ℝ≥0
hf : StrictMono ⇑f
⊢ MulArchimedean (ValueGroupWithZero R)
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case a
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
⊢ 1 ≤ embedRealFun 1

Tactic:
· rw [le_csSup_iff (ratLt'_bddAbove (1 : M)) (ratLt'_nonempty 1)]
    simp_rw [mem_upperBounds]
    suffices ∀ (x : ℝ), (∀ (y : ℚ), y.num • (1 : M) < (y.den : ℤ) • 1 → y ≤ x) → 1 ≤ x by
      simpa using this
    intro x h
    have h' (y : ℚ) (hy : y < 1) : y ≤ x :=
      h _ ((smul_lt_smul_iff_of_pos_right zero_lt_one).mpr (by simpa using (Rat.lt_iff _ _).mp hy))
    contrapose! h'
    obtain ⟨y, hxy, hy⟩ := exists_rat_btwn h'
    exact ⟨y, (by norm_cast at hy), hxy⟩

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑(toLex d) = φ.lexOrder
hφ : φ ≠ 0
ne : (⇑toLex '' Function.support φ).Nonempty
hφ' : toLex d = ⋯.min (⇑toLex '' Function.support φ) ne
⊢ (coeff d) φ ≠ 0

Tactic:
suffices toLex d ∈ toLex '' φ.support by
    simp only [Set.mem_image_equiv, toLex_symm_eq, ofLex_toLex] at this
    apply this

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑(toLex d) = φ.lexOrder
hφ : φ ≠ 0
ne : (⇑toLex '' Function.support φ).Nonempty
hφ' : toLex d = ⋯.min (⇑toLex '' Function.support φ) ne
⊢ toLex d ∈ ⇑toLex '' Function.support φ
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

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

Tactic:
rw [map_zero, ← mul_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsLeft R
x : MvPowerSeries σ R
hx : φ * x = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
⊢ constantCoeff φ * (coeff e) x = (coeff e) (φ * x)
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : φ⁻¹ = 0
⊢ constantCoeff φ = 0

Tactic:
by simpa using congr_arg constantCoeff h

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

Goal state before:
pp: k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), c ≤ Multiset.count X (normalizedFactors ↑P) ↔ c ≤ Multiset.count Polynomial.X (normalizedFactors P)

Tactic:
simp only [← Nat.cast_le (α := ℕ∞)]

Goal state after:
k : Type u_2
inst✝ : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ), ↑c ≤ ↑(Multiset.count X (normalizedFactors ↑P)) ↔ ↑c ≤ ↑(Multiset.count Polynomial.X (normalizedFactors P))
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : FinitePlace K
x : K
⊢ ‖(embedding w.maximalIdeal) x‖ = w x

Tactic:
by
  conv_rhs => rw [← mk_maximalIdeal w, mk_apply]

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.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
Y : C
f : Y ⟶ Z
x✝ : (E.sieve₁ gi gj).arrows f
k : E.I₁ i j
h : Y ⟶ E.Y k
hf₁ : f ≫ gi = h ≫ E.p₁ k
hf₂ : f ≫ gj = h ≫ E.p₂ k
⊢ (ConcreteCategory.hom (F.map (h ≫ E.p₁ k).op)) (s i) = (ConcreteCategory.hom (F.map (h ≫ E.p₂ k).op)) (s j)

Tactic:
simp only [op_comp, Functor.map_comp, comp_apply]

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.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
S : Sieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible
s : (i : E.I₀) → F.obj (op (E.X i))
hs : ∀ (i : E.I₀), (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun t_1 ↦ (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation t_1) y → y = s i
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
Y : C
f : Y ⟶ Z
x✝ : (E.sieve₁ gi gj).arrows f
k : E.I₁ i j
h : Y ⟶ E.Y k
hf₁ : f ≫ gi = h ≫ E.p₁ k
hf₂ : f ≫ gj = h ≫ E.p₂ k
⊢ (ConcreteCategory.hom (F.map h.op)) ((ConcreteCategory.hom (F.map (E.p₁ k).op)) (s i)) =
    (ConcreteCategory.hom (F.map h.op)) ((ConcreteCategory.hom (F.map (E.p₂ k).op)) (s j))
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hf : Presieve.IsSheaf J F
⊢ Presieve.IsSheafFor F E.presieve₀

Tactic:
rw [Presieve.isSheafFor_iff_generate]
    exact hf _ E.mem₀

Goal state after:
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:
by
  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.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.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
hx : ¬P x * Q z = Q x * P z
⊢ ⟦W.add P Q⟧ =
    ⟦![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)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]⟧

Tactic:
add_of_X_ne hP hQ hPz hQz hx,

Goal state after:
case neg
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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
hx : ¬P x * Q z = Q x * P z
⊢ ⟦W.addZ P Q •
        ![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)),
          W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
            (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
          1]⟧ =
    ⟦![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)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]⟧
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_1.refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
i j : 𝒰.I₀
y : ↑Y
xi : ↑(𝒰.X i)
hi : (ConcreteCategory.hom (𝒰.f i)) xi = y
⊢ ∀ (x_1 : ↑(𝒰.X j)) (h : (ConcreteCategory.hom (𝒰.f j)) x_1 = y),
    (Hom.hom (x i)) (⋯.toHomeomorph.symm ⟨y, ⋯⟩) = (Hom.hom (x j)) (⋯.toHomeomorph.symm ⟨y, ⋯⟩)

Tactic:
xj

Goal state after:
case refine_1.refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
i j : 𝒰.I₀
y : ↑Y
xi : ↑(𝒰.X i)
hi : (ConcreteCategory.hom (𝒰.f i)) xi = y
xj : ↑(𝒰.X j)
⊢ ∀ (h : (ConcreteCategory.hom (𝒰.f j)) xj = y),
    (Hom.hom (x i)) (⋯.toHomeomorph.symm ⟨y, ⋯⟩) = (Hom.hom (x j)) (⋯.toHomeomorph.symm ⟨y, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
⊢ P z * Q z * (P y * Q z - Q y * P z) * (P y * Q z - W'.negY Q * P z) = 0

Tactic:
by
  linear_combination (norm := (rw [negY]; ring1)) Q z ^ 3 * (equation_iff P).mp hP
    - P z ^ 3 * (equation_iff Q).mp hQ + (P x ^ 2 * Q z ^ 2 + P x * Q x * P z * Q z
      + Q x ^ 2 * P z ^ 2 - W'.a₁ * P y * P z * Q z ^ 2 + W'.a₂ * P x * Q z ^ 2 * P z
      + W'.a₂ * Q x * P z ^ 2 * Q z + W'.a₄ * P z ^ 2 * Q z ^ 2) * hx

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
p : Ideal A
P : Ideal B
inst✝⁴ : P.LiesOver p
inst✝³ : p.IsPrime
inst✝² : P.IsPrime
inst✝¹ : IsEtaleAt R p
inst✝ : IsEtaleAt A P
⊢ IsEtaleAt R P

Tactic:
let := Localization.AtPrime.algebraOfLiesOver p P

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
p : Ideal A
P : Ideal B
inst✝⁴ : P.LiesOver p
inst✝³ : p.IsPrime
inst✝² : P.IsPrime
inst✝¹ : IsEtaleAt R p
inst✝ : IsEtaleAt A P
this : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
⊢ IsEtaleAt R P
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
x y : AdicCompletion I R
H : ∀ (n : ℕ), (evalₐ I n) x = (evalₐ I n) y
⊢ x = y

Tactic:
by
  ext n
  have h : (I ^ n • ⊤ : Ideal R) = I ^ n := by ext x; simp
  exact (Ideal.quotientEquivAlgOfEq R h).injective (H n)

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
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ P.jacobian = (algebraMap P.Ring S) P.jacobiMatrix.det

Tactic:
by
  simp [jacobiMatrix, jacobian]

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
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : Fintype σ'
i j : σ
⊢ (Q.comp P).jacobiMatrix (Sum.inr i) (Sum.inr j) = (rename Sum.inr) (P.jacobiMatrix i j)

Tactic:
rw [jacobiMatrix_apply, jacobiMatrix_apply]
  simp only [comp_map, Sum.elim_inr]
  apply pderiv_rename Sum.inr_injective

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 σ
r : R
inst✝ : IsLocalization.Away r S
⊢ IsUnit (PreSubmersivePresentation.localizationAway S r).jacobian

Tactic:
localizationAway_jacobian

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Finite σ
r : R
inst✝ : IsLocalization.Away r S
⊢ IsUnit ((algebraMap R S) r)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: 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
⊢ W.addX P Q =
    ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
              W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
            P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
          Q x * P z * (P x * Q z - Q x * P z) ^ 2) *
        (P x * Q z - Q x * P z) /
      (P z * Q z) ^ 2

Tactic:
← addX_eq' hP hQ,

Goal state after:
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
⊢ W.addX P Q = W.addX P Q * (P z * Q z) ^ 2 / (P z * Q z) ^ 2
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case e_6
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
⊢ ((localizationAway S D.gbar).ofComp D.presLeft.toGenerators).toAlgHom (D.pres.relation (Sum.inl ())) =
    C D.gbar * X () - 1

Tactic:
have : Nontrivial D.T := inferInstance

Goal state after:
case e_6
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial D.T
⊢ ((localizationAway S D.gbar).ofComp D.presLeft.toGenerators).toAlgHom (D.pres.relation (Sum.inl ())) =
    C D.gbar * X () - 1
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
⊢ (Ideal.Quotient.mkₐ (↥(subalgebra R D))
            (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))).kerSquareLift.comp
      (Ideal.Quotient.liftₐ (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
        ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
              (RingHom.ker
                  (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                    (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
                2)).comp
          (aeval p))
        ⋯) =
    AlgHom.id (↥(subalgebra R D)) (Presentation.ModelOfHasCoeffs ↥(subalgebra R D))

Tactic:
rw [← AlgHom.cancel_right hf₀]

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
⊢ ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
                (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))).kerSquareLift.comp
          (Ideal.Quotient.liftₐ (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
            ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
                  (RingHom.ker
                      (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
                    2)).comp
              (aeval p))
            ⋯)).comp
      (Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) =
    (AlgHom.id (↥(subalgebra R D)) (Presentation.ModelOfHasCoeffs ↥(subalgebra R D))).comp
      (Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
⊢ (((Ideal.Quotient.mkₐ (↥(subalgebra R D))
                  (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))).kerSquareLift.comp
            (Ideal.Quotient.liftₐ (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
              ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
                    (RingHom.ker
                        (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                          (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
                      2)).comp
                (aeval p))
              ⋯)).comp
        (Ideal.Quotient.mkₐ (↥(subalgebra R D))
          (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))))
      (X i) =
    ((AlgHom.id (↥(subalgebra R D)) (Presentation.ModelOfHasCoeffs ↥(subalgebra R D))).comp
        (Ideal.Quotient.mkₐ (↥(subalgebra R D))
          (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))))
      (X i)

Tactic:
suffices h : ∃ p', p'.IsHomogeneous 1 ∧ (eval (D.P.relationOfHasCoeffs (D.subalgebra R))) p' =
        p i - X i by
      -- Reducible def-eq issues caused by `RingHom.ker f.toRingHom` discrepancies
      -- Can be fixed after #25138.
      apply (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mpr
      simpa [Ideal.mem_span_iff_exists_isHomogeneous, hp]

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
⊢ ∃ p', p'.IsHomogeneous 1 ∧ (eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) p' = p i - X i