mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Flat.Domain

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁴ : AddCommGroup P
inst✝³ : Module R P
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst✝ : Module.Flat R Q
hf : Injective ⇑f
hg : Injective ⇑g
K : Type u_1 := FractionRing R
H₁ : Injective ⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g))
H₂ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm
H₃ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N)
H₄ : Injective ⇑(AlgebraTensorModule.assoc R R K K P Q).symm
H₅ : Injective ⇑(AlgebraTensorModule.assoc R R K K M N)
H₆ : Injective ⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K))
H₇ : Injective ⇑(TensorProduct.lid R (P ⊗[R] Q)).symm
⊢ ⇑((mk R K (M ⊗[R] N)) 1 ∘ₗ map f g) =
    ⇑(↑R ↑(AlgebraTensorModule.assoc R R K K M N) ∘ₗ
        ↑R ↑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N) ∘ₗ
          ↑R (map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) ∘ₗ
            ↑R ↑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm ∘ₗ
              ↑R ↑(AlgebraTensorModule.assoc R R K K P Q).symm ∘ₗ
                LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K) ∘ₗ ↑(TensorProduct.lid R (P ⊗[R] Q)).symm)

Tactic:
congr! 1

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁴ : AddCommGroup P
inst✝³ : Module R P
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst✝ : Module.Flat R Q
hf : Injective ⇑f
hg : Injective ⇑g
K : Type u_1 := FractionRing R
H₁ : Injective ⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g))
H₂ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm
H₃ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N)
H₄ : Injective ⇑(AlgebraTensorModule.assoc R R K K P Q).symm
H₅ : Injective ⇑(AlgebraTensorModule.assoc R R K K M N)
H₆ : Injective ⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K))
H₇ : Injective ⇑(TensorProduct.lid R (P ⊗[R] Q)).symm
⊢ (mk R K (M ⊗[R] N)) 1 ∘ₗ map f g =
    ↑R ↑(AlgebraTensorModule.assoc R R K K M N) ∘ₗ
      ↑R ↑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N) ∘ₗ
        ↑R (map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) ∘ₗ
          ↑R ↑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm ∘ₗ
            ↑R ↑(AlgebraTensorModule.assoc R R K K P Q).symm ∘ₗ
              LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K) ∘ₗ ↑(TensorProduct.lid R (P ⊗[R] Q)).symm
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ (extendedHom A B) (mk0 I) = mk0 (extendedIdeal A B I)

Tactic:
rw [mk0_eq_quotientMk, mk0_eq_quotientMk, extendedHom_quotientMk]

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
I : ↥(Ideal A)⁰
⊢ ↑((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) ((FractionalIdeal.mk0 (FractionRing A)) I)) =
    ↑((FractionalIdeal.mk0 (FractionRing B)) (extendedIdeal A B I))
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
g : M
⊢ IsGroupLikeElem R ((fun x ↦ single x 1) g)

Tactic:
exact isGroupLikeElem_single_one _

Goal state after:
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝¹ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) := Nₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) := Mₚ ⧸ maximalIdeal (Localization.AtPrime p) • ⊤
x✝ : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this✝ : (maximalIdeal (Localization.AtPrime p)).IsPrime ∧ ∃ x, maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
x : LocalizedModule.AtPrime p M
hx : maximalIdeal (Localization.AtPrime p) = ⊥.colon {x}
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField := to_res' ∘ₗ (maximalIdeal (Localization.AtPrime p) • ⊤).mkQ
⊢ ⊥.colon {x} = (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x).ker

Tactic:
by simp [SetLike.ext_iff]

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case h.C
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
h_C : ∀ (a : R), P ↑(C a)
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
a : R
⊢ P ↑(C a)

Tactic:
| C a =>

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ ↑(X (n, x + y)) = ↑(∑ i ∈ antidiagonal n, X (i.1, x) * X (i.2, y))

