mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝² : PartialOrder Γ
inst✝¹ : AddCommMonoid R
M : Type ?u.14
inst✝ : SMulZeroClass M R
r : M
t : SummableFamily Γ R β
⊢ ∀ (g : Γ), {a | ((r • ⇑t) a).coeff g ≠ 0}.Finite

Tactic:
by
        intro g
        refine (t.finite_co_support g).subset ?_
        intro i hi
        simp only [Pi.smul_apply, coeff_smul, ne_eq, Set.mem_ofPred_eq] at hi
        simp only [Function.mem_support, ne_eq]
        exact right_ne_zero_of_smul hi

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
⊢ (⋃ a, (f a • s a).support).IsPWO

Tactic:
by
    refine Set.IsPWO.mono s.isPWO_iUnion_support fun g hg => ?_
    simp_all only [Set.mem_iUnion, mem_support, coeff_smul, ne_eq]
    obtain ⟨i, hi⟩ := hg
    exact Exists.intro i <| right_ne_zero_of_smul hi

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
i : α
hi : i ∈ {a | (f a • s a).coeff g ≠ 0}
⊢ i ∈ Function.support fun a ↦ (s a).coeff g

Tactic:
simp_all only [coeff_smul, ne_eq, Set.mem_ofPred_eq, Function.mem_support]

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : PartialOrder Γ
inst✝² : AddCommMonoid R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : α → R
s : SummableFamily Γ V α
g : Γ
i : α
hi : ¬f i • (s i).coeff g = 0
⊢ ¬(s i).coeff g = 0
Module: Mathlib.RingTheory.HopfAlgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a✝ b : A
a : GroupLike R A
⊢ a⁻¹ * a = 1

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
x✝ :
  ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
f : R[X]
hf : f.Monic
a₀ : R
h₂ : IsUnit (Polynomial.eval a₀ (derivative f))
H :
  (residue R) (Polynomial.eval a₀ f) = 0 →
    (residue R) (Polynomial.eval a₀ (derivative f)) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = (residue R) a₀
h₁ : (Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ f) = 0
aux : (Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f)) = 0 → False
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal R

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := H h₁ aux

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
x✝ :
  ∀ (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
f : R[X]
hf : f.Monic
a₀ : R
h₂ : IsUnit (Polynomial.eval a₀ (derivative f))
H :
  (residue R) (Polynomial.eval a₀ f) = 0 →
    (residue R) (Polynomial.eval a₀ (derivative f)) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = (residue R) a₀
h₁ : (Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ f) = 0
aux : (Ideal.Quotient.mk (maximalIdeal R)) (Polynomial.eval a₀ (derivative f)) = 0 → False
a : R
ha₁ : f.IsRoot a
ha₂ : (residue R) a = (residue R) a₀
⊢ ∃ a, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal R
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h✝ : Nontrivial R
⊢ IsUnit x

Tactic:
refine isUnit_of_isUnit_leadingCoeff_AddUnitOrder ?_ ?_

Goal state after:
case inr.refine_1
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h✝ : Nontrivial R
⊢ IsUnit x.leadingCoeff

case inr.refine_2
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h✝ : Nontrivial R
⊢ IsAddUnit x.order
Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
n : ℤ
⊢ (antipode R) (C a * T n) = C ((antipode R) a) * T (-n)

Tactic:
by
  simp [← single_eq_C_mul_T]

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : HopfAlgebraStruct R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Ideal.IsHopfIdeal R I
⊢ antipode R ∘ₗ (mkₐ R I).toLinearMap = (mkₐ R I).toLinearMap ∘ₗ antipode R

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.ClopenNhdofOne

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : g ∈ sInf {N | IsOpen ↑N ∧ ↑H ≤ N}
hg_not : g ∉ ↑H
U : Set G := (g • ↑H)ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : ↑N ⊆ U
NH : Subgroup G := ↑N.toOpenSubgroup ⊔ ↑H
hg' : g ∈ NH
⊢ False

Tactic:
rcases Subgroup.mem_sup_of_normal_left.mp hg' with ⟨y, hy, z, hz, hyz⟩

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : g ∈ sInf {N | IsOpen ↑N ∧ ↑H ≤ N}
hg_not : g ∉ ↑H
U : Set G := (g • ↑H)ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : ↑N ⊆ U
NH : Subgroup G := ↑N.toOpenSubgroup ⊔ ↑H
hg' : g ∈ NH
y : G
hy : y ∈ ↑N.toOpenSubgroup
z : G
hz : z ∈ ↑H
hyz : y * z = g
⊢ False
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
U : Set ↑(limit P.diagram).toProfinite.toTop
s : Set ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux P.diagram
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ : (a : OpenNormalSubgroup ↑P.toProfinite.toTop) → Set ↑(P.diagram.obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
⊢ (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty

Tactic:
have hM : M.Normal := Subgroup.normal_iInf_normal fun j => j.1.isNormal'

Goal state after:
P : ProfiniteGrp.{u}
U : Set ↑(limit P.diagram).toProfinite.toTop
s : Set ((j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : OpenNormalSubgroup ↑P.toProfinite.toTop) → ↑(P.diagram.obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux P.diagram
uDefaultSpec : spc ∈ s
J : Finset (OpenNormalSubgroup ↑P.toProfinite.toTop)
fJ : (a : OpenNormalSubgroup ↑P.toProfinite.toTop) → Set ↑(P.diagram.obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ spc a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑P.toProfinite.toTop := ⨅ j, ↑(↑j).toOpenSubgroup
hM : M.Normal
⊢ (U ∩ Set.range ⇑(Hom.hom P.toLimit)).Nonempty
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ p.height ≤ ↑(Submodule.spanFinrank I)

Tactic:
convert_to! p.height ≤ I.spanRank.toENat

Goal state after:
case e'_4
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ ↑(Submodule.spanFinrank I) = Cardinal.toENat (Submodule.spanRank I)

case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ ↑p.height
hs : (Submodule.generators I).Finite
⊢ p.height ≤ Cardinal.toENat (Submodule.spanRank I)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
⊢ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height ≤ P.height

Tactic:
have : l'.head.asIdeal.LiesOver lp.last.asIdeal := by
    simp only [LTSeries.head_map, hlp, l']
    refine ⟨?_⟩
    refine le_antisymm ?_ ?_
    · rw [← map_le_iff_le_comap, PrimeSpectrum.comap_asIdeal, ← map_le_iff_le_comap]
      simp
    · conv_rhs => rw [LiesOver.over (p := p) (P := P), under_def]
      refine comap_mono (le_trans (comap_mono (lq.head_le_last)) ?_)
      simp [hlq, map_le_iff_le_comap, LiesOver.over (p := p) (P := P)]

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
this : (RelSeries.head l').asIdeal.LiesOver (RelSeries.last lp).asIdeal
⊢ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height ≤ P.height
Module: Mathlib.RingTheory.LocalProperties.Injective

Goal state before:
pp: R : Type u
inst✝¹² : CommRing R
M : Type v
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u'
inst✝⁹ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁸ : ∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (Rₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type v'
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝² : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Rₚ I) (Mₚ I)
⊢ Injective R M

Tactic:
apply Module.injective_of_localization_maximal
  intro P hP
  refine Module.Injective.of_ringEquiv (M := Mₚ P)
    (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv
    { __ := IsLocalizedModule.linearEquiv P.primeCompl (f P)
        (LocalizedModule.mkLinearMap P.primeCompl M)
      map_smul' := ?_ }
  · intro r m
    obtain ⟨r, s, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl r
    apply ((Module.End.isUnit_iff _).mp
      (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap P.primeCompl M) s)).1
    dsimp
    simp only [← map_smul, ← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul,
      IsLocalization.map_id_mk']

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
ei : EnoughInjectives (ModuleCat R)
I : ModuleCat R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat R) := { X₁ := M, X₂ := I, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
S_exact : S.ShortExact
Sp : (m : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization m.asIdeal.primeCompl)) :=
  fun m ↦ S.map (localizedModuleFunctor m.asIdeal.primeCompl)
Sp_exact : ∀ (m : MaximalSpectrum R), (Sp m).ShortExact
⊢ HasInjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)

Tactic:
have ih' := ih S.X₃

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
ei : EnoughInjectives (ModuleCat R)
I : ModuleCat R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat R) := { X₁ := M, X₂ := I, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
S_exact : S.ShortExact
Sp : (m : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization m.asIdeal.primeCompl)) :=
  fun m ↦ S.map (localizedModuleFunctor m.asIdeal.primeCompl)
Sp_exact : ∀ (m : MaximalSpectrum R), (Sp m).ShortExact
ih' :
  HasInjectiveDimensionLE S.X₃ n ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (S.X₃.localizedModule m.asIdeal.primeCompl) n
⊢ HasInjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) (n + 1)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case negSucc
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ (Valued.v ((single (-(↑s + 1))) 1))⁻¹ = (exp (- -(↑s + 1)))⁻¹

Tactic:
← map_inv₀,

Goal state after:
case negSucc
K : Type u_2
inst✝ : Field K
s : ℕ
⊢ Valued.v ((single (-(↑s + 1))) 1)⁻¹ = (exp (- -(↑s + 1)))⁻¹
Module: Mathlib.RingTheory.LocalRing.Pullback

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Semiring T
f : R →+* T
g : S →+* T
a : R × S
a_in : a ∈ f.pullback g
⊢ IsUnit ⟨a, a_in⟩ ↔ IsUnit a.1 ∧ IsUnit a.2

Tactic:
rw [isUnit_eqLocus_mk_iff, Prod.isUnit_iff]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case zero
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ.totalDegree = 0
⊢ ((pderiv i) φ).IsHomogeneous (0 - 1)

Tactic:
totalDegree_eq_zero_iff_eq_C

Goal state after:
case zero
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ = C (coeff 0 φ)
⊢ ((pderiv i) φ).IsHomogeneous (0 - 1)
Module: Mathlib.RingTheory.Localization.AtPrime.Extension

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
R₁ : Type u_4 := Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P)
⊢ (length (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))
        (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P) ⧸
          Ideal.map (algebraMap Rₚ (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))) (maximalIdeal Rₚ))).toNat =
    (length (Localization.AtPrime P)
        (Localization.AtPrime P ⧸ Ideal.map (algebraMap R (Localization.AtPrime P)) p)).toNat

Tactic:
let R₂ := Localization.AtPrime P

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
p : Ideal R
inst✝¹² : p.IsPrime
Rₚ : Type u_3
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : Algebra R Rₚ
inst✝⁹ : IsLocalization.AtPrime Rₚ p
inst✝⁸ : IsLocalRing Rₚ
Sₚ : Type u_4
inst✝⁷ : CommRing Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
P : Ideal S
hPp : P.LiesOver p
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsScalarTower R Rₚ Sₚ
inst✝ : P.IsPrime
this✝¹ : (Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)
this✝ : (Ideal.map (algebraMap S Sₚ) P).LiesOver P
this : (Ideal.map (algebraMap S Sₚ) P).IsPrime
R₁ : Type u_4 := Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P)
R₂ : Type u_2 := Localization.AtPrime P
⊢ (length (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))
        (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P) ⧸
          Ideal.map (algebraMap Rₚ (Localization.AtPrime (Ideal.map (algebraMap S Sₚ) P))) (maximalIdeal Rₚ))).toNat =
    (length (Localization.AtPrime P)
        (Localization.AtPrime P ⧸ Ideal.map (algebraMap R (Localization.AtPrime P)) p)).toNat
Module: Mathlib.RingTheory.MvPolynomial.Expand

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k)) f) = f ^ p ^ k
⊢ (map (frobenius R p)) ((expand p) ((map (iterateFrobenius R p k)) ((expand (p ^ k)) f))) =
    (map (iterateFrobenius R p (k + 1))) ((expand (p * p ^ k)) f)

Tactic:
add_comm k,

Goal state after:
case succ
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : MvPolynomial σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k)) f) = f ^ p ^ k
⊢ (map (frobenius R p)) ((expand p) ((map (iterateFrobenius R p k)) ((expand (p ^ k)) f))) =
    (map (iterateFrobenius R p (1 + k))) ((expand (p * p ^ k)) f)
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ (if hi : (Iic ⟨i, him⟩ \ t).min' hne ∈ t then 1 else 0) <
    if hi : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ then 1 else 0

Tactic:
· rw [dif_neg hkm.2, dif_pos hkm.1]; exact Nat.zero_lt_one

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
⊢ ⇑(Finsupp.indicator (Iic ⟨↑i, him⟩) fun x x_1 ↦ 1) = (accumulate n m) ⇑fun₀ | i => 1

Tactic:
ext j

Goal state after:
R : Type u_3
n m : ℕ
inst✝¹ : CommSemiring R
i : Fin n
inst✝ : Nontrivial R
him : ↑i < m
j : Fin m
⊢ (Finsupp.indicator (Iic ⟨↑i, him⟩) fun x x_1 ↦ 1) j = (accumulate n m) (⇑fun₀ | i => 1) j
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w✝ : Set K⟮X⟯
hT : w✝ ∈ nhds 0
pre_T : (fun x ↦ x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < embedding ↑d}
X_def : X = {f | Valued.v f < embedding ↑d}
x : K⟮X⟯
hx : (restrict₀ (MonoidWithZeroHom.ofClass Valued.v)) x = ↑d
⊢ Valued.v.restrict ((algebraMap K⟮X⟯ K⸨X⸩) x) ≠ 0

Tactic:
simp only [ne_eq, map_eq_zero]
          intro h
          simp only [h, map_zero] at hx
          exact Units.ne_zero _ hx.symm

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x✝¹ x✝ : ↑M
⊢ (fun i ↦ ⟨single j i 1 • (x✝¹ + x✝), ⋯⟩) = (fun i ↦ ⟨single j i 1 • x✝¹, ⋯⟩) + fun i ↦ ⟨single j i 1 • x✝, ⋯⟩

Tactic:
by ext; simp

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

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
⊢ (map (frobenius R p)) ((expand p hp) ((map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f))) =
    (map (iterateFrobenius R p (k + 1))) ((expand (p * p ^ k) ⋯) f)

Tactic:
add_comm k,

Goal state after:
case succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
⊢ (map (frobenius R p)) ((expand p hp) ((map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f))) =
    (map (iterateFrobenius R p (1 + k))) ((expand (p * p ^ k) ⋯) f)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ (map f) (W_ R n) = W_ S n

Tactic:
rw [wittPolynomial, map_sum, wittPolynomial]
  refine sum_congr rfl fun i _ => ?_
  rw [map_monomial, map_pow, map_natCast]

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w ↦ (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial x') (MvPolynomial.coeff x' f)))).natDegree ≤
      ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).natDegree
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
h1 : x ∈ f.support
h2 : x ∉ {v}
⊢ ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial x) (MvPolynomial.coeff x f)))).natDegree ≠
    ((MvPolynomial.finSuccEquiv k n) ((T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).natDegree

Tactic:
simpa only [natDegree_finSuccEquiv]
      using degreeOf_t_ne_of_ne f _ _ h1 vin <| ne_of_not_mem_cons h2

Goal state after: