mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: case inr
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
this :
  ∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_2 : NormedField A] [IsAlgClosed A]
    [NormedAlgebra ℚ A] {x : K},
    x ≠ 0 →
      IsIntegral ℤ x →
        (∀ (φ : K →+* A), ‖φ x‖ ≤ 1) → ∀ (a b : ℕ), a ≠ b → x ^ a = x ^ b → b < a → ∃ n, ∃ (_ : 0 < n), x ^ n = 1
hlt : ¬b < a
⊢ ∃ n, ∃ (_ : 0 < n), x ^ n = 1

pp: K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ ∃ n, ∃ (_ : 0 < n), x ^ n = 1

Tactic:
· exact this K A hx₀ hxi hx b a habne.symm h.symm (habne.lt_or_gt.resolve_right hlt)

Goal state after:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hx₀ : x ≠ 0
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ ≤ 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ ∃ n, ∃ (_ : 0 < n), x ^ n = 1
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
num : ℤ
den : ℕ
hden : den ≠ 0
x : M
⊢ (mkRat num den).num • 1 < (mkRat num den).den • x ↔ num • 1 < den • x

Tactic:
obtain ⟨m, hm0, hnum, hden⟩ := Rat.mkRat_num_den hden (show mkRat num den = _ by rfl)

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
num : ℤ
den : ℕ
hden✝ : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).num *
      ↑m
hden :
  den =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).den *
      m
⊢ (mkRat num den).num • 1 < (mkRat num den).den • x ↔ num • 1 < den • x
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case H2
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X - C z ∣ map (algebraMap ℝ ℂ) p

Tactic:
· simpa [dvd_iff_isRoot]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x : L
⊢ 0 < ↑((RankOne.hom v) (v.restrict x)) ↔ 0 < v x

Tactic:
← NNReal.coe_zero,

Goal state after:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation L Γ₀
hv : v.RankOne
x : L
⊢ ↑0 < ↑((RankOne.hom v) (v.restrict x)) ↔ 0 < v x
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
⊢ {x | x ∈ v.integer} = Metric.closedBall 0 1

Tactic:
ext x
  simp [mem_integer_iff]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order = 0
| f

Tactic:
rw [← X_pow_order_mul_divXPowOrder (f := f), this, ENat.toNat_zero,
      pow_zero, one_mul]

Goal state after:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order = 0
| f.divXPowOrder
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j ≠ 0
h1728 : j ≠ 1728
⊢ (if j = 1728 then ofJ1728 F else ofJNe0Or1728 j) = ofJNe0Or1728 j

Tactic:
if_neg h1728

Goal state after:
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j ≠ 0
h1728 : j ≠ 1728
⊢ ofJNe0Or1728 j = ofJNe0Or1728 j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) W'.polynomialY = 2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2

Tactic:
by
  rw [polynomialY_eq]
  simp

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

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : Q z = 0
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
rw [add_of_Z_eq_zero_right hQ.left hPz hQz,
        toAffine_smul _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg,
        toAffine_of_Z_eq_zero hQz, add_zero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: J : Type u_1
inst✝⁴ : Category.{u_2, u_1} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
c : Cocone F
hc : IsColimit c
iso : c.pt ≅ colimit F := hc.coconePointUniqueUpToIso (colimit.isColimit F)
Y : Scheme
i : J
⊢ (Sieve.pullback iso.inv (Sieve.ofArrows F.obj c.ι.app)).arrows (colimit.ι F i)

Tactic:
exact ⟨_, 𝟙 _, c.ι.app i, ⟨i⟩, by simp [iso]⟩

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

Goal state before:
pp: case pos
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ (W.map f).dblXYZ (⇑f ∘ P) = ⇑f ∘ W.dblXYZ P

Tactic:
map_dblXYZ

Goal state after:
case pos
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Projective F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ ⇑f ∘ W.dblXYZ P = ⇑f ∘ W.dblXYZ P
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: R S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ (algebraMap R S).FormallyUnramified

Tactic:
rw [formallyUnramified_algebraMap]

Goal state after:
R S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Algebra.FormallyUnramified R S
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) ⋯ ⋯
⊢ J' i ^ 2 = ⊥

Tactic:
by rw [← Ideal.map_pow, hJ, Ideal.map_bot]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing A
inst✝ : Algebra R A
a : A
⊢ a • 0 = 0

Tactic:
by
  rw [← zero_tmul _ (0 : Ω[A⁄R]), mulActionBaseChange_smul_tmul, smul_zero]

Goal state after:
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))
⊢ (AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R])
      (1 ⊗ₜ[ResidueField S] (cotangentComplexBaseChange R S P (ResidueField S)) (1 ⊗ₜ[P] x✝)) =
    (cotangentComplexBaseChange R S P K) (1 ⊗ₜ[P] x✝)

Tactic:
cotangentComplexBaseChange_tmul,

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))
⊢ (AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R])
      (1 ⊗ₜ[ResidueField S] (1 • (kerToTensor R P (ResidueField S)) ⟨↑x✝, ⋯⟩)) =
    1 • (kerToTensor R P K) ⟨↑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
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
a : AdicCauchySequence I M
m n : ℕ
hmn : m ≤ n
⊢ (fun n ↦ f (↑a n)) m ≡ (fun n ↦ f (↑a n)) n [SMOD I ^ m • ⊤]

Tactic:
have hm : Submodule.map f (I ^ m • ⊤ : Submodule R M) ≤ (I ^ m • ⊤ : Submodule R N) := by
      rw [Submodule.map_smul'']
      exact smul_mono_right _ le_top

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
a : AdicCauchySequence I M
m n : ℕ
hmn : m ≤ n
hm : Submodule.map f (I ^ m • ⊤) ≤ I ^ m • ⊤
⊢ (fun n ↦ f (↑a n)) m ≡ (fun n ↦ f (↑a n)) n [SMOD I ^ m • ⊤]
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
x y : (n : ℕ) → R ⧸ I ^ n • ⊤
hx : x ∈ submodule I R
hy : y ∈ submodule I R
m n : ℕ
hmn : m ≤ n
⊢ (transitionMap I R hmn) ((x * y) n) = (x * y) m

Tactic:
by simp [hx hmn, hy hmn, transitionMap_map_mul I hmn]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
k : ℕ
h : (if j = i then 1 else 0) = ↑(if j = i then 1 else 0) k
⊢ ↑(((AlgebraTensorModule.curry (↑(piEquivOfFintype I fun x ↦ R) ∘ₗ ofTensorProduct I (ι → R))) 1 ∘ₗ
            LinearMap.single R (fun i ↦ R) i)
          1 j)
      k =
    ↑(((AlgebraTensorModule.curry ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)) 1 ∘ₗ
            LinearMap.single R (fun i ↦ R) i)
          1 j)
      k

Tactic:
by
    simpa [Pi.single_apply, -smul_eq_mul]

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))) ((pderiv ((Q.comp P).map (Sum.inl j))) ((Q.comp P).relation (Sum.inl i))) =
    (pderiv (Q.map j)) (Q.relation i)

Tactic:
comp_map,

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.elim (fun rq ↦ Sum.inl (Q.map rq)) (fun rp ↦ Sum.inr (P.map rp)) (Sum.inl j)))
        ((Q.comp P).relation (Sum.inl i))) =
    (pderiv (Q.map j)) (Q.relation i)
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_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : ↥D.presLeft.toExtension.ker
⊢ Extension.Cotangent.mk
      ⟨(RingHom.id
            (Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).Ring)
          ↑x,
        ⋯⟩ =
    Extension.Cotangent.mk ⟨↑x, ⋯⟩

Tactic:
Presentation.naive_toGenerators,

Goal state after:
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
x : ↥D.presLeft.toExtension.ker
⊢ Extension.Cotangent.mk
      ⟨(RingHom.id (naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).Ring) ↑x, ⋯⟩ =
    Extension.Cotangent.mk ⟨↑x, ⋯⟩
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ IsStandardSmoothOfRelativeDimension n (algebraMap S (S ⊗[R] T))

Tactic:
rw [RingHom.IsStandardSmoothOfRelativeDimension]

Goal state after:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ IsStandardSmoothOfRelativeDimension n (algebraMap S (S ⊗[R] T))

Tactic:
rw [RingHom.IsStandardSmoothOfRelativeDimension]
      convert! this; ext; simp_rw [Algebra.smul_def]; rfl

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

Goal state before:
pp: case refine_1
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
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
⊢ Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i ∈
    ↑(RingHom.ker
        ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
              (RingHom.ker
                  (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                    (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
                2)).comp
          (aeval p)))

Tactic:
simp only [← AlgHom.comap_ker, Ideal.coe_comap, Set.mem_preimage, SetLike.mem_coe]

Goal state after:
case refine_1
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
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
i : D.rels
⊢ (aeval p) (Presentation.relationOfHasCoeffs (↥(subalgebra R D)) i) ∈
    RingHom.ker
      (Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (RingHom.ker
            (Ideal.Quotient.mkₐ (↥(subalgebra R D))
              (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
          2))
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
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ ⊤ ≤ Submodule.comap (Submodule.subtype P.ker) J ⊔ P.ker • Submodule.comap (Submodule.subtype P.ker) P.ker

Tactic:
simp only [Submodule.comap_subtype_self, J]

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ ⊤ ≤ Submodule.comap (Submodule.subtype P.ker) (Ideal.span (Set.range (Subtype.val ∘ v))) ⊔ P.ker • ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
H✝ : smoothLocus f = ⊤
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V
H : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Smooth (resLE f U V hVU)

Tactic:
HasRingHomProperty.iff_of_isAffine (P := @Smooth)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
H✝ : smoothLocus f = ⊤
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V
H : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ (CommRingCat.Hom.hom (appTop (resLE f U V hVU))).Smooth
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_2
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H :
  (Algebra.adjoin k (a '' {i}ᶜ)).val
      (↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩)
        (((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)).coeff (σ i))) =
    (Algebra.adjoin k (a '' {i}ᶜ)).val 0
⊢ (aeval a) ((rename Subtype.val) (F₀.coeff (σ i))) = 0

Tactic:
AlgHom.coe_toRingHom,

Goal state after:
case refine_2
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H :
  (Algebra.adjoin k (a '' {i}ᶜ)).val
      ((aeval fun j ↦ ⟨a ↑j, ⋯⟩)
        (((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)).coeff (σ i))) =
    (Algebra.adjoin k (a '' {i}ᶜ)).val 0
⊢ (aeval a) ((rename Subtype.val) (F₀.coeff (σ i))) = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this✝² : (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).EssFiniteType
algInst✝ : Algebra ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
  ↑(X.presheaf.stalk (genericPoint ↥X)) :=
  (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).toAlgebra
algebraizeInst✝ :
  Algebra.EssFiniteType ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
    ↑(X.presheaf.stalk (genericPoint ↥X))
K' : CommRingCat := (Spec.structureSheaf K).presheaf.stalk (f (genericPoint ↥X))
e : K ≃ₐ[K] ↑K' := IsLocalization.atUnits (↑(CommRingCat.of K)) (f (genericPoint ↥X)).asIdeal.primeCompl ⋯
this✝¹ : Algebra.IsAlgebraic K ↑K'
this✝ : Field ↑K' := ⋯.toField
this : Field ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) := this✝
⊢ (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).FormallySmooth

Tactic:
have : PerfectField ((Spec (.of K)).presheaf.stalk (f (genericPoint X))) :=
    Algebra.IsAlgebraic.perfectField (K := K)
      (L := (Spec.structureSheaf K).presheaf.stalk (f (genericPoint X)))

Goal state after:
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this✝³ : (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).EssFiniteType
algInst✝ : Algebra ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
  ↑(X.presheaf.stalk (genericPoint ↥X)) :=
  (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).toAlgebra
algebraizeInst✝ :
  Algebra.EssFiniteType ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
    ↑(X.presheaf.stalk (genericPoint ↥X))
K' : CommRingCat := (Spec.structureSheaf K).presheaf.stalk (f (genericPoint ↥X))
e : K ≃ₐ[K] ↑K' := IsLocalization.atUnits (↑(CommRingCat.of K)) (f (genericPoint ↥X)).asIdeal.primeCompl ⋯
this✝² : Algebra.IsAlgebraic K ↑K'
this✝¹ : Field ↑K' := ⋯.toField
this✝ : Field ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) := this✝¹
this : PerfectField ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
⊢ (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).FormallySmooth