mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, s.indicator (Function.const E c) (X i ω)) atTop
      (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))

Tactic:
have F_meas : Measurable F := (measurable_indicator_const_iff 1).2 hs

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, s.indicator (Function.const E c) (X i ω)) atTop
      (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
X✝ Y✝ : Rep k G
x✝² : X✝ ⟶ Y✝
x✝¹ : ↑((coindFunctor k φ).obj X✝)
x✝ : H
⊢ (Hom.hom ((Hom.hom ((coindFunctor k φ).map x✝² ≫ (coindIso φ Y✝).hom)).toLinearMap x✝¹)).toLinearMap
      (MonoidAlgebra.single x✝ 1) =
    (Hom.hom ((Hom.hom ((coindIso φ X✝).hom ≫ (coindFunctor' k φ).map x✝²)).toLinearMap x✝¹)).toLinearMap
      (MonoidAlgebra.single x✝ 1)

Tactic:
by simp [coindIso, coindMap']

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ Tendsto (fun n ↦ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ) atTop (𝓝 0)

Tactic:
have I : ∀ᵐ ω ∂μ, ∀ i, X i ω = 0 := by
      rw [ae_all_iff]
      intro i
      exact (hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h
    have A (n : ℕ) : eLpNorm (fun ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω) - μ[X 0]) p μ = 0 := by
      simp only [integral_eq_zero_of_ae h, sub_zero]
      apply eLpNorm_eq_zero_of_ae_zero
      filter_upwards [I] with ω hω
      simp [hω]
    simp [A]

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
inst✝ : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max w u v, u, v} k G
f : res S.subtype B ⟶ A
⊢ ((resCoindAdjunction k S.subtype).homEquiv B A) f ≫ (indCoindNatIso k S).symm.hom.app A =
    (resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A) f ≫ A.indCoindIso.inv

Tactic:
simp [resCoindHomEquiv]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A
⊢ (ModuleCat.Hom.hom (d₁₂ A)) f = 0 ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0

Tactic:
simp_rw [funext_iff, d₁₂_hom_apply, Prod.forall]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A
⊢ (∀ (a b : G), (A.ρ a) (f b) - f (a * b) + f a = 0 (a, b)) ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B✝ : Rep k G
f✝ : G →* H
φ : res f✝ A✝ ⟶ B✝
n : ℕ
A B : Rep k G
f : A ⟶ B
inst✝ : Mono f
Z✝ : ModuleCat k
g h : Z✝ ⟶ groupCohomology A 0
hgh : g ≫ map (MonoidHom.id G) f 0 = h ≫ map (MonoidHom.id G) f 0
⊢ g = h

Tactic:
simp only [← cancel_mono (H0Iso B).hom, Category.assoc, map_id_comp_H0Iso_hom] at hgh

Goal state after:
k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A✝ : Rep k H
B✝ : Rep k G
f✝ : G →* H
φ : res f✝ A✝ ⟶ B✝
n : ℕ
A B : Rep k G
f : A ⟶ B
inst✝ : Mono f
Z✝ : ModuleCat k
g h : Z✝ ⟶ groupCohomology A 0
hgh : g ≫ (H0Iso A).hom ≫ (invariantsFunctor k G).map f = h ≫ (H0Iso A).hom ≫ (invariantsFunctor k G).map f
⊢ g = h
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : G × G →₀ ↑A
⊢ x ∈ cycles₂ A ↔ (x.sum fun g a ↦ single g.2 ((A.ρ g.1⁻¹) a) + single g.1 a) = x.sum fun g a ↦ single (g.1 * g.2) a

Tactic:
by
  change x.sum (fun g a => _) = 0 ↔ _
  simp [sub_add_eq_add_sub, sub_eq_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : Ideal.map constantCoeff I ≤ Ideal.map constantCoeff J
⊢ I = J

Tactic:
refine hJI.antisymm' ?_

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : Ideal.map constantCoeff I ≤ Ideal.map constantCoeff J
⊢ I ≤ J
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha✝ : a✝ ∈ antidiagonal (optionElim k x)
⊢ ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x

Tactic:
simp_all [Finsupp.ext_iff]

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

Goal state before:
pp: case refine_2.fst.none
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(a₁✝.1 none, a₁✝.2 none), (a₁✝.1.some, a₁✝.2.some)⟩ = ⟨(a₂✝.1 none, a₂✝.2 none), (a₂✝.1.some, a₂✝.2.some)⟩
⊢ a₁✝.1 none = a₂✝.1 none

Tactic:
simp_all [Finsupp.ext_iff]

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

Goal state before:
pp: case refine_2.fst.some
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(a₁✝.1 none, a₁✝.2 none), (a₁✝.1.some, a₁✝.2.some)⟩ = ⟨(a₂✝.1 none, a₂✝.2 none), (a₂✝.1.some, a₂✝.2.some)⟩
val✝ : σ
⊢ a₁✝.1 (Option.some val✝) = a₂✝.1 (Option.some val✝)

Tactic:
simp_all [Finsupp.ext_iff]

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

Goal state before:
pp: case refine_2.snd.none
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(a₁✝.1 none, a₁✝.2 none), (a₁✝.1.some, a₁✝.2.some)⟩ = ⟨(a₂✝.1 none, a₂✝.2 none), (a₂✝.1.some, a₂✝.2.some)⟩
⊢ a₁✝.2 none = a₂✝.2 none

Tactic:
simp_all [Finsupp.ext_iff]

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

Goal state before:
pp: case refine_2.snd.some
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a₁✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₁✝ : a₁✝ ∈ antidiagonal (optionElim k x)
a₂✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha₂✝ : a₂✝ ∈ antidiagonal (optionElim k x)
a✝ : ⟨(a₁✝.1 none, a₁✝.2 none), (a₁✝.1.some, a₁✝.2.some)⟩ = ⟨(a₂✝.1 none, a₂✝.2 none), (a₂✝.1.some, a₂✝.2.some)⟩
val✝ : σ
⊢ a₁✝.2 (Option.some val✝) = a₂✝.2 (Option.some val✝)

Tactic:
simp_all [Finsupp.ext_iff]

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

Goal state before:
pp: case h.none
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
⊢ (optionElim m u + optionElim n v) none = (optionElim k x) none

Tactic:
simp_all [Finsupp.ext_iff]

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

Goal state before:
pp: case h.some
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
val✝ : σ
⊢ (optionElim m u + optionElim n v) (Option.some val✝) = (optionElim k x) (Option.some val✝)

Tactic:
simp_all [Finsupp.ext_iff]

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

Goal state before:
pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
a✝ : (Option σ →₀ ℕ) × (Option σ →₀ ℕ)
ha✝ : a✝ ∈ antidiagonal (optionElim k x)
⊢ (coeff a✝.1) p * (coeff a✝.2) q =
    (coeff
          (optionElim ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩.fst.1
            ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩.snd.1))
        p *
      (coeff
          (optionElim ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩.fst.2
            ⟨(a✝.1 none, a✝.2 none), (a✝.1.some, a✝.2.some)⟩.snd.2))
        q

Tactic:
simp_all [Finsupp.ext_iff]

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (residue (AdicCompletion (maximalIdeal R) R)) ((algebraMap R (AdicCompletion (maximalIdeal R) R)) z) = x

Tactic:
← hy

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (residue (AdicCompletion (maximalIdeal R) R)) ((algebraMap R (AdicCompletion (maximalIdeal R) R)) z) =
    (residue (AdicCompletion (maximalIdeal R) R)) y
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
l m n : ℕ
h : l ≤ m
h' : l ≤ n
p : MvPowerSeries σ R
⊢ (truncTotal m) p - (truncTotal n) p ∈ MvPolynomial.idealOfVars σ R ^ l

Tactic:
refine (MvPolynomial.mem_pow_idealOfVars_iff' ..).mpr (fun x hx ↦ ?_)
  rw [MvPolynomial.coeff_sub, sub_eq_zero, coeff_truncTotal _ (by lia),
    coeff_truncTotal _ (by lia)]

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

Goal state before:
pp: σ : Type u_2
τ : Type u_3
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
a : σ → MvPowerSeries τ R
ha : MvPowerSeries.HasSubst a
⊢ MvPowerSeries.subst a ((toMvPowerSeries i) f) = subst (a i) f

Tactic:
by
  rw [toMvPowerSeries_eq_subst, subst, MvPowerSeries.subst_comp_subst_apply
    (HasSubst.const (HasSubst.X _)) ha, MvPowerSeries.subst_X ha, subst]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
k : ℕ
h : n ≤ k + n
⊢ ↑((ofPowSMul I M n) (ofValEqZero I hxn)) (k + n) = ↑x (k + n)

Tactic:
rw [ofPowSMul_val_apply _ rfl, ofValEqZero, ofValEqZeroAux_prop]

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

Goal state before:
pp: case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range

Tactic:
have hv : mapDomain (s ∘ QuotientGroup.mk) v = 0 := by
    rw [mapDomain_comp]
    simp only [QuotientGroup.coe_mk', lmapDomain_apply, mapDomain_sub, v] at hz ⊢
    simp [hz, hy, coe_mapCycles₁ (QuotientGroup.mk' S), Rep.hom_id (of _)]

Goal state after:
case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
Module: Mathlib.RingTheory.Congruence.Star

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : R
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star w✝ + Star.star y✝) (Star.star x✝ + Star.star z✝)

Tactic:
exact (h1.star hr).add (h2.star hr)

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

Goal state before:
pp: case h.h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial (A.toCoinvariants S) S).f)
      ((ConcreteCategory.hom (H1π (res S.subtype (A.toCoinvariants S)))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1CoresCoinf A S).f).range

Tactic:
| @h z =>

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✝ : Kˣ ⧸ (powMonoidHom n).range
hx : x✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
v : HeightOneSpectrum R
hv : v ∉ S
⊢ (v.valuationOfNeZeroMod n) x✝⁻¹ = 1

Tactic:
by rw [map_inv, hx v hv, inv_one]

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
i : ℕ
hi : i < n
⊢ Subsingleton (Ext N (of R (QuotSMulTop (x ^ k) ↑M)) i)

Tactic:
have zero1 := AddCommGrpCat.isZero_of_iff_subsingleton.mpr (h_ext i (by omega))

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : (Module.annihilator R ↑N).radical = I.radical
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
this✝ : Subsingleton (N ⟶ M)
this : Subsingleton (↑N →ₗ[R] ↑M)
x : R
mem_ann : x ∈ Module.annihilator R ↑N
hx : IsSMulRegular (↑M) x
k : ℕ
hk : x ^ k ∈ I
i : ℕ
hi : i < n
zero1 : IsZero (AddCommGrpCat.of (Ext N M i))
⊢ Subsingleton (Ext N (of R (QuotSMulTop (x ^ k) ↑M)) i)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case insert
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
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∑ x_1, dpow (↑x_1) (x a) * ∑ k ∈ s.sym (n - ↑x_1), ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i) =
    ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i)

Tactic:
mul_sum,

Goal state after:
case insert
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
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∑ x_1, ∑ i ∈ s.sym (n - ↑x_1), dpow (↑x_1) (x a) * ∏ i_1 ∈ s, dpow (Multiset.count i_1 ↑i) (x i_1) =
    ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i)
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
⊢ map R LinearMap.id = AlgHom.id R (DividedPowerAlgebra R M)

Tactic:
rw [algHom_ext_iff]
  intros
  simp [map_apply_dp]

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

Goal state before:
pp: case add
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
⊢ hI.dpow m (x + y) ∈ I • J

Tactic:
hI.dpow_add' (mul_le_left hx) (mul_le_left hy)

Goal state after:
case add
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 ∈ Finset.range (m + 1), hI.dpow k x * hI.dpow (m - k) y ∈ I • J
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 : ℕ
a : A
ha : a ∈ I
⊢ (dividedPowers hI hf hIJ hIf).dpow n (f a) = f (hI.dpow n a)

Tactic:
dpow_def,

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 : ℕ
a : A
ha : a ∈ I
⊢ dpow hI f n (f a) = f (hI.dpow n a)
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
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
⊢ {a | (if h : a ∈ Set.range ⇑f then s (Classical.choose h) else 0).coeff g ≠ 0} ⊆
    ⇑f '' Function.support fun a ↦ (s a).coeff g

Tactic:
by
        intro b h
        by_cases hb : b ∈ Set.range f
        · simp only [Ne, Set.mem_ofPred_eq, dif_pos hb] at h
          exact ⟨Classical.choose hb, h, Classical.choose_spec hb⟩
        · simp only [Ne, Set.mem_ofPred_eq, dif_neg hb, coeff_zero, not_true_eq_false] at h

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : ¬0 < x.orderTop
⊢ powers x = single 0 1

Tactic:
ext a
  obtain rfl | ha := eq_or_ne a 0 <;> simp [powers, *]

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
g : G
a : A
⊢ (antipode R) (single g a) = single g⁻¹ ((antipode R) a)

Tactic:
simp [antipode]

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

Goal state before:
pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : SpecializingMap (PrimeSpectrum.comap (algebraMap R S))
q : Ideal R
hq : q.IsPrime
P : Ideal S
hP : P.IsPrime
hlt : Ideal.under R P < q
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q

Tactic:
have : PrimeSpectrum.comap (algebraMap R S) ⟨P, hP⟩ ⤳ (⟨q, hq⟩ : PrimeSpectrum R) :=
      (PrimeSpectrum.le_iff_specializes _ _).mp hlt.le
    obtain ⟨Q, hs, heq⟩ := h this
    refine ⟨Q.asIdeal, (PrimeSpectrum.le_iff_specializes _ _).mpr hs, Q.2, ⟨?_⟩⟩
    simpa [PrimeSpectrum.ext_iff] using heq.symm

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
⊢ supportDim R M ≠ ⊥

Tactic:
by
  have : Nonempty (Module.support R M) := nonempty_support_of_nontrivial.to_subtype
  simp [supportDim]

Goal state after: