mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (↑x + ↑y * I)) 1 - (f' (↑x + ↑y * I)) I

Tactic:
set e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (↑x + ↑y * I)) 1 - (f' (↑x + ↑y * I)) I
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p : F[X]
σ τ : p.Gal
h : ∀ x ∈ p.rootSet p.SplittingField, σ x = τ x
x : p.SplittingField
⊢ ⊤ ≤ (↑σ).equalizer ↑τ

Tactic:
← SplittingField.adjoin_rootSet,

Goal state after:
F : Type u_1
inst✝ : Field F
p : F[X]
σ τ : p.Gal
h : ∀ x ∈ p.rootSet p.SplittingField, σ x = τ x
x : p.SplittingField
⊢ Algebra.adjoin F (p.rootSet p.SplittingField) ≤ (↑σ).equalizer ↑τ
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
⊢ p.natDegree ∣ finrank F p.SplittingField

Tactic:
let α : p.SplittingField :=
    rootOfSplits (SplittingField.splits p) (by rwa [degree_map])

Goal state after:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
⊢ p.natDegree ∣ finrank F p.SplittingField
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
F' : ℝ → ℝ →L[ℝ] E := fun x ↦ smulRight 1 (f' x)
⊢ ∫ (x : ℝ) in Set.Icc a b, f' x =
    ∑ i,
      ((∫ (x : Fin 0 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), f (e.symm (i.insertNth (e b i) x))) -
        ∫ (x : Fin 0 → ℝ) in Set.Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove), f (e.symm (i.insertNth (e a i) x)))

Tactic:
simp only [← interior_Icc] at Hd
      refine
        integral_divergence_of_hasFDerivAt_off_countable_of_equiv e ?_ ?_ (fun _ => f)
          (fun _ => F') s hs a b hle (fun _ => Hc) (fun x hx _ => Hd x hx) _ ?_ ?_
      · exact fun x y => (OrderIso.funUnique (Fin 1) ℝ).symm.le_iff_le
      · exact (volume_preserving_funUnique (Fin 1) ℝ).symm _
      · simp [F', e]
      · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hle] at Hi
        exact Hi.congr_set_ae Ioc_ae_eq_Icc.symm

Goal state after:
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ ↑B
⊢ ‖s.prod‖ ≤ ↑B ^ ((map f p).natDegree - i)

Tactic:
← coe_nnnorm,

Goal state after:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : p.Monic
h2 : (map f p).Splits
hi : i ≤ (map f p).natDegree
s : Multiset K
hs : s ≤ (map f p).roots ∧ s.card = (map f p).natDegree - i
B : ℝ≥0
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ ↑B
⊢ ↑‖s.prod‖₊ ≤ ↑B ^ ((map f p).natDegree - i)
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
he : StrictMono ⇑e
⊢ Units.mk0 (NNReal.mk (2 ^ (↑1).log) ⋯) ⋯ = 1

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := ⋯
he : StrictMono ⇑e
x✝¹ x✝ : Multiplicative ℝ
⊢ ↑↑(Units.mk0 (NNReal.mk (2 ^ (↑(x✝¹ * x✝)).log) ⋯) ⋯) =
    ↑↑(Units.mk0 (NNReal.mk (2 ^ (↑x✝¹).log) ⋯) ⋯ * Units.mk0 (NNReal.mk (2 ^ (↑x✝).log) ⋯) ⋯)

Tactic:
simp [Real.rpow_add]

Goal state after:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case inr
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : Archimedean M
h✝ : Nontrivial M
a : M
ha : a ≠ 0
one : One M := { one := |a| }
⊢ ∃ f, Function.Injective ⇑f

Tactic:
have : ZeroLEOneClass M := ⟨abs_nonneg a⟩

Goal state after:
case inr
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : Archimedean M
h✝ : Nontrivial M
a : M
ha : a ≠ 0
one : One M := { one := |a| }
this : ZeroLEOneClass M
⊢ ∃ f, Function.Injective ⇑f
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case pos
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : x = 0
⊢ x ∈ U

Tactic:
exact h (hx0 ▸ Metric.mem_ball_self hε)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ -((if (0, n).2 < (0, n).2 then (coeff (0, n).1) φ * (coeff (0, n).2) (φ.invOfUnit u) else 0) +
          ∑ x ∈ (antidiagonal n).erase (0, n),
            if x.2 < (0, n).2 then (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) else 0) +
      ∑ x ∈ (insert (0, n) ((antidiagonal n).erase (0, n))).erase (0, n), (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) =
    0

Tactic:
Finset.insert_erase this,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : constantCoeff φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ -((if (0, n).2 < (0, n).2 then (coeff (0, n).1) φ * (coeff (0, n).2) (φ.invOfUnit u) else 0) +
          ∑ x ∈ (antidiagonal n).erase (0, n),
            if x.2 < (0, n).2 then (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) else 0) +
      ∑ x ∈ (antidiagonal n).erase (0, n), (coeff x.1) φ * (coeff x.2) (φ.invOfUnit u) =
    0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : f = f.divXPowOrder
⊢ IsUnit f

Tactic:
by rw [h]; exact isUnit_divided_by_X_pow_order hf

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ Type u_2
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  (ConcreteCategory.hom (F.map (pullback.fst (E.f i) (E.f j)).op)) (s.val i) =
    (ConcreteCategory.hom (F.map (pullback.snd (E.f i) (E.f j)).op)) (s.val j)
⊢ (ConcreteCategory.hom (F.map (pullback.lift gi gj hgij ≫ pullback.fst (E.f i) (E.f j)).op)) (s.val i) =
    (ConcreteCategory.hom (F.map (pullback.lift gi gj hgij ≫ pullback.snd (E.f i) (E.f j)).op)) (s.val j)

Tactic:
op_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ Type u_2
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  (ConcreteCategory.hom (F.map (pullback.fst (E.f i) (E.f j)).op)) (s.val i) =
    (ConcreteCategory.hom (F.map (pullback.snd (E.f i) (E.f j)).op)) (s.val j)
⊢ (ConcreteCategory.hom (F.map ((pullback.fst (E.f i) (E.f j)).op ≫ (pullback.lift gi gj hgij).op))) (s.val i) =
    (ConcreteCategory.hom (F.map (pullback.lift gi gj hgij ≫ pullback.snd (E.f i) (E.f j)).op)) (s.val j)
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ Type u_2
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  (ConcreteCategory.hom (F.map (pullback.fst (E.f i) (E.f j)).op)) (s.val i) =
    (ConcreteCategory.hom (F.map (pullback.snd (E.f i) (E.f j)).op)) (s.val j)
⊢ (ConcreteCategory.hom (F.map (pullback.fst (E.f i) (E.f j)).op ≫ F.map (pullback.lift gi gj hgij).op)) (s.val i) =
    (ConcreteCategory.hom (F.map (pullback.lift gi gj hgij ≫ pullback.snd (E.f i) (E.f j)).op)) (s.val j)

Tactic:
op_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ Type u_2
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  (ConcreteCategory.hom (F.map (pullback.fst (E.f i) (E.f j)).op)) (s.val i) =
    (ConcreteCategory.hom (F.map (pullback.snd (E.f i) (E.f j)).op)) (s.val j)
⊢ (ConcreteCategory.hom (F.map (pullback.fst (E.f i) (E.f j)).op ≫ F.map (pullback.lift gi gj hgij).op)) (s.val i) =
    (ConcreteCategory.hom (F.map ((pullback.snd (E.f i) (E.f j)).op ≫ (pullback.lift gi gj hgij).op))) (s.val j)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
          (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
        0 ∧
      (W'.a₁ * b * 1 - (3 * a ^ 2 + 2 * W'.a₂ * a * 1 + W'.a₄ * 1 ^ 2) ≠ 0 ∨
        2 * b * 1 + W'.a₁ * a * 1 + W'.a₃ * 1 ^ 2 ≠ 0 ∨
          b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b * 1 - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a * 1 + 3 * W'.a₆ * 1 ^ 2) ≠ 0) ↔
    b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
          (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
        0 ∧
      (W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) ≠ 0 ∨
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ ≠ 0)

Tactic:
and_congr_right_iff,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    (W'.a₁ * b * 1 - (3 * a ^ 2 + 2 * W'.a₂ * a * 1 + W'.a₄ * 1 ^ 2) ≠ 0 ∨
        2 * b * 1 + W'.a₁ * a * 1 + W'.a₃ * 1 ^ 2 ≠ 0 ∨
          b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b * 1 - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a * 1 + 3 * W'.a₆ * 1 ^ 2) ≠ 0 ↔
      W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) ≠ 0 ∨
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ ≠ 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    (W'.a₁ * b * 1 - (3 * a ^ 2 + 2 * W'.a₂ * a * 1 + W'.a₄ * 1 ^ 2) ≠ 0 ∨
        2 * b * 1 + W'.a₁ * a * 1 + W'.a₃ * 1 ^ 2 ≠ 0 ∨
          b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b * 1 - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a * 1 + 3 * W'.a₆ * 1 ^ 2) ≠ 0 ↔
      W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) ≠ 0 ∨
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ ≠ 0)

Tactic:
← not_and_or,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    (¬(W'.a₁ * b * 1 - (3 * a ^ 2 + 2 * W'.a₂ * a * 1 + W'.a₄ * 1 ^ 2) = 0 ∧
          2 * b * 1 + W'.a₁ * a * 1 + W'.a₃ * 1 ^ 2 = 0 ∧
            b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b * 1 - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a * 1 + 3 * W'.a₆ * 1 ^ 2) = 0) ↔
      ¬(W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) = 0 ∧
          2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    (W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0 ∧
        2 * b + W'.a₁ * a + W'.a₃ = 0 ∧
          b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a + 3 * W'.a₆) = 0 ↔
      W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) = 0 ∧
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0)

Tactic:
and_congr_right_iff,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0 →
      (2 * b + W'.a₁ * a + W'.a₃ = 0 ∧
          b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a + 3 * W'.a₆) = 0 ↔
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0)
Module: Mathlib.RingTheory.RingHom.Smooth

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Smooth
hg : g.Smooth
⊢ (g.comp f).Smooth

Tactic:
algebraize [f, g, g.comp f]
  exact Algebra.Smooth.comp R S T

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
⊢ IsOpen (smoothLocus R A)

Tactic:
by
  rw [isOpen_iff_forall_mem_open]
  intro x hx
  obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hxf, hf⟩ :=
    isBasis_basic_opens.exists_subset_of_mem_open
    (smoothLocus_eq_compl_support_inter.le hx).2 Module.isOpen_freeLocus
  rw [Module.basicOpen_subset_freeLocus_iff] at hf
  let Af := Localization.Away f
  have : Algebra.FinitePresentation A (Localization.Away f) :=
    IsLocalization.Away.finitePresentation f
  have : Algebra.FinitePresentation R (Localization.Away f) :=
    .trans _ A _
  have : IsOpen (smoothLocus R Af) := by
    have := IsLocalizedModule.iso (.powers f)
      (KaehlerDifferential.map R R A (Localization.Away f))
    have := this.extendScalarsOfIsLocalization (.powers f) (Localization.Away f)
    have := Module.Projective.of_equiv this
    rw [smoothLocus_eq_compl_support_inter, Module.support_eq_zeroLocus]
    exact (isClosed_zeroLocus _).isOpen_compl.inter Module.isOpen_freeLocus
  rw [← smoothLocus_comap_of_isLocalization f] at this
  replace this := (PrimeSpectrum.localization_away_isOpenEmbedding Af f).isOpenMap _ this
  rw [Set.image_preimage_eq_inter_range, localization_away_comap_range Af f] at this
  exact ⟨_, Set.inter_subset_left, this, hx, hxf⟩

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

Goal state before:
pp: R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
⊢ FormallySmooth R (A i)

Tactic:
classical
  fapply FormallySmooth.of_split (Pi.evalAlgHom R A i)
  · apply AlgHom.ofLinearMap
      ((Ideal.Quotient.mkₐ R _).toLinearMap.comp (LinearMap.single _ _ i))
    · change Ideal.Quotient.mk _ (Pi.single i 1) = 1
      rw [← (Ideal.Quotient.mk _).map_one, ← sub_eq_zero, ← map_sub,
        Ideal.Quotient.eq_zero_iff_mem]
      have : Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom := by
        simp [RingHom.mem_ker]
      convert! neg_mem (Ideal.pow_mem_pow this 2) using 1
      simp [pow_two, sub_mul, mul_sub, ← Pi.single_mul]
    · intro x y
      change Ideal.Quotient.mk _ _ = Ideal.Quotient.mk _ _ * Ideal.Quotient.mk _ _
      simp +instances only [AlgHom.toRingHom_eq_coe, LinearMap.coe_single, Pi.single_mul, map_mul]
  · ext x
    change (Pi.single i x) i = x
    simp

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

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
⊢ f x →ₐ[R] B ⧸ J'

Tactic:
by
      apply AlgHom.ofLinearMap
        (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap.comp (LinearMap.single _ _ x))
      · simp only [AlgHom.comp_toLinearMap, LinearMap.coe_comp, LinearMap.coe_single,
          Function.comp_apply, AlgHom.toLinearMap_apply, Ideal.Quotient.mkₐ_eq_mk]
        rw [eq_comm, ← sub_eq_zero, ← (Ideal.Quotient.mk J').map_one, ← map_sub,
          Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton, H]
      · intro r s; simp [Pi.single_mul]

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

Goal state before:
pp: case e_6
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝² : CommRing B
x✝¹ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} := ⋯
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := ⋯
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i := ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
a : (i : I) → A i →ₐ[R] B ⧸ Ideal.span {1 - e i}
ha : ∀ (i : I) (x : A i), (Ideal.Quotient.mk (J' i)) ((a i) x) = (ι i) (g (Pi.single i x))
x✝ : (i : I) → A i
i : I
x : A i
y : B
hy : (Ideal.Quotient.mk (Ideal.span {1 - e i})) y = (a i) x
hy' : (Ideal.Quotient.mk (Ideal.span {1 - e i})) (y * e i) = (a i) x
⊢ iso (↑↑iso.symm ((AlgHom.pi fun i ↦ (a i).comp (Pi.evalAlgHom R A i)) (Pi.single i x))) = iso (y * e i)

Tactic:
ext j

Goal state after:
case e_6
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝² : CommRing B
x✝¹ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
a : (i : I) → A i →ₐ[R] B ⧸ Ideal.span {1 - e i}
ha : ∀ (i : I) (x : A i), (Ideal.Quotient.mk (J' i)) ((a i) x) = (ι i) (g (Pi.single i x))
x✝ : (i : I) → A i
i : I
x : A i
y : B
hy : (Ideal.Quotient.mk (Ideal.span {1 - e i})) y = (a i) x
hy' : (Ideal.Quotient.mk (Ideal.span {1 - e i})) (y * e i) = (a i) x
j : I
⊢ iso (↑↑iso.symm ((AlgHom.pi fun i ↦ (a i).comp (Pi.evalAlgHom R A i)) (Pi.single i x))) j = iso (y * e i) j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

Tactic:
by
  linear_combination (norm := (rw [negY, negY]; ring1)) -W'.a₁ * hx

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

Goal state before:
pp: case mpr
K : Type u_1
A : Type u
inst✝² : Field K
inst✝¹ : CommRing A
inst✝ : Algebra K A
⊢ (∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)) → Etale K A

Tactic:
intro ⟨I, _, Ai, _, _, e, H⟩
    choose h₁ h₂ using H
    have := Module.Finite.of_surjective e.symm.toLinearMap e.symm.surjective
    refine ⟨?_, FinitePresentation.of_finiteType.mp inferInstance⟩
    exact (FormallyEtale.iff_exists_algEquiv_prod K A).mpr ⟨_, inferInstance, _, _, _, e, h₂⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
hf₁ : Function.Surjective ⇑fP
this : (RingHom.ker f₀.toRingHom).FG
x : MvPolynomial (Fin n) R
s : ↥M'
hx : IsLocalization.mk' P' x s ∈ RingHom.ker fP
⊢ ∃ a ∈ M, a * f₀ x = 0

Tactic:
by
      simpa [fP, IsLocalization.lift_mk', IsLocalization.map_eq_zero_iff M] using hx

Goal state after: