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

Goal state before:
pp: case pos
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

pp: case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

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
    filter_upwards [I] with ω hω
    simpa [hω] using! (integral_eq_zero_of_ae h).symm

Goal state after:
case neg
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ)) →
    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:
hω

Goal state after:
Ω : 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
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
⊢ 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.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
⊢ (∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))) →
    (∀ (k : ℕ),
        Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))) →
      Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
hω

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
⊢ (∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))) →
    Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
ω : Ω
⊢ (∀ (i : ℕ), X i ω = 0) → Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
hω

Goal state after:
Ω : 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
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
ω : Ω
hω : ∀ (i : ℕ), X i ω = 0
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
X✝ Y✝ : Type w
inst✝¹² : TopologicalSpace k
inst✝¹¹ : Ring k
inst✝¹⁰ : Monoid G
inst✝⁹ : AddCommGroup X✝
inst✝⁸ : Module k X✝
inst✝⁷ : TopologicalSpace X✝
inst✝⁶ : IsTopologicalAddGroup X✝
inst✝⁵ : ContinuousSMul k X✝
inst✝⁴ : AddCommGroup Y✝
inst✝³ : Module k Y✝
inst✝² : TopologicalSpace Y✝
inst✝¹ : IsTopologicalAddGroup Y✝
inst✝ : ContinuousSMul k Y✝
ρ : ContRepresentation k G X✝
σ : ContRepresentation k G Y✝
A B C : TopRep k G
X Y : Action (TopModuleCat k) G
f : X ⟶ Y
g : G
⊢ TopModuleCat.Hom.hom f.hom ∘SL { toMonoidHom := X.V.endRingEquiv.toMonoidHom.comp X.ρ } g =
    { toMonoidHom := Y.V.endRingEquiv.toMonoidHom.comp Y.ρ } g ∘SL TopModuleCat.Hom.hom f.hom

Tactic:
by
    simpa [← toMonoidHom_apply] using congr(TopModuleCat.Hom.hom $(f.comm g))

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
ω : Ω
⊢ (∀ (i : ℕ), X i ω = 0) → (↑n)⁻¹ • ∑ i ∈ range n, X i ω = 0 ω

Tactic:
hω

Goal state after:
Ω : 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
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
ω : Ω
hω : ∀ (i : ℕ), X i ω = 0
⊢ (↑n)⁻¹ • ∑ i ∈ range n, X i ω = 0 ω
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k✝ : Type u_1
inst✝¹³ : Field k✝
G✝ : Type u_2
inst✝¹² : Finite G✝
inst✝¹¹ : NeZero ↑(Nat.card G✝)
inst✝¹⁰ : Group G✝
V✝ : Type u_3
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝[G✝] V✝
W : Type u_4
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝[G✝] W
G : Type u_5
k : Type u_6
V : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Field k
inst✝³ : Finite G
inst✝² : NeZero ↑(Nat.card G)
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.IsSemisimpleRepresentation

Tactic:
rw [isSemisimpleRepresentation_iff_isSemisimpleModule_asModule]
  infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ✝ φ ψ : ρ.Equiv σ
h1 : ⇑φ.toContinuousLinearEquiv = ⇑ψ.toContinuousLinearEquiv
h2 : (↑φ.toContinuousLinearEquiv).invFun = (↑ψ.toContinuousLinearEquiv).invFun
⊢ φ = ψ

Tactic:
cases φ; cases ψ; simp_all

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
b : Quotient (QuotientGroup.rightRel S)
⊢ b ∈ Finset.univ → b ≠ ⟦g⟧ → b.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0

Tactic:
_

Goal state after:
case h₀
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
b : Quotient (QuotientGroup.rightRel S)
a✝ : b ∈ Finset.univ
⊢ b ≠ ⟦g⟧ → b.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
⊢ resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (X.resolutionX i)

Tactic:
by
  induction i with
  | zero => rfl
  | succ i ih =>
    rw [resolutionMap_succ, ih]
    ext F x
    rfl

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀
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
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
b : Quotient (QuotientGroup.rightRel S)
⊢ b ∈ Finset.univ → b ≠ ⟦a⟧ → ↑(A.indToCoind (b.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0

Tactic:
_

Goal state after:
case h₀
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
inst✝ : S.FiniteIndex
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
b : Quotient (QuotientGroup.rightRel S)
a✝ : b ∈ Finset.univ
⊢ b ≠ ⟦a⟧ → ↑(A.indToCoind (b.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case zero
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ ShortComplex.QuasiIso
    ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
      ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
        ⟨(trivial k G k).leftRegularHom 1, ⋯⟩))

Tactic:
ShortComplex.quasiIso_iff_of_zeros' _ rfl rfl rfl

Goal state after:
case zero
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ {
        X₁ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).X₁,
        X₂ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).X₂,
        X₃ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((ChainComplex.single₀ (Rep k G)).obj (trivial k G k))).X₂,
        f :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).f,
        g :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
              ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
                ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂,
        zero := ⋯ }.Exact ∧
    Epi
      ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
          ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
            ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂
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✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
⊢ TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
      (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ s =
    TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)

Tactic:
simp only [MonoidalCategory.curriedTensor_obj_obj, tensor_V, tensor_ρ, tprod_apply,
      MonoidHom.coe_comp, Function.comp_apply]

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✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
⊢ TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ TensorProduct.map (A.ρ s) (B.ρ (φ s)) =
    TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 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
f : ↑(ModuleCat.of k (G → ↑A))
g : G × G × G
⊢ (ModuleCat.Hom.hom (d₁₂ A ≫ d₂₃ A)) f g = (ModuleCat.Hom.hom 0) f g

Tactic:
simp [mul_assoc, Pi.zero_apply (M := fun _ => A)]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↑(ModuleCat.of k (G → ↑A))
g : G × G × G
⊢ (A.ρ g.1) ((A.ρ g.2.1) (f g.2.2)) - (A.ρ g.1) (f (g.2.1 * g.2.2)) + (A.ρ g.1) (f g.2.1) -
          ((A.ρ g.1) ((A.ρ g.2.1) (f g.2.2)) - f (g.1 * (g.2.1 * g.2.2)) + f (g.1 * g.2.1)) +
        ((A.ρ g.1) (f (g.2.1 * g.2.2)) - f (g.1 * (g.2.1 * g.2.2)) + f g.1) -
      ((A.ρ g.1) (f g.2.1) - f (g.1 * g.2.1) + f g.1) =
    0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G → A
hf : IsCocycle₁ f
g : G
⊢ g • f g⁻¹ + f g = 0

Tactic:
← map_one_of_isCocycle₁ hf,

Goal state after:
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G → A
hf : IsCocycle₁ f
g : G
⊢ g • f g⁻¹ + f g = f 1
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: case pos
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g✝ : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
j : ℕ
a : ↑A
g : G
hj : Even (j + 1)
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d (j + 1) j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d (j + 1) j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1

Tactic:
simpa [hj, coinvariantsTensorMk, ofCoinvariantsTprodLeftRegular, Rep.norm,
        Representation.norm, ← Module.End.mul_apply, ← map_mul, mul_comm g⁻¹] using
        Finset.sum_bijective _ (MulEquiv.inv G).bijective (by simp) (by simp)

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∀ (g : G),
    (rightFDRep ⊗ rightFDRep).ρ g ≫ InducedCategory.homMk (↟(LinearMap.mul' k (G → k))) =
      InducedCategory.homMk (↟(LinearMap.mul' k (G → k))) ≫ rightFDRep.ρ g

Tactic:
intro
    ext u
    refine TensorProduct.induction_on u rfl (fun _ _ ↦ rfl) (fun _ _ hx hy ↦ ?_)
    simp only [map_add, hx, hy]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
f g : G → k
nat :
  (forget k G).map mulRepHom ≫ η.hom.hom.app rightFDRep =
    η.hom.hom.app (rightFDRep ⊗ rightFDRep) ≫ (forget k G).map mulRepHom
tensor : ∀ (X Y : FDRep k G), η.hom.hom.app (X ⊗ Y) = η.hom.hom.app X ⊗ₘ η.hom.hom.app Y
⊢ let α := Hom.hom (η.hom.hom.app rightFDRep).hom;
  α (f * g) = α f * α g

Tactic:
tensor

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
f g : G → k
nat :
  (forget k G).map mulRepHom ≫ η.hom.hom.app rightFDRep =
    (η.hom.hom.app rightFDRep ⊗ₘ η.hom.hom.app rightFDRep) ≫ (forget k G).map mulRepHom
tensor : ∀ (X Y : FDRep k G), η.hom.hom.app (X ⊗ Y) = η.hom.hom.app X ⊗ₘ η.hom.hom.app Y
⊢ let α := Hom.hom (η.hom.hom.app rightFDRep).hom;
  α (f * g) = α f * α g
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
a₁✝ : MvPowerSeries σ R
⊢ ∀ ⦃a₂ : MvPowerSeries σ R⦄, (rename ⇑e) a₁✝ = (rename ⇑e) a₂ → a₁✝ = a₂

Tactic:
_

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
a₁✝ a₂✝ : MvPowerSeries σ R
⊢ (rename ⇑e) a₁✝ = (rename ⇑e) a₂✝ → a₁✝ = a₂✝
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

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

Tactic:
simp [mem_cycles₂_iff, mapRange_add, eq_comm]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
d : τ →₀ ℕ
x : σ
a✝ : x ∉ ⋃ i ∈ ↑d.support, f ⁻¹' {i}
⊢ x ∉ {s | (coeff d) ((X ∘ f) s) ≠ 0}

Tactic:
_

Goal state after:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
d : τ →₀ ℕ
x : σ
a✝¹ : x ∉ ⋃ i ∈ ↑d.support, f ⁻¹' {i}
a✝ : x ∈ {s | (coeff d) ((X ∘ f) s) ≠ 0}
⊢ False
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 : ↑A
⊢ (ConcreteCategory.hom (iCycles A 0))
      (cyclesMk 0 0 cyclesMk₀_eq._proof_1 ((ConcreteCategory.hom (chainsIso₀ A).inv) x) ⋯) =
    (ConcreteCategory.hom (iCycles A 0)) ((ConcreteCategory.hom (cyclesIso₀ A).inv) x)

Tactic:
rw [iCycles_mk]; simp

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
⊢ H0π A ≫ (H0Iso A).hom = (coinvariantsMk k G).app A

Tactic:
by
  simp [H0π]

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
⊢ (cyclesIso₀ A).hom ≫ H0π A = π A 0

Tactic:
by
  simp [H0π]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
⊢ IsPrecomplete (Ideal.map e I) S ↔ IsPrecomplete I R

Tactic:
let : WithIdeal R := ⟨I⟩
  let : WithIdeal S := ⟨I.map e⟩
  rw [iff_comm, IsAdic.isPrecomplete_iff (by rfl), IsAdic.isPrecomplete_iff (by rfl)]
  exact completeSpace_congr (e := WithIdeal.uniformEquiv e rfl) (by
    simpa using UniformEquiv.isUniformEmbedding ..)

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : WithIdeal S
f : R →+* S
hf : Ideal.map f i ≤ i
⊢ ContinuousAt (⇑f) 0

Tactic:
rw [ContinuousAt, map_zero, i.hasBasis_nhds_zero_adic.tendsto_iff i.hasBasis_nhds_zero_adic]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : WithIdeal S
f : R →+* S
hf : Ideal.map f i ≤ i
⊢ ∀ (ib : ℕ), True → ∃ ia, True ∧ ∀ x ∈ ↑(i ^ ia), f x ∈ ↑(i ^ ib)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
⊢ H0π A ≫ map f φ 0 = Hom.toModuleCatHom φ ≫ H0π B

Tactic:
by
  simp [H0π]

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

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ Quotient.out (↑f (degree x + 1)) - Quotient.out (↑f n) ∈ MvPolynomial.idealOfVars σ R ^ (degree x + 1)

pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ degree x < degree x + 1

Tactic:
· nth_rw 1 [← Ideal.mul_top (MvPolynomial.idealOfVars σ R ^ (degree x + 1)),
      ← smul_eq_mul, ← Ideal.Quotient.eq]
    simp only [Submodule.mapQ_eq_factor, Submodule.factor_eq_factor, Ideal.Quotient.mk_out]
    rw [← AdicCompletion.transitionMap_ideal_mk _ (Nat.lt_iff_add_one_le.mp h), eq_comm]
    convert! f.prop h; simp

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ degree x < degree x + 1