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

Goal state before:
pp: p : ↑unitInterval
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
⊢ Integrable f (Measure.sum fun n ↦ ENNReal.ofReal ((1 - ↑p) ^ n * ↑p) • Measure.dirac n) ↔
    Summable fun n ↦ (1 - ↑p) ^ n * ↑p * ‖f n‖

Tactic:
integrable_sum_dirac_iff (by simp)

Goal state after:
p : ↑unitInterval
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
⊢ (Summable fun i ↦ (ENNReal.ofReal ((1 - ↑p) ^ i * ↑p)).toReal * ‖f i‖) ↔ Summable fun n ↦ (1 - ↑p) ^ n * ↑p * ‖f n‖
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
⊢ Integrable f (Measure.sum fun n ↦ ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !) • Measure.dirac n) ↔
    Summable fun n ↦ rexp (-↑r) * ↑r ^ n / ↑n ! * ‖f n‖

Tactic:
integrable_sum_dirac_iff (by simp)

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
⊢ (Summable fun i ↦ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ i / ↑i !)).toReal * ‖f i‖) ↔
    Summable fun n ↦ rexp (-↑r) * ↑r ^ n / ↑n ! * ‖f n‖
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
p : PMF α
x y : α
hy : y ≠ x
⊢ p y * 0 = 0

Tactic:
mul_zero

Goal state after:
α : Type u_1
p : PMF α
x y : α
hy : y ≠ x
⊢ 0 = 0
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
⊢ (p.bindOnSupport f).support = ⋃ a, ⋃ (h : a ∈ p.support), (f a h).support

Tactic:
by
  ext
  -- `simp` suffices; squeezed for performance
  simp only [mem_support_iff, bindOnSupport_apply, ne_eq, ENNReal.tsum_eq_zero,
    dite_eq_left_iff, mul_eq_zero, not_forall, not_or, and_exists_self,
    Set.mem_iUnion]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
H : ¬(f a' h) b = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * (g b ⋯) a)

Tactic:
absurd H

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
H : ¬(f a' h) b = 0
⊢ (f a' h) b = 0
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (P i)
i j : ι
hij : i ≠ j
⊢ map (fun ω ↦ (ω i, ω j)) (infinitePi P) = (P i).prod (P j)

Tactic:
rw [IndepFun.map_prod_eq_prod_map_map]; rotate_right
  · exact iIndepFun_infinitePi (X := fun x ω ↦ ω) (by fun_prop) |>.indepFun hij
  · simp [infinitePi_map_eval]
  all_goals exact Measurable.aemeasurable (by fun_prop)

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η₁ : Y₁✝ ⟶ Z₁✝
η₂ : Y₂✝ ⟶ Z₂✝
⊢ Kernel.id ∥ₖ η₂.hom ∘ₖ (η₁.hom ∥ₖ Kernel.id) ∘ₖ (Kernel.id ∥ₖ κ₂.hom ∘ₖ (κ₁.hom ∥ₖ Kernel.id)) =
    Kernel.id ∥ₖ (η₂.hom ∘ₖ κ₂.hom) ∘ₖ (η₁.hom ∘ₖ κ₁.hom ∥ₖ Kernel.id)

Tactic:
simp only [Kernel.id_parallelComp_comp_parallelComp_id]

Goal state after:
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η₁ : Y₁✝ ⟶ Z₁✝
η₂ : Y₂✝ ⟶ Z₂✝
⊢ η₁.hom ∥ₖ η₂.hom ∘ₖ (κ₁.hom ∥ₖ κ₂.hom) = η₁.hom ∘ₖ κ₁.hom ∥ₖ (η₂.hom ∘ₖ κ₂.hom)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
⊢ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      (Kernel.id ∥ₖ η.hom ∘ₖ (Kernel.id ∥ₖ κ₂.hom ∘ₖ (κ₁.hom ∥ₖ Kernel.id) ∥ₖ Kernel.id)) =
    Kernel.id ∥ₖ (Kernel.id ∥ₖ η.hom ∘ₖ (κ₂.hom ∥ₖ Kernel.id)) ∘ₖ (κ₁.hom ∥ₖ Kernel.id) ∘ₖ
      Kernel.deterministic ⇑prodAssoc ⋯

Tactic:
simp only [Kernel.id_parallelComp_comp_parallelComp_id]

Goal state after:
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
⊢ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ (κ₁.hom ∥ₖ κ₂.hom ∥ₖ η.hom) =
    κ₁.hom ∥ₖ (κ₂.hom ∥ₖ η.hom) ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.discard (X.carrier × Y.carrier) =
    Kernel.id.map Prod.snd ∘ₖ (Kernel.id ∥ₖ Kernel.discard Y.carrier ∘ₖ (Kernel.discard X.carrier ∥ₖ Kernel.id))

Tactic:
simp only [Kernel.id_parallelComp_comp_parallelComp_id]

Goal state after:
X Y : SFinKer
⊢ Kernel.discard (X.carrier × Y.carrier) =
    Kernel.id.map Prod.snd ∘ₖ (Kernel.discard X.carrier ∥ₖ Kernel.discard Y.carrier)
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: case e_6.mpr
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : ↑ξ ≤ (κ a).real (Icc 0 x)
⊢ ∀ b ∈ {x | (κ a).real (Icc 0 x) < ↑ξ}, b ≤ x

Tactic:
intro c

Goal state after:
case e_6.mpr
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : ↑ξ ≤ (κ a).real (Icc 0 x)
c : ↑I
⊢ c ∈ {x | (κ a).real (Icc 0 x) < ↑ξ} → c ≤ x
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ω' : Ω'
hm : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
t : ℝ
⊢ mgf (-X) (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
by simpa [mgf] using hm (-t)

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
⊢ {ω | ⊥ < hpX.localSeq n ω ∧ ⊥ < hqX.localSeq n ω}.indicator (stoppedProcess X (hpX.localSeq n ⊓ hqX.localSeq n) i) ω =
    {ω | ⊥ < hqX.localSeq n ω}.indicator
      ({ω | ⊥ < hpX.localSeq n ω}.indicator (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i)) ω

Tactic:
inf_comm (hpX.localSeq n)

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
⊢ {ω | ⊥ < hpX.localSeq n ω ∧ ⊥ < hqX.localSeq n ω}.indicator (stoppedProcess X (hqX.localSeq n ⊓ hpX.localSeq n) i) ω =
    {ω | ⊥ < hqX.localSeq n ω}.indicator
      ({ω | ⊥ < hpX.localSeq n ω}.indicator (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i)) ω
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k✝ : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁸ : Monoid G
inst✝⁷ : Semiring k✝
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k✝ V
inst✝⁴ : AddCommGroup W
inst✝³ : Module k✝ W
σ✝ : Representation k✝ G V
ρ✝ : Representation k✝ G W
X Y Z : Action (Type w) G
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
⊢ ↑(MonoidAlgebra.tensorEquiv k) ∘ₗ ((linearize k G X).tprod (linearize k G Y)) g =
    (linearize k G (X ⊗ Y)) g ∘ₗ ↑(MonoidAlgebra.tensorEquiv k)

Tactic:
by ext; simp [linearize_single _]; rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁵ : Monoid G
inst✝⁴ : Semiring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
X✝ Y Z : Action (Type w) G
X : Type w
g : G
⊢ ↑(LinearEquiv.refl k k[(Action.trivial G X).V]) ∘ₗ LinearMap.id =
    (trivial k G k[X]) g ∘ₗ ↑(LinearEquiv.refl k k[(Action.trivial G X).V])

Tactic:
LinearMap.comp_id

Goal state after:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁵ : Monoid G
inst✝⁴ : Semiring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
X✝ Y Z : Action (Type w) G
X : Type w
g : G
⊢ ↑(LinearEquiv.refl k k[(Action.trivial G X).V]) = ↑(LinearEquiv.refl k k[(Action.trivial G X).V])
Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic

Goal state before:
pp: A : Type u_1
V : Type u_2
k : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : Ring A
inst✝⁸ : Algebra k A
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module A V
inst✝⁴ : IsScalarTower k A V
inst✝³ : IsSimpleModule A V
inst✝² : FiniteDimensional k V
inst✝¹ : IsAlgClosed k
inst✝ : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
⊢ Module.finrank k V = 1

Tactic:
set U : Submodule A V := { Submodule.span k {v} with
    smul_mem' a w hw := by
      have ⟨t, ht⟩ := (IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed k).2
        (Module.toModuleEnd A V a)
      simpa only [← show _ = a • w from congr($ht w)] using! (k ∙ v).smul_mem t hw }

Goal state after:
A : Type u_1
V : Type u_2
k : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : Ring A
inst✝⁸ : Algebra k A
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module A V
inst✝⁴ : IsScalarTower k A V
inst✝³ : IsSimpleModule A V
inst✝² : FiniteDimensional k V
inst✝¹ : IsAlgClosed k
inst✝ : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
U : Submodule A V :=
  let __src := k ∙ v;
  { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := ⋯ }
⊢ Module.finrank k V = 1
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case mp
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
⊢ Y.ρ g ∘ₗ f ∘ₗ LinearMap.id = Y.ρ g ∘ₗ f

Tactic:
LinearMap.comp_id

Goal state after:
case mp
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
⊢ Y.ρ g ∘ₗ f = Y.ρ g ∘ₗ f
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case mpr
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
⊢ f ∘ₗ LinearMap.id = f

Tactic:
LinearMap.comp_id

Goal state after:
case mpr
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
⊢ f = f
Module: Mathlib.Probability.StrongLaw

Goal state before:
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 +instances only [pos, neg, ← integral_sub hint.pos_part hint.neg_part,
      max_zero_sub_max_neg_zero_eq_self, Function.comp_apply, mΩ]

Goal state after:
Module: Mathlib.Probability.StrongLaw

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

Tactic:
intro c

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

Goal state before:
pp: k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
A B C : Rep k G
f : B ⟶ (ihom A).obj C
⊢ (Hom.hom ((linearHomEquiv A B C).symm f)).toLinearMap =
    (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Hom.hom f).flip

Tactic:
simp [linearHomEquiv]

Goal state after:
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
A B C : Rep k G
f : B ⟶ (ihom A).obj C
⊢ (Hom.hom
        ({ toFun := ⇑(A.tensorHomEquiv B C), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(A.tensorHomEquiv B C).symm,
              left_inv := ⋯, right_inv := ⋯ }.symm
          f)).toLinearMap =
    (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Hom.hom f).flip
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
g : G
a : ↑A
⊢ A.coindToInd
      (A.indToCoind
        ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
          ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a))) =
    (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
      ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a)

Tactic:
coindToInd_of_support_subset_orbit g

Goal state after:
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 : G
a : ↑A
⊢ (IndV.mk S.subtype A.ρ g)
      (↑(A.indToCoind
            ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
              ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a)))
        g) =
    (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
      ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a)

case hx
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 : G
a : ↑A
⊢ Function.support
      ↑(A.indToCoind
          ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a))) ⊆
    MulAction.orbit (↥S) g
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x : ↑X
h : ContinuousMap.const G x ∈ (X.resolution'.X 0).ρ.invariants
⊢ ↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1)) ⟨ContinuousMap.const G x, h⟩ = 0

Tactic:
Subtype.ext_iff,

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x : ↑X
h : ContinuousMap.const G x ∈ (X.resolution'.X 0).ρ.invariants
⊢ ↑(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1)) ⟨ContinuousMap.const G x, h⟩) = ↑0
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x✝ : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
x : C(G, ↑X)
hx' : x ∈ (X.resolution'.X 0).ρ.invariants
hx✝ : ⟨x, hx'⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
hx : ↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1)) ⟨x, hx'⟩ = 0
g : G
⊢ ↑↑((fun x ↦
              match x with
              | ⟨x, hx⟩ => ⟨⟨ContinuousMap.const G x, ⋯⟩, ⋯⟩)
            ((fun x ↦
                match x with
                | ⟨σ, hσ⟩ => ⟨↑σ 1, ⋯⟩)
              ⟨⟨x, hx'⟩, hx✝⟩))
      g =
    ↑↑⟨⟨x, hx'⟩, hx✝⟩ g

Tactic:
Subtype.ext_iff,

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x✝ : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
x : C(G, ↑X)
hx' : x ∈ (X.resolution'.X 0).ρ.invariants
hx✝ : ⟨x, hx'⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
hx : ↑(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1)) ⟨x, hx'⟩) = ↑0
g : G
⊢ ↑↑((fun x ↦
              match x with
              | ⟨x, hx⟩ => ⟨⟨ContinuousMap.const G x, ⋯⟩, ⋯⟩)
            ((fun x ↦
                match x with
                | ⟨σ, hσ⟩ => ⟨↑σ 1, ⋯⟩)
              ⟨⟨x, hx'⟩, hx✝⟩))
      g =
    ↑↑⟨⟨x, hx'⟩, hx✝⟩ g
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
⊢ (ModuleCat.Hom.hom ((cochainsIso₀ X.X₃).inv ≫ (inhomogeneousCochains X.X₃).d 0 (0 + 1))) ↑z = 0

Tactic:
eq_d₀₁_comp_inv

Goal state after:
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
⊢ (ModuleCat.Hom.hom (d₀₁ X.X₃ ≫ (cochainsIso₁ X.X₃).inv)) ↑z = 0
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 ((cochainsIso₀ X.X₂).inv ≫ (inhomogeneousCochains X.X₂).d 0 (0 + 1))) y g

Tactic:
eq_d₀₁_comp_inv

Goal state after:
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
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
h :
  (shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso.hom =
    cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData.π ≫
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso.hom
⊢ (ConcreteCategory.hom (H2π A)) x = 0 ↔ ⇑x ∈ coboundaries₂ A

Tactic:
simp only [H2π, isoCocycles₂, π, HomologicalComplex.homologyπ, homologyπ,
    cyclesMapIso'_inv, leftHomologyπ, ← h, ← leftHomologyMapIso'_inv, ModuleCat.hom_comp,
    LinearMap.coe_comp, Function.comp_apply, map_eq_zero_iff _
    ((ModuleCat.mono_iff_injective <| _).1 inferInstance)]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
h :
  (shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso.hom =
    cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyData.π ≫
        (HomologicalComplex.sc (inhomogeneousCochains A) 2).leftHomologyIso.hom
⊢ (ModuleCat.Hom.hom (shortComplexH2 A).moduleCatLeftHomologyData.π) x = 0 ↔ ⇑x ∈ coboundaries₂ A
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✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map (↑e.symm) (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) n ≫
      map (↑e) (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n =
    𝟙 (groupCohomology B n)

Tactic:
by
    rw [← groupCohomology.map_comp, ← groupCohomology.map_id]
    exact map_congr (by simp) (by simp [res_id]) n

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPowerSeries (Fin (n + 1)) R
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff x) ((PowerSeries.coeff k) ((finSuccEquiv R n) p)) = (coeff (Finsupp.cons k x)) p

Tactic:
suffices coeff x (PowerSeries.coeff k (optionEquivLeft (Fin n) R
    (rename (_root_.finSuccEquiv n) p))) = coeff (Finsupp.cons k x) p by simpa [finSuccEquiv]

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPowerSeries (Fin (n + 1)) R
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff x) ((PowerSeries.coeff k) ((optionEquivLeft (Fin n) R) ((rename ⇑(_root_.finSuccEquiv n)) p))) =
    (coeff (Finsupp.cons k x)) p