mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: S : Type u_5
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ (Ideal.Quotient.mk (I ^ n • ⊤)) ((ofAlgEquiv I).symm x) = (eval I S n) ((of I S) ((ofAlgEquiv I).symm x))

Tactic:
]

Goal state after:
S : Type u_5
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ (Ideal.Quotient.mk (I ^ n • ⊤)) ((ofAlgEquiv I).symm x) = (eval I S n) ((of I S) ((ofAlgEquiv I).symm x))
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: S : Type u_5
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ (Ideal.Quotient.mk (I ^ n)) ((ofAlgEquiv I).symm x) =
    ↑(Ideal.quotientEquivAlgOfEq S ⋯) ((Ideal.Quotient.mk (I ^ n • ⊤)) ((ofAlgEquiv I).symm x))

Tactic:
]

Goal state after:
S : Type u_5
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
n : ℕ
x : AdicCompletion I S
⊢ (Ideal.Quotient.mk (I ^ n)) ((ofAlgEquiv I).symm x) =
    ↑(Ideal.quotientEquivAlgOfEq S ⋯) ((Ideal.Quotient.mk (I ^ n • ⊤)) ((ofAlgEquiv I).symm x))
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
x : M
h : (of I M) x = (ofTensorProductEquivOfFiniteNoetherian I M) (1 ⊗ₜ[R] x)
⊢ 1 ⊗ₜ[R] x = 1 ⊗ₜ[R] x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m : ℕ
T : Type u_3 := S ⧸ I ^ (m + 1 + 1)
J : Ideal T := Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))
q : A →ₐ[R] T ⧸ J := (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯).symm).comp (liftAdicCompletionAux (m + 1))
⊢ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ ((m + 1) * (m + 1 + 1))) = ⊥

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m : ℕ
T : Type u_3 := S ⧸ I ^ (m + 1 + 1)
J : Ideal T := Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))
q : A →ₐ[R] T ⧸ J := (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯).symm).comp (liftAdicCompletionAux (m + 1))
⊢ Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ ((m + 1) * (m + 1 + 1))) = ⊥
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
⊢ AlgebraTensorModule.map LinearMap.id f =
    ↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f

Tactic:
]

Goal state after:
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
⊢ AlgebraTensorModule.map LinearMap.id f =
    ↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f
Module: Mathlib.RingTheory.Smooth.AdicCompletion

Goal state before:
pp: case succ
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m : ℕ
⊢ ((↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯)).comp
          (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1))))).comp
      (lift (Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))) ⋯
        ((↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯).symm).comp (liftAdicCompletionAux I f (m + 1)))) =
    liftAdicCompletionAux I f (m + 1)

Tactic:
]

Goal state after:
case succ
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m : ℕ
⊢ ((↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯)).comp
          (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1).succ)) (I ^ (m + 1))))).comp
      (lift (Ideal.map (Ideal.Quotient.mkₐ R (I ^ (m + 1 + 1))) (I ^ (m + 1))) ⋯
        ((↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R ⋯).symm).comp (liftAdicCompletionAux I f (m + 1)))) =
    liftAdicCompletionAux I f (m + 1)
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hf : Function.Injective ⇑f
⊢ Function.Injective
    ⇑(↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ map I f ∘ₗ ↑(ofTensorProductEquivOfFiniteNoetherian I M))

Tactic:
]

Goal state after:
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hf : Function.Injective ⇑f
⊢ Function.Injective
    ⇑(↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ map I f ∘ₗ ↑(ofTensorProductEquivOfFiniteNoetherian 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
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Finite σ
inst✝ : DecidableEq σ
i j : σ
⊢ (aeval P.val) ((pderiv (P.map j)) (P.relation i)) = (aeval P.val) ((pderiv (P.map j)) (P.relation i))

Tactic:
]

Goal state after:
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
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
i j : σ
⊢ (LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ)) P.aevalDifferential i j =
    (aeval P.val).mapMatrix P.jacobiMatrix i j

Tactic:
]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
i j : σ
⊢ (LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ)) P.aevalDifferential i j =
    (aeval P.val).mapMatrix P.jacobiMatrix i j
Module: Mathlib.RingTheory.Smooth.AdicCompletion

Goal state before:
pp: case succ
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m n✝ n : ℕ
hmn : m ≤ n
ih : (Ideal.Quotient.factorₐ R ⋯).comp (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m
⊢ (Ideal.Quotient.factorₐ R ⋯).comp ((Ideal.Quotient.factorₐ R ⋯).comp (liftAdicCompletionAux I f (n + 1))) =
    liftAdicCompletionAux I f m

Tactic:
]

Goal state after:
case succ
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Ideal S
f : A →ₐ[R] S ⧸ I
inst✝ : FormallySmooth R A
m n✝ n : ℕ
hmn : m ≤ n
ih : (Ideal.Quotient.factorₐ R ⋯).comp (liftAdicCompletionAux I f n) = liftAdicCompletionAux I f m
⊢ (Ideal.Quotient.factorₐ R ⋯).comp ((Ideal.Quotient.factorₐ R ⋯).comp (liftAdicCompletionAux I f (n + 1))) =
    liftAdicCompletionAux I f 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
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
i j : σ
⊢ ((Pi.basisFun S σ).repr (P.aevalDifferential ((Pi.basisFun S σ) j))) i = (aeval P.val).mapMatrix P.jacobiMatrix i j

Tactic:
]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
i j : σ
⊢ ((Pi.basisFun S σ).repr (P.aevalDifferential ((Pi.basisFun S σ) j))) i = (aeval P.val).mapMatrix P.jacobiMatrix i j
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case refine_2
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
y : AdicCompletion I N
b : AdicCauchySequence I N
hz : (mk I N) b ∈ (map I g).ker
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
hb : ∀ (n : ℕ), g (↑b n) ∈ I ^ n • ⊤
a : (n : ℕ) → ↑{a | f a - ↑b (k + n) ∈ I ^ (k + n) • ⊤} := mapExactAux hf hfg hg hk b hb
n : ℕ
⊢ f ↑(a n) - ↑b (k + n) ∈ I ^ n • ⊤

Tactic:
]

Goal state after:
case refine_2
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
y : AdicCompletion I N
b : AdicCauchySequence I N
hz : (mk I N) b ∈ (map I g).ker
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
hb : ∀ (n : ℕ), g (↑b n) ∈ I ^ n • ⊤
a : (n : ℕ) → ↑{a | f a - ↑b (k + n) ∈ I ^ (k + n) • ⊤} := mapExactAux hf hfg hg hk b hb
n : ℕ
⊢ f ↑(a n) - ↑b (k + n) ∈ I ^ n • ⊤
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
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
⊢ IsUnit P.aevalDifferential ↔ Function.Bijective ⇑P.aevalDifferential

Tactic:
]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
⊢ IsUnit P.aevalDifferential ↔ Function.Bijective ⇑P.aevalDifferential
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
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
hli : LinearIndependent S fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))
hsp : Submodule.span S (Set.range fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) = ⊤
⊢ Function.Bijective ⇑P.aevalDifferential

Tactic:
]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
hli : LinearIndependent S fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))
hsp : Submodule.span S (Set.range fun j i ↦ (aeval P.val) ((pderiv (P.map i)) (P.relation j))) = ⊤
⊢ Function.Bijective ⇑P.aevalDifferential
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
e : S ≃ₐ[R] T
inst✝ : Finite σ
val✝ : Fintype σ
⊢ (algebraMap (P.ofAlgEquiv e).Ring T) (P.ofAlgEquiv e).jacobiMatrix.det = e ((algebraMap P.Ring S) P.jacobiMatrix.det)

Tactic:
]

Goal state after:
case intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : PreSubmersivePresentation R S ι σ
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
e : S ≃ₐ[R] T
inst✝ : Finite σ
val✝ : Fintype σ
⊢ (algebraMap (P.ofAlgEquiv e).Ring T) (P.ofAlgEquiv e).jacobiMatrix.det = e ((algebraMap P.Ring S) P.jacobiMatrix.det)
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
this : (algebraMap (ofBijectiveAlgebraMap h).Ring S).mapMatrix (ofBijectiveAlgebraMap h).jacobiMatrix = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
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
h : (pderiv ()) (C r * X () - 1) = C r
i j : Unit
⊢ (pderiv ((localizationAway S r).map i)) ((localizationAway S r).relation j) = Matrix.diagonal (fun x ↦ C r) i j

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
h : (pderiv ()) (C r * X () - 1) = C r
i j : Unit
⊢ (pderiv ((localizationAway S r).map i)) ((localizationAway S r).relation j) = Matrix.diagonal (fun x ↦ C r) i j
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:
]

Goal state after:
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
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 : σ
⊢ (pderiv ((Q.comp P).map (Sum.inl i))) ((Q.comp P).relation (Sum.inr j)) = 0

Tactic:
]

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✝¹ : Fintype σ
inst✝ : Fintype σ'
i : σ'
j : σ
⊢ (pderiv ((Q.comp P).map (Sum.inl i))) ((Q.comp P).relation (Sum.inr j)) = 0
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 : σ'
⊢ (aeval (Sum.elim X (⇑C ∘ P.val))) ((pderiv (Sum.inl (Q.map j))) ((Q.comp P).relation (Sum.inl i))) =
    (pderiv (Q.map j)) ((aeval (Sum.elim X (⇑C ∘ P.val))) ((Q.comp P.toPresentation).relation (Sum.inl i)))

Tactic:
]

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✝¹ : Fintype σ
inst✝ : Fintype σ'
i j : σ'
⊢ (aeval (Sum.elim X (⇑C ∘ P.val))) ((pderiv (Sum.inl (Q.map j))) ((Q.comp P).relation (Sum.inl i))) =
    (pderiv (Q.map j)) ((aeval (Sum.elim X (⇑C ∘ P.val))) ((Q.comp P.toPresentation).relation (Sum.inl i)))
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 σ'
⊢ ((aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁).det =
    ((algebraMap Q.Ring T).mapMatrix Q.jacobiMatrix).det

Tactic:
]

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✝¹ : Fintype σ
inst✝ : Fintype σ'
⊢ ((aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₁₁).det =
    ((algebraMap Q.Ring T).mapMatrix Q.jacobiMatrix).det
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 = W.negDblY P

Tactic:
]

Goal state after:
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 : σ
⊢ (pderiv ((Q.comp P).map (Sum.inr i))) ((Q.comp P).relation (Sum.inr j)) =
    (rename Sum.inr) ((pderiv (P.map i)) (P.relation j))

Tactic:
]

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✝¹ : Fintype σ
inst✝ : Fintype σ'
i j : σ
⊢ (pderiv ((Q.comp P).map (Sum.inr i))) ((Q.comp P).relation (Sum.inr j)) =
    (rename Sum.inr) ((pderiv (P.map i)) (P.relation j))
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 σ'
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det =
    (algebraMap S T) ((algebraMap P.Ring S) P.jacobiMatrix.det)

Tactic:
]

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✝¹ : Fintype σ
inst✝ : Fintype σ'
⊢ (aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det =
    (algebraMap S T) ((algebraMap P.Ring S) P.jacobiMatrix.det)
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 σ'
⊢ ((aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₂₂).det =
    ((algebraMap S T).mapMatrix ((algebraMap P.Ring S).mapMatrix P.jacobiMatrix)).det

Tactic:
]

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✝¹ : Fintype σ
inst✝ : Fintype σ'
⊢ ((aeval (Q.comp P).val).mapMatrix (Q.comp P).jacobiMatrix.toBlocks₂₂).det =
    ((algebraMap S T).mapMatrix ((algebraMap P.Ring S).mapMatrix P.jacobiMatrix)).det
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 : σ
⊢ (aeval (Q.comp P).val) ((rename Sum.inr) (P.jacobiMatrix i j)) =
    eval₂ (algebraMap R T) (fun i ↦ (algebraMap S T) (P.val i)) (P.jacobiMatrix i j)

Tactic:
]

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✝¹ : Fintype σ
inst✝ : Fintype σ'
i j : σ
⊢ (aeval (Q.comp P).val) ((rename Sum.inr) (P.jacobiMatrix i j)) =
    eval₂ (algebraMap R T) (fun i ↦ (algebraMap S T) (P.val i)) (P.jacobiMatrix i j)
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
⊢ ∀ x ∈ Submodule.span R (Set.range (v ∘ a)), x ∈ f.range → x = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
⊢ ∀ x ∈ Submodule.span R (Set.range (v ∘ a)), x ∈ f.range → x = 0
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
y : K
hy : f y ∈ Submodule.span R (Set.range (v ∘ a))
hz : s (f y) = 0
hs : s (f y) = y
⊢ 0 = 0

Tactic:
]

Goal state after: