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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Projective R
W : Projective F
P : W.Point
⊢ (toAffineAddEquiv W) (-P + P) = (toAffineAddEquiv W) 0

Tactic:
simp only [map_add, toAffineAddEquiv_apply, toAffineLift_neg, neg_add_cancel, toAffineLift_zero]

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
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ smoothLocus R A ↔ FormallySmooth R (Localization.Away f)

Tactic:
rw [smoothLocus_eq_compl_support_inter, Set.subset_inter_iff, Set.subset_compl_comm,
    PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl,
    ← LocalizedModule.subsingleton_iff_support_subset,
    Algebra.formallySmooth_iff, iff_comm, and_comm]
  congr! 1
  · have := IsLocalizedModule.iso (.powers f) (H1Cotangent.map R R A (Localization.Away f))
    rw [this.subsingleton_congr]
  · rw [← PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Module.basicOpen_subset_freeLocus_iff]
    have := IsLocalizedModule.iso (.powers f)
        (KaehlerDifferential.map R R A (Localization.Away f))
    have := this.extendScalarsOfIsLocalization (.powers f) (Localization.Away f)
    exact ⟨fun _ ↦ .of_equiv this.symm, fun _ ↦ .of_equiv this⟩

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
⊢ ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J

Tactic:
intro g

Goal state after:
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
g : (i : I) → f i
⊢ f₁ g - f₂ g ∈ J
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
⊢ f₂ e * (1 - f₁ e) = -f₂ e * (f₁ e - f₂ e)

Tactic:
rw [neg_mul, mul_sub, mul_sub, mul_one, neg_sub, (he.map f₂).eq]

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

Goal state before:
pp: case intro.mpr.a
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₂' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
r : f x
⊢ ((Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₁') r =
    ((Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₂') r

Tactic:
← sub_eq_zero

Goal state after:
case intro.mpr.a
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₂' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
r : f x
⊢ ((Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₁') r -
      ((Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₂') r =
    0
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
r s : A
x : S ⊗[R] Ω[A⁄R]
⊢ (r + s) • x = r • x + s • x

Tactic:
by induction x <;> simp [add_smul, tmul_add, *, add_add_add_comm]

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

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

Tactic:
have : FormallyEtale (Localization.AtPrime p) (Localization.AtPrime P) :=
    .localization_base p.primeCompl

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
p : Ideal A
P : Ideal B
inst✝⁴ : P.LiesOver p
inst✝³ : p.IsPrime
inst✝² : P.IsPrime
inst✝¹ : IsEtaleAt R p
inst✝ : IsEtaleAt A P
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
this : FormallyEtale (Localization.AtPrime p) (Localization.AtPrime P)
⊢ IsEtaleAt R P
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
this✝² : FinitePresentation Rp Sp
this✝¹ : Algebra S (𝓀[Rp] ⊗[R] S) := TensorProduct.rightAlgebra
this✝ : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[R] S ⊗[S] Sq)
e : 𝓀[Rp] ⊗[R] S ≃ₐ[S] S ⊗[R] 𝓀[Rp] :=
  let __spread.0 := TensorProduct.comm R 𝓀[Rp] S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e' : 𝓀[Rp] ⊗[R] S ⊗[S] Sq ≃ₐ[R] 𝓀[Rp] ⊗[Rp] Sq :=
  (AlgEquiv.restrictScalars R (TensorProduct.comm S (𝓀[Rp] ⊗[R] S) Sq)).trans
    ((AlgEquiv.restrictScalars R (TensorProduct.congr AlgEquiv.refl e)).trans
      ((AlgEquiv.restrictScalars R (TensorProduct.cancelBaseChange R S S Sq 𝓀[Rp])).trans
        ((TensorProduct.comm R Sq 𝓀[Rp]).trans (TensorProduct.equivOfCompatibleSMul Rp R R 𝓀[Rp] Sq))))
this :
  (↑e').comp (IsScalarTower.toAlgHom R p.ResidueField (𝓀[Rp] ⊗[R] S ⊗[S] Sq)) =
    IsScalarTower.toAlgHom R p.ResidueField (𝓀[Rp] ⊗[Rp] Sq)
e'' : 𝓀[Rp] ⊗[R] S ⊗[S] Sq ≃ₐ[𝓀[Rp]] 𝓀[Rp] ⊗[Rp] Sq :=
  let __spread.0 := e';
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[Rp] Sq)

Tactic:
exact .of_equiv e''

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
I : Ideal R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCompletion I M
a : AdicCauchySequence I M
hx : (map I f) ((mk I M) a) = 0
n : ℕ
x✝ : n ≥ 42
⊢ ↑a (n + k) ∈ I ^ n • ⊤

Tactic:
← Submodule.comap_map_eq_of_injective hf (I ^ n • ⊤ : Submodule R M),

Goal state after:
R : Type u
inst✝⁶ : CommRing R
I : Ideal R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCompletion I M
a : AdicCauchySequence I M
hx : (map I f) ((mk I M) a) = 0
n : ℕ
x✝ : n ≥ 42
⊢ ↑a (n + k) ∈ Submodule.comap f (Submodule.map f (I ^ n • ⊤))
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
n : ℕ
d : N
hdmem : d ∈ I ^ (k + n + 1) • ⊤
y yₙ : M
hd : f y = ↑x (k + n + 1) - d
hyₙ : f yₙ - ↑x (k + n) ∈ I ^ (k + n) • ⊤
h : f (y - yₙ) ∈ I ^ (k + n) • ⊤
hincl : I ^ (k + n - k) • (I ^ k • ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
⊢ y - yₙ ∈ I ^ n • ⊤

Tactic:
convert_to y - yₙ ∈ (I ^ (k + n - k) • ⊤ : Submodule R M)

Goal state after:
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
n : ℕ
d : N
hdmem : d ∈ I ^ (k + n + 1) • ⊤
y yₙ : M
hd : f y = ↑x (k + n + 1) - d
hyₙ : f yₙ - ↑x (k + n) ∈ I ^ (k + n) • ⊤
h : f (y - yₙ) ∈ I ^ (k + n) • ⊤
hincl : I ^ (k + n - k) • (I ^ k • ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
⊢ I ^ n • ⊤ = I ^ (k + n - k) • ⊤

R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
n : ℕ
d : N
hdmem : d ∈ I ^ (k + n + 1) • ⊤
y yₙ : M
hd : f y = ↑x (k + n + 1) - d
hyₙ : f yₙ - ↑x (k + n) ∈ I ^ (k + n) • ⊤
h : f (y - yₙ) ∈ I ^ (k + n) • ⊤
hincl : I ^ (k + n - k) • (I ^ k • ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
⊢ y - yₙ ∈ I ^ (k + n - k) • ⊤
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
y : AdicCompletion I N
b : AdicCauchySequence I N
⊢ (mk I N) b ∈ (map I g).ker → (mk I N) b ∈ (map I f).range

Tactic:
intro hz

Goal state after:
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
y : AdicCompletion I N
b : AdicCauchySequence I N
hz : (mk I N) b ∈ (map I g).ker
⊢ (mk I N) b ∈ (map I f).range
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
h : Function.Bijective ⇑(algebraMap R S)
⊢ (ofBijectiveAlgebraMap h).jacobian = 1

Tactic:
by
  have : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix
      (ofBijectiveAlgebraMap h).jacobiMatrix = 1 := by
    ext (i j : PEmpty)
    contradiction
  rw [jacobian_eq_jacobiMatrix_det, RingHom.map_det, this, Matrix.det_one]

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

Goal state before:
pp: case intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
val✝ : Fintype σ
h : (baseChange T P).jacobiMatrix = (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix
⊢ (algebraMap (baseChange T P).Ring (T ⊗[R] S)) (baseChange T P).jacobiMatrix.det =
    1 ⊗ₜ[R] (algebraMap P.Ring S) P.jacobiMatrix.det

Tactic:
rw [h, ← RingHom.map_det, Generators.algebraMap_apply, aeval_map_algebraMap, P.algebraMap_apply]

Goal state after:
case intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
val✝ : Fintype σ
h : (baseChange T P).jacobiMatrix = (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix
⊢ (aeval (baseChange T P).val) P.jacobiMatrix.det = 1 ⊗ₜ[R] (aeval P.val) P.jacobiMatrix.det
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 ι σ
κ : Type u_5
f : κ → ι
hf : Function.Injective f
hcompl : IsCompl (Set.range f) (Set.range P.map)
⊢ Basis κ S Ω[S⁄R]

Tactic:
by
  apply P.cotangentSpaceBasis.ofSplitExact (sectionCotangent_comp P)
    Extension.exact_cotangentComplex_toKaehler Extension.toKaehler_surjective hf (b := P.map)
  · intro i
    apply sectionCotangent_zero_of_notMem_range _ _
    simp [← hcompl.compl_eq]
  · simp only [sectionCotangent, LinearMap.coe_comp, Function.comp_assoc, LinearEquiv.coe_coe]
    apply LinearIndependent.map' _ _ P.cotangentEquiv.symm.ker
    convert! (Pi.basisFun S σ).linearIndependent
    classical
    ext i j
    simp only [Function.comp_apply, Basis.repr_self, Finsupp.linearEquivFunOnFinite_apply,
      Pi.basisFun_apply]
    simp [Finsupp.single_eq_pi_single]
  · exact hcompl.2

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ W'.addZ (u • P) (v • Q) = (u * v) ^ 2 * W'.addZ P Q

Tactic:
simp only [addZ, smul_fin3_ext]
  ring1

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
inst✝ : Smooth R S
f : (p : Ideal S) → [inst : p.IsPrime] → [IsSmoothAt R p] → S
hf₁ : ∀ (p : Ideal S) [inst : p.IsPrime] [inst_1 : IsSmoothAt R p], f p ∉ p
hf₂ : ∀ (p : Ideal S) [inst : p.IsPrime] [inst_1 : IsSmoothAt R p], IsStandardSmooth R (Localization.Away (f p))
⊢ ∀ x ∈ Set.range fun p ↦ f p.asIdeal, IsStandardSmooth R (Localization.Away x)

Tactic:
simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]; intro; apply hf₂

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.FormallyUnramified ∧ f.Smooth

Tactic:
by
  algebraize [f]
  simp only [Etale, Smooth, FormallyUnramified]
  exact ⟨fun h ↦ ⟨inferInstance, inferInstance, inferInstance⟩,
    fun ⟨h1, h2⟩ ↦ ⟨.of_formallyUnramified_and_formallySmooth, inferInstance⟩⟩

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

Goal state before:
pp: 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
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
hdiag : (Ideal.Quotient.mkₐ A (RingHom.ker f ^ 2)).comp (aeval h) = σ.comp (aeval P.val)
p :
  Fin (Presentation.ofFinitePresentationRels A B) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B))
      (MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
homog : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (p j).IsHomogeneous 2
hp : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (eval P.relation) (p j) = (aeval h) (P.relation j)
i : Fin (Presentation.ofFinitePresentationVars A B)
⊢ f (h i) = P.val i

Tactic:
rw [← AlgHom.kerSquareLift_mk]

Goal state after:
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
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
hdiag : (Ideal.Quotient.mkₐ A (RingHom.ker f ^ 2)).comp (aeval h) = σ.comp (aeval P.val)
p :
  Fin (Presentation.ofFinitePresentationRels A B) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B))
      (MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
homog : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (p j).IsHomogeneous 2
hp : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (eval P.relation) (p j) = (aeval h) (P.relation j)
i : Fin (Presentation.ofFinitePresentationVars A B)
⊢ f.kerSquareLift ((Ideal.Quotient.mk (RingHom.ker f.toRingHom ^ 2)) (h i)) = P.val i
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: 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
inst✝ : Smooth A B
⊢ ∃ A₀ B₀ x x_1 x_2 x_3 x_4,
    Function.Injective ⇑(algebraMap A₀ A) ∧ FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[A₀] B₀)

Tactic:
obtain ⟨A₀, B₀, _, _, hA₀, _, _⟩ := exists_subalgebra_fg R A B

Goal state after:
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
inst✝ : Smooth A B
A₀ : Subalgebra R A
B₀ : Type u
w✝¹ : CommRing B₀
w✝ : Algebra (↥A₀) B₀
hA₀ : A₀.FG
left✝ : Smooth (↥A₀) B₀
right✝ : Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
⊢ ∃ A₀ B₀ x x_1 x_2 x_3 x_4,
    Function.Injective ⇑(algebraMap A₀ A) ∧ FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[A₀] B₀)