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

Goal state before:
pp: case e'_3
Ω : 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
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x ↦ max x 0
neg : ℝ → ℝ := fun x ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
ω : Ω
hωpos : Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
hωneg : Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
x✝ : ℕ
⊢ (∑ i ∈ range x✝, X i ω) / ↑x✝ = (∑ i ∈ range x✝, (pos ∘ X i) ω) / ↑x✝ - (∑ i ∈ range x✝, (neg ∘ X i) ω) / ↑x✝

pp: case e'_5
Ω : 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
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x ↦ max x 0
neg : ℝ → ℝ := fun x ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
ω : Ω
hωpos : Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
hωneg : Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
⊢ ∫ (x : Ω), X 0 x ∂μ = (∫ (a : Ω), (pos ∘ X 0) a) - ∫ (a : Ω), (neg ∘ X 0) a

Tactic:
· simp only [pos, neg, ← sub_div, ← sum_sub_distrib, max_zero_sub_max_neg_zero_eq_self,
      Function.comp_apply]

Goal state after:
case e'_5
Ω : 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
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x ↦ max x 0
neg : ℝ → ℝ := fun x ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
ω : Ω
hωpos : Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
hωneg : Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
⊢ ∫ (x : Ω), X 0 x ∂μ = (∫ (a : Ω), (pos ∘ X 0) a) - ∫ (a : Ω), (neg ∘ X 0) a
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 ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
⊢ ∃ k, ∫ (ω : Ω), ‖X 0 ω - Y k 0 ω‖ ∂μ < δ

Tactic:
norm_sub_rev (X 0 _)

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 ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
⊢ ∃ k, ∫ (ω : Ω), ‖Y k 0 ω - X 0 ω‖ ∂μ < δ
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Monoid G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ map ρ ρ (IntertwiningMap.id ρ) = LinearMap.id

Tactic:
ext; rfl

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

Goal state before:
pp: case mk''
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
ψ : σ.Equiv ρ
toContinuousLinearEquiv✝ : W ≃L[R] V
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h :
  { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
        isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv =
    ψ.toContinuousLinearEquiv
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ } = ψ

Tactic:
cases ψ

Goal state after:
case mk''.mk''
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
toContinuousLinearEquiv✝¹ : W ≃L[R] V
cont✝¹ : Continuous (↑↑toContinuousLinearEquiv✝¹).toFun
isIntertwining'✝¹ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ }
toContinuousLinearEquiv✝ : W ≃L[R] V
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h :
  { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹,
        isIntertwining' := isIntertwining'✝¹ }.toContinuousLinearEquiv =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
        isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: case mk''
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
ψ : ρ.Equiv σ
toContinuousLinearEquiv✝ : V ≃L[R] W
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h : ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ } = ⇑ψ
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ } = ψ

Tactic:
cases ψ

Goal state after:
case mk''.mk''
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
toContinuousLinearEquiv✝¹ : V ≃L[R] W
cont✝¹ : Continuous (↑↑toContinuousLinearEquiv✝¹).toFun
isIntertwining'✝¹ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ }
toContinuousLinearEquiv✝ : V ≃L[R] W
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h :
  ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A B C : Rep k G
x✝ : Rep k G
⊢ ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑x✝ ↑x✝) (Hom.hom (𝟙 x✝)).toLinearMap, isIntertwining' := ⋯ } =
    𝟙 (of (A.ρ.linHom x✝.ρ))

Tactic:
ext; rfl

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

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A B C : Rep k G
X✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑X✝ ↑Z✝) (Hom.hom (x✝¹ ≫ x✝)).toLinearMap, isIntertwining' := ⋯ } =
    ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑X✝ ↑Y✝) (Hom.hom x✝¹).toLinearMap, isIntertwining' := ⋯ } ≫
      ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑Y✝ ↑Z✝) (Hom.hom x✝).toLinearMap, isIntertwining' := ⋯ }

Tactic:
ext; rfl

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

Goal state before:
pp: k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
A B : Rep k G
⊢ (Hom.hom ((ihom.ev A).app B)).toLinearMap =
    (TensorProduct.uncurry (RingHom.id k) (↑A) (↑A →ₗ[k] ↑B) ↑B) LinearMap.id.flip

Tactic:
ext; rfl

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Action (Type u) G
⊢ ofHom (μ X Y) ▷ (linearization k G).obj Z ≫ ofHom (μ (X ⊗ Y) Z) ≫ (linearization k G).map (α_ X Y Z).hom =
    (α_ ((linearization k G).obj X) ((linearization k G).obj Y) ((linearization k G).obj Z)).hom ≫
      (linearization k G).obj X ◁ ofHom (μ Y Z) ≫ ofHom (μ X (Y ⊗ Z))

Tactic:
ext1; simp [μ_comp_assoc _]

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
a : ↑A
⊢ (A.ρ ⟨g * g⁻¹, ⋯⟩) a = a

pp: case hc
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
⊢ (QuotientGroup.rightRel S) g g

Tactic:
· simp [← S.1.one_def]

Goal state after:
case hc
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
⊢ (QuotientGroup.rightRel S) g g
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
inst✝ : S.FiniteIndex
x✝¹ x✝ : ↑(coind.{u, v, v, w} S.subtype A)
⊢ ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑(x✝¹ + x✝) g)) ⋯ =
    ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑x✝¹ g)) ⋯ +
      ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑x✝ g)) ⋯

Tactic:
by simpa [← Finset.sum_add_distrib, TensorProduct.tmul_add] using
      Finset.sum_congr rfl fun z _ => Quotient.inductionOn z fun _ => by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x✝¹ : ↑(leftRegular k G)
x✝ : x✝¹ ∈ (Hom.hom (leftRegular k G).norm).range
w✝ : ↑(leftRegular k G)
h : (Hom.hom (leftRegular k G).norm).toLinearMap w✝ = x✝¹
⊢ x✝¹ ∈ (Hom.hom ((leftRegular k G).applyAsHom g - 𝟙 (leftRegular k G))).ker

Tactic:
by simp [sub_hom, applyAsHom_apply _, ← h, norm]

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 x✝ : Rep k G
⊢ indMap φ (𝟙 x✝) = 𝟙 (ind φ x✝)

Tactic:
ext; rfl

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 X✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ indMap φ (x✝¹ ≫ x✝) = indMap φ x✝¹ ≫ indMap φ x✝

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
j : Discrete (Fin ((Opposite.unop Y✝).len + 1))
⊢ limit.lift (Discrete.functor fun x ↦ Action.ofMulAction G G)
        (Fan.mk (∏ᶜ fun x ↦ Action.ofMulAction G G) fun i ↦
          Pi.π (fun x ↦ Action.ofMulAction G G) ((SimplexCategory.Hom.toOrderHom f.unop) i)) ≫
      limit.π (Discrete.functor fun i ↦ Action.ofMulAction G G) j =
    ((limit.isoLimitCone (Action.ofMulActionLimitCone G fun x ↦ G)).hom ≫ (classifyingSpaceUniversalCover G).map f) ≫
      (Action.ofMulActionLimitCone G fun x ↦ G).cone.π.app j

Tactic:
limit.lift_π,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
j : Discrete (Fin ((Opposite.unop Y✝).len + 1))
⊢ (Fan.mk (∏ᶜ fun x ↦ Action.ofMulAction G G) fun i ↦
            Pi.π (fun x ↦ Action.ofMulAction G G) ((SimplexCategory.Hom.toOrderHom f.unop) i)).π.app
      j =
    ((limit.isoLimitCone (Action.ofMulActionLimitCone G fun x ↦ G)).hom ≫ (classifyingSpaceUniversalCover G).map f) ≫
      (Action.ofMulActionLimitCone G fun x ↦ G).cone.π.app j
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: case h
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
hxinv : (Algebra.norm K) x⁻¹ = 1
y : Lˣ
hy : g ↑y = x⁻¹ * ↑y
⊢ ↑y / (x⁻¹ * ↑y) = x

Tactic:
field_simp

Goal state after:
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
hf : Function.Surjective ⇑f
inst✝ : Mono φ
i : ℕ
⊢ Mono ((cochainsMap f φ).f i)

Tactic:
simpa [ModuleCat.mono_iff_injective] using!
    ((Rep.mono_iff_injective φ).1 inferInstance).comp_left.comp <|
    LinearMap.funLeft_injective_of_surjective k A _ hf.comp_left

Goal state after:
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
⊢ H1π A ≫ map f φ 1 = mapCocycles₁ f φ ≫ H1π B

Tactic:
simp [H1π, Iso.inv_comp_eq, ← cocyclesMap_comp_isoCocycles₁_hom_assoc]

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

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

Tactic:
apply le_antisymm
  · simp [idealOfVars, Ideal.span_le, Set.range_subset_iff, restrictSupportIdeal, X]
  · simp only [SetLike.le_def, restrictSupportIdeal, Submodule.mem_mk, Submodule.mem_toAddSubmonoid,
      ← Submodule.restrictScalars_mem R (idealOfVars σ R)]
    rw [← SetLike.le_def, restrictSupport_eq_span, Submodule.span_le, Set.image_subset_iff]
    intro x hx
    obtain ⟨i, hi⟩ : x.support.Nonempty := by aesop
    obtain ⟨c, rfl⟩ := le_iff_exists_add'.mp (show single i 1 ≤ x by simp_all; lia)
    simpa [monomial_add_single] using Ideal.mul_mem_left _ _ (Ideal.subset_span (by simp))

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
p : MvPowerSeries σ R
⊢ (rename f) p = subst (X ∘ f) p

Tactic:
classical
  ext n
  rw [coeff_rename, coeff_subst (HasSubst.X_comp _) p n, finsum_eq_sum _
    (coeff_subst_finite (HasSubst.X_comp _) p n)]
  have (d : σ →₀ ℕ) (hd : (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0) :
      mapDomain f d = n := by
    simp_rw [← monomial_mapDomain_apply_one] at hd
    exact (eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hd)).symm
  refine (Finset.sum_subset_zero_on_sdiff ?_ ?_ (fun x hx => ?_)).symm
  · exact Set.Finite.toFinset_mono this
  · simp +contextual [← monomial_mapDomain_apply_one]
  · simp only [Set.Finite.mem_toFinset] at hx
    simp [← this _ hx, ← monomial_mapDomain_apply_one, coeff_monomial_same]

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
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
r : R
⊢ r ∈ S → r ∈ ⇑constantCoeff '' ↑I

Tactic:
hr

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
r : R
hr : r ∈ S
⊢ r ∈ ⇑constantCoeff '' ↑I
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
r₁ r₂ : R
⊢ r₁ ∈ Submodule.span R S →
    r₂ ∈ Submodule.span R S →
      (∃ x ∈ span T, constantCoeff x = r₁) →
        (∃ x ∈ span T, constantCoeff x = r₂) → ∃ x ∈ span T, constantCoeff x = r₁ + r₂

Tactic:
hr₁

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
r₁ r₂ : R
hr₁ : r₁ ∈ Submodule.span R S
⊢ r₂ ∈ Submodule.span R S →
    (∃ x ∈ span T, constantCoeff x = r₁) →
      (∃ x ∈ span T, constantCoeff x = r₂) → ∃ x ∈ span T, constantCoeff x = r₁ + r₂
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case refine_3
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
r₁ r₂ : R
⊢ r₂ ∈ Submodule.span R S → (∃ x ∈ span T, constantCoeff x = r₂) → ∃ x ∈ span T, constantCoeff x = r₁ • r₂

Tactic:
hr₁

Goal state after:
case refine_3
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
r₁ r₂ : R
hr₁ : r₂ ∈ Submodule.span R S
⊢ (∃ x ∈ span T, constantCoeff x = r₂) → ∃ x ∈ span T, constantCoeff x = r₁ • r₂
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
p : MvPolynomial σ R
n : ℕ
this : p - (truncTotal n) ↑p ∈ MvPolynomial.idealOfVars σ R ^ n
⊢ ↑((AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) p) n = ↑((toAdicCompletion σ R) ↑p) n

Tactic:
by
    simpa [toAdicCompletion, AdicCompletion.liftAlgHom, AdicCompletion.liftRingHom,
      Ideal.Quotient.mk_eq_mk_iff_sub_mem]

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

Goal state before:
pp: k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ mapShortComplexH1 (g.comp f) (φ ≫ (resFunctor f).map ψ) = mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ

Tactic:
by
  refine ShortComplex.hom_ext _ _ ?_ ?_ rfl
  all_goals
  { simp only [shortComplexH1]
    ext
    simp [Prod.map]}

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
⊢ RingHom.ker (evalOneₐ I).toRingHom = Ideal.map (algebraMap R (AdicCompletion I R)) I

Tactic:
ext x
  trans x ∈ (AdicCompletion.eval I R 1).ker
  · have eq : I ^ 1 * ⊤ = I := by simp
    have : Function.Injective (Ideal.Quotient.factor ((le_of_eq eq))) := by
      simpa [RingHom.injective_iff_ker_eq_bot, Ideal.Quotient.factor_ker]
        using Ideal.map_mk_eq_bot_of_le (le_of_eq eq.symm)
    simpa [← factorₐ_evalₐ_one, ← factor_eval_eq_evalₐ] using map_eq_zero_iff _ this
  · simp [← pow_smul_top_eq_ker_eval fg]

Goal state after: