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✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦P⟧

Tactic:
by_cases hPz : P z = 0

Goal state after:
case pos
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.addMap ⟦P⟧ ⟦Q⟧ = ⟦P⟧

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.addMap ⟦P⟧ ⟦Q⟧ = ⟦P⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P

Tactic:
by_cases hPz : P z = 0

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (u • P) = toAffine W P

case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (u • P) = toAffine W P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P

Tactic:
· rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]

Goal state after:
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.Nonsingular P ↔ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)

Tactic:
nonsingular_of_Z_ne_zero hPz,

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
by_cases hPz : P z = 0

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

Tactic:
by_cases hPz : P z = 0

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

case neg
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
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q
Module: Mathlib.Topology.Category.TopCat.ULift

Goal state before:
pp: J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
⊢ (uliftFunctor.mapCone c).pt.str =
    ⨅ j,
      TopologicalSpace.induced (⇑(ConcreteCategory.hom ((uliftFunctor.mapCone c).π.app j)))
        ((K ⋙ uliftFunctor).obj j).str

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
⊢ (uliftFunctor.mapCone c).pt.str ≤
    ⨅ j,
      TopologicalSpace.induced (⇑(ConcreteCategory.hom ((uliftFunctor.mapCone c).π.app j)))
        ((K ⋙ uliftFunctor).obj j).str

case refine_2
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
⊢ ⨅ j,
      TopologicalSpace.induced (⇑(ConcreteCategory.hom ((uliftFunctor.mapCone c).π.app j)))
        ((K ⋙ uliftFunctor).obj j).str ≤
    (uliftFunctor.mapCone c).pt.str
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
inst✝ : DecidableEq F
⊢ Function.LeftInverse fromAffine toAffineLift

Tactic:
rintro @⟨⟨P⟩, hP⟩

Goal state after:
case mk
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
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
⊢ fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case mk
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
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
⊢ fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }

Tactic:
by_cases hPz : P z = 0

Goal state after:
case pos
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
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }

case neg
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
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: ⊢ OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
intro R S _ _ f s hs H

Goal state after:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ f.FormallyUnramified
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case intro.mpr
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
⊢ f₁ g = f₂ g

Tactic:
← Finset.univ_sum_single g,

Goal state after:
case intro.mpr
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
⊢ f₁ (∑ i, Pi.single i (g i)) = f₂ (∑ i, Pi.single i (g i))
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) ∈ Submodule.comap f (I ^ n • f.range)

Tactic:
apply (smul_mono_right _ inf_le_right : I ^ n • (I ^ k • ⊤ ⊓ (range f)) ≤ _)

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
⊢ f (↑a (n + k)) ∈ I ^ n • (I ^ k • ⊤ ⊓ f.range)
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
⊢ f (y - yₙ) ∈ I ^ (k + n - k) • (I ^ k • ⊤ ⊓ f.range)

Tactic:
← hkn (k + n) (by lia)

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
⊢ f (y - yₙ) ∈ I ^ (k + n) • ⊤ ⊓ f.range
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝³ : Finite ι
inst✝² : Finite ι'
inst✝¹ : Finite σ
inst✝ : Finite σ'
this : Nat.card σ ≤ Nat.card ι
⊢ Nat.card (ι' ⊕ ι) - Nat.card (σ' ⊕ σ) = Nat.card ι' - Nat.card σ' + (Nat.card ι - Nat.card σ)

Tactic:
have : Nat.card σ' ≤ Nat.card ι' :=
    card_relations_le_card_vars_of_isFinite Q

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✝³ : Finite ι
inst✝² : Finite ι'
inst✝¹ : Finite σ
inst✝ : Finite σ'
this✝ : Nat.card σ ≤ Nat.card ι
this : Nat.card σ' ≤ Nat.card ι'
⊢ Nat.card (ι' ⊕ ι) - Nat.card (σ' ⊕ σ) = Nat.card ι' - Nat.card σ' + (Nat.card ι - Nat.card σ)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
⊢ W.negDblY P =
    (-(eval P) W.polynomialX *
          ((eval P) W.polynomialX ^ 2 - W.a₁ * (eval P) W.polynomialX * P z * (P y - W.negY P) -
                W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
              2 * P x * P z * (P y - W.negY P) ^ 2 -
            P x * P z * (P y - W.negY P) ^ 2) +
        P y * P z ^ 2 * (P y - W.negY P) ^ 3) /
      P z ^ 2

Tactic:
← negDblY_eq' hP,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
⊢ W.negDblY P = W.negDblY P * P z ^ 2 / P z ^ 2
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case intro.intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ'
val✝ : Fintype σ
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₁₁.det *
      (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det =
    P.jacobian • Q.jacobian

Tactic:
· rw [jacobiMatrix_comp_₁₁_det, jacobiMatrix_comp_₂₂_det, mul_comm, Algebra.smul_def]

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 : σ
⊢ P.basisCotangent r = Cotangent.mk ⟨P.relation r, ⋯⟩

Tactic:
by
  symm
  apply P.cotangentEquiv.injective
  ext
  simp_rw [basisCotangent, Basis.map_apply, LinearEquiv.apply_symm_apply, basisDeriv_apply]
  apply P.toPreSubmersivePresentation.cotangentComplexAux_apply _ _

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
⊢ x ∈ P.toExtension.toKaehler.ker ⊓ Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)) → x = 0

Tactic:
⟨hx, hxs⟩

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 : x ∈ ↑(Submodule.span S (Set.range fun x ↦ P.cotangentSpaceBasis (v x)))
⊢ x = 0
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
κ : Type u_5
P : Generators R S ι
u : σ → ι
hu : Function.Injective u
v : κ → ι
huv : IsCompl (Set.range v) (Set.range u)
b : Module.Basis κ S Ω[S⁄R]
hb : ∀ (k : κ), b k = (D R S) (P.val (v k))
inst✝ : Subsingleton (H1Cotangent R S)
⊢ Function.Bijective ⇑(P.cotangentRestrict hu)

Tactic:
refine P.cotangentRestrict_bijective_of_isCompl _ huv ?_ ?_
  · simp_rw [← hb]
    exact b.span_eq
  · apply disjoint_ker_toKaehler_of_linearIndependent
    simp_rw [← hb]
    exact b.linearIndependent

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
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * P x ^ 2 * Q x * 0 + 3 * P x * Q x ^ 2 * P z + P y ^ 2 * 0 ^ 2 - Q y ^ 2 * P z ^ 2 + W'.a₁ * P x * P y * 0 ^ 2 -
                  W'.a₁ * Q x * Q y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * 0 ^ 2 +
              W'.a₂ * Q x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * 0 ^ 2 -
          W'.a₃ * Q y * P z ^ 2 * 0 -
        W'.a₄ * P x * P z * 0 ^ 2 +
      W'.a₄ * Q x * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P z

Tactic:
X_eq_zero_of_Z_eq_zero hQ hQz

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * P x ^ 2 * 0 * 0 + 3 * P x * 0 ^ 2 * P z + P y ^ 2 * 0 ^ 2 - Q y ^ 2 * P z ^ 2 + W'.a₁ * P x * P y * 0 ^ 2 -
                  W'.a₁ * 0 * Q y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * 0 ^ 2 +
              W'.a₂ * 0 ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * 0 ^ 2 -
          W'.a₃ * Q y * P z ^ 2 * 0 -
        W'.a₄ * P x * P z * 0 ^ 2 +
      W'.a₄ * 0 * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P z
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
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -P x * Q y ^ 2 * P z + Q x * P y ^ 2 * 0 - 2 * P x * P y * Q y * 0 + 2 * Q x * P y * Q y * P z -
                            W'.a₁ * P x ^ 2 * Q y * 0 +
                          W'.a₁ * Q x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * Q x * 0 -
                      W'.a₂ * P x * Q x ^ 2 * P z -
                    W'.a₃ * P x * P y * 0 ^ 2 +
                  W'.a₃ * Q x * Q y * P z ^ 2 -
                2 * W'.a₃ * P x * Q y * P z * 0 +
              2 * W'.a₃ * Q x * P y * P z * 0 +
            W'.a₄ * P x ^ 2 * 0 ^ 2 -
          W'.a₄ * Q x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * 0 ^ 2 -
      3 * W'.a₆ * Q x * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P x

Tactic:
X_eq_zero_of_Z_eq_zero hQ hQz

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -P x * Q y ^ 2 * P z + 0 * P y ^ 2 * 0 - 2 * P x * P y * Q y * 0 + 2 * 0 * P y * Q y * P z -
                            W'.a₁ * P x ^ 2 * Q y * 0 +
                          W'.a₁ * 0 ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * 0 * 0 -
                      W'.a₂ * P x * 0 ^ 2 * P z -
                    W'.a₃ * P x * P y * 0 ^ 2 +
                  W'.a₃ * 0 * Q y * P z ^ 2 -
                2 * W'.a₃ * P x * Q y * P z * 0 +
              2 * W'.a₃ * 0 * P y * P z * 0 +
            W'.a₄ * P x ^ 2 * 0 ^ 2 -
          W'.a₄ * 0 ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * 0 ^ 2 -
      3 * W'.a₆ * 0 * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P x
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Subsingleton S
⊢ ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
let P' : Presentation R S (Unit ⊕ α) (Unit ⊕ σ) :=
      { toGenerators := .ofSurjective (fun i : Unit ⊕ α ↦ 0) (Function.surjective_to_subsingleton _)
        relation _ := 1
        span_range_relation_eq_ker := by simpa using (RingHom.ker_eq_top_of_subsingleton _).symm }
    have : Subsingleton P'.toExtension.Cotangent := Module.subsingleton S _
    exact ⟨P', default, by subsingleton, by subsingleton⟩

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

Goal state before:
pp: 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

Tactic:
exact isStandardSmooth_stableUnderCompositionWithLocalizationAway.left

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

Goal state before:
pp: n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
hf : SmoothOfRelativeDimension n f
hg : SmoothOfRelativeDimension m g
x : ↥X
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V,
        ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (f ≫ g) ⁻¹ᵁ U),
          IsStandardSmoothOfRelativeDimension (n + m) (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) U V e))

Tactic:
obtain ⟨U₂, hU₂, V₂, hV₂, hfx₂, e₂, hf₂⟩ := hg.exists_isStandardSmoothOfRelativeDimension (f x)

Goal state after:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
hf : SmoothOfRelativeDimension n f
hg : SmoothOfRelativeDimension m g
x : ↥X
U₂ : Z.Opens
hU₂ : IsAffineOpen U₂
V₂ : Y.Opens
hV₂ : IsAffineOpen V₂
hfx₂ : f x ∈ V₂
e₂ : V₂ ≤ g ⁻¹ᵁ U₂
hf₂ : IsStandardSmoothOfRelativeDimension m (CommRingCat.Hom.hom (Scheme.Hom.appLE g U₂ V₂ e₂))
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V,
        ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (f ≫ g) ⁻¹ᵁ U),
          IsStandardSmoothOfRelativeDimension (n + m) (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) U V e))
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : (aeval a) q₁ = 0
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
⊢ IsUnit q₁ ∨ IsUnit q₂

Tactic:
have := HF q₁ ne.1 h₁

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : (aeval a) q₁ = 0
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : F.totalDegree ≤ q₁.totalDegree
⊢ IsUnit q₁ ∨ IsUnit q₂
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : (aeval a) q₁ = 0
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : q₁.totalDegree + q₂.totalDegree ≤ q₁.totalDegree
⊢ IsUnit q₁ ∨ IsUnit q₂

Tactic:
add_le_iff_nonpos_right,

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : (aeval a) q₁ = 0
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : q₂.totalDegree ≤ 0
⊢ IsUnit q₁ ∨ IsUnit q₂