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

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
s : Set ℂ
h0 : 0 < R
n : ℕ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
this : (n.factorial • (cauchyPowerSeries f c (↑(NNReal.mk R ⋯)) n) fun x ↦ 1) = iteratedDeriv n f c
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z =
    (2 * ↑π * I * (2 * ↑π * I)⁻¹) • ∮ (z : ℂ) in C(c, ↑(NNReal.mk R ⋯)), (1 / (z - c)) ^ n • (z - c)⁻¹ • f z

Tactic:
mul_inv_cancel₀ two_pi_I_ne_zero

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
s : Set ℂ
h0 : 0 < R
n : ℕ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
this : (n.factorial • (cauchyPowerSeries f c (↑(NNReal.mk R ⋯)) n) fun x ↦ 1) = iteratedDeriv n f c
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z =
    1 • ∮ (z : ℂ) in C(c, ↑(NNReal.mk R ⋯)), (1 / (z - c)) ^ n • (z - c)⁻¹ • f z
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ x ^ (a - b) = 1

Tactic:
rw [← Nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h

Goal state after:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
⊢ x ^ (a - b) = 1
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: case mpr
R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
⊢ MulArchimedean (ofClass v).ValueGroup₀ → Nonempty v.RankOne

Tactic:
intro _
    obtain ⟨f, hf⟩ :=
      Archimedean.exists_orderAddMonoidHom_real_injective (Additive (ValueGroup₀ (.ofClass v))ˣ)
    let e := AddMonoidHom.toMultiplicativeRight (α := (ValueGroup₀ (.ofClass v))ˣ) (β := ℝ) f
    have he : StrictMono e := by
      simp only [AddMonoidHom.coe_toMultiplicativeRight, AddMonoidHom.coe_coe, e]
      -- toAdd_strictMono is already in an applied form, do defeq abuse instead
      exact StrictMono.comp strictMono_id (f.monotone'.strictMono_of_injective hf)
    let rf : Multiplicative ℝ →* ℝ≥0ˣ := {
      toFun x := Units.mk0 (.mk ((2 : ℝ) ^ (log (M := ℝ) x)) (by positivity)) <| by
        simp only [ne_eq, NNReal.eq_iff, NNReal.coe_mk, NNReal.coe_zero]
        positivity
      map_one' := by ext; simp
      map_mul' _ _ := by ext; simp [Real.rpow_add]
      }
    have H : StrictMono (map' (rf.comp e)) := by
      refine map'_strictMono ?_
      intro a b h
      simpa [← Units.val_lt_val, ← NNReal.coe_lt_coe, rf] using he h
    exact ⟨{
      hom' := withZeroUnitsEquiv.toMonoidWithZeroHom.comp <| (map' (rf.comp e)).comp
        withZeroUnitsEquiv.symm.toMonoidWithZeroHom
      strictMono' := withZeroUnitsEquiv_strictMono.comp <| H.comp
        withZeroUnitsEquiv_symm_strictMono
    }⟩

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

Goal state before:
pp: 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
⊢ ratLt (x + y) = ratLt x + ratLt y

Tactic:
by
  ext a
  rw [Set.mem_add]
  constructor
  · /- Given `a ∈ ratLt 1 (x + y)`, find `u ∈ ratLt 1 x`, `v ∈ ratLt 1 y`
      such that `u + v = a`.
      In a naive attempt, one can take the denominator `d` of `a`,
      and find the largest `u = p / d < x / 1`.
      However, `d` could be too "coarse", and `v = a - u` could be 1/d too large than `y / 1`.
      To ensure a large enough denominator, we take `d * k`, where
      `1 + 1 ≤ k • (d • (x + y) - a.num • 1)`. -/
    intro h
    rw [Set.mem_ofPred_eq] at h
    obtain ⟨k, hk⟩ := Archimedean.arch (1 + 1) <| sub_pos.mpr h
    have hk0 : k ≠ 0 := by
      contrapose! hk
      simp [hk]
    have hka0 : k * a.den ≠ 0 := mul_ne_zero hk0 a.den_ne_zero
    obtain ⟨m, ⟨hm1, hm2⟩, _⟩ := existsUnique_add_zsmul_mem_Ico zero_lt_one 0 (k • a.den • x - 1)
    refine ⟨mkRat m (k * a.den), ?_, mkRat (k * a.num - m) (k * a.den), ?_, ?_⟩
    · rw [mkRat_mem_ratLt hka0, ← smul_smul]
      simpa using hm2
    · have hk' : 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1 := by
        rw [smul_add, smul_sub, smul_add, le_sub_iff_add_le, ← sub_le_iff_le_add] at hk
        rw [le_sub_iff_add_le]
        convert! hk using 1
        abel
      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)
      rw [mkRat_mem_ratLt hka0, sub_smul, sub_lt_comm, ← smul_smul, ← smul_smul, natCast_zsmul]
      exact this
    · rw [Rat.mkRat_add_mkRat_of_den _ _ hka0]
      rw [add_sub_cancel, Rat.mkRat_mul_left hk0, Rat.mkRat_num_den']
  · -- `u ∈ ratLt 1 x`, `v ∈ ratLt 1 y` → `u + v ∈ ratLt 1 (x + y)`
    intro ⟨u, hu, v, hv, huv⟩
    rw [← huv]
    rw [Set.mem_ofPred_eq] at hu hv ⊢
    exact num_smul_one_lt_den_smul_add hu hv

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

Goal state before:
pp: case refine_1
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ofClass v.restrict).ValueGroup₀ˣ
h : (hom v.restrict) ↑x < γ
k : K
hk :
  (if h : (if h : v k = 0 then 0 else ↑⟨Units.mk0 (v k) h, ⋯⟩) = 0 then 0
    else ↑⟨Units.mk0 (if h : v k = 0 then 0 else ↑⟨Units.mk0 (v k) ⋯, ⋯⟩) ⋯, ⋯⟩) =
    ↑x
h0 : k = 0
⊢ False

Tactic:
rw [dif_pos (by rw [dif_pos ((zero_iff v).mpr h0)]), eq_comm] at hk

Goal state after:
case refine_1
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankOne
γ : ℝ≥0
hγ : γ ≠ 0
hγ_pos : 0 < γ
x : (ofClass v.restrict).ValueGroup₀ˣ
h : (hom v.restrict) ↑x < γ
k : K
hk : ↑x = 0
h0 : k = 0
⊢ False
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r s : ℝ
⊢ closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨ Disjoint (closedBall x r) (closedBall y s)

Tactic:
wlog! hrs : r ≤ s generalizing x y r s
  · rw [disjoint_comm, ← or_assoc, or_comm (b := (_ : Set X) ⊆ _), or_assoc]
    exact this y x s r hrs.le
  · refine Set.disjoint_or_nonempty_inter (closedBall x r) (closedBall y s) |>.symm.imp
      (fun h ↦ ?_) (Or.inr ·)
    obtain ⟨hxz, hyz⟩ := (Set.mem_inter_iff _ _ _).mp h.some_mem
    have hx := closedBall_subset_closedBall hrs (x := x)
    rwa [closedBall_eq_of_mem hyz |>.trans (closedBall_eq_of_mem <| hx hxz).symm]

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
⊢ ∃ f, Function.Injective ⇑f

Tactic:
let one : One M := ⟨|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| }
⊢ ∃ f, Function.Injective ⇑f
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
⊢ ∃ f, Function.Injective ⇑f

Tactic:
· obtain ⟨a, ha⟩ := exists_ne (0 : M)
    let one : One M := ⟨|a|⟩
    have : ZeroLEOneClass M := ⟨abs_nonneg a⟩
    have : NeZero (1 : M) := ⟨abs_ne_zero.mpr ha⟩
    exact ⟨embedReal M, embedReal_injective M⟩

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
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
⊢ (coeff (p + q)) (φ * ψ) = (coeff p) φ * (coeff q) ψ

Tactic:
rw [coeff_mul, Finset.sum_eq_single_of_mem ⟨p, q⟩ (by simp)]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
⊢ ∀ b ∈ Finset.antidiagonal (p + q), b ≠ (p, q) → (coeff b.1) φ * (coeff b.2) ψ = 0
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
⊢ φ ∈ nonZeroDivisorsRight (MvPowerSeries σ R)

Tactic:
by
  classical
  intro x hx
  ext d
  apply WellFoundedLT.induction d
  intro e he
  rw [map_zero, ← mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e x φ).symm
  rw [Finset.sum_eq_single (e, 0), coeff_zero_eq_constantCoeff]
  · rintro ⟨u, _⟩ huv _
    suffices u < e by simp only [he u this, zero_mul, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]
    · rintro rfl
      simp_all
  · simp

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

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hv : ↑(toLex v) < ψ.lexOrder
⊢ (coeff u) φ * (coeff v) ψ = 0

Tactic:
rw [coeff_eq_zero_of_lt_lexOrder hv, mul_zero]

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 φ ∈ nonZeroDivisorsLeft R
⊢ φ ∈ nonZeroDivisorsLeft (MvPowerSeries σ R)

Tactic:
by
  classical
  intro x hx
  ext d
  apply WellFoundedLT.induction d
  intro e he
  rw [map_zero, ← mul_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e φ x).symm
  rw [Finset.sum_eq_single (0, e), coeff_zero_eq_constantCoeff]
  · rintro ⟨_, u⟩ huv _
    suffices u < e by simp only [he u this, mul_zero, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_left, zero_le]
    · rintro rfl
      simp_all
  · simp only [mem_antidiagonal, zero_add, not_true_eq_false, coeff_zero_eq_constantCoeff,
      false_implies]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
⊢ (∃ i, True ∧ {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U) ↔ ∃ i, U ∈ 𝓟 {p | v.norm (p.1 - p.2) < ↑i}

Tactic:
simp only [true_and, mem_principal, Subtype.exists, gt_iff_lt, exists_prop]
        refine ⟨fun ⟨ε, hε⟩ => ?_, fun ⟨r, hr_pos, hr⟩ => ?_⟩
        · set δ : ℝ≥0 := hv.hom _ ε with hδ
          have hδ_pos : 0 < δ := by
            rw [hδ, ← map_zero hv.hom]
            exact hv.strictMono _ (Units.zero_lt ε)
          use δ, hδ_pos
          apply subset_trans _ hε
          intro x hx
          simp only [mem_ofPred_eq, Valuation.norm, hδ, NNReal.coe_lt_coe] at hx
          rw [mem_ofPred, ← neg_sub, Valuation.map_neg]
          exact (RankOne.strictMono Valued.v).lt_iff_lt.mp hx
        · have : Nontrivial Γ₀ˣ := (nontrivial_iff_exists_ne (1 : Γ₀ˣ)).mpr
            ⟨RankOne.unit val.v, RankOne.unit_ne_one val.v⟩
          obtain ⟨u, hu⟩ := Real.exists_lt_of_strictMono hv.strictMono hr_pos
          use u
          apply subset_trans _ hr
          intro x hx
          simp only [Valuation.norm, mem_ofPred_eq]
          apply lt_trans _ hu
          rw [NNReal.coe_lt_coe, ← neg_sub, Valuation.map_neg]
          exact (RankOne.strictMono Valued.v).lt_iff_lt.mpr hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 3)
⊢ (ofJ0 R).j = 0

Tactic:
rw [j, ofJ0_c₄]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 3)
⊢ ↑(ofJ0 R).Δ'⁻¹ * 0 ^ 3 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q

Tactic:
add_of_equiv <| (smul_equiv_smul P Q hu hv).mpr h,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.dblXYZ (u • P) = u ^ 4 • W'.add P Q
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
⊢ (W'⁄B).polynomialY = (MvPolynomial.map ↑f) (W'⁄A).polynomialY

Tactic:
by
  rw [← map_polynomialY, map_baseChange]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GluingOneHypercover

Goal state before:
pp: D : GlueData
i₁ i₂ : D.J
x✝ : PUnit.{u + 1}
⊢ D.f i₁ i₂ ≫ D.ι i₁ = (D.t i₁ i₂ ≫ D.f i₂ i₁) ≫ D.ι i₂

Tactic:
by simp only [Category.assoc, Scheme.GlueData.glue_condition]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : ℕ → R
hx : x ∈ submodule I R
hy : y ∈ submodule I R
m n : ℕ
hmn : m ≤ n
⊢ (x * y) m ≡ (x * y) n [SMOD I ^ m • ⊤]

Tactic:
by
      simp only [Pi.mul_apply]
      exact SModEq.mul (hx hmn) (hy hmn)

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R✝¹ : Type u_1
S✝ : Type u_2
inst✝⁹ : CommRing R✝¹
inst✝⁸ : CommRing S✝
I✝ : Ideal R✝¹
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R✝¹ M
R✝ : Type u_4
S : Type u_5
inst✝⁵ : NonAssocSemiring R✝
inst✝⁴ : CommRing S
I : Ideal S
f✝ : (n : ℕ) → R✝ →+* S ⧸ I ^ n
hf✝ : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f✝ n) = f✝ m
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
r : R
n : ℕ
⊢ (evalₐ I n) ((↑↑(liftRingHom I (fun n ↦ (f n).toRingHom) ⋯)).toFun ((algebraMap R A) r)) =
    (evalₐ I n) ((algebraMap R (AdicCompletion I S)) r)

Tactic:
simp [evalₐ_liftRingHom _ _ <| fun hle ↦ by ext x; exact congr($(hf hle) x)]

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✝³ : Finite ι
inst✝² : Finite ι'
inst✝¹ : Finite σ
inst✝ : Finite σ'
⊢ (Q.comp P).dimension = Q.dimension + P.dimension

Tactic:
by
  simp only [Presentation.dimension]
  have : Nat.card σ ≤ Nat.card ι :=
    card_relations_le_card_vars_of_isFinite P
  have : Nat.card σ' ≤ Nat.card ι' :=
    card_relations_le_card_vars_of_isFinite Q
  simp only [Nat.card_sum]
  lia

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

Goal state before:
pp: case intro.intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ
val✝ : Fintype σ'
⊢ ((aeval P.val).mapMatrix ((rename ⇑e).mapMatrix ((rename ⇑e.symm).mapMatrix (P.jacobiMatrix.submatrix ⇑f ⇑f)))).det =
    ((aeval P.val).mapMatrix (P.jacobiMatrix.submatrix ⇑f ⇑f)).det

Tactic:
AlgHom.mapMatrix_apply,

Goal state after:
case intro.intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ
val✝ : Fintype σ'
⊢ ((((P.jacobiMatrix.submatrix ⇑f ⇑f).map ⇑(rename ⇑e.symm)).map ⇑(rename ⇑e)).map ⇑(aeval P.val)).det =
    ((P.jacobiMatrix.submatrix ⇑f ⇑f).map ⇑(aeval P.val)).det
Module: Mathlib.RingTheory.Extension.Presentation.Core

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
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
⊢ Set.range (relationOfHasCoeffs R₀) ⊆ ↑(RingHom.ker (MvPolynomial.aeval P.val))

Tactic:
rintro a ⟨i, rfl⟩

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
i : σ
⊢ relationOfHasCoeffs R₀ i ∈ ↑(RingHom.ker (MvPolynomial.aeval P.val))
Module: Mathlib.RingTheory.Extension.Presentation.Core

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
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
⊢ Set.range P.relation ⊆
    ↑(RingHom.ker
        ((TensorProduct.map (AlgHom.id R R)
              (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
          ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm))

Tactic:
rintro a ⟨i, rfl⟩

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
i : σ
⊢ P.relation i ∈
    ↑(RingHom.ker
        ((TensorProduct.map (AlgHom.id R R)
              (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
          ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm))
Module: Mathlib.RingTheory.Extension.Presentation.Core

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 : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
this : Fintype σ := Fintype.ofFinite σ
⊢ (MvPolynomial.aeval P.val) ((MvPolynomial.map (algebraMap R₀ R)) (P.jacobianOfHasCoeffs R₀)) = P.jacobian

Tactic:
map_jacobianOfHasCoeffs,

Goal state after:
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 : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
this : Fintype σ := Fintype.ofFinite σ
⊢ (MvPolynomial.aeval P.val) P.jacobiMatrix.det = P.jacobian
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.negDblY P * P z ^ 2 = -(eval P) W'.polynomialX ^ 3

Tactic:
by
  rw [negDblY_eq' hP, Y_eq_negY_of_Y_eq hQz hx hy hy']
  ring1

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.Etale ↔ f.Flat ∧ f.FormallyUnramified ∧ f.FinitePresentation

Tactic:
by
  algebraize [f]
  simp_rw [← f.algebraMap_toAlgebra, RingHom.etale_algebraMap, RingHom.flat_algebraMap_iff,
    RingHom.formallyUnramified_algebraMap, RingHom.finitePresentation_algebraMap]
  refine ⟨fun h ↦ ⟨inferInstance, inferInstance, inferInstance⟩,
    fun ⟨_, _, _⟩ ↦ .of_formallyUnramified_of_flat⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F.totalDegree ≤ ((rename Subtype.val) (F₀.coeff (σ i))).totalDegree
⊢ σ i ≤ ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F).totalDegree

Tactic:
totalDegree_renameEquiv

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F.totalDegree ≤ ((rename Subtype.val) (F₀.coeff (σ i))).totalDegree
⊢ σ i ≤ F.totalDegree
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_3
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F.totalDegree ≤ ((rename Subtype.val) (F₀.coeff (σ i))).totalDegree
this : (F₀.coeff (σ i)).totalDegree + σ i ≤ ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F).totalDegree
⊢ False

Tactic:
totalDegree_renameEquiv

Goal state after:
case refine_3
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F.totalDegree ≤ ((rename Subtype.val) (F₀.coeff (σ i))).totalDegree
this : (F₀.coeff (σ i)).totalDegree + σ i ≤ F.totalDegree
⊢ False