Tactic:
exact Quotient.sound <| RingCon.le_ringConGen _ _ Rel.add

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ 0 = ↑(#(∅.sym n))

Tactic:
eq_comm,

Goal state after:
case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ ↑(#(∅.sym n)) = 0
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case a
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| ⊤ = Ideal.ofList (r :: rs) • ⊤

Tactic:
eq_comm,

Goal state after:
case a
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| Ideal.ofList (r :: rs) • ⊤ = ⊤
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case b
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| ⊤ = Ideal.ofList rs • ⊤

Tactic:
eq_comm,

Goal state after:
case b
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| Ideal.ofList rs • ⊤ = ⊤
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case succ
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
n : ℕ
h : ↑n ! * dp R n x = dp R 1 x ^ n
⊢ ↑(n + 1)! * dp R (n + 1) x = dp R 1 x ^ (n + 1)

Tactic:
rw [pow_succ, ← h, mul_assoc, dp_mul, nsmul_eq_mul, ← mul_assoc, ← Nat.cast_mul]
    simp [mul_comm _ (n + 1), Nat.factorial_succ]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ antidiagonal n, dpow k.1 x * dpow k.2 y
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
x : ι → M
hx : ∀ i ∈ s, x i ∈ I
n : ℕ
⊢ dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)

Tactic:
by
  simp only [sum_antidiagonal_eq_sum_range_succ_mk] at dpow_add
  induction s using Finset.induction generalizing n with
  | empty =>
    simp only [sum_empty, prod_empty, sum_const, nsmul_eq_mul, mul_one]
    by_cases hn : n = 0
    · rw [hn]
      rw [dpow_zero I.zero_mem]
      simp only [sym_zero, card_singleton, cast_one]
    · rw [dpow_eval_zero hn, eq_comm, ← cast_zero]
      apply congr_arg
      rw [card_eq_zero, sym_eq_empty]
      exact ⟨hn, rfl⟩
  | insert a s ha ih =>
    -- This should be golfable using `Finset.symInsertEquiv`
    have hx' : ∀ i, i ∈ s → x i ∈ I := fun i hi ↦ hx i (mem_insert_of_mem hi)
    simp_rw [sum_insert ha,
      dpow_add (hx a (mem_insert_self a s)) (I.sum_mem fun i ↦ hx' i),
      sum_range, ih hx', mul_sum, sum_sigma', eq_comm]
    apply sum_bij'
      (fun m _ ↦ m.filterNe a)
      (fun m _ ↦ m.2.fill a m.1)
      (fun m hm ↦ mem_sigma.2 ⟨mem_univ _, _⟩)
      (fun m hm ↦ by
        simp only [succ_eq_add_one, mem_sym_iff, mem_insert, Sym.mem_fill_iff]
        simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
        intro b
        apply Or.imp (fun h ↦ h.2) (fun h ↦ hm b h))
      (fun m _ ↦ m.fill_filterNe a)
    · intro m hm
      simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
      exact Sym.filter_ne_fill a m fun a_1 ↦ ha (hm a a_1)
    · intro m hm
      simp only [mem_sym_iff, mem_insert] at hm
      rw [prod_insert ha]
      apply congr_arg₂ _ rfl
      apply prod_congr rfl
      intro i hi
      apply congr_arg₂ _ _ rfl
      conv_lhs => rw [← m.fill_filterNe a]
      exact Sym.count_coe_fill_of_ne (ne_of_mem_of_not_mem hi ha)
    · intro m hm
      convert! sym_filterNe_mem a hm
      rw [erase_insert ha]

Goal state after:
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
h : ⊤ = ⊥
⊢ False

Tactic:
eq_comm,

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
h : ⊥ = ⊤
⊢ False
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hJ : DividedPowers J
⊢ ofRingEquiv h (ofRingEquiv ⋯ hJ) = hJ

Tactic:
by ext n b; simp [ofRingEquiv]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
hnorm : 0 < ‖↑n !‖
⊢ 1 < ↑p

Tactic:
exact_mod_cast Nat.Prime.one_lt hp.elim

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
I : Ideal R
inst✝¹ : DecidablePred fun x ↦ x ∈ I
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ʳ * x ^ n

Tactic:
eq_comm,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
I : Ideal R
inst✝¹ : DecidablePred fun x ↦ x ∈ I
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ (↑n !)⁻¹ʳ * x ^ n = hI.dpow n x
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ x ∈ I → ∃ a, ε * a = x

Tactic:
eq_comm,

Goal state after:
case refine_1
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ x ∈ I → ∃ a, x = ε * a
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ (∃ a, ε * a = x) → x ∈ I

Tactic:
eq_comm,

Goal state after:
case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
x : K[ε]
⊢ (∃ a, x = ε * a) → x ∈ I
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ ↑P.cotangentExtendScalarsEquiv ∘ₗ
      h1Cotangentι ∘ₗ
        H1Cotangent.map
          ((defaultHom P.Ring S P.extendScalars).comp
            ((Generators.self R S).defaultHom (Generators.self P.Ring S)).toExtensionHom) =
    h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P)

Tactic:
eq_comm,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P) =
    ↑P.cotangentExtendScalarsEquiv ∘ₗ
      h1Cotangentι ∘ₗ
        H1Cotangent.map
          ((defaultHom P.Ring S P.extendScalars).comp
            ((Generators.self R S).defaultHom (Generators.self P.Ring S)).toExtensionHom)
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
⊢ invOneSubPow S 0 = 1

Tactic:
delta invOneSubPow
  simp only

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k : ℕ
⊢ (↑↑(toOrderTopSubOnePos ⋯ ^ s)).coeff (k • g) = Ring.choose s k • r ^ k

Tactic:
simp only [val_toOrderTopSubOnePos_coe, binomial_power, coeff_hsum, smul_eq_mul]
  rw [finsum_eq_single _ k, binomialFamily_apply (orderTop_sub_pos hg r), add_sub_cancel_left,
    single_pow, coeff_smul, coeff_single_same (k • g) (r ^ k), smul_eq_mul]
  intro n hn
  rw [binomialFamily_apply, add_sub_cancel_left, coeff_smul, single_pow, coeff_single_of_ne,
    smul_zero]
  · contrapose hn
    apply (StrictMono.injective (nsmul_left_strictMono hg)) hn.symm
  · by_cases hr : r = 0 <;> simp [hr, hg]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
⊢ (heval x) (C r) = r • 1

Tactic:
by
  ext g
  simp only [heval_apply, coeff_hsum, smulFamily_toFun, powers_toFun, HahnSeries.coeff_smul,
    HahnSeries.coeff_one, smul_eq_mul, mul_ite, mul_one, mul_zero]
  rw [finsum_eq_single _ 0 (fun n hn ↦ by simp [coeff_C_of_ne_zero hn])]
  by_cases hg : g = 0 <;> simp

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ∑ x ∈ VAddAntidiagonal g ⋯, (s i.1).coeff x.1 • (t i.2).coeff x.2 =
    ∑ x ∈ VAddAntidiagonal g ⋯,
      (∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1) • ∑ i ∈ (t.coeff x.2).support, (t i).coeff x.2

Tactic:
sum_vAddAntidiagonal_eq,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ∑ x ∈ VAddAntidiagonal g ⋯, (s i.1).coeff x.1 • (t i.2).coeff x.2 =
    ∑ x ∈ VAddAntidiagonal g ⋯,
      (∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1) • ∑ i ∈ (t.coeff x.2).support, (t i).coeff x.2
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
⊢ ∃ f,
    Function.Injective ⇑f ∧
      ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop

Tactic:
have hf₁ : Function.Injective f₁ := DivisibleHull.coe_injective

Goal state after:
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
⊢ ∃ f,
    Function.Injective ⇑f ∧
      ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
g : A →ₐ[R] B
⊢ g.toLinearMap ∘ₗ ofConv 1 = ofConv 1

Tactic:
by
  ext a; simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
g : A →ₗc[R] B
⊢ ofConv 1 ∘ₗ g.toLinearMap = ofConv 1

Tactic:
by
  ext a; simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
⊢ p.height ≤ 1

Tactic:
have := Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing (I.map f) ?_

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this✝ : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
this : (IsLocalRing.maximalIdeal (Localization.AtPrime p)).height ≤ 1
⊢ p.height ≤ 1

case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
⊢ IsLocalRing.maximalIdeal (Localization.AtPrime p) ∈ (map f I).minimalPrimes
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
x : ↑P.toProfinite.toTop
⊢ ↑x = ↑(Quotient.out i) ↔ x ∈ Quotient.out i • (↑H.toOpenSubgroup).carrier

Tactic:
eq_comm,

Goal state after:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
x : ↑P.toProfinite.toTop
⊢ ↑(Quotient.out i) = ↑x ↔ x ∈ Quotient.out i • (↑H.toOpenSubgroup).carrier
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
w✝ : IsLocalRing R
this✝ : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : maximalIdeal R ∈ (span ↑(insert x s')).minimalPrimes
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : ↑s' ⊆ ↑(q ⊔ span {x}).radical
⊢ q.height ≤ ↑n

Tactic:
obtain ⟨t, ht, hspan⟩ := exists_subset_radical_span_sup_of_subset_radical_sup _ _ _ h

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
w✝ : IsLocalRing R
this✝ : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : maximalIdeal R ∈ (span ↑(insert x s')).minimalPrimes
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : ↑s' ⊆ ↑(q ⊔ span {x}).radical
t : ↑↑s' → R
ht : Set.range t ⊆ ↑q
hspan : ↑s' ⊆ ↑(span (Set.range t) ⊔ span {x}).radical
⊢ q.height ≤ ↑n
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Set R
hs : s.Finite
hI : p ∈ (span s).minimalPrimes
⊢ p.height ≤ ↑s.ncard

Tactic:
s.ncard_eq_toFinset_card hs

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Set R
hs : s.Finite
hI : p ∈ (span s).minimalPrimes
⊢ p.height ≤ ↑hs.toFinset.card
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : PrimeSpectrum R
⊢ Order.krullDim ↑(PrimeSpectrum.comap C ⁻¹' {p}) ≤ ↑1

Tactic:
rw [show C = (algebraMap R (Polynomial R)) from rfl, Order.krullDim_eq_of_orderIso
      (PrimeSpectrum.preimageOrderIsoFiber R (Polynomial R) p), ← ringKrullDim,
      ← ringKrullDim_eq_of_ringEquiv (polyEquivTensor R (p.asIdeal.ResidueField)).toRingEquiv,
      ← Ring.krullDimLE_iff]

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : PrimeSpectrum R
⊢ Ring.KrullDimLE 1 p.asIdeal.ResidueField[X]
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
⊢ (∃ I, p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n) → p.height ≤ n

Tactic:
· rintro ⟨I, hp, hI⟩
    exact le_trans
      (Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes I p hp)
      (by simpa using (Cardinal.toENat.monotone' hI))

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
p : Ideal R
inst✝² : p.IsMaximal
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
x✝ : Field (R ⧸ p) := Quotient.field p
h : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p)) P).height = 1
⊢ P.height = p.height + 1

Tactic:
by
    rw [height_eq_height_add_of_liesOver_of_hasGoingDown p, h]

Goal state after: