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

Goal state before:
pp: case neg
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)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
i j : α
a : Equalizer.Presieve.Arrows.FirstObj F X
hi : ¬i = j
this : PreservesLimit (Functor.empty Cᵒᵖ) F
⊢ (ConcreteCategory.hom (F.map (pullback.fst (c.inj i) (c.inj j)).op))
      ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) i)) a) =
    (ConcreteCategory.hom (F.map (pullback.snd (c.inj i) (c.inj j)).op))
      ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) j)) a)

Tactic:
apply_fun (F.mapIso ((hd hi).isoPullback).op ≪≫ F.mapIso (terminalIsoIsTerminal
      (terminalOpOfInitial initialIsInitial)).symm ≪≫ (PreservesTerminal.iso F)).hom using
      injective_of_mono _

Goal state after:
case neg
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)
hI : IsInitial I
α : Type u_1
inst✝³ : Small.{w, u_1} α
X : α → C
c : Cofan X
inst✝² : (ofArrows X c.inj).HasPairwisePullbacks
inst✝¹ : HasInitial C
inst✝ : ∀ (i : α), Mono (c.inj i)
hd : Pairwise fun i j ↦ IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
i j : α
a : Equalizer.Presieve.Arrows.FirstObj F X
hi : ¬i = j
this : PreservesLimit (Functor.empty Cᵒᵖ) F
⊢ (ConcreteCategory.hom
        (F.mapIso (IsPullback.isoPullback ⋯).op ≪≫
            F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫
              PreservesTerminal.iso F).hom)
      ((ConcreteCategory.hom (F.map (pullback.fst (c.inj i) (c.inj j)).op))
        ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) i)) a)) =
    (ConcreteCategory.hom
        (F.mapIso (IsPullback.isoPullback ⋯).op ≪≫
            F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫
              PreservesTerminal.iso F).hom)
      ((ConcreteCategory.hom (F.map (pullback.snd (c.inj i) (c.inj j)).op))
        ((ConcreteCategory.hom (Pi.π (fun i ↦ F.obj (op (X i))) j)) a))
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
⊢ (uliftFunctor.mapCone c).pt.str ≤
    ⨅ j,
      TopologicalSpace.induced (⇑(ConcreteCategory.hom ((uliftFunctor.mapCone c).π.app j)))
        ((K ⋙ uliftFunctor).obj j).str

Tactic:
le_iInf_iff

Goal state after:
case refine_1
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
⊢ ∀ (i : J✝),
    (uliftFunctor.mapCone c).pt.str ≤
      TopologicalSpace.induced (⇑(ConcreteCategory.hom ((uliftFunctor.mapCone c).π.app i)))
        ((K ⋙ uliftFunctor).obj i).str
Module: Mathlib.Topology.Category.TopCat.ULift

Goal state before:
pp: case refine_2
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
⊢ TopologicalSpace.generateFrom (⋃ i, {s | IsOpen s}) ≤
    ⨅ i,
      TopologicalSpace.induced ULift.down (TopologicalSpace.induced (⇑(ConcreteCategory.hom (c.π.app i))) (K.obj i).str)

Tactic:
le_iInf_iff

Goal state after:
case refine_2
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ TopCat
c : Cone K
hc : IsLimit c
⊢ ∀ (i : J✝),
    TopologicalSpace.generateFrom (⋃ i, {s | IsOpen s}) ≤
      TopologicalSpace.induced ULift.down (TopologicalSpace.induced (⇑(ConcreteCategory.hom (c.π.app i))) (K.obj i).str)
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case refine_1
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) ⋯) ⋯
⊢ (fun t ↦ x.IsAmalgamation t) e

Tactic:
rintro Z e ⟨j⟩

Goal state after:
case refine_1
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) ⋯) ⋯
Y : Scheme
j : 𝓤.I₀
⊢ (ConcreteCategory.hom ((yoneda.obj X).map (𝓤.f j).op)) e = x (𝓤.f j) ⋯
Module: Mathlib.RingTheory.RingHom.Smooth

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FormallySmooth ∧ f.FinitePresentation
⊢ f.FormallySmooth

Tactic:
exact hf.1

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

Goal state before:
pp: 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✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
g' : A i →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  AlgHom.ofLinearMap (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) ⋯ ⋯
⊢ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) ⊥ = ⊥

Tactic:
Ideal.map_bot

Goal state after:
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✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
g' : A i →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  AlgHom.ofLinearMap (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) ⋯ ⋯
⊢ ⊥ = ⊥
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case intro.mpr.hI
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) ⋯ ⋯
⊢ Ideal.map (algebraMap B (B ⧸ J')) ⊥ = ⊥

Tactic:
Ideal.map_bot

Goal state after:
case intro.mpr.hI
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) ⋯ ⋯
⊢ ⊥ = ⊥
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
this :
  ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R]) ∘ₗ
      LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S)) ∘ₗ
        ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K ↥(RingHom.ker (algebraMap P S))).symm =
    cotangentComplexBaseChange R S P K
⊢ Function.Injective ⇑(LinearMap.lTensor K (cotangentComplexBaseChange R S P (ResidueField S))) ↔
    Function.Injective
      ⇑(LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S)) ∘ₗ
          ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K ↥(RingHom.ker (algebraMap P S))).symm)

Tactic:
exact ((AlgebraTensorModule.cancelBaseChange _ _ _ _ _).symm.injective_comp _).symm

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
  have : Algebra.IsPushout R A S B := .symm inferInstance
  obtain ⟨b, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective b
  induction b with
  | zero => simp
  | add x y _ _ => simp only [map_add, *, add_tmul, add_smul]
  | tmul a' s =>
  trans s • a' • D S B (algebraMap A B a)
  · simp [tensorKaehlerEquiv]
  · simp [Algebra.IsPushout.equiv_tmul, mul_smul, smul_comm]

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:
obtain ⟨n, f₀, hf₀⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp
    (inferInstance : Algebra.FiniteType R P)
  let M' := M.comap f₀
  let P' := Localization M'
  let fP : P' →ₐ[R] S := IsLocalization.liftAlgHom (M := M')
      (f := (IsScalarTower.toAlgHom R P S).comp f₀) fun x ↦ by
    simpa using IsLocalization.map_units (M := M) _ ⟨f₀ x.1, x.2⟩
  have hf₁ : Function.Surjective fP := by
    intro x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x
    obtain ⟨x, rfl⟩ := hf₀ x
    obtain ⟨s, rfl⟩ := hf₀ s
    refine ⟨IsLocalization.mk' (M := M') _ x ⟨s, hs⟩, ?_⟩
    simp [fP, IsLocalization.lift_mk', Units.mul_inv_eq_iff_eq_mul, IsUnit.liftRight]
  have hfP : (RingHom.ker fP).FG := by
    have := Algebra.FinitePresentation.ker_fG_of_surjective _ hf₀
    convert! this.map (algebraMap _ P')
    refine le_antisymm ?_ (Ideal.map_le_iff_le_comap.mpr fun x hx ↦ by simp_all [fP])
    intro x hx
    obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M' x
    obtain ⟨a, ha, e⟩ : ∃ a ∈ M, a * f₀ x = 0 := by
      simpa [fP, IsLocalization.lift_mk', IsLocalization.map_eq_zero_iff M] using hx
    obtain ⟨a, rfl⟩ := hf₀ a
    rw [IsLocalization.mk'_mem_map_algebraMap_iff]
    exact ⟨a, ha, by simpa⟩
  algebraize [fP.toRingHom]
  have : FormallyEtale (MvPolynomial (Fin n) R) P' := .of_isLocalization M'
  have : FormallySmooth R P' := .comp _ (MvPolynomial (Fin n) R) _
  have : Module.Free P' Ω[P'⁄R] :=
    .of_equiv (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R (MvPolynomial (Fin n) R) P')
  exact FormallySmooth.of_formallySmooth_residueField_tensor_aux (R := R) (S := S) hf₁ hfP

Goal state after:
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
f : M →ₗ[R] N
g : N →ₗ[R] P
x : AdicCompletion I M
⊢ (map I g ∘ₗ map I f) x = (map I (g ∘ₗ f)) x

Tactic:
map_comp

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
f : M →ₗ[R] N
g : N →ₗ[R] P
x : AdicCompletion I M
⊢ (map I (g ∘ₗ f)) x = (map I (g ∘ₗ f)) 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
ι' : 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 : σ
p : P.Ring
⊢ { toRingHom := eval₂Hom (algebraMap R T) (Q.comp P).val, commutes' := ⋯ } ((rename Sum.inr) p) =
    eval₂ (algebraMap R T) (fun i ↦ (algebraMap S T) (P.val i)) p

Tactic:
induction p using MvPolynomial.induction_on with
  | C a =>
    simp only [algHom_C, algebraMap_eq, eval₂_C]
  | add p q hp hq => simp [hp, hq]
  | mul_X p i hp =>
    simp only [map_mul, eval₂_mul, hp]
    simp [Presentation.toGenerators_comp, toPresentation_comp]

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

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
e : S ≃ₐ[R] T
inst✝ : IsStandardSmoothOfRelativeDimension n R S
⊢ IsStandardSmoothOfRelativeDimension n R T

Tactic:
by
  obtain ⟨_, _, _, _, ⟨P, hP⟩⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›
  exact (P.ofAlgEquiv e).isStandardSmoothOfRelativeDimension (by simpa)

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

Goal state before:
pp: case hr
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 : ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0
this✝ : ↑x ∈ Ideal.span (Set.range P.relation)
c : σ →₀ P.Ring
hc : (c.sum fun i a ↦ a * P.relation i) = ↑x
heq : ∀ (i : σ), ∑ x ∈ c.support, (aeval P.val) (c x) * (aeval P.val) ((pderiv (P.map i)) (P.relation x)) = 0
heq2 : (∑ i ∈ c.support, (aeval P.val) (c i) • fun j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))) = 0
this : ∀ (i : σ), (aeval P.val) (c i) = 0
i : σ
hi : i ∈ c.support
⊢ c i ∈ P.ker

Tactic:
rw [P.ker_eq_ker_aeval_val]
    simpa using this i

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Smooth
⊢ f.Flat

Tactic:
by
  algebraize [f]
  exact Algebra.Smooth.flat R S

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FormallyUnramified ∧ f.Smooth
⊢ f.FormallyUnramified

Tactic:
exact hf.1

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

Goal state before:
pp: case refine_3
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
⊢ IsUnit ((algebraMap P.Ring S) D.g)

Tactic:
· suffices h : (algebraMap P.Ring S) D.g = 1 by simp [h]
    rw [← map_one (algebraMap P.Ring S), ← sub_eq_zero, ← map_sub, ← RingHom.mem_ker]
    exact D.hgmem

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

Goal state before:
pp: ⊢ ∀ {R S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.IsStandardSmooth

Tactic:
introv

Goal state after:
R S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ e.toRingHom.IsStandardSmooth
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e : P.dimension = n
⊢ Nat.card ↑(Set.range P.map)ᶜ = n

Tactic:
rw [Nat.card_coe_set_eq, Set.ncard_compl,
        Set.ncard_range_of_injective P.map_inj, ← e, Algebra.Presentation.dimension]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig : f.kerSquareLift.comp σ = AlgHom.id A B
this :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), ∃ a, (Ideal.Quotient.mk (RingHom.ker f ^ 2)) a = σ (P.val i)
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
choose h hh using this

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: ⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    f.Etale ↔ RingHom.Locally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.IsStandardSmoothOfRelativeDimension 0) f

Tactic:
introv

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.Etale ↔ RingHom.Locally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.IsStandardSmoothOfRelativeDimension 0) f
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct ↑R ↑S ↑S →+* ↑S := (Algebra.TensorProduct.lmul' ↑R).toRingHom
hF : Function.Surjective ⇑F
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
e : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom F)) = Ideal.span {e}
x : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
hx : e * x ∈ KaehlerDifferential.ideal ↑R ↑S
⊢ ↑⟨e * x, hx⟩ ∈ KaehlerDifferential.ideal ↑R ↑S * KaehlerDifferential.ideal ↑R ↑S

Tactic:
Subtype.coe_mk,

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct ↑R ↑S ↑S →+* ↑S := (Algebra.TensorProduct.lmul' ↑R).toRingHom
hF : Function.Surjective ⇑F
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
e : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom F)) = Ideal.span {e}
x : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
hx : e * x ∈ KaehlerDifferential.ideal ↑R ↑S
⊢ e * x ∈ KaehlerDifferential.ideal ↑R ↑S * KaehlerDifferential.ideal ↑R ↑S
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: case hf
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
heq :
  pullback.fst (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g) =
    (pullbackSymmetry (pullback.fst (pullback.snd g g ≫ g) f) (pullback.diagonal g)).hom ≫
      (pullbackRightPullbackFstIso (pullback.snd g g ≫ g) f (pullback.diagonal g)).hom ≫
        (pullback.congrHom ⋯ ⋯).hom ≫
          (pullbackSymmetry g f).hom ≫ pullback.diagonal (pullback.fst f g) ≫ (diagonalObjPullbackFstIso f g).hom
⊢ Q (pullback.fst (pullback.snd g g ≫ g) f)

Tactic:
exact MorphismProperty.pullback_fst _ _ hf

Goal state after: