mathlib-initiative/mathlib-tactics huggingface dataset:
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
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • x + a.den • y) - k • 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
⊢ 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1

Tactic:
smul_add,

Goal state after:
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 + k • a.den • y - k • 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
⊢ 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case mpr
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 u : ℚ
hu : u ∈ ratLt x
v : ℚ
hv : v ∈ ratLt y
huv : u + v = a
⊢ u + v ∈ ratLt (x + y)

Tactic:
Set.mem_ofPred_eq

Goal state after:
case mpr
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 u : ℚ
hu : u.num • 1 < u.den • x
v : ℚ
hv : v.num • 1 < v.den • y
huv : u + v = a
⊢ (u + v).num • 1 < (u + v).den • (x + y)
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
r s : ℝ
p : X → Prop
x✝² x✝¹ x✝ : Subtype p
⊢ dist x✝² x✝ ≤ max (dist x✝² x✝¹) (dist x✝¹ x✝)

Tactic:
by simpa [Subtype.dist_eq] using dist_triangle_max _ _ _

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

Goal state before:
pp: case refine_2.refine_1
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : (ofClass valuation).ValueGroup₀ˣ
hε : {x | valuation.restrict x < ↑ε} ⊆ U
⊢ ↑(embedding ↑ε) > 0

Tactic:
exact NNReal.coe_pos.mpr <| embedding_strictMono.lt_iff_lt.mpr ε.zero_lt

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
v : HeightOneSpectrum A
hv : Finite (A ⧸ v.asIdeal)
⊢ ¬(Set.range ⇑(valuation K v)).Subsingleton

Tactic:
simpa using (v.valuation K).toMonoidWithZeroHom.range_nontrivial

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

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j ≠ 0
h1728 : j ≠ 1728
⊢ (if j = 0 then if 3 = 0 then ofJ1728 F else ofJ0 F else if j = 1728 then ofJ1728 F else ofJNe0Or1728 j) =
    ofJNe0Or1728 j

Tactic:
if_neg h0,

Goal state after:
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j ≠ 0
h1728 : j ≠ 1728
⊢ (if j = 1728 then ofJ1728 F else ofJNe0Or1728 j) = ofJNe0Or1728 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
⊢ Function.Bijective (E.toPreOneHypercover.multifork F).toSections ↔ Presieve.IsSheafFor F E.presieve₀

Tactic:
Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,

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
⊢ Function.Bijective (E.toPreOneHypercover.multifork F).toSections ↔
    Function.Bijective (Presieve.Arrows.toCompatible F E.f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ W.Nonsingular (W.add P Q)

Tactic:
by
  by_cases hPz : P z = 0
  · by_cases hQz : Q z = 0
    · simp only [add_of_Z_eq_zero hP hQ hPz hQz,
        nonsingular_smul _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4, nonsingular_zero]
    · simpa only [add_of_Z_eq_zero_left hP.left hPz hQz,
        nonsingular_smul _ <| ((isUnit_Y_of_Z_eq_zero hP hPz).pow 2).mul <| Ne.isUnit hQz]
  · by_cases hQz : Q z = 0
    · simpa only [add_of_Z_eq_zero_right hQ.left hPz hQz,
        nonsingular_smul _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg]
    · by_cases hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
      · by_cases hy : P y * Q z = Q y * P z
        · simp only [add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right, nonsingular_smul _ <|
              isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, nonsingular_zero]
        · simp only [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            nonsingular_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, nonsingular_zero]
      · classical
        have := nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy
        by_cases hx : P x * Q z = Q x * P z
        · simpa only [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            nonsingular_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hQz hx <|
              not_and.mp hxy hx]
        · simpa only [add_of_X_ne hP.left hQ.left hPz hQz hx,
            nonsingular_smul _ <| isUnit_addZ_of_X_ne hP.left hQ.left hx]

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

Goal state before:
pp: case e'_3
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
P : Fin 3 → A
h : (W'⁄A).Equation P
⊢ W'⁄B = (W'⁄A).map f.toRingHom

Tactic:
AlgHom.toRingHom_eq_coe,

Goal state after:
case e'_3
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
P : Fin 3 → A
h : (W'⁄A).Equation P
⊢ W'⁄B = (W'⁄A).map ↑f
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).Equation (⇑↑f ∘ P) ↔ ((W'⁄A).map f.toRingHom).Equation (⇑f.toRingHom ∘ P)

Tactic:
AlgHom.toRingHom_eq_coe,

Goal state after:
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).Equation (⇑↑f ∘ P) ↔ ((W'⁄A).map ↑f).Equation (⇑↑f ∘ P)
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).map f.toRingHom).Nonsingular (⇑f.toRingHom ∘ P)

Tactic:
AlgHom.toRingHom_eq_coe,

Goal state after:
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).map ↑f).Nonsingular (⇑↑f ∘ P)
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: case g.map_mul
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
x y : A i
⊢ ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i)
      (x * y) =
    ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i) x *
      ((Ideal.Quotient.mkₐ R (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)).toLinearMap ∘ₗ LinearMap.single R A i) y

Tactic:
change Ideal.Quotient.mk _ _ = Ideal.Quotient.mk _ _ * Ideal.Quotient.mk _ _

Goal state after:
case g.map_mul
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
x y : A i
⊢ (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) ((LinearMap.single R A i) (x * y)) =
    (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) ((LinearMap.single R A i) x) *
      (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) ((LinearMap.single R A i) y)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
x y : S ⊗[R] Ω[A⁄R]
⊢ (TensorProduct.comm R S Ω[A⁄R]).symm (a • ((TensorProduct.comm R S Ω[A⁄R]) x + (TensorProduct.comm R S Ω[A⁄R]) y)) =
    a • x + a • y

Tactic:
smul_add,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
x y : S ⊗[R] Ω[A⁄R]
⊢ (TensorProduct.comm R S Ω[A⁄R]).symm (a • (TensorProduct.comm R S Ω[A⁄R]) x + a • (TensorProduct.comm R S Ω[A⁄R]) y) =
    a • x + a • y
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case smul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
b : B
x : S
y : B
e :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (y * b) =
    y • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b + b • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) y
⊢ x • (y • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b + b • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) y) =
    (x • y) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b + b • x • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) y

Tactic:
smul_add,

Goal state after:
case smul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
b : B
x : S
y : B
e :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (y * b) =
    y • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b + b • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) y
⊢ x • y • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b + x • b • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) y =
    (x • y) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b + b • x • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) y
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.smul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
z : A
s✝ : S
n✝ : B
e :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
⊢ s✝ •
      ((algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
        n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)) =
    (algebraMap A B) z • s✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      (s✝ • n✝) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)

Tactic:
smul_add,

Goal state after:
case tmul.smul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
z : A
s✝ : S
n✝ : B
e :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
⊢ s✝ • (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      s✝ • n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z) =
    (algebraMap A B) z • s✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      (s✝ • n✝) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
Module: Mathlib.RingTheory.Smooth.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Flat R S
inst✝⁴ : FinitePresentation R S
p : Ideal R
q : Ideal S
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom ⋯
algInst✝ : Algebra Sp Sq := f.toAlgebra
this✝¹ : IsScalarTower R Sp Sq
this✝ : IsScalarTower Rp Sp Sq
this : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
⊢ FinitePresentation Rp Sp

Tactic:
have : Algebra.IsPushout R Rp S Sp :=
      .symm <| Algebra.isPushout_of_isLocalization p.primeCompl _ _ _

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Flat R S
inst✝⁴ : FinitePresentation R S
p : Ideal R
q : Ideal S
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this✝³ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom ⋯
algInst✝ : Algebra Sp Sq := f.toAlgebra
this✝² : IsScalarTower R Sp Sq
this✝¹ : IsScalarTower Rp Sp Sq
this✝ : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this : IsPushout R Rp S Sp
⊢ FinitePresentation Rp Sp
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
h : (pderiv ()) (C r * X () - 1) = C r
i j : Unit
⊢ (localizationAway S r).jacobiMatrix i j = Matrix.diagonal (fun x ↦ C r) i j

Tactic:
rwa [jacobiMatrix_apply]

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 σ'
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = (algebraMap S T) P.jacobian

Tactic:
rw [jacobian_eq_jacobiMatrix_det]

Goal state after:
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 σ'
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det =
    (algebraMap S T) ((algebraMap P.Ring S) P.jacobiMatrix.det)
Module: Mathlib.RingTheory.Smooth.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmooth R S
inst✝ : IsStandardSmooth S T
⊢ ∃ ι σ, ∃ (x : Finite σ), Finite ι ∧ Nonempty (SubmersivePresentation R T ι σ)

Tactic:
by
    obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
    obtain ⟨_, _, _, _, ⟨Q⟩⟩ := ‹IsStandardSmooth S T›
    exact ⟨_, _, _, inferInstance, ⟨Q.comp P⟩⟩

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

Goal state before:
pp: case e'_4
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 ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
⊢ ⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘
      ⇑(Finsupp.lcomapDomain P.map ⋯) ∘ ⇑P.cotangentSpaceBasis.repr ∘ ⇑P.cotangentSpaceBasis ∘ P.map =
    ⇑(Pi.basisFun S σ)

Tactic:
ext i j

Goal state after:
case e'_4
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 ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
i j : σ
⊢ (⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘
        ⇑(Finsupp.lcomapDomain P.map ⋯) ∘ ⇑P.cotangentSpaceBasis.repr ∘ ⇑P.cotangentSpaceBasis ∘ P.map)
      i j =
    (Pi.basisFun S σ) i j
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))

pp: case hmap
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
⊢ Submodule.map g (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:
case hmap
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
⊢ Submodule.map g (Submodule.span S (Set.range fun x ↦ Finsupp.single (v x) 1)) = ⊤
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
hPz : P z ≠ 0
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.dblXYZ P = W.dblU P • ![0, 1, 0]

Tactic:
by
  erw [dblXYZ, dblX_of_Y_eq hP hPz hQz hx hy hy', dblY_of_Y_eq hP hPz hQz hx hy hy',
    dblZ_of_Y_eq hQz hx hy hy', smul_fin3, mul_zero, mul_one]

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_4
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
b : Module.Basis σ S P.toExtension.Cotangent
hb : ∀ (r : σ), b r = Extension.Cotangent.mk ⟨P.relation r, ⋯⟩
h : Function.Bijective ⇑(P.cotangentRestrict ⋯)
⊢ (fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) =
    ⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘ ⇑(P.cotangentRestrict ⋯) ∘ ⇑b

Tactic:
ext i j

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_4
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
b : Module.Basis σ S P.toExtension.Cotangent
hb : ∀ (r : σ), b r = Extension.Cotangent.mk ⟨P.relation r, ⋯⟩
h : Function.Bijective ⇑(P.cotangentRestrict ⋯)
i j : σ
⊢ (aeval P.val) ((pderiv (P.map j)) (P.relation i)) =
    (⇑(Finsupp.linearEquivFunOnFinite S S σ) ∘ ⇑(P.cotangentRestrict ⋯) ∘ ⇑b) i j