mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
y : ℚ
hy : y.num • 1 < 0
hyx : ↑y = x
⊢ y ≤ 0

Tactic:
← Rat.num_nonpos

Goal state after:
case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
y : ℚ
hy : y.num • 1 < 0
hyx : ↑y = x
⊢ y.num ≤ 0
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: case mpr
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
⊢ IsRankLeOne R

Tactic:
by_cases H : IsNontrivial R

Goal state after:
case pos
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
H : IsNontrivial R
⊢ IsRankLeOne R

case neg
R : Type u_3
inst✝¹ : Ring R
inst✝ : ValuativeRel R
h : MulArchimedean (ValueGroupWithZero R)
H : ¬IsNontrivial R
⊢ IsRankLeOne R
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case inr
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : Archimedean M
h✝ : Nontrivial M
a : M
ha : a ≠ 0
one : One M := { one := |a| }
this : ZeroLEOneClass M
⊢ ∃ f, Function.Injective ⇑f

Tactic:
have : NeZero (1 : M) := ⟨abs_ne_zero.mpr ha⟩

Goal state after:
case inr
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : Archimedean M
h✝ : Nontrivial M
a : M
ha : a ≠ 0
one : One M := { one := |a| }
this✝ : ZeroLEOneClass M
this : NeZero 1
⊢ ∃ f, Function.Injective ⇑f
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
r : R
⊢ (monomial n) r ∈ nonZeroDivisorsLeft (MvPowerSeries σ R) ↔ r ∈ nonZeroDivisorsLeft R

Tactic:
constructor
  · intro H s hrs
    have := H (C s) (by rw [← monomial_zero_eq_C, monomial_mul_monomial]; ext; simp [hrs])
    simpa using congr(coeff 0 $(this))
  · intro H p hrp
    ext i
    have := congr(coeff (i + n) $hrp)
    rw [coeff_monomial_mul, if_pos le_add_self, add_tsub_cancel_right] at this
    simpa using H _ this

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit φ ↔ IsUnit (constantCoeff φ)

Tactic:
constructor
  · exact IsUnit.map _
  · intro ⟨u, hu⟩
    exact ⟨⟨_, φ.invOfUnit u, mul_invOfUnit φ u hu.symm, invOfUnit_mul φ u hu.symm⟩, rfl⟩

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

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
⊢ (coeff 0) φ⁻¹ = (constantCoeff φ)⁻¹

Tactic:
coeff_inv,

Goal state after:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
⊢ (if 0 = 0 then (constantCoeff φ)⁻¹
    else -(constantCoeff φ)⁻¹ * ∑ x ∈ antidiagonal 0, if x.2 < 0 then (coeff x.1) φ * (coeff x.2) φ⁻¹ else 0) =
    (constantCoeff φ)⁻¹
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
⊢ (coeff n) (inv.aux a φ) =
    if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) (inv.aux a φ) else 0

Tactic:
coeff,

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff (single () n)) (inv.aux a φ) =
    if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) (inv.aux a φ) else 0
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ constantCoeff (C r) ≠ 0

Tactic:
simpa using hr

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
j : R
⊢ (ofJNe0Or1728 j).Δ = j ^ 2 * (j - 1728) ^ 9

Tactic:
simp only [ofJNe0Or1728, Δ, b₂, b₄, b₆, b₈]

Goal state after:
R : Type u_1
inst✝ : CommRing R
j : R
⊢ -((j - 1728) ^ 2 + 4 * 0) ^ 2 *
            ((j - 1728) ^ 2 * -(j - 1728) ^ 5 + 4 * 0 * -(j - 1728) ^ 5 - (j - 1728) * 0 * (-36 * (j - 1728) ^ 3) +
                0 * 0 ^ 2 -
              (-36 * (j - 1728) ^ 3) ^ 2) -
          8 * (2 * (-36 * (j - 1728) ^ 3) + (j - 1728) * 0) ^ 3 -
        27 * (0 ^ 2 + 4 * -(j - 1728) ^ 5) ^ 2 +
      9 * ((j - 1728) ^ 2 + 4 * 0) * (2 * (-36 * (j - 1728) ^ 3) + (j - 1728) * 0) * (0 ^ 2 + 4 * -(j - 1728) ^ 5) =
    j ^ 2 * (j - 1728) ^ 9
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 = 0
⊢ 1728 = 0

Tactic:
linear_combination 864 * h2

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
h1728 : j = 1728
⊢ (ofJ j).IsElliptic

Tactic:
have h2 : (2 : F) ≠ 0 := fun h ↦ h0 (by linear_combination h1728 + 864 * h)
      have := Fact.mk h2.isUnit
      rw [h1728, ofJ_1728_of_two_ne_zero h2]
      infer_instance

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomial / P z ^ 3 = Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomial

Tactic:
by
  linear_combination (norm := (rw [eval_polynomial, Affine.evalEval_polynomial]; ring1))
    P y ^ 2 / P z ^ 2 * div_self hPz + W.a₁ * P x * P y / P z ^ 2 * div_self hPz
      + W.a₃ * P y / P z * div_self (pow_ne_zero 2 hPz) - W.a₂ * P x ^ 2 / P z ^ 2 * div_self hPz
      - W.a₄ * P x / P z * div_self (pow_ne_zero 2 hPz) - W.a₆ * div_self (pow_ne_zero 3 hPz)

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![0, 1, 0]⟧

Tactic:
by_cases hy : P y * Q z = Q y * P z
  · rw [addMap_eq, add_of_Y_eq hP.left hPz hQz hx hy hy',
      smul_eq _ <| isUnit_dblU_of_Y_eq hP hPz hQz hx hy hy']
  · rw [addMap_eq, add_of_Y_ne hP.left hQ hPz hQz hx hy,
      smul_eq _ <| isUnit_addU_of_Y_ne hPz hQz hy]

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

Goal state before:
pp: 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:
refine le_antisymm ?_ ?_
    · rw [le_iInf_iff]
      rintro j s ⟨t, ht, rfl⟩
      refine ⟨Homeomorph.ulift.symm ⁻¹' ((uliftFunctor.map (c.π.app j)) ⁻¹' t), ?_, rfl⟩
      apply Homeomorph.ulift.continuous_invFun.isOpen_preimage
      apply (uliftFunctor.map (c.π.app j)).hom.continuous_toFun.isOpen_preimage _ ht
    · change _ ≤ TopologicalSpace.induced _ _
      rw [← generateFrom_iUnion_isOpen, induced_of_isLimit _ hc, induced_iInf, le_iInf_iff]
      rintro i s ⟨-, ⟨t, ht, rfl⟩, rfl⟩
      refine .basic _ ?_
      rw [Set.mem_iUnion]
      exact ⟨i, ULift.down ⁻¹' t, Homeomorph.ulift.continuous_toFun.isOpen_preimage _ ht, rfl⟩

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
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
⊢ toAffine W (W.dblU P • ![0, 1, 0]) = 0

Tactic:
toAffine_smul _ <| isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right,

Goal state after:
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
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
⊢ toAffine W ![0, 1, 0] = 0
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: case h₁
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ jointlySurjectivePrecoverage ≤
    Precoverage.comap (forgetToTop ⋙ CategoryTheory.forget TopCat) Types.jointlySurjectivePrecoverage

Tactic:
forgetToTop_comp_forget

Goal state after:
case h₁
this : (precoverage IsOpenImmersion).PullbacksPreservedBy forgetToTop
⊢ jointlySurjectivePrecoverage ≤ Precoverage.comap forget Types.jointlySurjectivePrecoverage
Module: Mathlib.AlgebraicGeometry.Sites.BigZariski

Goal state before:
pp: P : MorphismProperty Scheme
F : Schemeᵒᵖ ⥤ Type u_1
inst✝¹ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : Finite 𝒰.I₀
this✝ : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
⊢ 𝒰.sigma.presieve₀ = Presieve.singleton (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f)

Tactic:
𝒰.presieve₀_sigma

Goal state after:
P : MorphismProperty Scheme
F : Schemeᵒᵖ ⥤ Type u_1
inst✝¹ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf zariskiTopology F
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : Finite 𝒰.I₀
this✝ : PreservesLimitsOfShape (Discrete (𝒰.I₀ × 𝒰.I₀)) F
this : PreservesLimitsOfShape (Discrete 𝒰.I₀) F
c : Cofan 𝒰.X := Cofan.mk (∐ 𝒰.X) (Sigma.ι 𝒰.X)
⊢ Presieve.singleton (Sigma.desc 𝒰.f) = Presieve.singleton (Cofan.IsColimit.desc (coproductIsCoproduct 𝒰.X) 𝒰.f)
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
this : A ≃ₐ[A] Localization.Away 1
⊢ smoothLocus R A = Set.univ ↔ FormallySmooth R A

Tactic:
Algebra.FormallySmooth.iff_of_equiv (this.restrictScalars R),

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
this : A ≃ₐ[A] Localization.Away 1
⊢ smoothLocus R A = Set.univ ↔ FormallySmooth R (Localization.Away 1)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case add
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
h : Algebra.IsPushout R S A B
x : S ⊗[R] Ω[A⁄R]
b₁ b₂ : B
e₁ : (LinearMap.liftBaseChange S (↑R (map R S A B))) (b₁ • x) = b₁ • (LinearMap.liftBaseChange S (↑R (map R S A B))) x
e₂ : (LinearMap.liftBaseChange S (↑R (map R S A B))) (b₂ • x) = b₂ • (LinearMap.liftBaseChange S (↑R (map R S A B))) x
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((b₁ + b₂) • x) =
    (b₁ + b₂) • (LinearMap.liftBaseChange S (↑R (map R S A B))) x

Tactic:
| add b₁ b₂ e₁ e₂ =>

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

Goal state before:
pp: case add
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
h : Algebra.IsPushout R S A B
b b₁ b₂ : B
e₁ :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (b₁ * b) =
    b₁ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b + b • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b₁
e₂ :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (b₂ * b) =
    b₂ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b + b • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b₂
⊢ (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((b₁ + b₂) * b) =
    (b₁ + b₂) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b + b • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (b₁ + b₂)

Tactic:
| add b₁ b₂ e₁ e₂ =>

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
x : AdicCauchySequence I N
n : ℕ
y yₙ : M
hy : f y = ↑x (n + 1)
hyₙ : f yₙ = ↑x n
⊢ ↑x (n + 1) - ↑x n ∈ I ^ n • ⊤

Tactic:
← SModEq.sub_mem

Goal state after:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
x : AdicCauchySequence I N
n : ℕ
y yₙ : M
hy : f y = ↑x (n + 1)
hyₙ : f yₙ = ↑x n
⊢ ↑x (n + 1) ≡ ↑x n [SMOD I ^ n • ⊤]
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:
by ext x; exact congr($(hf hle) x)

Goal state after:
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:
by ext x; exact congr($(hf hle) x)

Goal state after:
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:
by ext x; exact congr($(hf hle) x)

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

Goal state before:
pp: 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✝ : IsStandardSmooth R S
w✝² w✝¹ : Type
w✝ : Finite w✝¹
left✝ : Finite w✝²
P : SubmersivePresentation R S w✝² w✝¹
⊢ IsStandardSmooth R T

Tactic:
exact (P.ofAlgEquiv e).isStandardSmooth

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

Goal state before:
pp: ⊢ IsStableUnderBaseChange @IsStandardSmooth

Tactic:
apply IsStableUnderBaseChange.mk
  · exact isStandardSmooth_respectsIso
  · introv h
    replace h : Algebra.IsStandardSmooth R T := by
      rw [RingHom.IsStandardSmooth] at h; convert! h; ext; simp_rw [Algebra.smul_def]; rfl
    suffices Algebra.IsStandardSmooth S (S ⊗[R] T) by
      rw [RingHom.IsStandardSmooth]; convert! this; ext; simp_rw [Algebra.smul_def]; rfl
    infer_instance

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
D : DescentAux A B
⊢ D.P.coeffs ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)

Tactic:
by
    #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
    without the `rw`. It is not yet clear whether this is due to defeq abuse in Mathlib or a
    problem in the new canonicalizer; a minimization would help. The original proof was:
    `grind [subalgebra, Subalgebra.setRange_algebraMap, Algebra.subset_adjoin]` -/
    rw [Subalgebra.setRange_algebraMap]
    grind [subalgebra, Algebra.subset_adjoin]

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
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
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
h : ∃ p', p'.IsHomogeneous 1 ∧ (eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) p' = p i - X i
⊢ ↑(aeval p) (X i) - X i ∈ Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))

Tactic:
simpa [Ideal.mem_span_iff_exists_isHomogeneous, hp]

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✝ : Etale A B
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ Etale (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
simp only [Etale.iff_isStandardSmoothOfRelativeDimension_zero] at *
  exact IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg ..

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this : IsNoetherian X
x : ↥X
⊢ IsOpen (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ

Tactic:
by
      rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]
      exact TopologicalSpace.NoetherianSpace.finite_irreducibleComponents.sdiff.isClosed_biUnion
        fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion (pullback.diagonal f)
hY : ∃ R, Y = Spec R
⊢ FormallyUnramified f

Tactic:
obtain ⟨R, rfl⟩ := hY

Goal state after:
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : IsOpenImmersion (pullback.diagonal f)
⊢ FormallyUnramified f
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: 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✝² : Q.IsStableUnderBaseChange
inst✝¹ : P.HasOfPrecompProperty Q
inst✝ : P.RespectsRight Q
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
⊢ P g

Tactic:
apply P.of_precomp (W' := Q) _ _ (Q.of_isPullback h hf)
    rw [← h.1.1]
    exact RespectsRight.postcomp _ hf _ hfst

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
s : S
inst✝ : IsNoetherianRing R
H' : R⁰ ≤ Submonoid.comap (algebraMap R S) S⁰
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • s ^ n ∈ (algebraMap R S).range
f : ↥R[s] →ₗ[R] ↥(R ∙ Localization.Away.invSelf ((algebraMap R S) r)) :=
  (IsScalarTower.toAlgHom R S (Localization.Away ((algebraMap R S) r))).toLinearMap.restrict ⋯
⊢ Function.Injective ⇑(algebraMap S (Localization.Away ((algebraMap R S) r)))

Tactic:
apply IsLocalization.injective (M := .powers (algebraMap R S r))

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
s : S
inst✝ : IsNoetherianRing R
H' : R⁰ ≤ Submonoid.comap (algebraMap R S) S⁰
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • s ^ n ∈ (algebraMap R S).range
f : ↥R[s] →ₗ[R] ↥(R ∙ Localization.Away.invSelf ((algebraMap R S) r)) := ⋯
⊢ Submonoid.powers ((algebraMap R S) r) ≤ S⁰
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective ⇑((algebraMap K[X] K⟮X⟯).comp Polynomial.C)

Tactic:
RingHom.coe_comp

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective (⇑(algebraMap K[X] K⟮X⟯) ∘ ⇑Polynomial.C)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : p.natDegree = 0
⊢ IsAlmostIntegral R (p.coeff i)

pp: case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
· obtain ⟨p, rfl⟩ := natDegree_eq_zero.mp hp'
    simp only [coeff_C]
    split_ifs with h
    · simpa using H hp
    · exact (completeIntegralClosure R S).zero_mem

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
⊢ IsAlmostIntegral R (p.coeff i)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
hi : ¬i = p.natDegree
r : R
hr : r ∈ R⁰
hr' : ∀ (n : ℕ), r • p.leadingCoeff ^ n ∈ (algebraMap R S).range
⊢ C r ∈ R[X]⁰

Tactic:
simpa using hr

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
hY : ∃ R, Y = Spec R
hX : ∃ S, X = Spec S
⊢ id (IsLocallyArtinian X)

Tactic:
obtain ⟨R, rfl⟩ := hY

Goal state after:
X : Scheme
hX : ∃ S, X = Spec S
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian (Spec R)
⊢ id (IsLocallyArtinian X)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian Y
hY : ∃ R, Y = Spec R
⊢ id (IsFinite f)

Tactic:
obtain ⟨R, rfl⟩ := hY

Goal state after:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian (Spec R)
⊢ id (IsFinite f)