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

Goal state before:
pp: case e'_2
p : ℝ≥0
h : p ≤ 1
n i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ (if h : i < n + 1 then p ^ ↑⟨i, h⟩ * (1 - p) ^ (n - ↑⟨i, h⟩) * ↑(n.choose ↑⟨i, h⟩) else 0) =
    p ^ i * (1 - p) ^ (n - i) * ↑(n.choose i)

Tactic:
Finset.mem_range

Goal state after:
case e'_2
p : ℝ≥0
h : p ≤ 1
n i : ℕ
hi : i < n + 1
⊢ (if h : i < n + 1 then p ^ ↑⟨i, h⟩ * (1 - p) ^ (n - ↑⟨i, h⟩) * ↑(n.choose ↑⟨i, h⟩) else 0) =
    p ^ i * (1 - p) ^ (n - i) * ↑(n.choose i)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω' : Ω'
h2 : (κ ω') {ω | 0 < X ω} = 0
h1 : (κ ω') {ω | X ω < 0} = 0
⊢ (κ ω') {ω | X ω ≠ 0} = (κ ω') {ω | X ω < 0 ∨ 0 < X ω}

Tactic:
ne_iff_lt_or_gt

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
⊢ (∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')) →
    ∀ (t : ℝ), mgf (fun ω ↦ X ω + Y ω) (κ ω') t ≤ rexp (↑((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) * t ^ 2 / 2)

Tactic:
hlY

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
hlY : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')
⊢ ∀ (t : ℝ), mgf (fun ω ↦ X ω + Y ω) (κ ω') t ≤ rexp (↑((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case insert
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h : (∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ) → HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
⊢ HasSubgaussianMGF (fun ω ↦ X i ω + ∑ c ∈ s, X c ω) (c i + ∑ i ∈ s, c i) μ

Tactic:
refine add_of_indepFun (h_subG _ (Finset.mem_insert_self _ _)) (h ?_) ?_

Goal state after:
case insert.refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h : (∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ) → HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
⊢ ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ

case insert.refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h : (∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ) → HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
⊢ X i ⟂ᵢ[μ] fun ω ↦ ∑ c ∈ s, X c ω
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (fun ω ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2
⊢ iteratedDeriv 2 (cgf X μ) u = Var[X; μ.tilted fun x ↦ u * X x]

Tactic:
← variance_tilted_mul (hs (Set.mem_Icc_of_Ioo h1))

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (fun ω ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2
⊢ Var[X; μ.tilted fun x ↦ u * X x] = Var[X; μ.tilted fun x ↦ u * X x]
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (fun ω ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2
⊢ iteratedDeriv 2 (cgf X μ) u = Var[X; μ.tilted fun x ↦ u * X x]

Tactic:
by
    rw [← variance_tilted_mul (hs (Set.mem_Icc_of_Ioo h1))]

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case hc
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ -0 = 0

Tactic:
neg_zero

Goal state after:
case hc
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ 0 = 0
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: case of
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
⊢ ∀ (m : G),
    f ((((lift k (V →ₗ[k] V) G) ρ) ((MonoidAlgebra.of k G) m)) x) =
      (((lift k (W →ₗ[k] W) G) σ) ((MonoidAlgebra.of k G) m)) (f x)

Tactic:
intro g
    simp only [one_smul, MonoidAlgebra.lift_single, MonoidAlgebra.of_apply]
    exact LinearMap.congr_fun (w g) x

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
⊢ ∀ (x_1 y : k[G]),
    f ((((lift k (V →ₗ[k] V) G) ρ) x_1) x) = (((lift k (W →ₗ[k] W) G) σ) x_1) (f x) →
      f ((((lift k (V →ₗ[k] V) G) ρ) y) x) = (((lift k (W →ₗ[k] W) G) σ) y) (f x) →
        f ((((lift k (V →ₗ[k] V) G) ρ) (x_1 + y)) x) = (((lift k (W →ₗ[k] W) G) σ) (x_1 + y)) (f x)

Tactic:
intro g h gw hw; simp only [map_add, LinearMap.add_apply, hw, gw]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
σ : Representation k G W
f : V →ₗ[k] W
⊢ (∀ (g : G), σ g ∘ₗ f ∘ₗ ρ g⁻¹ = f) ↔ ρ.IsIntertwiningMap σ f

Tactic:
refine ⟨fun hf ↦ ⟨fun γ v ↦ ?_⟩, fun hf γ ↦ ?_⟩
  · specialize hf γ
    nth_rewrite 1 [← hf]
    simp
  · ext v
    simp [hf.isIntertwining]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Group G
X Y : FDRep k G
⊢ ↥(((forget₂ (FDRep k G) (Rep k G)).obj X).ρ.linHom Y.ρ).invariants ≃ₗ[k] X ⟶ Y

Tactic:
← FDRep.forget₂_ρ

Goal state after:
k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Group G
X Y : FDRep k G
⊢ ↥(((forget₂ (FDRep k G) (Rep k G)).obj X).ρ.linHom ((forget₂ (FDRep k G) (Rep k G)).obj Y).ρ).invariants ≃ₗ[k] X ⟶ Y
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✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
⊢ ∃ a, (Hom.hom ((coindFunctor k S.subtype).map f)) a = y

Tactic:
by
    let := QuotientGroup.rightRel S
    choose! s hs using (Rep.epi_iff_surjective f).1 ‹_›
    choose! i hi using Quotient.mk'_surjective (α := G)
    let γ (g : G) : S := ⟨g * (i (Quotient.mk' g))⁻¹,
      (QuotientGroup.rightRel_apply.1 (Quotient.eq'.1 (hi (Quotient.mk' g))))⟩
    have hmk (s : S) (g : G) : Quotient.mk' (s.1 * g) = Quotient.mk' g :=
      Quotient.eq'.2 (QuotientGroup.rightRel_apply.2 (by simp))
    have hγ (s : S) (g : G) : γ (s.1 * g) = s * γ g := by ext; simp [mul_assoc, γ, hmk]
    let x (g : G) : X := X.ρ (γ g) (s (y.1 (i (Quotient.mk' g))))
    refine ⟨⟨x, fun _ _ => ?_⟩, Subtype.ext <| funext fun g => ?_⟩
    · simp [x, ← Module.End.mul_apply, ← map_mul, hmk, hγ]
    · simp only [coindFunctor_obj, coindFunctor_map, hom_ofHom,
        Representation.coindMap_coe_apply_apply, hom_comm_apply, x]
      simp_all [← y.2 (γ g), γ]

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)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : ↑A
s : ↥S
⊢ (A.indToCoindAux (↑s * g₁)) ((A.ρ s) a) g₂ = (A.indToCoindAux g₁) a g₂

Tactic:
rcases em ((QuotientGroup.rightRel S).r g₂ g₁) with ⟨s₁, rfl⟩ | h

Goal state after:
case inl
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g₁ : G
a : ↑A
s s₁ : ↥S
⊢ (A.indToCoindAux (↑s * g₁)) ((A.ρ s) a) ((fun m ↦ m • g₁) s₁) = (A.indToCoindAux g₁) a ((fun m ↦ m • g₁) s₁)

case inr
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ (A.indToCoindAux (↑s * g₁)) ((A.ρ s) a) g₂ = (A.indToCoindAux g₁) a g₂
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝ : CommRing k
n : ℕ
c : Fin (n + 1) → G
r : k
⊢ (d k G n) (MonoidAlgebra.single c r) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) (r * (-1) ^ ↑p)

Tactic:
rw [← mul_one r, ← smul_eq_mul, ← MonoidAlgebra.smul_single, map_smul, d_of]
  simp [Finset.smul_sum]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
g : Fin (0 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₁ X.X₁).inv) x) g =
    (ModuleCat.Hom.hom (d₀₁ X.X₂ ≫ (cochainsIso₁ X.X₂).inv)) y g

Tactic:
simpa [← hx] using! congr_fun (congr($((CommSq.vert_inv
        ⟨cochainsMap_f_1_comp_cochainsIso₁ (MonoidHom.id G) X.f⟩).w) x)) g

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
r : k
x : G → ↑A
g : G × G
⊢ r • (A.ρ g.1) (x g.2) - r • x (g.1 * g.2) + r • x g.1 = r • ((A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1)

Tactic:
smul_add,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G → ↑A
g : G × G
⊢ r • (A.ρ g.1) (x g.2) - r • x (g.1 * g.2) + r • x g.1 = r • ((A.ρ g.1) (x g.2) - x (g.1 * g.2)) + r • x g.1
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (cochainsIso₁ A).hom ≫ d₁₂ A = (inhomogeneousCochains A).d 1 2 ≫ (cochainsIso₂ A).hom

Tactic:
by
  ext x y
  change A.ρ y.1 (x _) - x _ + x _ = _ + _
  rw [Fin.sum_univ_two]
  simp only [Fin.val_zero, zero_add, pow_one, neg_smul, one_smul, Fin.val_one,
    Nat.one_add, neg_one_sq, sub_eq_add_neg, add_assoc]
  rcongr i <;> rw [Subsingleton.elim i 0] <;> rfl

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
⊢ (∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0) ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g

Tactic:
sub_add_eq_add_sub,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A
⊢ (∀ (g h : G), (A.ρ g) (f h) + f g - f (g * h) = 0) ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g
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 × G → ↑A
⊢ (∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) = f (g, h)) ↔
    ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)

Tactic:
sub_add_eq_add_sub,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A
⊢ (∀ (g h j : G), (A.ρ g) (f (h, j)) + f (g, h * j) - f (g * h, j) = f (g, h)) ↔
    ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)
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✝ : ℕ
S : Subgroup G
inst✝ : S.Normal
n : ℕ
X Y : Rep k G
φ : X ⟶ Y
⊢ (quotientToInvariantsFunctor k S ⋙ functor k (G ⧸ S) n).map φ ≫
      map (QuotientGroup.mk' S) (ofHom (Y.ρ.quotientToInvariants_lift S)) n =
    map (QuotientGroup.mk' S) (ofHom (X.ρ.quotientToInvariants_lift S)) n ≫ (functor k G n).map φ

Tactic:
simp only [Functor.comp_map, functor_map, ← cancel_epi (groupCohomology.π _ n),
      HomologicalComplex.homologyπ_naturality_assoc, HomologicalComplex.homologyπ_naturality,
      ← HomologicalComplex.cyclesMap_comp_assoc, ← cochainsMap_comp]
    congr 1

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

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ idealOfVars σ R ≤ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯

Tactic:
simp [idealOfVars, Ideal.span_le, Set.range_subset_iff, restrictSupportIdeal, X]

Goal state after:
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✝¹ : Fin 3 → G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom ((chainsIso₃ A).hom ≫ d₃₂ A)) (single x✝¹ x✝) =
    (ModuleCat.Hom.hom ((inhomogeneousChains A).d 3 2 ≫ (chainsIso₂ A).hom)) (single x✝¹ x✝)

Tactic:
simp [chainsIso₂, ChainComplex.of.d, pow_succ, chainsIso₃,
      -domLCongr_apply, domLCongr_single, d₃₂, Fin.sum_univ_three,
      Fin.contractNth, Fin.tail_def, sub_eq_add_neg, add_assoc,
      inhomogeneousChains.d_single (G := G), add_rotate' (-(single (_ * _, _) _)),
      add_left_comm (single (_, _ * _) _)]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ d₂₁ A ≫ d₁₀ A = 0

Tactic:
by
  ext x g
  simp [d₁₀, d₂₁, sum_add_index', sum_sub_index, sub_sub_sub_comm, add_sub_add_comm]

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
m : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
m' : ↥(maximalIdeal (AdicCompletion (maximalIdeal R) R))
hm' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).toCotangent m' = m
l : R
hl : Submodule.Quotient.mk l = ↑↑m' 2
lmem : l ∈ maximalIdeal R
⊢ (of (maximalIdeal R) R) l - ↑m' ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ 2

Tactic:
simp only [maximalIdeal_eq_map, ← Ideal.map_pow]

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
inj : Function.Injective ⇑f
m : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
m' : ↥(maximalIdeal (AdicCompletion (maximalIdeal R) R))
hm' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).toCotangent m' = m
l : R
hl : Submodule.Quotient.mk l = ↑↑m' 2
lmem : l ∈ maximalIdeal R
⊢ (of (maximalIdeal R) R) l - ↑m' ∈ Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal R ^ 2)
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
h : c = b + a
x : AdicCompletion I ↥(I ^ a • ⊤)
⊢ ↑((ofPowSMul I M a) x) c = (powSMulQuotInclusion I M h ⊤) (↑x b)

Tactic:
rw [← x.prop (show b ≤ c by lia), map_val_apply]
  refine Quotient.induction_on _ (x.val c) fun z ↦ ?_
  simp [powSMulQuotInclusion]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
x : AdicCompletion I ↥(I ^ n • ⊤)
x✝ : ↥s →₀ M
⊢ ((lsum R) fun i ↦ ↑i • LinearMap.id) x✝ ∈ I ^ n • ⊤

Tactic:
by simp [← hs, span_smul_eq, smul_top_eq_range_lsum]

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

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
⊢ (x ∈ Set.range fun x ↦ single x 1) → IsGroupLikeElem R x

Tactic:
rintro ⟨g, rfl⟩; exact isGroupLikeElem_single_one _

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ r • ⊤ ⊓ f₂.range ≤ r • f₂.range

Tactic:
exact smul_top_inf_eq_smul_of_isSMulRegular_on_quot this

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
Ia : Ideal R
hIa : Ia ∈ associatedPrimes R M
⊢ ∀ i ∈ associatedPrimes R M, i ≠ Ia → i ≠ Ia → i.IsPrime

Tactic:
exact fun I hin _ _ ↦ IsAssociatedPrime.isPrime hin

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h : (fun h ↦ h.dpow) hI = (fun h ↦ h.dpow) hI'
⊢ hI = hI'

Tactic:
ext n x
  exact congr_fun (congr_fun h n) x

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 : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ map R (g ∘ₗ f) = (map R g).comp (map R f)

Tactic:
rw [algHom_ext_iff]

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ ∀ (n : ℕ) (m : M), (map R (g ∘ₗ f)) (dp R n m) = ((map R g).comp (map R f)) (dp R n m)
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]

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (n : ℕ) (m : M), (map R LinearMap.id) (dp R n m) = (AlgHom.id R (DividedPowerAlgebra R M)) (dp R n m)
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (↑m !)⁻¹ʳ * (x ^ m * ((↑k !)⁻¹ʳ * x ^ k)) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))

Tactic:
← mul_assoc (x ^ m),

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (↑m !)⁻¹ʳ * (x ^ m * (↑k !)⁻¹ʳ * x ^ k) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * (x ^ m * ((↑k !)⁻¹ʳ * x ^ k)) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))

Tactic:
← mul_assoc (x ^ m),

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * (x ^ m * (↑k !)⁻¹ʳ * x ^ k) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ x ^ (n * 2) = 0

Tactic:
pow_mul

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ (x ^ n) ^ 2 = 0
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
x✝ : ℕ
hn : x✝ ≠ 0
x : A
hx : x ∈ ⊥
⊢ hI.dpow x✝ x ∈ ⊥

Tactic:
rw [mem_bot.mp hx, hI.dpow_eval_zero hn, mem_bot]

Goal state after: