mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ (∀ (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:
hlX

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) (κ ω')
⊢ (∀ (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.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
B : ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
⊢ ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc ↑j ↑N, 1 ∂ρ) =
    ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ)

Tactic:
congr 1
      refine sum_congr rfl fun j hj => ?_
      rw [intervalIntegral.integral_of_le (Nat.cast_le.2 ((mem_range.1 hj).le.trans hKN))]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
⊢ 2 / (↑k + 1) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ ≤ ∫ (x : ℝ) in ↑k..↑(k + 1), 2 * x ∂ρ

Tactic:
rw [← intervalIntegral.integral_const_mul, intervalIntegral.integral_of_le Ik,
        intervalIntegral.integral_of_le Ik]

Goal state after:
case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
⊢ ∫ (x : ℝ) in Set.Ioc ↑k ↑(k + 1), 2 / (↑k + 1) * x ^ 2 ∂ρ ≤ ∫ (x : ℝ) in Set.Ioc ↑k ↑(k + 1), 2 * x ∂ρ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
t : ℝ
p : ℝ≥0
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) μ

Tactic:
simpa using h.memLp_exp_mul t p

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

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * id ω)) (Measure.map X μ)

Tactic:
rw [integrable_map_measure (by fun_prop) hX]

Goal state after:
case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ Integrable ((fun ω ↦ rexp (t * id ω)) ∘ X) μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) ((‖b - a‖₊ / 2) ^ 2) μ

Tactic:
rw [← sub_sub_sub_cancel_right b a μ[X]]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) ((‖b - ∫ (x : Ω), X x ∂μ - (a - ∫ (x : Ω), X x ∂μ)‖₊ / 2) ^ 2) μ
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FDRep R G
f : X ⟶ Y
g : G
⊢ ModuleCat.Hom.hom ((forget₂ (FGModuleCat R) (ModuleCat R)).map f.hom) ∘ₗ
      ((((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V.endRingEquiv.toMonoidHom.comp
          (((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).ρ)
        g =
    ((((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).V.endRingEquiv.toMonoidHom.comp
          (((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).ρ)
        g ∘ₗ
      ModuleCat.Hom.hom ((forget₂ (FGModuleCat R) (ModuleCat R)).map f.hom)

Tactic:
by
    ext x
    exact ConcreteCategory.congr_hom ((forget (FGModuleCat R)).congr_map (f.comm g)) x

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
g : G
⊢ (ρ g) (ρ.averageMap v) = ρ.averageMap v

Tactic:
rw [averageMap, ← asAlgebraHom_single_one, ← Module.End.mul_apply, ← map_mul (asAlgebraHom ρ),
    mul_average_left]

Goal state after:
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.{?u.16, u, v} k G
⊢ ∀ {X' X : Rep.{max w t, u, w} k H} {Y : Rep.{max w t, u, v} k G} (f : X' ⟶ X) (g : X ⟶ (coindFunctor k φ).obj Y),
    (resCoindHomEquiv.{?u.42, u, v, w} φ X' Y).toEquiv.symm (f ≫ g) =
      (resFunctor φ).map f ≫ (resCoindHomEquiv.{?u.42, u, v, w} φ X Y).toEquiv.symm g

Tactic:
intros

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep.{?u.16, u, v} k G
X'✝ X✝ : Rep.{max w t, u, w} k H
Y✝ : Rep.{max w t, u, v} k G
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (coindFunctor k φ).obj Y✝
⊢ (resCoindHomEquiv.{?u.42, u, v, w} φ X'✝ Y✝).toEquiv.symm (f✝ ≫ g✝) =
    (resFunctor φ).map f✝ ≫ (resCoindHomEquiv.{?u.42, u, v, w} φ X✝ Y✝).toEquiv.symm g✝
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.{?u.16, u, v} k G
⊢ ∀ {X : Rep.{max w t, u, w} k H} {Y Y' : Rep.{max w t, u, v} k G} (f : (resFunctor φ).obj X ⟶ Y) (g : Y ⟶ Y'),
    (resCoindHomEquiv.{t, u, v, w} φ X Y').toEquiv (f ≫ g) =
      (resCoindHomEquiv.{t, u, v, w} φ X Y).toEquiv f ≫ (coindFunctor k φ).map g

Tactic:
intros

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep.{?u.16, u, v} k G
X✝ : Rep.{max w t, u, w} k H
Y✝ Y'✝ : Rep.{max w t, u, v} k G
f✝ : (resFunctor φ).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
⊢ (resCoindHomEquiv.{t, u, v, w} φ X✝ Y'✝).toEquiv (f✝ ≫ g✝) =
    (resCoindHomEquiv.{t, u, v, w} φ X✝ Y✝).toEquiv f✝ ≫ (coindFunctor k φ).map g✝
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁹ : CommRing k
G : Type u_2
inst✝⁸ : Group G
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module k[G] V
inst✝⁴ : IsScalarTower k k[G] V
W : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module k[G] W
inst✝ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
h : ∀ (v : V), π (i v) = v
g : G
v : V
⊢ (π.conjugate g) (i v) = v

Tactic:
rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
    ← one_def, one_smul]

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ (equivariantProjection G π) (i v) = v

Tactic:
rw [equivariantProjection_apply]

Goal state after:
k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ (↑(Nat.card G))⁻¹ʳ • ∑ g, (π.conjugate g) (i v) = v
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
Ω : 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
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ UnifIntegrable (fun n ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) p μ

Tactic:
(_ : (fun (n : ℕ) ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω))
            = fun (n : ℕ) => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i))

Goal state after:
case neg
Ω : 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
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ UnifIntegrable (fun n ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i) p μ

Ω : 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
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ (fun n ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) = fun n ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
⊢ Simple V ↔ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)

Tactic:
by
  have := invertibleOfNonzero (NeZero.ne (Nat.card G : k))
  constructor <;> intro h
  · symm; simpa [Nonempty.intro (Iso.refl V), inv_mul_eq_one₀] using char_orthonormal V V
  · have eq := V.scalar_product_char_eq_finrank_equivariant V
    rw [h, inv_mul_cancel_of_invertible] at eq
    rw [simple_iff_end_is_rank_one, ← Nat.cast_inj (R := k), ← eq, Nat.cast_one]

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
⊢ ∀ {X : Rep k G} {Y Y' : Rep k H} (f : (indFunctor k φ).obj X ⟶ Y) (g : Y ⟶ Y'),
    (indResHomEquiv φ X Y').toEquiv (f ≫ g) = (indResHomEquiv φ X Y).toEquiv f ≫ (resFunctor φ).map g

Tactic:
intros

Goal state after:
k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
X✝ : Rep k G
Y✝ Y'✝ : Rep k H
f✝ : (indFunctor k φ).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
⊢ (indResHomEquiv φ X✝ Y'✝).toEquiv (f✝ ≫ g✝) = (indResHomEquiv φ X✝ Y✝).toEquiv f✝ ≫ (resFunctor φ).map g✝
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
m : ℕ
⊢ barComplex.d k G (m + 1) ≫ barComplex.d k G m ≫ (diagonalSuccIsoFree k G m).inv = 0

Tactic:
d_comp_diagonalSuccIsoFree_inv_eq,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
m : ℕ
⊢ barComplex.d k G (m + 1) ≫ (diagonalSuccIsoFree k G (m + 1)).inv ≫ (standardComplex k G).d (m + 1) m = 0
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
m : ℕ
⊢ (barComplex.d k G (m + 1) ≫ (diagonalSuccIsoFree k G (m + 1)).inv) ≫ (standardComplex k G).d (m + 1) m = 0

Tactic:
d_comp_diagonalSuccIsoFree_inv_eq,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
m : ℕ
⊢ ((diagonalSuccIsoFree k G (m + 1 + 1)).inv ≫ (standardComplex k G).d (m + 1 + 1) (m + 1)) ≫
      (standardComplex k G).d (m + 1) m =
    0
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel i j →
    (diagonalSuccIsoFree k G i).symm.hom ≫ (standardComplex k G).d i j =
      (barComplex k G).d i j ≫ (diagonalSuccIsoFree k G j).symm.hom

Tactic:
by
    rintro (rfl : j + 1 = i)
    rw [d_def, Iso.symm_hom, Iso.symm_hom, d_comp_diagonalSuccIsoFree_inv_eq]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
⊢ ∀ (X Y : FDRep k G),
    Functor.LaxMonoidal.μ (forget k G).toFunctor X Y ≫ (equivApp g (X ⊗ Y)).hom =
      ((equivApp g X).hom ⊗ₘ (equivApp g Y).hom) ≫ Functor.LaxMonoidal.μ (forget k G).toFunctor X Y

Tactic:
intros

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
X✝ Y✝ : FDRep k G
⊢ Functor.LaxMonoidal.μ (forget k G).toFunctor X✝ Y✝ ≫ (equivApp g (X✝ ⊗ Y✝)).hom =
    ((equivApp g X✝).hom ⊗ₘ (equivApp g Y✝).hom) ≫ Functor.LaxMonoidal.μ (forget k G).toFunctor X✝ Y✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
P : Ideal R
hP : Maximal (fun x ↦ x ∈ kaplanskySet S) P
⊢ ∃ P ∈ kaplanskySet S, ∀ I ∈ kaplanskySet S, P ≤ I → I = P

Tactic:
exact ⟨P, hP.1, fun _ hI H ↦ le_antisymm (hP.2 hI H) H⟩

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 : 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:
change x.sum (fun g a => _) = 0 ↔ _
  simp [sub_add_eq_add_sub, sub_eq_zero]

Goal state after:
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 ∈ antidiagonal (optionElim k x),
    ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x

Tactic:
intros

Goal state after:
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
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
⊢ ∀ a₁ ∈ antidiagonal (optionElim k x),
    ∀ a₂ ∈ antidiagonal (optionElim k x),
      ⟨(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₁ = a₂

Tactic:
intros

Goal state after:
case refine_2
σ : 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₁✝ = a₂✝
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mpr
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
⊢ DiscreteTopology A → (∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s

Tactic:
intros

Goal state after:
case mpr
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
a✝ : DiscreteTopology A
⊢ (∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s
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 ∈ 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:
intros

Goal state after:
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
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ optionElim 0 (single i 1) = single (Option.some i) 1

Tactic:
classical
    ext a; cases a <;> simp [single_apply]

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

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(k = 0 ∧ x = 0)
h3 : k = 0
⊢ 0 = (coeff x) (C r)

Tactic:
rw [coeff_C, if_neg (by tauto)]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : Semiring A
X : Type u_3
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x : X
a : A
⊢ comul (single x a) = (TensorProduct.map (lsingle x) (lsingle x)) (comul a)

Tactic:
simp [comul_def, TensorProduct.map_map]

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : Semiring A
X : Type u_3
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x : X
a : A
⊢ (TensorProduct.map (↑(coeffLinearEquiv R).symm ∘ₗ Finsupp.lsingle x)
        (↑(coeffLinearEquiv R).symm ∘ₗ Finsupp.lsingle x))
      (comul a) =
    (TensorProduct.map (lsingle x) (lsingle x)) (comul a)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: 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)
⊢ (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x) ∈
    (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial (A.toCoinvariants S) S).g).ker

Tactic:
by
    simpa only [H1CoresCoinfOfTrivial_X₂, H1CoresCoinfOfTrivial_X₃, H1CoresCoinfOfTrivial_g,
      Iso.refl_inv, LinearMap.mem_ker, H1π_comp_map_apply (QuotientGroup.mk' S),
      ← mapCycles₁_comp_apply (x := x)] using! hx

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
⊢ Function.Exact ⇑((lsmul R M) r) ⇑(r • ⊤).mkQ

Tactic:
by
  intro x
  simp [Submodule.mem_smul_pointwise_iff_exists, Submodule.mem_smul_pointwise_iff_exists]

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

Goal state before:
pp: case inl
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R n 0 = if n = 0 then 1 else 0

Tactic:
rw [if_pos hn, hn, dp_zero]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) * ↑(multinomial s✝ n) =
    ↑((n a✝ + ∑ i ∈ s✝, n i).choose (n a✝)) * ↑(multinomial s✝ n)

Tactic:
sum_insert hi

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑((n a✝ + ∑ x ∈ s✝, n x).choose (n a✝)) * ↑(multinomial s✝ n) =
    ↑((n a✝ + ∑ i ∈ s✝, n i).choose (n a✝)) * ↑(multinomial s✝ n)
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case insert.e_a
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
n : ι → ℕ
m : M
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, dp R (n i) m = ↑(multinomial s✝ n) * dp R (s✝.sum n) m
⊢ ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) * ↑(multinomial s✝ n) =
    ↑((n a✝ + ∑ i ∈ s✝, n i).choose (n a✝)) * ↑(multinomial s✝ n)

Tactic:
sum_insert hi

Goal state after:
case insert.e_a
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
n : ι → ℕ
m : M
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, dp R (n i) m = ↑(multinomial s✝ n) * dp R (s✝.sum n) m
⊢ ↑((n a✝ + ∑ x ∈ s✝, n x).choose (n a✝)) * ↑(multinomial s✝ n) =
    ↑((n a✝ + ∑ i ∈ s✝, n i).choose (n a✝)) * ↑(multinomial s✝ n)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: 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
⊢ (map f I ≤ J ∧ ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)) ↔
    map f I ≤ J ∧ ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)

Tactic:
and_congr_right_iff

Goal state after:
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
⊢ map f I ≤ J →
    ((∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)) ↔
      ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a))