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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negMap ⟦P⟧ = ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧

Tactic:
negMap_eq,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ⟦W.neg P⟧ = ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
⊢ ⟦W.add P Q⟧ = ⟦P⟧

Tactic:
add_of_Z_eq_zero_right hQ.left hPz hQz,

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
⊢ ⟦-(Q y ^ 2 * P z) • P⟧ = ⟦P⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : PointClass F
Q : Fin 3 → F
hP : W.NonsingularLift P
hQ : W.Nonsingular Q
hQz : Q z = 0
⊢ W.addMap P ⟦Q⟧ = P

Tactic:
by
  revert hP
  refine P.inductionOn (motive := fun P => _ → W.addMap P _ = P) fun P hP => ?_
  by_cases hPz : P z = 0
  · rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz,
      smul_eq _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4, Quotient.eq]
    exact Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz
  · rw [addMap_eq, add_of_Z_eq_zero_right hQ.left hPz hQz,
      smul_eq _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg]

Goal state after:
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
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
add_of_Z_eq_zero_right hQ.left hPz hQz,

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
⊢ toAffine W (-(Q y ^ 2 * P z) • P) = toAffine W P + toAffine W Q
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: P : MorphismProperty Scheme
F : Schemeᵒᵖ ⥤ Type u_1
inst✝¹ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : Finite 𝒰.I₀
this✝ : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.sigma.X 𝒰.sigma.f) ↔ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)

Tactic:
← Presieve.isSheafFor_sigmaDesc_iff 𝒰.f (coproductIsCoproduct _)
    (FinitaryExtensive.isVanKampen_finiteCoproducts (coproductIsCoproduct _)).isUniversal

Goal state after:
P : MorphismProperty Scheme
F : Schemeᵒᵖ ⥤ Type u_1
inst✝¹ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : Finite 𝒰.I₀
this✝ : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.sigma.X 𝒰.sigma.f) ↔
    Presieve.IsSheafFor F (Presieve.singleton (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f))
Module: Mathlib.RingTheory.RingHom.Smooth

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Smooth
hg : g.Smooth
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.Smooth R S
algebraizeInst✝ : Algebra.Smooth S T
⊢ (g.comp f).Smooth

Tactic:
exact Algebra.Smooth.comp R S T

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

Goal state before:
pp: case g.map_one
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
⊢ (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) (Pi.single i 1) = 1

Tactic:
← (Ideal.Quotient.mk _).map_one,

Goal state after:
case g.map_one
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
⊢ (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) (Pi.single i 1) =
    (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) 1
Module: Mathlib.RingTheory.Smooth.Pi

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

Tactic:
← (Ideal.Quotient.mk _).map_one,

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ (eval P) W.polynomialY = (P y - (-P y - W.a₁ * P x - W.a₃ * P z)) * P z

Tactic:
eval_polynomialY

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ 2 * P y * P z + W.a₁ * P x * P z + W.a₃ * P z ^ 2 = (P y - (-P y - W.a₁ * P x - W.a₃ * P z)) * P z
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
A : Type u
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K L
inst✝³ : Algebra K A
inst✝² : EssFiniteType K A
inst✝¹ : FormallyEtale K A
p : Ideal A
inst✝ : p.IsPrime
this✝³ : Module.Finite K A
this✝² : IsArtinianRing A
this✝¹ : IsReduced A
this✝ : Field (A ⧸ p) := Ideal.Quotient.field p
this : FormallyEtale K ((m : MaximalSpectrum A) → A ⧸ m.asIdeal)
⊢ FormallyEtale K (A ⧸ p)

Tactic:
Algebra.FormallyEtale.pi_iff

Goal state after:
K : Type u_1
L : Type u_2
A : Type u
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K L
inst✝³ : Algebra K A
inst✝² : EssFiniteType K A
inst✝¹ : FormallyEtale K A
p : Ideal A
inst✝ : p.IsPrime
this✝³ : Module.Finite K A
this✝² : IsArtinianRing A
this✝¹ : IsReduced A
this✝ : Field (A ⧸ p) := Ideal.Quotient.field p
this : ∀ (i : MaximalSpectrum A), FormallyEtale K (A ⧸ i.asIdeal)
⊢ FormallyEtale K (A ⧸ p)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case add
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
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A ⊗[R] A
a✝¹ :
  (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo x✝) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo x✝)
a✝ :
  (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo y✝) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo y✝)
⊢ (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ + y✝)) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ + y✝))

Tactic:
· simp only [map_add, TensorProduct.tmul_add, *]

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
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
n : ℕ
y : N ⧸ I ^ n • ⊤
y' : N ⧸ I ^ (n + 1) • ⊤
hyy' : (factor ⋯) y' = y
hxy : (I ^ n • ⊤).mkQ (f x) = y
y0 : N
hy0 : (I ^ (n + 1) • ⊤).mkQ y0 = y'
⊢ (I ^ n • ⊤).mkQ (f x) = (factor ⋯) ((I ^ n.succ • ⊤).mkQ y0)

Tactic:
hy0,

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
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
n : ℕ
y : N ⧸ I ^ n • ⊤
y' : N ⧸ I ^ (n + 1) • ⊤
hyy' : (factor ⋯) y' = y
hxy : (I ^ n • ⊤).mkQ (f x) = y
y0 : N
hy0 : (I ^ (n + 1) • ⊤).mkQ y0 = y'
⊢ (I ^ n • ⊤).mkQ (f x) = (factor ⋯) y'
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case convert_6
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) • ⊤
⊢ ↑x (k + n + 1) - ↑x (k + n) - d - (f yₙ - ↑x (k + n)) ∈ I ^ (k + n) • ⊤

Tactic:
· refine Submodule.sub_mem _ (Submodule.sub_mem _ ?_ ?_) hyₙ
      · rw [← Submodule.Quotient.eq]
        exact AdicCauchySequence.mk_eq_mk (by lia) _
      · exact (Submodule.smul_mono_left (Ideal.pow_le_pow_right (by lia))) hdmem

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑(ofTensorProductInvOfPiFintype I ι) ∘ₗ ofTensorProduct I (ι → R) = LinearMap.id

Tactic:
dsimp only [ofTensorProductInvOfPiFintype]

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑((piEquivOfFintype I fun x ↦ R).trans (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm) ∘ₗ
      ofTensorProduct I (ι → R) =
    LinearMap.id
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ofTensorProduct I (ι → R) ∘ₗ ↑(ofTensorProductInvOfPiFintype I ι) = LinearMap.id

Tactic:
dsimp only [ofTensorProductInvOfPiFintype]

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ofTensorProduct I (ι → R) ∘ₗ
      ↑((piEquivOfFintype I fun x ↦ R).trans (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm) =
    LinearMap.id
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(kerProj hf)

Tactic:
by
  dsimp [kerProj]
  exact (AlgEquiv.surjective _).comp (evalOneₐ_surjective _)

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
⊢ Function.Bijective ⇑(ofTensorProduct I M)

Tactic:
obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M

Goal state after:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective ⇑f
⊢ Function.Bijective ⇑(ofTensorProduct I M)
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 σ'
i j : σ
p : P.Ring
⊢ { toRingHom := eval₂Hom (algebraMap R T) (Q.comp P).val, commutes' := ⋯ } ((rename Sum.inr) p) =
    eval₂ (algebraMap R T) (fun i ↦ (algebraMap S T) (P.val i)) p

Tactic:
induction p using MvPolynomial.induction_on with

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

Goal state before:
pp: case a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
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'.dblY P * P z ^ 2 + W'.negDblY P * P z ^ 2 - ((eval P) W'.polynomialX ^ 3 + -(eval P) W'.polynomialX ^ 3) = 0

Tactic:
rw [dblY, negY_eq, dblX_of_Y_eq hP hPz hQz hx hy hy',
    dblZ_of_Y_eq hQz hx hy hy']

Goal state after:
case a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
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'.a₁ * 0 - W'.a₃ * 0) * P z ^ 2 + W'.negDblY P * P z ^ 2 -
      ((eval P) W'.polynomialX ^ 3 + -(eval P) W'.polynomialX ^ 3) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ ![u ^ 4 * W'.dblX P, W'.dblY (u • P), W'.dblZ (u • P)] = u ^ 4 • W'.dblXYZ P

Tactic:
dblY_smul,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ ![u ^ 4 * W'.dblX P, u ^ 4 * W'.dblY P, W'.dblZ (u • P)] = u ^ 4 • W'.dblXYZ P
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: ⊢ PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Etale

Tactic:
by
  rw [eq_formallyUnramified_and_smooth]
  exact FormallyUnramified.propertyIsLocal.and Smooth.propertyIsLocal

Goal state after:
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
⊢ IsStandardSmoothOfRelativeDimension (n + m) (g.comp f)

Tactic:
by
  rw [IsStandardSmoothOfRelativeDimension]
  algebraize [f, g, (g.comp f)]
  exact Algebra.IsStandardSmoothOfRelativeDimension.trans m n R S T

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

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ D.basis (Sum.inr r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩

Tactic:
· rw [basis_inr, cotangentEquivProd_symm_apply, cotangentCompLocalizationAwayEquiv_symm_inl,
      basisLeft, Module.Basis.map_apply, tensorCotangentEquiv_symm_apply,
      LinearMap.liftBaseChange_tmul, one_smul, Extension.Cotangent.map_mk]
    simp only [Extension.Hom.toAlgHom_apply, Hom.toExtensionHom_toRingHom, AlgHom.toRingHom_eq_coe]
    congr! 2 with x
    simp [pres, Presentation.comp_relation_inr, kerGen, presLeft, Generators.toComp_toAlgHom]
    rfl

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

Goal state before:
pp: K : Type u_1
L : Type u_2
ι : Type u_3
inst✝² : Field L
inst✝¹ : Field K
inst✝ : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
⊢ FormallySmooth K ↥(IntermediateField.adjoin K (Set.range v))

Tactic:
have : Algebra.FormallySmooth K (adjoin K (Set.range v)) :=
    .of_equiv hb.aevalEquiv
  have : Algebra.FormallySmooth (adjoin K (Set.range v))
      (IntermediateField.adjoin K (Set.range v)) :=
    .of_isLocalization (nonZeroDivisors _)
  exact .comp _ (adjoin K (Set.range v)) _

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ Smooth f ↔
    ∀ (x : ↥X),
      ∃ U,
        ∃ (_ : IsAffineOpen U),
          ∃ V,
            ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth

Tactic:
rw [HasRingHomProperty.iff_exists_appLE_locally (P := @Smooth)]

Goal state after:
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ (∀ (x : ↥X),
      ∃ U V,
        ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).IsStandardSmooth) ↔
    ∀ (x : ↥X),
      ∃ U,
        ∃ (_ : IsAffineOpen U),
          ∃ V,
            ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth

case hQ
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth

case hQi
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↥X
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral

Tactic:
rw [← IsIntegralHom.SpecMap_iff, IsIntegralHom.iff_universallyClosed_and_isAffineHom]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↥X
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ UniversallyClosed (Spec.map (Scheme.Hom.appTop f)) ∧ IsAffineHom (Spec.map (Scheme.Hom.appTop f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ closure ↑(smoothLocus f)

Tactic:
have := this (U.ι ≫ f) (isCompact_iff_compactSpace.mp hU.isCompact) ⟨x, hxU⟩

Goal state after:
case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this✝ :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this : ⟨x, hxU⟩ ∈ closure ↑(smoothLocus (U.ι ≫ f))
⊢ x ∈ closure ↑(smoothLocus f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
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 Q : Fin 3 → A
⊢ (W'⁄B).addY (⇑↑f ∘ P) (⇑↑f ∘ Q) = ↑f ((W'⁄A).addY P Q)

Tactic:
← map_addY,

Goal state after:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Projective R
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 Q : Fin 3 → A
⊢ (W'⁄B).addY (⇑↑f ∘ P) (⇑↑f ∘ Q) = ((W'⁄A).map ↑f).addY (⇑↑f ∘ P) (⇑↑f ∘ Q)
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
inst✝² : CompactSpace ↥X
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.ContainsIdentities
⊢ ∃ Y p, Surjective p ∧ P p ∧ IsAffine Y

Tactic:
let 𝒰 := X.affineCover.finiteSubcover
  let p : ∐ (fun i : 𝒰.I₀ ↦ 𝒰.X i) ⟶ X := Sigma.desc (fun i ↦ 𝒰.f i)
  refine ⟨_, p, ⟨fun x ↦ ?_⟩, ?_, inferInstance⟩
  · obtain ⟨i, x, rfl⟩ := X.affineCover.finiteSubcover.exists_eq x
    use Sigma.ι X.affineCover.finiteSubcover.X i x
    rw [← Scheme.Hom.comp_apply, Sigma.ι_desc]
  · rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (sigmaOpenCover _)]
    exact fun i ↦ by simpa [p] using IsZariskiLocalAtSource.of_isOpenImmersion _

Goal state after: