mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Module.Flat R S
inst✝¹⁰ : CommRing P
inst✝⁹ : Algebra R P
inst✝⁸ : Algebra P S
inst✝⁷ : IsScalarTower R P S
inst✝⁶ : IsLocalRing R
inst✝⁵ : IsLocalRing S
inst✝⁴ : IsLocalHom (algebraMap R S)
inst✝³ : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst✝³ : Algebra Pp Sp := φ.toAlgebra
algInst✝² : Algebra P Sp := (φ.comp (algebraMap P Pp)).toAlgebra
algInst✝¹ : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst✝ : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst✝¹ : IsScalarTower P Pp Sp := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P Sp))
scalarTowerInst✝ : IsScalarTower Pp Sp 𝓀[S] := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Pp 𝓀[S]))
this✝¹ : IsScalarTower 𝓀[R] Pp Sp
this✝ : IsScalarTower R Sp 𝓀[S]
this : IsScalarTower P S Sp
r : S
⊢ (algebraMap S 𝓀[S]) r = (algebraMap Sp 𝓀[S]) ((algebraMap S Sp) r)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Pointwise

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
c : R
hc : c ∈ I
⊢ c • x ≡ c • y [SMOD I • U]

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Module.Flat R S
inst✝¹⁰ : CommRing P
inst✝⁹ : Algebra R P
inst✝⁸ : Algebra P S
inst✝⁷ : IsScalarTower R P S
inst✝⁶ : IsLocalRing R
inst✝⁵ : IsLocalRing S
inst✝⁴ : IsLocalHom (algebraMap R S)
inst✝³ : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst✝³ : Algebra Pp Sp := φ.toAlgebra
algInst✝² : Algebra P Sp := (φ.comp (algebraMap P Pp)).toAlgebra
algInst✝¹ : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst✝ : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst✝¹ : IsScalarTower P Pp Sp := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P Sp))
scalarTowerInst✝ : IsScalarTower Pp Sp 𝓀[S] := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Pp 𝓀[S]))
this✝⁶ : IsScalarTower 𝓀[R] Pp Sp
this✝⁵ : IsScalarTower R Sp 𝓀[S]
this✝⁴ : IsScalarTower P S Sp
this✝³ : IsScalarTower S Sp 𝓀[S]
this✝² : IsScalarTower P Sp 𝓀[S]
this✝¹ : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp).symm
this✝ : Module.Free Pp Ω[Pp⁄𝓀[R]]
this : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (algebraMap P S)) := kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
h₁' : Function.Surjective ⇑φ
⊢ (RingHom.ker φ).FG

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
a b : B
⊢ (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (a * b) =
    a • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b + b • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Module.Flat R S
inst✝¹⁰ : CommRing P
inst✝⁹ : Algebra R P
inst✝⁸ : Algebra P S
inst✝⁷ : IsScalarTower R P S
inst✝⁶ : IsLocalRing R
inst✝⁵ : IsLocalRing S
inst✝⁴ : IsLocalHom (algebraMap R S)
inst✝³ : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst✝³ : Algebra Pp Sp := φ.toAlgebra
algInst✝² : Algebra P Sp := (φ.comp (algebraMap P Pp)).toAlgebra
algInst✝¹ : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst✝ : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst✝¹ : IsScalarTower P Pp Sp := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P Sp))
scalarTowerInst✝ : IsScalarTower Pp Sp 𝓀[S] := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Pp 𝓀[S]))
this✝⁶ : IsScalarTower 𝓀[R] Pp Sp
this✝⁵ : IsScalarTower R Sp 𝓀[S]
this✝⁴ : IsScalarTower P S Sp
this✝³ : IsScalarTower S Sp 𝓀[S]
this✝² : IsScalarTower P Sp 𝓀[S]
this✝¹ : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp).symm
this✝ : Module.Free Pp Ω[Pp⁄𝓀[R]]
this : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (algebraMap P S)) := kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
h₁' : Function.Surjective ⇑φ
h₂' : (RingHom.ker φ).FG
x : Sp
hx : x ∈ 𝓂[Sp]
⊢ Function.Surjective ⇑(algebraMap R 𝓀[R])

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : Module.Flat R S
inst✝¹⁰ : CommRing P
inst✝⁹ : Algebra R P
inst✝⁸ : Algebra P S
inst✝⁷ : IsScalarTower R P S
inst✝⁶ : IsLocalRing R
inst✝⁵ : IsLocalRing S
inst✝⁴ : IsLocalHom (algebraMap R S)
inst✝³ : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst✝³ : Algebra Pp Sp := φ.toAlgebra
algInst✝² : Algebra P Sp := (φ.comp (algebraMap P Pp)).toAlgebra
algInst✝¹ : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst✝ : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst✝¹ : IsScalarTower P Pp Sp := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P Sp))
scalarTowerInst✝ : IsScalarTower Pp Sp 𝓀[S] := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Pp 𝓀[S]))
this✝⁶ : IsScalarTower 𝓀[R] Pp Sp
this✝⁵ : IsScalarTower R Sp 𝓀[S]
this✝⁴ : IsScalarTower P S Sp
this✝³ : IsScalarTower S Sp 𝓀[S]
this✝² : IsScalarTower P Sp 𝓀[S]
this✝¹ : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp).symm
this✝ : Module.Free Pp Ω[Pp⁄𝓀[R]]
this : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (algebraMap P S)) := kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
h₁' : Function.Surjective ⇑φ
h₂' : (RingHom.ker φ).FG
⊢ 𝓂[Sp] ≤ RingHom.ker ψ

Tactic:
by

Goal state after:
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
inst✝ : Algebra.IsPushout R S A B
⊢ ↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B)) =
    LinearMap.id

Tactic:
by

Goal state after:
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
⊢ W'.dblX (u • P) = u ^ 4 * W'.dblX P

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
x : Ω[B⁄S]
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))).toFun ((derivationTensorProduct R S A B).liftKaehlerDifferential x) =
    x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
⊢ IsBaseChange S (↑R (map R S A B))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this✝ : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[R] S :=
  AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B).symm) (LinearEquiv.refl A Ω[A⁄R]) ≪≫ₗ
      TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
y : Ω[A⁄R]
x : A
z : S
this : b • z • a • x • (map R S A B) y = ((algebraMap A B) a * (algebraMap S B) b) • z • x • (map R S A B) y
⊢ e₂ ((Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • (Algebra.IsPushout.equiv R A S B) (x ⊗ₜ[R] z) ⊗ₜ[A] y) =
    (Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • e₂ ((Algebra.IsPushout.equiv R A S B) (x ⊗ₜ[R] z) ⊗ₜ[A] y)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
⊢ B ⊗[A] Ω[A⁄R] ≃ₗ[B] Ω[B⁄S]

Tactic:
by

Goal state after:
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
inst✝ : Algebra.IsPushout R S A B
b : B
a : A
⊢ (tensorKaehlerEquiv R S A B) (b ⊗ₜ[A] (D R A) a) = b • (D S B) ((algebraMap A B) a)

Tactic:
by

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

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

Tactic:
by

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
⊢ (tensorKaehlerEquiv R S A (S ⊗[R] A)).symm ((D S (S ⊗[R] A)) (s ⊗ₜ[R] a)) =
    (algebraMap S (S ⊗[R] A)) s ⊗ₜ[A] (D R A) a

Tactic:
by

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
⊢ (tensorKaehlerEquiv R S A (A ⊗[R] S)).symm ((D S (A ⊗[R] S)) (a ⊗ₜ[R] s)) =
    (algebraMap S (A ⊗[R] S)) s ⊗ₜ[A] (D R A) a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
x : ↥M'
⊢ IsUnit (((IsScalarTower.toAlgHom R P S).comp f₀) ↑x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
⊢ Function.Surjective ⇑fP

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
hf₁ : Function.Surjective ⇑fP
this : (RingHom.ker f₀.toRingHom).FG
x : MvPolynomial (Fin n) R
hx : x ∈ RingHom.ker f₀.toRingHom
⊢ x ∈ Ideal.comap (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker fP)

Tactic:
by

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 : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblX P = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
hf₁ : Function.Surjective ⇑fP
this : (RingHom.ker f₀.toRingHom).FG
x : MvPolynomial (Fin n) R
s : ↥M'
hx : IsLocalization.mk' P' x s ∈ RingHom.ker fP
⊢ ∃ a ∈ M, a * f₀ x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
hf₁ : Function.Surjective ⇑fP
this : (RingHom.ker f₀.toRingHom).FG
x : MvPolynomial (Fin n) R
s : ↥M'
hx : IsLocalization.mk' P' x s ∈ RingHom.ker fP
a : MvPolynomial (Fin n) R
ha : f₀ a ∈ M
e : f₀ a * f₀ x = 0
⊢ a * x ∈ RingHom.ker f₀.toRingHom

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
hf₁ : Function.Surjective ⇑fP
⊢ (RingHom.ker fP).FG

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
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'.dblX P = 0

Tactic:
by

Goal state after:
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
n d : F
hd : d ≠ 0
⊢ W.toAffine.addX (P x / P z) (P x / P z) (-n / P z / d) =
    (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d / P z / (P z * d ^ 3)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
⊢ FormallySmooth R S

Tactic:
by

Goal state after:
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
x : R
hx : x ∈ ↑p.primeCompl
⊢ (algebraMap R S) x ∈ q.primeCompl

Tactic:
by

Goal state after:
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
⊢ ∀ (y : ↥(algebraMapSubmonoid S p.primeCompl)), IsUnit ((ofId S Sq) ↑y)

Tactic:
by

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.dblX 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))

Tactic:
by

Goal state after:
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
⊢ algebraMap Rp Sq = (algebraMap Sp Sq).comp (algebraMap Rp Sp)

Tactic:
by

Goal state after:
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
⊢ algebraMapSubmonoid S p.primeCompl ≤ q.primeCompl

Tactic:
by

Goal state after: