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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
⊢ transitionMap I N hmn ∘ₗ ↑R (reduceModIdeal (I ^ n) f) = ↑R (reduceModIdeal (I ^ m) f) ∘ₗ transitionMap I M hmn

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
x : M
⊢ ((transitionMap I N hmn ∘ₗ ↑R (reduceModIdeal (I ^ n) f)) ∘ₗ (I ^ n • ⊤).mkQ) x =
    ((↑R (reduceModIdeal (I ^ m) f) ∘ₗ transitionMap I M hmn) ∘ₗ (I ^ n • ⊤).mkQ) x
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Sort u_6
f g : AdicCompletion I M → N
h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)
⊢ f = g

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Sort u_6
f g : AdicCompletion I M → N
h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)
x : AdicCompletion I M
⊢ f x = g x
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f g : AdicCompletion I M →ₗ[AdicCompletion I R] T
h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)
⊢ f = g

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f g : AdicCompletion I M →ₗ[AdicCompletion I R] T
h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)
x : AdicCompletion I M
⊢ f x = g x
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : AdicCompletion I M →ₗ[R] N
h : f ∘ₗ mk I M = g ∘ₗ mk I M
⊢ f = g

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : AdicCompletion I M →ₗ[R] N
h : f ∘ₗ mk I M = g ∘ₗ mk I M
x : AdicCompletion I M
⊢ f x = g x
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
n : ℕ
⊢ I ^ n • ⊤ = I ^ n

Tactic:
ext x

Goal state after:
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
n : ℕ
x : R
⊢ x ∈ I ^ n • ⊤ ↔ x ∈ I ^ n
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
x y : AdicCompletion I R
H : ∀ (n : ℕ), (evalₐ I n) x = (evalₐ I n) y
n : ℕ
⊢ I ^ n • ⊤ = I ^ n

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ y : AdicCompletion I R
H : ∀ (n : ℕ), (evalₐ I n) x✝ = (evalₐ I n) y
n : ℕ
x : R
⊢ x ∈ I ^ n • ⊤ ↔ x ∈ I ^ n
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: case h
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 : R ⧸ I • ⊤
b₁ b₂ : R
h✝ : b₁ ≈ b₂
a✝ : M
h : b₁ - b₂ ∈ I
⊢ b₁ • Quotient.mk'' a✝ = b₂ • Quotient.mk'' a✝

Tactic:
rw [← sub_eq_zero, ← sub_smul, Submodule.Quotient.mk''_eq_mk,
        ← Submodule.Quotient.mk_smul, Submodule.Quotient.mk_eq_zero]

Goal state after:
case h
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 : R ⧸ I • ⊤
b₁ b₂ : R
h✝ : b₁ ≈ b₂
a✝ : M
h : b₁ - b₂ ∈ I
⊢ (b₁ - b₂) • a✝ ∈ I • ⊤
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✝ : Type u_4
S : Type u_5
inst✝⁵ : NonAssocSemiring R✝
inst✝⁴ : CommRing S
I : Ideal S
f✝ : (n : ℕ) → R✝ →+* S ⧸ I ^ n
hf✝ : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f✝ n) = f✝ m
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
⊢ (Ideal.Quotient.factorPow I hle).comp (f n✝).toRingHom = (f m✝).toRingHom

Tactic:
ext x

Goal state after:
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✝ : Type u_4
S : Type u_5
inst✝⁵ : NonAssocSemiring R✝
inst✝⁴ : CommRing S
I : Ideal S
f✝ : (n : ℕ) → R✝ →+* S ⧸ I ^ n
hf✝ : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f✝ n) = f✝ m
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x : A
⊢ ((Ideal.Quotient.factorPow I hle).comp (f n✝).toRingHom) x = (f m✝).toRingHom x
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✝ : Type u_4
S : Type u_5
inst✝⁵ : NonAssocSemiring R✝
inst✝⁴ : CommRing S
I : Ideal S
f✝ : (n : ℕ) → R✝ →+* S ⧸ I ^ n
hf✝ : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f✝ n) = f✝ m
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
r : R
n m✝ n✝ : ℕ
hle : m✝ ≤ n✝
⊢ (Ideal.Quotient.factorPow ?m.137 hle).comp (?m.138 n✝) = ?m.138 m✝

Tactic:
ext x

Goal state after:
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✝ : Type u_4
S : Type u_5
inst✝⁵ : NonAssocSemiring R✝
inst✝⁴ : CommRing S
I : Ideal S
f✝ : (n : ℕ) → R✝ →+* S ⧸ I ^ n
hf✝ : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f✝ n) = f✝ m
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
r : R
n m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x : ?m.133
⊢ ((Ideal.Quotient.factorPow ?m.137 hle).comp (?m.138 n✝)) x = (?m.138 m✝) x
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: S : Type u_5
inst✝⁴ : CommRing S
I : Ideal S
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
n : ℕ
x : A
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
⊢ (Ideal.Quotient.factorPow I hle).comp (f n✝).toRingHom = (f m✝).toRingHom

Tactic:
ext x

Goal state after:
S : Type u_5
inst✝⁴ : CommRing S
I : Ideal S
R : Type u_6
A : Type u_7
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m
n : ℕ
x✝ : A
m✝ n✝ : ℕ
hle : m✝ ≤ n✝
x : A
⊢ ((Ideal.Quotient.factorPow I hle).comp (f n✝).toRingHom) x = (f m✝).toRingHom x
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:
ext x

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
x : M
⊢ ((AlgebraTensorModule.curry (AlgebraTensorModule.map LinearMap.id f)) 1) x =
    ((AlgebraTensorModule.curry
          (↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ
            ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f))
        1)
      x
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 : ℕ
⊢ (Ideal.Quotient.factorₐ R ⋯).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:
← DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ

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.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
inst✝¹ : FormallySmooth R A
I : Ideal S
inst✝ : IsAdicComplete I S
f : A →ₐ[R] S ⧸ I
g : A →ₐ[R] AdicCompletion I S
hg : (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)).comp g = f
⊢ (Ideal.Quotient.mkₐ R I).comp ((AlgHom.restrictScalars R ↑(AdicCompletion.ofAlgEquiv I).symm).comp g) = f

Tactic:
ext x

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
inst✝¹ : FormallySmooth R A
I : Ideal S
inst✝ : IsAdicComplete I S
f : A →ₐ[R] S ⧸ I
g : A →ₐ[R] AdicCompletion I S
hg : (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)).comp g = f
x : A
⊢ ((Ideal.Quotient.mkₐ R I).comp ((AlgHom.restrictScalars R ↑(AdicCompletion.ofAlgEquiv I).symm).comp g)) x = f x
Module: Mathlib.RingTheory.Smooth.AdicCompletion

Goal state before:
pp: case h
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
inst✝ : FormallySmooth R A
f : S →ₐ[R] A
hf : Function.Surjective ⇑f
g : A →ₐ[R] AdicCompletion (ker f) S
hg :
  (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ (ker f))).comp g = ↑(Ideal.quotientKerAlgEquivOfSurjective hf).symm
⊢ (AdicCompletion.kerProj hf).comp g = AlgHom.id R A

Tactic:
ext x

Goal state after:
case h
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
inst✝ : FormallySmooth R A
f : S →ₐ[R] A
hf : Function.Surjective ⇑f
g : A →ₐ[R] AdicCompletion (ker f) S
hg :
  (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ (ker f))).comp g = ↑(Ideal.quotientKerAlgEquivOfSurjective hf).symm
x : A
⊢ ((AdicCompletion.kerProj hf).comp g) x = (AlgHom.id R A) x
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 ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst✝³ : Fintype σ'
inst✝² : DecidableEq σ'
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
i j : σ'
⊢ (P.reindex e f).jacobiMatrix i j = ((Matrix.reindex f.symm f.symm) P.jacobiMatrix).map (⇑(rename ⇑e.symm)) i j

Tactic:
simp [jacobiMatrix_apply,
    MvPolynomial.pderiv_rename e.symm.injective, reindex, Presentation.reindex]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Core

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
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
⊢ (P.tensorModelOfHasCoeffsHom R₀).comp
      ((Ideal.Quotient.liftₐ P.ker
            ((TensorProduct.map (AlgHom.id R R)
                  (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
              ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
            ⋯).comp
        (Ideal.Quotient.mkₐ R P.ker)) =
    (↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
h : Function.Surjective ⇑((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker))
x : ι
⊢ ((P.tensorModelOfHasCoeffsHom R₀).comp
        ((Ideal.Quotient.liftₐ P.ker
              ((TensorProduct.map (AlgHom.id R R)
                    (Ideal.Quotient.mkₐ R₀ (Ideal.span (Set.range (relationOfHasCoeffs R₀))))).comp
                ↑(MvPolynomial.algebraTensorAlgEquiv R₀ R).symm)
              ⋯).comp
          (Ideal.Quotient.mkₐ R P.ker)))
      (MvPolynomial.X x) =
    ((↑(AlgEquiv.restrictScalars R P.quotientEquiv)).comp (Ideal.Quotient.mkₐ R P.ker)) (MvPolynomial.X x)
Module: Mathlib.RingTheory.Extension.Presentation.Core

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
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
⊢ (P.tensorModelOfHasCoeffsInv R₀).comp (P.tensorModelOfHasCoeffsHom R₀) = AlgHom.id R (R ⊗[R₀] ModelOfHasCoeffs R₀)

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
x : ModelOfHasCoeffs R₀
⊢ ((AlgHom.restrictScalars R₀ ((P.tensorModelOfHasCoeffsInv R₀).comp (P.tensorModelOfHasCoeffsHom R₀))).comp
        TensorProduct.includeRight)
      x =
    ((AlgHom.restrictScalars R₀ (AlgHom.id R (R ⊗[R₀] ModelOfHasCoeffs R₀))).comp TensorProduct.includeRight) x
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 ι σ
x : P.toExtension.Cotangent
hx : x ∈ P.cotangentComplexAux.ker
⊢ x ∈ ⊥

Tactic:
obtain ⟨(x : P.ker), rfl⟩ := Cotangent.mk_surjective x

Goal state after:
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 ι σ
x : ↥P.ker
hx : Cotangent.mk x ∈ P.cotangentComplexAux.ker
⊢ Cotangent.mk x ∈ ⊥
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: case a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.dblY P * P z ^ 2 + W'.negDblY P * P z ^ 2 - ((eval P) W'.polynomialX ^ 3 + -(eval P) W'.polynomialX ^ 3) = 0

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

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.dblY P = W.dblU P

Tactic:
rw [dblU, ← dblY_of_Y_eq' hP hPz hQz hx hy hy', mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]

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 * P z) ^ 3 / (P z * Q z) = 0

Tactic:
hPz,

Goal state after:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hPz : P z = 0
⊢ -(P y * Q z - Q y * 0) ^ 3 / (0 * Q z) = 0
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)

Tactic:
let eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
    IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p) e

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
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
⊢ -3 * P x ^ 2 * Q x * Q z + 3 * P x * Q x ^ 2 * P z + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * Q z ^ 2 -
                  W'.a₁ * Q x * Q y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * Q z ^ 2 +
              W'.a₂ * Q x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * Q z ^ 2 -
          W'.a₃ * Q y * P z ^ 2 * Q z -
        W'.a₄ * P x * P z * Q z ^ 2 +
      W'.a₄ * Q x * P z ^ 2 * Q z =
    P y ^ 2 * Q z * Q z

Tactic:
hPz,

Goal state after:
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
⊢ -3 * P x ^ 2 * Q x * Q z + 3 * P x * Q x ^ 2 * 0 + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * 0 ^ 2 + W'.a₁ * P x * P y * Q z ^ 2 -
                  W'.a₁ * Q x * Q y * 0 ^ 2 -
                W'.a₂ * P x ^ 2 * Q z ^ 2 +
              W'.a₂ * Q x ^ 2 * 0 ^ 2 +
            W'.a₃ * P y * 0 * Q z ^ 2 -
          W'.a₃ * Q y * 0 ^ 2 * Q z -
        W'.a₄ * P x * 0 * Q z ^ 2 +
      W'.a₄ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q z
Module: Mathlib.RingTheory.Smooth.Flat

Goal state before:
pp: R : Type u_1
A : Type u_2
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective ⇑f
inst✝² : Module.Flat R S
inst✝¹ : IsNoetherianRing S
inst✝ : FormallySmooth R A
this : Module.Flat R (AdicCompletion (RingHom.ker f) S)
g : A →ₐ[R] AdicCompletion (RingHom.ker f) S
hg : (AdicCompletion.kerProj hf).comp g = AlgHom.id R A
⊢ Module.Flat R A

Tactic:
exact .of_retract g.toLinearMap
    (AdicCompletion.kerProj hf).toLinearMap (LinearMap.ext fun x ↦ congr($hg x))

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

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
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ ⇑(algebraMap D.T S) ∘ ⇑(algebraMap P.Ring D.T) = ⇑(algebraMap P.Ring S)

Tactic:
ext x

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_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : P.Ring
⊢ (⇑(algebraMap D.T S) ∘ ⇑(algebraMap P.Ring D.T)) x = (algebraMap P.Ring S) x
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
⊢ -P x * Q y ^ 2 * P z + Q x * P y ^ 2 * Q z - 2 * P x * P y * Q y * Q z + 2 * Q x * P y * Q y * P z -
                            W'.a₁ * P x ^ 2 * Q y * Q z +
                          W'.a₁ * Q x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * Q x * Q z -
                      W'.a₂ * P x * Q x ^ 2 * P z -
                    W'.a₃ * P x * P y * Q z ^ 2 +
                  W'.a₃ * Q x * Q y * P z ^ 2 -
                2 * W'.a₃ * P x * Q y * P z * Q z +
              2 * W'.a₃ * Q x * P y * P z * Q z +
            W'.a₄ * P x ^ 2 * Q z ^ 2 -
          W'.a₄ * Q x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * Q z ^ 2 -
      3 * W'.a₆ * Q x * P z ^ 2 * Q z =
    P y ^ 2 * Q z * Q x

Tactic:
hPz,

Goal state after:
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
⊢ -P x * Q y ^ 2 * 0 + Q x * P y ^ 2 * Q z - 2 * P x * P y * Q y * Q z + 2 * Q x * P y * Q y * 0 -
                            W'.a₁ * P x ^ 2 * Q y * Q z +
                          W'.a₁ * Q x ^ 2 * P y * 0 +
                        W'.a₂ * P x ^ 2 * Q x * Q z -
                      W'.a₂ * P x * Q x ^ 2 * 0 -
                    W'.a₃ * P x * P y * Q z ^ 2 +
                  W'.a₃ * Q x * Q y * 0 ^ 2 -
                2 * W'.a₃ * P x * Q y * 0 * Q z +
              2 * W'.a₃ * Q x * P y * 0 * Q z +
            W'.a₄ * P x ^ 2 * Q z ^ 2 -
          W'.a₄ * Q x ^ 2 * 0 ^ 2 +
        3 * W'.a₆ * P x * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q x