mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
⊢ IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃ IsLimit (E.toPreOneHypercover.multifork F)

Tactic:
have hc' : IsColimit c' := by
    refine (c'.isColimitEquivOfEquiv equiv.symm).symm (Nonempty.some ?_)
    exact IsUniversalColimit.nonempty_isColimit_prod_of_isPullback
      huniv huniv E.f E.f ((E.sigmaOfIsColimit hc).f ⟨⟩) ((E.sigmaOfIsColimit hc).f ⟨⟩)
      (fun i j ↦ .of_hasPullback _ _) (.of_hasPullback _ _) (.refl _) (by simp) (by simp)
      (by simp [c', equiv, Equiv.sigmaPUnit]) (by simp [c', equiv, Equiv.sigmaPUnit])

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
inst✝⁵ : Category.{v_2, u_2} A
S : C
E : PreZeroHypercover S
inst✝⁴ : E.HasPullbacks
c : Cofan E.X
hc : IsColimit c
huniv : IsUniversalColimit c
inst✝³ : (E.sigmaOfIsColimit hc).HasPullbacks
inst✝² : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F
c' : Cofan E.toPreOneHypercover.Y' :=
  Cofan.mk ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y PUnit.unit) fun b ↦
    pullback.map (E.f b.fst.1) (E.f b.fst.2) ((E.sigmaOfIsColimit hc).f PUnit.unit)
      ((E.sigmaOfIsColimit hc).f PUnit.unit) (c.inj b.fst.1) (c.inj b.fst.2) (𝟙 S) ⋯ ⋯
equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ := Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
hc' : IsColimit c'
⊢ IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃ IsLimit (E.toPreOneHypercover.multifork F)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case neg.refine_1
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ P x * Q z = Q x * P z

Tactic:
apply f.injective

Goal state after:
case neg.refine_1
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P x * Q z) = f (Q x * P z)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case neg.refine_2
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ P y * Q z = Q y * P z

Tactic:
apply f.injective

Goal state after:
case neg.refine_2
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ f (P y * Q z) = f (Q y * P z)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : W.Point
⊢ (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift

Tactic:
by
  rcases P, Q with ⟨@⟨⟨_⟩, hP⟩, @⟨⟨_⟩, hQ⟩⟩
  exact toAffine_add hP hQ

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

Goal state before:
pp: case pos
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
rw [add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h, add_of_equiv h, map_dblXYZ]

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

Goal state before:
pp: ⊢ ∀ ⦃R S T : Type u_3⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], (algebraMap R T).FormallySmooth → (algebraMap S (S ⊗[R] T)).FormallySmooth

Tactic:
introv H

Goal state after:
R S T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
H : (algebraMap R T).FormallySmooth
⊢ (algebraMap S (S ⊗[R] T)).FormallySmooth
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: ⊢ ∀ ⦃R S T : Type u_3⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    (algebraMap R T).FormallyUnramified → (algebraMap S (TensorProduct R S T)).FormallyUnramified

Tactic:
introv H

Goal state after:
R S T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
H : (algebraMap R T).FormallyUnramified
⊢ (algebraMap S (TensorProduct R S T)).FormallyUnramified
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
⊢ (W.a₁ * P y * 0 - (3 * P x ^ 2 + 2 * W.a₂ * P x * 0 + W.a₄ * 0)) ^ 3 / 0 = 0

Tactic:
div_zero

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z = 0
⊢ 0 = 0
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 : Extension R S
inst✝² : FormallySmooth R P.Ring
inst✝¹ : Module.Free P.Ring Ω[P.Ring⁄R]
inst✝ : Module.Finite P.Ring Ω[P.Ring⁄R]
h' : P.ker.FG
this✝ : Module.Finite P.Ring P.Cotangent
this : Module.Finite S P.Cotangent
⊢ FormallySmooth R S ↔ Function.Injective ⇑(LinearMap.lTensor (ResidueField S) P.cotangentComplex)

Tactic:
rw [← IsLocalRing.split_injective_iff_lTensor_residueField_injective,
    P.formallySmooth_iff_split_injection]

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

Goal state before:
pp: case zero
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
⊢ (r + s) • 0 = r • 0 + s • 0

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
r s : A
x✝ : S
y✝ : Ω[A⁄R]
⊢ (r + s) • x✝ ⊗ₜ[R] y✝ = r • x✝ ⊗ₜ[R] y✝ + s • x✝ ⊗ₜ[R] y✝

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
r s : A
x✝ y✝ : S ⊗[R] Ω[A⁄R]
a✝¹ : (r + s) • x✝ = r • x✝ + s • x✝
a✝ : (r + s) • y✝ = r • y✝ + s • y✝
⊢ (r + s) • (x✝ + y✝) = r • (x✝ + y✝) + s • (x✝ + y✝)

Tactic:
<;>

Goal state after:
case zero
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
⊢ (r + s) • 0 = r • 0 + s • 0

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
r s : A
x✝ : S
y✝ : Ω[A⁄R]
⊢ (r + s) • x✝ ⊗ₜ[R] y✝ = r • x✝ ⊗ₜ[R] y✝ + s • x✝ ⊗ₜ[R] y✝

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
r s : A
x✝ y✝ : S ⊗[R] Ω[A⁄R]
a✝¹ : (r + s) • x✝ = r • x✝ + s • x✝
a✝ : (r + s) • y✝ = r • y✝ + s • y✝
⊢ (r + s) • (x✝ + y✝) = r • (x✝ + y✝) + s • (x✝ + y✝)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case zero
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
⊢ 0 • 0 = 0

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
x✝ : S
y✝ : Ω[A⁄R]
⊢ 0 • x✝ ⊗ₜ[R] y✝ = 0

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
x✝ y✝ : S ⊗[R] Ω[A⁄R]
a✝¹ : 0 • x✝ = 0
a✝ : 0 • y✝ = 0
⊢ 0 • (x✝ + y✝) = 0

Tactic:
<;>

Goal state after:
case zero
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
⊢ 0 • 0 = 0

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
x✝ : S
y✝ : Ω[A⁄R]
⊢ 0 • x✝ ⊗ₜ[R] y✝ = 0

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
x✝ y✝ : S ⊗[R] Ω[A⁄R]
a✝¹ : 0 • x✝ = 0
a✝ : 0 • y✝ = 0
⊢ 0 • (x✝ + y✝) = 0
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
h : Algebra.IsPushout R S A B
x y : B ⊗[S] B
e₁ :
  (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
e₂ :
  (LinearMap.liftBaseChange S (↑R (map R S A B)))
      ((derivationTensorProduct R S A B).liftKaehlerDifferential ((D S B).tensorProductTo y)) =
    (D S B).tensorProductTo y
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B)))
      ((derivationTensorProduct R S A B).liftKaehlerDifferential ((D S B).tensorProductTo (x + y))) =
    (D S B).tensorProductTo (x + y)

Tactic:
| add x y e₁ e₂ =>

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (A ⊗[R] S)) (a ⊗ₜ[R] s) = (algebraMap S (A ⊗[R] S)) s • (D S (A ⊗[R] S)) (a ⊗ₜ[R] 1)

Tactic:
rw [algebraMap_smul, ← Derivation.map_smul, Algebra.smul_def,
    Algebra.TensorProduct.right_algebraMap_apply]

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : S
a : A
⊢ (D S (A ⊗[R] S)) (a ⊗ₜ[R] s) = (D S (A ⊗[R] S)) (1 ⊗ₜ[R] s * a ⊗ₜ[R] 1)
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : AdicCompletion I R
x : AdicCompletion I M
⊢ (r + s) • x = r • x + s • x

Tactic:
ext n; simp [add_smul]

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

Goal state before:
pp: case isTrue
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
h✝ : j = i
⊢ 1 = ↑1 k

pp: case isFalse
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
h✝ : ¬j = i
⊢ 0 = ↑0 k

Tactic:
<;>

Goal state after:
case isTrue
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
h✝ : j = i
⊢ 1 = ↑1 k

case isFalse
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
h✝ : ¬j = i
⊢ 0 = ↑0 k
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (algebraMap (localizationAway S r).Ring S) (Matrix.diagonal fun x ↦ C r).det = (algebraMap R S) r

Tactic:
simp [show Fintype.card (localizationAway r (S := S)).rels = 1 from rfl]

Goal state after:
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
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial S
inst✝ : IsStandardSmooth R S
n : ℕ
h : Module.rank S Ω[S⁄R] = ↑n
w✝² w✝¹ : Type
w✝ : Finite w✝¹
left✝ : Finite w✝²
P : SubmersivePresentation R S w✝² w✝¹
⊢ ↑P.dimension = ↑n

Tactic:
rwa [← P.rank_kaehlerDifferential]

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq 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
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.dblXYZ P =
    W.dblZ P •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]

Tactic:
have hZ : IsUnit <| W.dblZ P := isUnit_dblZ_of_Y_ne' hP hQ hPz hQz hx hy
  erw [dblXYZ, smul_fin3, ← dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel,
    ← dblY_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel, mul_one]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z = 0
⊢ -(P y * Q z - Q y * 0) ^ 3 / 0 = 0

Tactic:
div_zero

Goal state after:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z = 0
⊢ 0 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ -(P y * 0 - Q y * P z) ^ 3 / 0 = 0

Tactic:
div_zero

Goal state after:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a.a
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 ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
      Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

pp: case a
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 ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
      Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
<;>

Goal state after:
case a.a
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 ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
      Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

case a
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 ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} *
      Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: ⊢ RespectsIso @IsStandardSmooth

Tactic:
by
  apply isStandardSmooth_stableUnderComposition.respectsIso
  introv
  exact (IsStandardSmoothOfRelativeDimension.equiv e).isStandardSmooth

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

Goal state before:
pp: n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsStandardSmoothOfRelativeDimension n (algebraMap R T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T

Tactic:
RingHom.IsStandardSmoothOfRelativeDimension

Goal state after:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ IsStandardSmoothOfRelativeDimension n (algebraMap S (S ⊗[R] T))

Tactic:
RingHom.IsStandardSmoothOfRelativeDimension

Goal state after:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
Module: Mathlib.RingTheory.Smooth.Field

Goal state before:
pp: case e'_1
K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
x✝ : L
⊢ Set.range Subtype.val = ↑s

pp: case e'_3.e'_2
K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
e_1✝ : ↥(IntermediateField.adjoin K (Set.range Subtype.val)) = ↥(IntermediateField.adjoin K ↑s)
⊢ Set.range Subtype.val = ↑s

pp: case e'_5
K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
e_1✝ : ↥(IntermediateField.adjoin K (Set.range Subtype.val)) = ↥(IntermediateField.adjoin K ↑s)
e_3✝ :
  (IntermediateField.adjoin K (Set.range Subtype.val)).toField.toCommRing ≍
    (IntermediateField.adjoin K ↑s).toField.toCommRing
⊢ Set.range Subtype.val = ↑s

Tactic:
<;>

Goal state after:
case e'_1
K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
x✝ : L
⊢ Set.range Subtype.val = ↑s

case e'_3.e'_2
K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
e_1✝ : ↥(IntermediateField.adjoin K (Set.range Subtype.val)) = ↥(IntermediateField.adjoin K ↑s)
⊢ Set.range Subtype.val = ↑s

case e'_5
K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
e_1✝ : ↥(IntermediateField.adjoin K (Set.range Subtype.val)) = ↥(IntermediateField.adjoin K ↑s)
e_3✝ :
  (IntermediateField.adjoin K (Set.range Subtype.val)).toField.toCommRing ≍
    (IntermediateField.adjoin K ↑s).toField.toCommRing
⊢ Set.range Subtype.val = ↑s