mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬constantCoeff (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
· rw [MvPowerSeries.inv_eq_iff_mul_eq_one h]
    simp only [not_or, map_mul, mul_eq_zero] at h
    rw [← mul_assoc, mul_assoc _⁻¹, MvPowerSeries.inv_mul_cancel _ h.left, mul_one,
      MvPowerSeries.inv_mul_cancel _ h.right]

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

Goal state before:
pp: k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬constantCoeff f = 0
hfI : f ∈ I
this : C (f 0) = f - (f - C (f 0))
⊢ constantCoeff (f - C (f 0)) = 0

Tactic:
map_sub,

Goal state after:
k : Type u_2
inst✝ : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬constantCoeff f = 0
hfI : f ∈ I
this : C (f 0) = f - (f - C (f 0))
⊢ constantCoeff f - constantCoeff (C (f 0)) = 0
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
⊢ (mk v).maximalIdeal = v

Tactic:
rw [← mk_eq_iff, mk_maximalIdeal]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
h_x_nezero : x ≠ 0
⊢ Function.HasFiniteMulSupport fun w ↦ w x

Tactic:
by
  rcases IsFractionRing.div_surjective (𝓞 K) x with ⟨a, b, hb, rfl⟩
  simp_all only [ne_eq, div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or, map_div₀]
  obtain ⟨ha, hb⟩ := h_x_nezero
  simp_rw [← RingOfIntegers.coe_eq_algebraMap]
  fun_prop

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
inst✝ : IsEmpty ↥X
⊢ ⊥ ∈ (grothendieckTopology P) X

Tactic:
← Sieve.generate_bot

Goal state after:
P : MorphismProperty Scheme
X : Scheme
inst✝ : IsEmpty ↥X
⊢ Sieve.generate ⊥ ∈ (grothendieckTopology P) X
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:
polynomialY_eq

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) (C 2 * Y * Z + C W'.a₁ * X * Z + C W'.a₃ * Z ^ 2) = 2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomialY = (MvPolynomial.map ↑f) (W'⁄A).polynomialY

Tactic:
← map_polynomialY,

Goal state after:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomialY = ((W'⁄A).map ↑f).polynomialY
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_1.refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
i j : 𝒰.I₀
y : ↑Y
xi : ↑(𝒰.X i)
hi : (ConcreteCategory.hom (𝒰.f i)) xi = y
xj : ↑(𝒰.X j)
hj : (ConcreteCategory.hom (𝒰.f j)) xj = y
⊢ (Hom.hom (x i)) (⋯.toHomeomorph.symm ⟨y, ⋯⟩) = (Hom.hom (x j)) (⋯.toHomeomorph.symm ⟨y, ⋯⟩)

Tactic:
conv_lhs => simp only [← hi]

Goal state after:
case refine_1.refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
i j : 𝒰.I₀
y : ↑Y
xi : ↑(𝒰.X i)
hi : (ConcreteCategory.hom (𝒰.f i)) xi = y
xj : ↑(𝒰.X j)
hj : (ConcreteCategory.hom (𝒰.f j)) xj = y
⊢ (Hom.hom (x i)) (⋯.toHomeomorph.symm ⟨(ConcreteCategory.hom (𝒰.f i)) xi, ⋯⟩) =
    (Hom.hom (x j)) (⋯.toHomeomorph.symm ⟨y, ⋯⟩)
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.FinitePresentation

Tactic:
exact hf.2

Goal state after:
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.Smooth
⊢ f.FinitePresentation

Tactic:
by
  rw [smooth_def] at hf
  exact hf.2

Goal state after:
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
Af : Type u_3
inst✝⁴ : CommRing Af
inst✝³ : Algebra A Af
inst✝² : Algebra R Af
inst✝¹ : IsScalarTower R A Af
f : A
inst✝ : IsLocalization.Away f Af
p : PrimeSpectrum Af
q : PrimeSpectrum A := PrimeSpectrum.comap (algebraMap A Af) p
⊢ p ∈ PrimeSpectrum.comap (algebraMap A Af) ⁻¹' smoothLocus R A ↔ p ∈ smoothLocus R Af

Tactic:
have : IsLocalization.AtPrime (Localization.AtPrime p.asIdeal) q.asIdeal :=
    IsLocalization.isLocalization_isLocalization_atPrime_isLocalization (.powers f) _ p.asIdeal

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
Af : Type u_3
inst✝⁴ : CommRing Af
inst✝³ : Algebra A Af
inst✝² : Algebra R Af
inst✝¹ : IsScalarTower R A Af
f : A
inst✝ : IsLocalization.Away f Af
p : PrimeSpectrum Af
q : PrimeSpectrum A := PrimeSpectrum.comap (algebraMap A Af) p
this : IsLocalization.AtPrime (Localization.AtPrime p.asIdeal) q.asIdeal
⊢ p ∈ PrimeSpectrum.comap (algebraMap A Af) ⁻¹' smoothLocus R A ↔ p ∈ smoothLocus R Af
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
g : (i : I) → f i
⊢ (Ideal.Quotient.mk J) (f₁ g - f₂ g) = 0

Tactic:
map_sub,

Goal state after:
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
g : (i : I) → f i
⊢ (Ideal.Quotient.mk J) (f₁ g) - (Ideal.Quotient.mk J) (f₂ g) = 0
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case w.hy
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (Ideal.Quotient.mk I) u * 0 = 0

Tactic:
mul_zero

Goal state after:
case w.hy
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ 0 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
⊢ W.dblU (u • P) = u ^ 4 * W.dblU P

Tactic:
by
  simp [field, dblU_eq]

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ P z * 0 = 0

Tactic:
mul_zero

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ 0 = 0
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h✝ : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
x y : L
h : x ∈ K⟮y⟯
e : K⟮x⟯ ≤ K⟮y⟯
⊢ ∀ (x_1 : ↥K⟮x⟯),
    ((Ideal.Quotient.mkₐ K I).comp ((g y).comp (IntermediateField.inclusion e))) x_1 =
      (f.comp (IsScalarTower.toAlgHom K (↥K⟮x⟯) L)) x_1

Tactic:
← AlgHom.comp_assoc,

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h✝ : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
x y : L
h : x ∈ K⟮y⟯
e : K⟮x⟯ ≤ K⟮y⟯
⊢ ∀ (x_1 : ↥K⟮x⟯),
    (((Ideal.Quotient.mkₐ K I).comp (g y)).comp (IntermediateField.inclusion e)) x_1 =
      (f.comp (IsScalarTower.toAlgHom K (↥K⟮x⟯) L)) x_1
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
A : Type u
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K L
inst✝³ : Algebra K A
inst✝² : EssFiniteType K A
inst✝¹ : FormallyEtale K A
p : Ideal A
inst✝ : p.IsPrime
⊢ Algebra.IsSeparable K (A ⧸ p)

Tactic:
have := Algebra.FormallyUnramified.finite_of_free K A

Goal state after:
K : Type u_1
L : Type u_2
A : Type u
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K L
inst✝³ : Algebra K A
inst✝² : EssFiniteType K A
inst✝¹ : FormallyEtale K A
p : Ideal A
inst✝ : p.IsPrime
this : Module.Finite K A
⊢ Algebra.IsSeparable K (A ⧸ p)
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
s : A
a : S
x : S ⊗[R] Ω[A⁄R]
⊢ s • a • x = a • s • x

Tactic:
← smul_comm

Goal state after:
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
s : A
a : S
x : S ⊗[R] Ω[A⁄R]
⊢ a • s • x = a • s • x
Module: Mathlib.RingTheory.Smooth.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Flat R S
inst✝⁴ : FinitePresentation R S
p : Ideal R
q : Ideal S
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom ⋯
algInst✝ : Algebra Sp Sq := f.toAlgebra
this : IsScalarTower R Sp Sq
⊢ IsSmoothAt R q

Tactic:
have : IsScalarTower Rp Sp Sq := .of_algebraMap_eq' <| by
    apply IsLocalization.ringHom_ext p.primeCompl
    simp only [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Flat R S
inst✝⁴ : FinitePresentation R S
p : Ideal R
q : Ideal S
inst✝³ : p.IsPrime
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom ⋯
algInst✝ : Algebra Sp Sq := f.toAlgebra
this✝ : IsScalarTower R Sp Sq
this : IsScalarTower Rp Sp Sq
⊢ IsSmoothAt R q
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
⊢ f (yₙ - y) ∈ I ^ n • ⊤

Tactic:
map_sub,

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
⊢ f yₙ - f y ∈ I ^ 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
x : M
hx : x ∈ I • ⊤
⊢ x ∈ Submodule.comap f (I • ⊤)

Tactic:
refine Submodule.smul_induction_on hx (fun r hr x _ ↦ ?_) (fun x y hx hy ↦ ?_)
        · simp [Submodule.smul_mem_smul hr Submodule.mem_top]
        · simp [Submodule.add_mem _ hx hy]

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

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R ⧸ I • ⊤
b₁ b₂ : R
h : b₁ ≈ b₂
a✝ : M
⊢ b₁ • Quotient.mk'' a✝ = b₂ • Quotient.mk'' a✝

Tactic:
have h : b₁ - b₂ ∈ (I : Submodule R R) := by
        rwa [show I = I • ⊤ by simp, ← Submodule.quotientRel_def]

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R ⧸ I • ⊤
b₁ b₂ : R
h✝ : b₁ ≈ b₂
a✝ : M
h : b₁ - b₂ ∈ I
⊢ b₁ • Quotient.mk'' a✝ = b₂ • Quotient.mk'' a✝
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: case smul
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
y : K
x : M
a✝¹ : R
x✝ : M
hx✝ : x✝ ∈ Submodule.span R (Set.range (v ∘ a))
a✝ : s x✝ = 0
⊢ s (a✝¹ • x✝) = 0

Tactic:
| smul =>

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

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
⊢ (MvPolynomial.aeval P.val) (P.jacobianOfHasCoeffs R₀) = P.jacobian

Tactic:
let : Fintype σ := Fintype.ofFinite _

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₀ : Type u_5
inst✝⁴ : CommRing R₀
inst✝³ : Algebra R₀ R
inst✝² : Algebra R₀ S
inst✝¹ : IsScalarTower R₀ R S
inst✝ : P.HasCoeffs R₀
this : Fintype σ := Fintype.ofFinite σ
⊢ (MvPolynomial.aeval P.val) (P.jacobianOfHasCoeffs R₀) = P.jacobian
Module: Mathlib.RingTheory.Extension.Presentation.Core

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P✝ : Presentation R S ι σ
inst✝⁶ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁵ : CommRing R₀
inst✝⁴ : Algebra R₀ R
inst✝³ : Algebra R₀ S
inst✝² : IsScalarTower R₀ R S
inst✝¹ : P.HasCoeffs R₀
inst✝ : FaithfulSMul R₀ R
⊢ IsUnit (P.ofHasCoeffs R₀).jacobian

Tactic:
let : Fintype σ := Fintype.ofFinite _

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P✝ : Presentation R S ι σ
inst✝⁶ : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst✝⁵ : CommRing R₀
inst✝⁴ : Algebra R₀ R
inst✝³ : Algebra R₀ S
inst✝² : IsScalarTower R₀ R S
inst✝¹ : P.HasCoeffs R₀
inst✝ : FaithfulSMul R₀ R
this : Fintype σ := Fintype.ofFinite σ
⊢ IsUnit (P.ofHasCoeffs R₀).jacobian
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
⊢ P.sectionCotangent x = y ↔ ∀ (i : σ), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i

Tactic:
by
  simp only [sectionCotangent, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply]
  rw [← (cotangentEquiv P).injective.eq_iff, funext_iff, LinearEquiv.apply_symm_apply]
  simp

Goal state after:
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 ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
⊢ (localizationAway T g).ker =
    Ideal.span {((localizationAway T g).ofComp P).toAlgHom ((rename Sum.inr) f * X (Sum.inl ()) - 1)}

Tactic:
map_sub,

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 ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
⊢ (localizationAway T g).ker =
    Ideal.span
      {((localizationAway T g).ofComp P).toAlgHom ((rename Sum.inr) f * X (Sum.inl ())) -
          ((localizationAway T g).ofComp P).toAlgHom 1}
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) ((rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1) = 0

Tactic:
map_sub,

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 ι
⊢ (compLocalizationAwayAlgHom T g P) ((rename Sum.inr) (P.σ g) * X (Sum.inl ())) -
      (compLocalizationAwayAlgHom T g P) 1 =
    0
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).IsStandardSmooth ↔ Algebra.IsStandardSmooth R S

Tactic:
by
  rw [RingHom.IsStandardSmooth, toAlgebra_algebraMap]

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.negAddY P Q = P y ^ 2 * Q z * W'.negY Q

Tactic:
rw [negAddY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, negY]
  ring1

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ HasOfPostcompProperty @Etale @Etale

Tactic:
apply MorphismProperty.HasOfPostcompProperty.of_le (W := @Etale)
    (Q := (@LocallyOfFiniteType ⊓ @FormallyUnramified))
  intro X Y f hf
  constructor <;> infer_instance

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

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
X : Scheme
inst✝² : CompactSpace ↥X
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun i ↦ 𝒰.X i) ⟶ X := Sigma.desc fun i ↦ 𝒰.f i
x : ↥X
⊢ ∃ a, p a = x

Tactic:
obtain ⟨i, x, rfl⟩ := X.affineCover.finiteSubcover.exists_eq x
    use Sigma.ι X.affineCover.finiteSubcover.X i x
    rw [← Scheme.Hom.comp_apply, Sigma.ι_desc]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Defs

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : K[X]
hq : q ≠ 0
⊢ RatFunc.mk p q = { toFractionRing := Localization.mk p ⟨q, ⋯⟩ }

Tactic:
by
  rw [mk_def_of_ne _ hq, Localization.mk_eq_mk']

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Defs

Goal state before:
pp: case pos
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H' : ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
hq : q = 0
⊢ (RatFunc.mk p q).liftOn f H = f p q

Tactic:
subst hq
    simp only [mk_zero, f0, ← Localization.mk_zero 1,
      liftOn_ofFractionRing_mk, Submonoid.coe_one]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
r : K
x : K⟮X⟯
⊢ (algebraMap K K⟮X⟯) r * x = C r * x

Tactic:
algebraMap_eq_C

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
r : K
x : K⟮X⟯
⊢ C r * x = C r * x