mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ ∀ (x : ℕ),
    p.coeff x ≠ 0 → 1 ≤ (v.intAdicAbv hb) (p.coeff x) → 1 ≤ p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)

Tactic:
intro _

Goal state after:
case neg.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
x✝ : ℕ
⊢ p.coeff x✝ ≠ 0 → 1 ≤ (v.intAdicAbv hb) (p.coeff x✝) → 1 ≤ p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_1
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
a✝¹ : G × G × G
x✝ : ↑A
a✝ : K × K × K
⊢ ((ModuleCat.Hom.hom (mapShortComplexH2 (g.comp f) (φ ≫ resMap f ψ)).τ₁ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁ ∘ₗ lsingle a✝¹) x✝) a✝

Tactic:
simp [Prod.map]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
g₁ g₂ : G
⊢ f (single (g₁ * g₂) 1) = single (mapDomainOfBialgHomFun f g₁ * mapDomainOfBialgHomFun f g₂) 1

Tactic:
← mul_one (1 : R),

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
g₁ g₂ : G
⊢ f (single (g₁ * g₂) (1 * 1)) = single (mapDomainOfBialgHomFun f g₁ * mapDomainOfBialgHomFun f g₂) (1 * 1)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_2
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
a✝¹ : G × G
x✝ : ↑A
a✝ : K × K
⊢ ((ModuleCat.Hom.hom (mapShortComplexH2 (g.comp f) (φ ≫ resMap f ψ)).τ₂ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂ ∘ₗ lsingle a✝¹) x✝) a✝

Tactic:
simp [Prod.map]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_3
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
a✝¹ : G
x✝ : ↑A
a✝ : K
⊢ ((ModuleCat.Hom.hom (mapShortComplexH2 (g.comp f) (φ ≫ resMap f ψ)).τ₃ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃ ∘ₗ lsingle a✝¹) x✝) a✝

Tactic:
simp [Prod.map]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x y : ↥selmerGroup
⊢ (fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑(x * y)) =
    (fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑x) * fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑y

Tactic:
simp only [Subgroup.coe_mul, map_mul]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x y : ↥selmerGroup
⊢ (fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑x * ((↑v).valuationOfNeZeroMod n) ↑y) =
    (fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑x) * fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑y
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case h.mul_X
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)
g : MvPolynomial (ℕ × M) R
nm : ℕ × M
h : P ↑g
⊢ P ↑(g * X nm)

Tactic:
rw [RingCon.coe_mul]
    exact h_dp _ _ _ h

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

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
hn : n = 0
⊢ ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)

Tactic:
intro _

Goal state after:
case pos
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
hn : n = 0
a✝ : A
⊢ a✝ ∈ I → hJ.dpow n (f a✝) = f (hI.dpow n a✝)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.mem.smul
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x✝ : DividedPowerAlgebra R M
k : ℕ
i : ι
r : R
x : DividedPowerAlgebra R M
hxmem : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hx : x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ r • x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
rw [smul_mul_assoc]

Goal state after:
case dp.mem.smul
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x✝ : DividedPowerAlgebra R M
k : ℕ
i : ι
r : R
x : DividedPowerAlgebra R M
hxmem : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hx : x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ r • (x * dp R k (v i)) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : map f I ≤ J
⊢ hI.IsDPMorphism hJ f

Tactic:
by
    exact ⟨h, fun a ha ↦ by
      rw [← fromGens_coe hI hJ hS h hdp, (fromGens hI hJ hS h hdp).dpow_comp a ha]⟩

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
m✝ n✝ : ℕ
x✝ : A
hx : x✝ ∈ J
⊢ ((if x✝ ∈ J then hI.dpow m✝ x✝ else 0) * if x✝ ∈ J then hI.dpow n✝ x✝ else 0) =
    ↑((m✝ + n✝).choose m✝) * if x✝ ∈ J then hI.dpow (m✝ + n✝) x✝ else 0

Tactic:
simp [if_pos hx, hI.mul_dpow (hJ.isSubideal hx)]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : x ∈ Ideal.span {↑p}
hiff : ‖⟨dpow' p n ↑x, ⋯⟩‖ ≤ ↑p ^ (-↑1) ↔ ⟨dpow' p n ↑x, ⋯⟩ ∈ Ideal.span {↑p}
⊢ ⟨dpow' p n ↑x, ⋯⟩ ∈ Ideal.span {↑p}

Tactic:
rw [← hiff]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : x ∈ Ideal.span {↑p}
hiff : ‖⟨dpow' p n ↑x, ⋯⟩‖ ≤ ↑p ^ (-↑1) ↔ ⟨dpow' p n ↑x, ⋯⟩ ∈ Ideal.span {↑p}
⊢ ‖⟨dpow' p n ↑x, ⋯⟩‖ ≤ ↑p ^ (-↑1)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S
hSI : span S ≤ I
m : ℕ
hm : m ≠ 0
z : A
hz : z ∈ span S
⊢ hI.dpow m z ∈ span S

Tactic:
induction hz using Submodule.span_induction generalizing m hm with

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑J ∪ ↑K
⊢ hI.dpow n a ∈ span (↑J ∪ ↑K)

Tactic:
rcases ha with ha | ha

Goal state after:
case inl
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑J
⊢ hI.dpow n a ∈ span (↑J ∪ ↑K)

case inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ ↑K
⊢ hI.dpow n a ∈ span (↑J ∪ ↑K)
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
h : a + b = 1
⊢ IsUnit a ∨ IsUnit b

Tactic:
by
    rw [add_comm, ← eq_sub_iff_add_eq] at h
    rcases eq_or_ne (fst a) 0 with ha | ha <;>
    simp [isUnit_iff_isUnit_fst, h, ha]

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

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x✝ x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ), m ≠ 0 → hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ), m ≠ 0 → hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
k : ℕ
a✝ : k ∈ Finset.range (m + 1)
hk0 : k = 0
⊢ hI.dpow k x * hI.dpow (m - k) y ∈ I • J

Tactic:
exact hk0 ▸ mul_mem_left (I • J) _ (hy' _ hm)

Goal state after:
Module: Mathlib.RingTheory.Flat.LocallyFree

Goal state before:
pp: case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Nontrivial R
Rₚ : Type u_1 := Localization.AtPrime p
n : ℕ := rankAtStalk M { asIdeal := p, isPrime := ⋯ }
f : (Fin n →₀ R) →ₗ[R] Fin n →₀ Rₚ := Finsupp.mapRange.linearMap (Algebra.linearMap R Rₚ)
g : M →ₗ[R] LocalizedModule.AtPrime p M := mkLinearMap p.primeCompl M
φ : (Fin n →₀ R) →ₗ[R] M
hφps : Function.Surjective ⇑((IsLocalizedModule.map p.primeCompl f g) φ)
⊢ ∃ a ∉ p, Free (Localization.Away a) (LocalizedModule.Away a M)

Tactic:
obtain ⟨a, hap, hφas⟩ := by
      refine exists_localizedMap_away_surjective_of_localizedMap_atPrime_surjective p φ ?_
      simpa [LocalizedModule.coe_map_eq f g]

Goal state after:
case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Nontrivial R
Rₚ : Type u_1 := Localization.AtPrime p
n : ℕ := rankAtStalk M { asIdeal := p, isPrime := ⋯ }
f : (Fin n →₀ R) →ₗ[R] Fin n →₀ Rₚ := Finsupp.mapRange.linearMap (Algebra.linearMap R Rₚ)
g : M →ₗ[R] LocalizedModule.AtPrime p M := mkLinearMap p.primeCompl M
φ : (Fin n →₀ R) →ₗ[R] M
hφps : Function.Surjective ⇑((IsLocalizedModule.map p.primeCompl f g) φ)
a : R
hap : a ∉ p
hφas : Function.Surjective ⇑((map (Submonoid.powers a)) φ)
⊢ ∃ a ∉ p, Free (Localization.Away a) (LocalizedModule.Away a M)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x y : B
hy : y ∈ J
⊢ dpow hI f n (x * y) = x ^ n * dpow hI f n y

Tactic:
obtain ⟨a, rfl⟩ := hf x

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
y : B
hy : y ∈ J
a : A
⊢ dpow hI f n (f a * y) = f a ^ n * dpow hI f n y
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✝³ : PartialOrder Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
⊢ (Function.support fun i ↦ (s i.1).coeff gh.1 • (t i.2).coeff gh.2) ⊆ ↑⋯.toFinset

Tactic:
intro _

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✝³ : PartialOrder Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
a✝ : α × β
⊢ (a✝ ∈ Function.support fun i ↦ (s i.1).coeff gh.1 • (t i.2).coeff gh.2) → a✝ ∈ ↑⋯.toFinset
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
⊢ Nonempty (HahnEmbedding.Seed ℚ M ℝ)

Tactic:
by
  obtain ⟨strata⟩ : Nonempty (HahnEmbedding.ArchimedeanStrata ℚ M) := inferInstance
  choose f hf using fun c ↦ Archimedean.exists_orderAddMonoidHom_real_injective (strata.stratum c)
  refine ⟨strata, fun c ↦ (f c).toRatLinearMap, fun c ↦ ?_⟩
  apply Monotone.strictMono_of_injective
  · simpa using OrderHomClass.monotone (f c)
  · simpa using hf c

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
r : R
n : Γ
hn : n = 0
⊢ (embDomain Nat.castOrderEmbedding (toPowerSeries.symm (PowerSeries.C r))).coeff n = r

Tactic:
subst hn
    convert! embDomain_coeff (a := 0) <;> simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : AddCommGroup Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
x : R⟦Γ⟧
⊢ x⁻¹.cardSupp ≤ max ℵ₀ x.cardSupp

Tactic:
obtain rfl | hx := eq_or_ne x 0; · simp
  apply (cardSupp_single_mul_le ..).trans (cardSupp_hsum_powers_le ..) |>.trans
  gcongr
  refine (cardSupp_single_mul_le _ (-x.order) x.leadingCoeff⁻¹).trans' <| cardSupp_mono fun _ ↦ ?_
  aesop (add simp [coeff_single_mul])

Goal state after:
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
G : Type u_3
inst✝ : Group G
a : G
b : A
⊢ ((LinearMap.mul' R A[G] ∘ₗ LinearMap.lTensor A[G] (antipode R) ∘ₗ comul) ∘ₗ lsingle a) b =
    ((Algebra.linearMap R A[G] ∘ₗ counit) ∘ₗ lsingle a) b

Tactic:
simpa [← (ℛ R b).eq] using congr(lsingle (R := R) (1 : G)
      $(sum_mul_antipode_eq_algebraMap_counit (ℛ R b)))

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_3
p : ι → Submodule R M
I : Ideal R
⊢ (submodule fun i ↦ I • p i) = I • submodule p

Tactic:
simp only [Finsupp.submodule_eq_iSup, Submodule.map_smul'', ← Submodule.smul_iSup]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
q p : Ideal R
inst✝ : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : p ∈ (span (insert x s)).minimalPrimes
t : Set R
htq : t ⊆ ↑q
hsp : s ⊆ ↑(span (insert x t)).radical
⊢ q ∈ (span t).minimalPrimes

Tactic:
by
  let f := Quotient.mk (span t)
  have hf : Function.Surjective f := Quotient.mk_surjective
  have hI'q : span t ≤ q := span_le.mpr htq
  have hI'p : span t ≤ p := hI'q.trans hqp.le
  have := hp.isPrime
  have : (p.map f).IsPrime := map_isPrime_of_surjective hf (by rwa [mk_ker])
  suffices h : (p.map f).height ≤ 1 by
    have h_lt : q.map f < p.map f := (map_mono hqp.le).lt_of_not_ge fun e ↦ hqp.not_ge <| by
      simpa only [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot, f, mk_ker,
        sup_eq_left.mpr hI'q, sup_eq_left.mpr hI'p] using comap_mono (f := f) e
    have : (q.map f).IsPrime := map_isPrime_of_surjective hf (by rwa [mk_ker])
    have : (p.map f).FiniteHeight := ⟨Or.inr (h.trans_lt (WithTop.coe_lt_top 1)).ne⟩
    have := (height_strict_mono_of_isPrime_of_isPrime h_lt).trans_le h
    rw [Order.lt_one_iff, height_eq_zero_iff] at this
    have := minimalPrimes_comap_of_surjective hf this
    rwa [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot,
      mk_ker, sup_eq_left.mpr hI'q] at this
  refine height_le_one_of_isPrincipal_of_mem_minimalPrimes ((span {x}).map f) (p.map f) ⟨⟨this,
    map_mono <| span_le.mpr <| Set.singleton_subset_iff.mpr <| hp.le <| subset_span <| .inl rfl⟩,
    fun r ⟨hr, hxr⟩ hrp ↦ map_le_iff_le_comap.mpr (hp.2 ⟨hr.comap f, ?_⟩ ?_)⟩
  · rw [span_le, Set.insert_subset_iff]
    have := map_le_iff_le_comap.mp hxr (subset_span rfl)
    refine ⟨this, hsp.trans ((hr.comap f).isRadical.radical_le_iff.mpr ?_)⟩
    rw [span_le, Set.insert_subset_iff]
    exact ⟨this, span_le.mp (mk_ker.symm.trans_le (ker_le_comap _))⟩
  · conv_rhs => rw [← sup_eq_left.mpr hI'p, ← (span t).mk_ker, RingHom.ker_eq_comap_bot,
      ← comap_map_of_surjective f hf p]
    exact comap_mono hrp

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

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

Tactic:
intro h
    obtain ⟨I, hI, e₁, e₂⟩ := exists_spanRank_eq_and_height_eq p (IsPrime.ne_top ‹_›)
    refine ⟨I, Ideal.mem_minimalPrimes_of_height_le hI e₂.ge, e₁.symm ▸ ?_⟩
    norm_cast

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
eq : ofList rs = ofList rs • ⊤
⊢ supportDim R (R ⧸ ofList rs • ⊤) + ↑rs.length = supportDim R R

Tactic:
exact supportDim_add_length_eq_supportDim_of_isRegular rs reg

Goal state after:
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
⊢ False

Tactic:
suffices Φₙ.eval ↑q ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) by
    have contra : Φₙ.eval _ ∣ _ := eval_dvd (cyclotomic.dvd_X_pow_sub_one n ℤ) (x := (q : ℤ))
    rw [eval_sub, eval_X_pow, eval_one, ← key, Int.dvd_add_left this] at contra
    refine (Nat.le_of_dvd ?_ ?_).not_gt (sub_one_lt_natAbs_cyclotomic_eval (n := n) ?_ hq.ne')
    · exact tsub_pos_of_lt hq
    · convert! Int.natAbs_dvd_natAbs.mpr contra
      clear_value q
      simp only [eq_comm, Int.natAbs_eq_iff, Nat.cast_sub hq.le, Nat.cast_one, neg_sub, true_or]
    · by_contra! h
      obtain ⟨x, hx⟩ := finrank_le_one_iff.mp h
      refine not_le_of_gt hZ.lt_top (fun y _ ↦ Subring.mem_center_iff.mpr fun z ↦ ?_)
      obtain ⟨r, rfl⟩ := hx y
      obtain ⟨s, rfl⟩ := hx z
      rw [smul_mul_smul_comm, smul_mul_smul_comm, mul_comm]

Goal state after:
case intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
⊢ eval (↑q) Φₙ ∣ ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card)
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h✝ : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
hq' : PrimeSpectrum.comap (algebraMap S (T i)) q' = { asIdeal := q, isPrime := hq }
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion R (Localization.Away g')
n : ℕ
g : S
hg : g' * (algebraMap S (T i)) (f i) ^ n = (algebraMap S (T i)) g
⊢ IsStandardOpenImmersion R (Localization.Away (g * f i))

Tactic:
have : IsLocalization.Away g' (Localization.Away (algebraMap S (T i) g)) := by
      rw [← hg]
      exact .of_associated
        (associated_mul_unit_right _ _ ((IsLocalization.Away.algebraMap_isUnit (f i)).pow n)).symm

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h✝ : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
hq' : PrimeSpectrum.comap (algebraMap S (T i)) q' = { asIdeal := q, isPrime := hq }
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion R (Localization.Away g')
n : ℕ
g : S
hg : g' * (algebraMap S (T i)) (f i) ^ n = (algebraMap S (T i)) g
this : IsLocalization.Away g' (Localization.Away ((algebraMap S (T i)) g))
⊢ IsStandardOpenImmersion R (Localization.Away (g * f i))