mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
hy : P y * Q z = Q y * P z
⊢ W.Nonsingular (W.add P Q)

pp: case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
hy : ¬P y * Q z = Q y * P z
⊢ W.Nonsingular (W.add P Q)

Tactic:
· simp only [add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right, nonsingular_smul _ <|
              isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, nonsingular_zero]

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
hy : ¬P y * Q z = Q y * P z
⊢ W.Nonsingular (W.add P Q)
Module: Mathlib.CategoryTheory.Sites.Preserves

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
F : Cᵒᵖ ⥤ Type w
hF : IsSheafFor F (ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a)
⊢ IsTerminal (F.obj (op I))

Tactic:
refine @IsTerminal.ofUnique _ _ _ fun Y ↦ ?_
  choose t h using hF (by tauto) (by tauto)
  exact ⟨⟨↾fun _ ↦ t⟩, fun a ↦ by ext; exact h.2 _ (by tauto)⟩

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
⊢ P y ≠ 0

Tactic:
by
  intro hPy
  simp only [nonsingular_of_Z_eq_zero hPz, X_eq_zero_of_Z_eq_zero hP.left hPz, hPy, add_zero,
    sub_zero, mul_zero, zero_pow two_ne_zero, or_self, ne_self_iff_false, and_false] at hP

Goal state after:
Module: Mathlib.Topology.Category.TopCat.ULift

Goal state before:
pp: case refine_1
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
j : J✝
t : Set ↑((K ⋙ uliftFunctor).obj j)
ht : IsOpen t
⊢ IsOpen (⇑(ConcreteCategory.hom ((uliftFunctor.mapCone c).π.app j)) ⁻¹' t)

Tactic:
refine ⟨Homeomorph.ulift.symm ⁻¹' ((uliftFunctor.map (c.π.app j)) ⁻¹' t), ?_, rfl⟩

Goal state after:
case refine_1
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
j : J✝
t : Set ↑((K ⋙ uliftFunctor).obj j)
ht : IsOpen t
⊢ IsOpen (⇑Homeomorph.ulift.symm ⁻¹' ⇑(ConcreteCategory.hom (uliftFunctor.map (c.π.app j))) ⁻¹' t)
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case refine_2
X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible
e : Y ⟶ X := Cover.glueMorphisms 𝓤 (fun j ↦ x (𝓤.f j) ⋯) ⋯
e' : (yoneda.obj X).obj (op Y)
h : x.IsAmalgamation e'
⊢ e' = e

Tactic:
apply 𝓤.hom_ext

Goal state after:
case refine_2
X Y : Scheme
𝓤 : Y.OpenCover
hS : Presieve.ofArrows 𝓤.X 𝓤.f ∈ (precoverage IsOpenImmersion).coverings Y
x : Presieve.FamilyOfElements (yoneda.obj X) (Presieve.ofArrows 𝓤.X 𝓤.f)
hx : x.Compatible
e : Y ⟶ X := ⋯
e' : (yoneda.obj X).obj (op Y)
h : x.IsAmalgamation e'
⊢ ∀ (x : 𝓤.I₀), 𝓤.f x ≫ e' = 𝓤.f x ≫ e
Module: Mathlib.RingTheory.RingHom.Unramified

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

Tactic:
intro R S _ _ _ M _
  rw [formallyUnramified_algebraMap]
  exact .of_isLocalization M

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

Goal state before:
pp: case g.map_mul
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : FormallySmooth R ((i : I) → A i)
i : I
x y : A i
⊢ (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) ((LinearMap.single R A i) (x * y)) =
    (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) ((LinearMap.single R A i) x) *
      (Ideal.Quotient.mk (RingHom.ker (Pi.evalAlgHom R A i).toRingHom ^ 2)) ((LinearMap.single R A i) y)

Tactic:
simp +instances only [AlgHom.toRingHom_eq_coe, LinearMap.coe_single, Pi.single_mul, map_mul]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
⊢ f x →ₐ[R] B ⧸ J'

Tactic:
apply AlgHom.ofLinearMap
        (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap.comp (LinearMap.single _ _ x))
      · simp only [AlgHom.comp_toLinearMap, LinearMap.coe_comp, LinearMap.coe_single,
          Function.comp_apply, AlgHom.toLinearMap_apply, Ideal.Quotient.mkₐ_eq_mk]
        rw [eq_comm, ← sub_eq_zero, ← (Ideal.Quotient.mk J').map_one, ← map_sub,
          Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton, H]
      · intro r s; simp [Pi.single_mul]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case intro.mpr.a
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
f₂' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
r : f x
⊢ ((Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₁') r -
      ((Ideal.Quotient.mkₐ R (Ideal.map (algebraMap B (B ⧸ J')) J)).comp f₂') r =
    0

Tactic:
simp only [Ideal.Quotient.algebraMap_eq, AlgHom.coe_comp, Ideal.Quotient.mkₐ_eq_mk,
        Function.comp_apply, ← map_sub, Ideal.Quotient.eq_zero_iff_mem, f₁', f₂',
        AlgHom.comp_toLinearMap, AlgHom.ofLinearMap_apply, LinearMap.coe_comp,
        LinearMap.coe_single, Function.comp_apply, AlgHom.toLinearMap_apply,
        Ideal.Quotient.mkₐ_eq_mk]

Goal state after:
case intro.mpr.a
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
f₂' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
r : f x
⊢ (Ideal.Quotient.mk J') (f₁ (Pi.single x r) - f₂ (Pi.single x r)) ∈ Ideal.map (Ideal.Quotient.mk J') J
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
⊢ FormallySmooth R S ↔ Function.Injective ⇑(LinearMap.lTensor (ResidueField S) P.cotangentComplex)

Tactic:
have : Module.Finite P.Ring P.Cotangent :=
    have : Module.Finite P.Ring P.ker := .of_fg h'
    .of_surjective _ Extension.Cotangent.mk_surjective

Goal state after:
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
⊢ FormallySmooth R S ↔ Function.Injective ⇑(LinearMap.lTensor (ResidueField S) P.cotangentComplex)
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 : Type u_3
K : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : Algebra S K
inst✝⁴ : Algebra P K
inst✝³ : IsScalarTower P S K
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
h₃ : maximalIdeal S ≤ RingHom.ker (algebraMap S K)
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this✝¹ : Algebra (ResidueField S) K := f.toAlgebra
this✝ : IsScalarTower S (ResidueField S) K
this : IsScalarTower P (ResidueField S) K
x✝ : ↥(RingHom.ker (algebraMap P S))
⊢ ((curry
          (↑P ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R]) ∘ₗ
            ↑P (LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S))) ∘ₗ
              ↑P ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K ↥(RingHom.ker (algebraMap P S))).symm))
        1)
      x✝ =
    ((curry (↑P (cotangentComplexBaseChange R S P K))) 1) x✝

Tactic:
curry_apply,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsLocalRing S
inst✝¹¹ : Algebra R S
P : Type u_3
K : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : Algebra S K
inst✝⁴ : Algebra P K
inst✝³ : IsScalarTower P S K
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
h₃ : maximalIdeal S ≤ RingHom.ker (algebraMap S K)
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this✝¹ : Algebra (ResidueField S) K := f.toAlgebra
this✝ : IsScalarTower S (ResidueField S) K
this : IsScalarTower P (ResidueField S) K
x✝ : ↥(RingHom.ker (algebraMap P S))
⊢ (↑P ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R]) ∘ₗ
        ↑P (LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S))) ∘ₗ
          ↑P ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K ↥(RingHom.ker (algebraMap P S))).symm)
      (1 ⊗ₜ[P] x✝) =
    (↑P (cotangentComplexBaseChange R S P K)) (1 ⊗ₜ[P] x✝)
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:
simp_all [fP]

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
hfP : (RingHom.ker fP).FG
⊢ FormallySmooth R S

Tactic:
algebraize [fP.toRingHom]

Goal state after:
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
hfP : (RingHom.ker fP).FG
algInst✝ : Algebra P' S := fP.toAlgebra
⊢ FormallySmooth R S
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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
r : AdicCompletion I R
x : AdicCompletion I M
n✝ : ℕ
⊢ (reduceModIdeal (I ^ n✝) f) (↑r n✝ • ↑x n✝) = ↑r n✝ • (reduceModIdeal (I ^ n✝) f) (↑x n✝)

Tactic:
val_smul_eq_evalₐ_smul,

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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
r : AdicCompletion I R
x : AdicCompletion I M
n✝ : ℕ
⊢ (reduceModIdeal (I ^ n✝) f) ((evalₐ I n✝) r • ↑x n✝) = ↑r n✝ • (reduceModIdeal (I ^ n✝) f) (↑x n✝)
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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
r : AdicCompletion I R
x : AdicCompletion I M
n✝ : ℕ
⊢ (reduceModIdeal (I ^ n✝) f) ((evalₐ I n✝) r • ↑x n✝) = ↑r n✝ • (reduceModIdeal (I ^ n✝) f) (↑x n✝)

Tactic:
val_smul_eq_evalₐ_smul,

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
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
r : AdicCompletion I R
x : AdicCompletion I M
n✝ : ℕ
⊢ (reduceModIdeal (I ^ n✝) f) ((evalₐ I n✝) r • ↑x n✝) = (evalₐ I n✝) r • (reduceModIdeal (I ^ n✝) f) (↑x n✝)
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
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
y : N
n : ℕ
hxy : f x ≡ y [SMOD I ^ n • ⊤]
z : M
hz : z ∈ I ^ n • ⊤
hz' : f z ≡ y - f x [SMOD I ^ (n + 1) • ⊤]
⊢ ∃ x', x ≡ x' [SMOD I ^ n • ⊤] ∧ f x' ≡ y [SMOD I ^ (n + 1) • ⊤]

Tactic:
use x + z

Goal state after:
case h
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
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
y : N
n : ℕ
hxy : f x ≡ y [SMOD I ^ n • ⊤]
z : M
hz : z ∈ I ^ n • ⊤
hz' : f z ≡ y - f x [SMOD I ^ (n + 1) • ⊤]
⊢ x ≡ x + z [SMOD I ^ n • ⊤] ∧ f (x + z) ≡ y [SMOD I ^ (n + 1) • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

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
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
⊢ Function.Surjective ⇑(ofTensorProduct I M)

Tactic:
let g := map I p ∘ₗ ofTensorProduct I (Fin n → R)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
⊢ Function.Surjective ⇑(ofTensorProduct I M)
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 ⇑(AlgebraTensorModule.map LinearMap.id f)

Tactic:
rw [tensor_map_id_left_eq_map I f]
  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective,
    EquivLike.injective_comp]
  exact map_injective I hf

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
inst✝ : FormallySmooth R A
f : S →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ ∃ g, (AdicCompletion.kerProj hf).comp g = AlgHom.id R A

Tactic:
obtain ⟨g, hg⟩ := exists_adicCompletionEvalOneₐ_comp_eq
    (Ideal.quotientKerAlgEquivOfSurjective hf).symm.toAlgHom
  use g
  ext x
  simpa using! congr(Ideal.quotientKerAlgEquivOfSurjective hf ($hg x))

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 : σ'
⊢ (aeval (Sum.elim X (⇑C ∘ P.val))) ((Q.comp P).jacobiMatrix (Sum.inl j) (Sum.inl i)) = Q.jacobiMatrix j i

Tactic:
rw [jacobiMatrix_apply, jacobiMatrix_apply, comp_map, Sum.elim_inl,
    ← Q.comp_aeval_relation_inl P.toPresentation]

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: case intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
val✝ : Fintype σ
h : (baseChange T P).jacobiMatrix = (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix
⊢ (algebraMap (baseChange T P).Ring (T ⊗[R] S)) ((MvPolynomial.map (algebraMap R T)) P.jacobiMatrix.det) =
    1 ⊗ₜ[R] (algebraMap P.Ring S) P.jacobiMatrix.det

Tactic:
Generators.algebraMap_apply,

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
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
val✝ : Fintype σ
h : (baseChange T P).jacobiMatrix = (MvPolynomial.map (algebraMap R T)).mapMatrix P.jacobiMatrix
⊢ (aeval (baseChange T P).val) ((MvPolynomial.map (algebraMap R T)) P.jacobiMatrix.det) =
    1 ⊗ₜ[R] (algebraMap P.Ring S) P.jacobiMatrix.det
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
r : σ
⊢ P.basisCotangent r = Cotangent.mk ⟨P.relation r, ⋯⟩

Tactic:
symm

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 ι σ
r : σ
⊢ Cotangent.mk ⟨P.relation r, ⋯⟩ = P.basisCotangent r
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: 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 ι
⊢ (compLocalizationAwayAlgHom T g P) (((localizationAway T g).toComp P).toAlgHom (P.σ g)) *
        (compLocalizationAwayAlgHom T g P) (X (Sum.inl ())) -
      1 =
    0

Tactic:
compLocalizationAwayAlgHom_toAlgHom_toComp,

Goal state after:
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 ι
⊢ (algebraMap P.Ring (Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)))) (P.σ g) *
        (compLocalizationAwayAlgHom T g P) (X (Sum.inl ())) -
      1 =
    0
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ (Extension.Cotangent.map ((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toExtensionHom)
      (Extension.Cotangent.mk (D.kerGen r)) =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩

Tactic:
Extension.Cotangent.map_mk

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ Extension.Cotangent.mk
      ⟨((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toExtensionHom.toAlgHom ↑(D.kerGen r), ⋯⟩ =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