mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) W'.polynomial = 0 ↔
    P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3) =
      0

Tactic:
eval_polynomial,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3) =
      0 ↔
    P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3) =
      0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ 3 * (eval P) W'.polynomial =
    P x * (eval P) W'.polynomialX + P y * (eval P) W'.polynomialY + P z * (eval P) W'.polynomialZ

Tactic:
eval_polynomial,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ 3 *
      (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)) =
    P x * (eval P) W'.polynomialX + P y * (eval P) W'.polynomialY + P z * (eval P) W'.polynomialZ
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
⊢ W.Equation P ∧
      ((eval P) W.polynomialX ≠ 0 ∧ P z ^ 2 ≠ 0 ∨
        Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
    W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)

Tactic:
and_iff_left <| pow_ne_zero 2 hPz,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY ≠ 0) ↔
    W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

Tactic:
add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right,

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
hy : P y * Q z = Q y * P z
⊢ toAffine W (W.dblU P • ![0, 1, 0]) = 0
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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z - W'.negY Q * P z = 0
hy : P y = W'.negY P
⊢ P y * Q z = Q y * P z

Tactic:
linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z * hy - hy'

Goal state after:
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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z - Q y * P z = 0
hy : P y = W'.negY P
⊢ P y * Q z = W'.negY Q * P z

Tactic:
linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z * hy - hy'

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : IsLocalRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
inst✝⁴ : Algebra P S
inst✝³ : IsScalarTower R P S
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
⊢ FormallySmooth R S ↔ Function.Injective ⇑(cotangentComplexBaseChange R S P (ResidueField S))

Tactic:
let P' : Extension R S := { Ring := P, σ := _, algebraMap_σ := Function.surjInv_eq h₁ }

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : IsLocalRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
inst✝⁵ : Algebra R P
inst✝⁴ : Algebra P S
inst✝³ : IsScalarTower R P S
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
P' : Extension R S :=
  { Ring := P, commRing := inst✝⁶, algebra₁ := inst✝⁵, algebra₂ := inst✝⁴, isScalarTower := inst✝³,
    σ := Function.surjInv h₁, algebraMap_σ := ⋯ }
⊢ FormallySmooth R S ↔ Function.Injective ⇑(cotangentComplexBaseChange R S P (ResidueField S))
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: 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
x : B ⊗[S] B
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B)))
      ((derivationTensorProduct R S A B).liftKaehlerDifferential ((D S B).tensorProductTo x)) =
    (D S B).tensorProductTo x

Tactic:
induction x with

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.tmul
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
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[R] S :=
  AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B).symm) (LinearEquiv.refl A Ω[A⁄R]) ≪≫ₗ
      TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
y : Ω[A⁄R]
x : A ⊗[R] S
⊢ e₂ ((Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • (Algebra.IsPushout.equiv R A S B) x ⊗ₜ[A] y) =
    (Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • e₂ ((Algebra.IsPushout.equiv R A S B) x ⊗ₜ[A] y)

Tactic:
induction x with

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul
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
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[R] S :=
  AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B).symm) (LinearEquiv.refl A Ω[A⁄R]) ≪≫ₗ
      TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
x : B ⊗[A] Ω[A⁄R]
a : A
b : S
⊢ e₂ ((Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • x) = (Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • e₂ x

Tactic:
induction x with

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)
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst✝³ : Algebra Pp Sp := φ.toAlgebra
algInst✝² : Algebra P Sp := (φ.comp (algebraMap P Pp)).toAlgebra
algInst✝¹ : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst✝ : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst✝¹ : IsScalarTower P Pp Sp := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P Sp))
scalarTowerInst✝ : IsScalarTower Pp Sp 𝓀[S] := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Pp 𝓀[S]))
this✝⁷ : IsScalarTower 𝓀[R] Pp Sp
this✝⁶ : IsScalarTower R Sp 𝓀[S]
this✝⁵ : IsScalarTower P S Sp
this✝⁴ : IsScalarTower S Sp 𝓀[S]
this✝³ : IsScalarTower P Sp 𝓀[S]
this✝² : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp).symm
this✝¹ : Module.Free Pp Ω[Pp⁄𝓀[R]]
this✝ : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (algebraMap P S)) := kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
h₁' : Function.Surjective ⇑φ
h₂' : (RingHom.ker φ).FG
h₃ : 𝓂[Sp] ≤ RingHom.ker ψ
this : Function.Injective ⇑(KaehlerDifferential.cotangentComplexBaseChange 𝓀[R] Sp Pp 𝓀[S])
eᵣ : 𝓀[S] ⊗[Pp] Ω[Pp⁄𝓀[R]] ≃ₗ[S] 𝓀[S] ⊗[P] Ω[P⁄R] :=
  LinearEquiv.restrictScalars S (AlgebraTensorModule.congr (LinearEquiv.refl 𝓀[S] 𝓀[S]) e₀) ≪≫ₗ
    LinearEquiv.restrictScalars S (AlgebraTensorModule.cancelBaseChange P Pp Sp 𝓀[S] Ω[P⁄R])
eₗ : 𝓀[S] ⊗[Pp] ↥(RingHom.ker φ) ≃ₗ[S] 𝓀[S] ⊗[P] ↥(RingHom.ker (algebraMap P S)) :=
  LinearEquiv.restrictScalars S (AlgebraTensorModule.congr (LinearEquiv.refl 𝓀[S] 𝓀[S]) e₁) ≪≫ₗ
    LinearEquiv.restrictScalars S (AlgebraTensorModule.cancelBaseChange P Pp Sp 𝓀[S] ↥(RingHom.ker (algebraMap P S)))
x : 𝓀[S] ⊗[P] ↥(RingHom.ker (algebraMap P S))
⊢ (KaehlerDifferential.cotangentComplexBaseChange R S P 𝓀[S]) x =
    eᵣ ((KaehlerDifferential.cotangentComplexBaseChange 𝓀[R] Sp Pp 𝓀[S]) (eₗ.symm x))

Tactic:
induction x with

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
⊢ ↑R (reduceModIdeal (I ^ m) f) ∘ₗ transitionMap I M hmn ∘ₗ eval I M n = ↑R (reduceModIdeal (I ^ m) f) ∘ₗ eval I M m

Tactic:
transitionMap_comp_eval

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
⊢ ↑R (reduceModIdeal (I ^ m) f) ∘ₗ eval I M m = ↑R (reduceModIdeal (I ^ m) f) ∘ₗ eval I M m
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.negDblY P = -W.dblU P

Tactic:
rw [dblU, ← neg_div, ← negDblY_of_Y_eq' hP hQz hx hy hy',
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
r x✝ : σ
⊢ P.cotangentEquiv (Cotangent.mk ⟨P.relation r, ⋯⟩) x✝ = P.cotangentEquiv (P.basisCotangent r) x✝

Tactic:
basisCotangent,

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 x✝ : σ
⊢ P.cotangentEquiv (Cotangent.mk ⟨P.relation r, ⋯⟩) x✝ =
    P.cotangentEquiv ((P.basisDeriv.map P.cotangentEquiv.symm) r) x✝
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsStandardSmooth R S
w✝² w✝¹ : Type
w✝ : Finite w✝¹
left✝ : Finite w✝²
P : SubmersivePresentation R S w✝² w✝¹
⊢ Free S Ω[S⁄R]

Tactic:
exact P.free_kaehlerDifferential

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
⊢ ((localizationAway T g).comp P).ker =
    Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1}

Tactic:
have : (localizationAway T g).ker = Ideal.map ((localizationAway T g).ofComp P).toAlgHom
      (Ideal.span {MvPolynomial.rename Sum.inr f * MvPolynomial.X (Sum.inl ()) - 1}) := by
    rw [Ideal.map_span, Set.image_singleton, map_sub, map_mul, map_one, ker_localizationAway,
      Hom.toAlgHom_X, toAlgHom_ofComp_rename, h, ofComp_val, Sum.elim_inl]
  rw [ker_comp_eq_sup, Algebra.Generators.map_toComp_ker, this,
    Ideal.comap_map_of_surjective _ (toAlgHom_ofComp_surjective _ P), ← RingHom.ker_eq_comap_bot,
    ← sup_assoc]
  simp

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

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

Tactic:
Finsupp.mem_span_range_iff_exists_finsupp

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_3
κ : Type u_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S fun k ↦ (D R S) (P.val (v k))
x : P.toExtension.CotangentSpace
hx : x ∈ ↑P.toExtension.toKaehler.ker
hxs : ∃ c, (c.sum fun i a ↦ a • P.cotangentSpaceBasis (v i)) = x
⊢ x = 0
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
⊢ IsStandardSmooth R S ↔ Subsingleton (H1Cotangent R S) ∧ ∃ I b, Set.range ⇑b ⊆ Set.range ⇑(D R S)

Tactic:
refine ⟨fun h ↦ ⟨inferInstance, ?_⟩, fun ⟨h, ⟨_, b, hb⟩⟩ ↦ .of_basis_kaehlerDifferential b hb⟩
  obtain ⟨ι, σ, _, _, ⟨P⟩⟩ := Algebra.IsStandardSmooth.out (R := R) (S := S)
  exact ⟨_, P.basisKaehler, by simp [Set.range_subset_iff]⟩

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
⊢ eₚ = ↑b.repr.symm

Tactic:
ext i

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := ⋯
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p := ⋯
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := ⋯
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] := ⋯
i : κ
⊢ (eₚ ∘ₗ Finsupp.lsingle i) 1 = (↑b.repr.symm ∘ₗ Finsupp.lsingle i) 1
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
⊢ Algebra.IsStandardSmooth R T

Tactic:
algebraize [f, g, (g.comp f)]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.IsStandardSmooth S T
algebraizeInst✝ : Algebra.IsStandardSmooth R S
⊢ Algebra.IsStandardSmooth R T
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n m : ℕ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
⊢ Algebra.IsStandardSmoothOfRelativeDimension (n + m) R T

Tactic:
algebraize [f, g, (g.comp f)]

Goal state after:
n m : ℕ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.IsStandardSmoothOfRelativeDimension n S T
algebraizeInst✝ : Algebra.IsStandardSmoothOfRelativeDimension m R S
⊢ Algebra.IsStandardSmoothOfRelativeDimension (n + m) R T
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
inst✝¹ : Finite D.vars
inst✝ : Finite D.rels
⊢ (⋃ i, ↑(D.h i).coeffs).Finite

Tactic:
refine Set.finite_iUnion fun i ↦ Finset.finite_toSet _

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

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.Etale ↔ IsStandardSmoothOfRelativeDimension 0 f

Tactic:
exact Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝¹ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this✝ : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
hr : Algebra.Smooth (↑Γ(Y, U)) (Localization.Away r)
this : IsLocalization.Away r ↑Γ(X, X.basicOpen r)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)).Smooth

Tactic:
← RingHom.smooth_algebraMap

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝¹ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this✝ : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
hr : (algebraMap (↑Γ(Y, U)) (Localization.Away r)).Smooth
this : IsLocalization.Away r ↑Γ(X, X.basicOpen r)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)).Smooth
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : Smooth f
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.Smooth ↑Γ(Y, U) ↑Γ(X, V)
⊢ x ∈ smoothLocus f

Tactic:
Scheme.Hom.mem_smoothLocus,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : Smooth f
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.Smooth ↑Γ(Y, U) ↑Γ(X, V)
⊢ (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth
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
hx : P x * Q z = Q x * P z
⊢ ![0, addU P Q, W.addZ P Q] = addU P Q • ![0, 1, 0]

Tactic:
addZ_of_X_eq hP hQ hPz hQz hx,

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
hx : P x * Q z = Q x * P z
⊢ ![0, addU P Q, 0] = addU P Q • ![0, 1, 0]