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

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
⊢ Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)

Tactic:
Measure.map_map (by fun_prop) (by fun_prop)

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
⊢ Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e ∘ fun a ↦ (k a, g a, f a)) μ
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
suffices (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0 by
    filter_upwards [this] with ω hω
    simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
⊢ (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
suffices (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0 by
    filter_upwards [this] with ω hω
    simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
⊢ (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
⊢ mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') ↑q =
    ∫ (x : Ω), rexp (↑q * X x) * ∫ (y : Ω''), rexp (↑q * Y y) ∂η (ω', x) ∂κ ω'

Tactic:
mgf,

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
⊢ ∫ (x : Ω × Ω''), rexp (↑q * (X x.1 + Y x.2)) ∂(κ ⊗ₖ η) ω' =
    ∫ (x : Ω), rexp (↑q * X x) * ∫ (y : Ω''), rexp (↑q * Y y) ∂η (ω', x) ∂κ ω'
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ mgf X (μ.trim hm) t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
mgf,

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ ∫ (x : Ω), (fun ω ↦ rexp (t * X ω)) x ∂μ.trim hm ≤ rexp (↑c * t ^ 2 / 2)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e_f.e_a.h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
N i : ℕ
⊢ (↑(range (u i))).Pairwise fun i j ↦ Y i ⟂ᵢ Y j

Tactic:
intro k _ l _ hkl
          exact (hindep hkl).comp (A k).measurable (A l).measurable

Goal state after:
Module: Mathlib.RepresentationTheory.Irreducible

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁶ : Monoid G
inst✝⁵ : Field k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AddCommGroup W
inst✝¹ : Module k W
ρ : Representation k G V
σ : Representation k G W
inst✝ : ρ.IsIrreducible
g : σ.IntertwiningMap ρ
⊢ Surjective ⇑g ∨ g = 0

Tactic:
← LinearEquiv.map_eq_zero_iff (equivLinearMapAsModule σ ρ)

Goal state after:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁶ : Monoid G
inst✝⁵ : Field k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AddCommGroup W
inst✝¹ : Module k W
ρ : Representation k G V
σ : Representation k G W
inst✝ : ρ.IsIrreducible
g : σ.IntertwiningMap ρ
⊢ Surjective ⇑g ∨ (equivLinearMapAsModule σ ρ) g = 0
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
⊢ (↑(Nat.card G))⁻¹ * ∑ g, W.character g * V.character g⁻¹ = ↑(finrank k (V ⟶ W))

Tactic:
conv_lhs => congr; rfl; congr; rfl; intro _; rw [mul_comm, ← FDRep.char_linHom]

Goal state after:
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
⊢ (↑(Nat.card G))⁻¹ * Finset.univ.sum (of (linHom V.ρ W.ρ)).character = ↑(finrank k (V ⟶ W))
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
ι : Type u'
M N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module k M
inst✝ : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
s : Finset ι
⊢ ofHom (∑ i ∈ s, f i) = ∑ i ∈ s, ofHom (f i)

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s ha h => simp [Finset.sum_insert ha, ofHom_add, h]

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case refine_2
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
hf : f ≠ 0
⊢ Epi (Abelian.image.ι f)

Tactic:
rw [← Abelian.image.fac f] at hf

Goal state after:
case refine_2
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
hf : Abelian.factorThruImage f ≫ Abelian.image.ι f ≠ 0
⊢ Epi (Abelian.image.ι f)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
            snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
            inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
            inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.fst ≫
        { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
            snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
            inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
            inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.inl +
      { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
            snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
            inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
            inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.snd ≫
        { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
            snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
            inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
            inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.inr =
    𝟙
      { pt := of (A.ρ.prod B.ρ), fst := ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ),
          snd := ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ),
          inl := ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ),
          inr := ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ), inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
          inr_snd := ⋯ }.pt

Tactic:
by
    ext1; simp [Rep.add_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

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

Tactic:
rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]
    exact mt (fun ⟨s₁, hs₁⟩ => ⟨s₁ * s, by simp_all [S.1.smul_def, mul_assoc]⟩) h

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

Goal state before:
pp: case a.a.a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.hom ≫ (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.inv

pp: case a.a.a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| ((barComplex k G).linearYonedaObj k A).d (n + 1) (n + 1 + 1)

pp: case a.a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A).toModuleIso.hom

pp: case a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv

pp: case a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| ((barComplex k G).linearYonedaObj k A).d n (n + 1)

Tactic:
rw [Iso.hom_inv_id]

Goal state after:
case a.a.a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| 𝟙 (((barComplex k G).linearYonedaObj k A).X (n + 1))

case a.a.a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| ((barComplex k G).linearYonedaObj k A).d (n + 1) (n + 1 + 1)

case a.a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A).toModuleIso.hom

case a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv

case a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| ((barComplex k G).linearYonedaObj k A).d n (n + 1)
Module: Mathlib.RepresentationTheory.Homological.Resolution

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

Tactic:
Limits.comp_zero

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
m : ℕ
⊢ 0 = 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
i j : ℕ
y : (Fin i → G) → ↑X.X₂
x : (Fin j → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d X.X₁ j)) x = 0

Tactic:
simpa [CochainComplex.of.d] using!
    ((map_cochainsFunctor_shortExact hX).d_eq_zero_of_f_eq_d_apply i j y x
      (by simpa using! hx) (j + 1))

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

Goal state before:
pp: case a.a.a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.hom ≫
    (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.inv

pp: case a.a.a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n

pp: case a.a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom

pp: case a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G)).toModuleIso.inv

pp: case a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1)

Tactic:
rw [Iso.hom_inv_id]

Goal state after:
case a.a.a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| 𝟙 ((HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X (n + 1))

case a.a.a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n

case a.a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom

case a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G)).toModuleIso.inv

case a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i j : ℕ
hij : j + 1 = i
z : (Fin i → G) →₀ ↑X.X₃
hz : (ConcreteCategory.hom ((inhomogeneousChains X.X₃).d i j)) z = 0
y : (Fin i → G) →₀ ↑X.X₂
hy : (ConcreteCategory.hom ((chainsMap (MonoidHom.id G) X.g).f i)) y = z
x : (Fin j → G) →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom ((inhomogeneousChains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom (δ hX i j hij)) ((ConcreteCategory.hom (π X.X₃ i)) (cyclesMk i j ⋯ z ⋯)) =
    (ConcreteCategory.hom (π X.X₁ j)) (cyclesMkOfCompEqD hX hx)

Tactic:
exact (map_chainsFunctor_shortExact hX).δ_apply i j hij z hz y hy x (by simpa using! hx) _ rfl

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
x : σ →₀ ℕ
r : R
⊢ renameFun f ((monomial x) r) = (monomial (mapDomain f x)) r

Tactic:
ext; simp [coeff_renameFun, coeff_monomial, eq_comm]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : TendstoCofinite g
p : MvPowerSeries σ R
y : γ →₀ ℕ
⊢ (coeff y) ((rename g) ((rename f) p)) = (coeff y) ((rename (g ∘ f)) p)

Tactic:
simp only [coeff_rename]

Goal state after:
σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : TendstoCofinite g
p : MvPowerSeries σ R
y : γ →₀ ℕ
⊢ ∑ x ∈ ⋯.toFinset, ∑ x ∈ ⋯.toFinset, (coeff x) p = ∑ x ∈ ⋯.toFinset, (coeff x) p
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 ↔ _

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : G × G →₀ ↑A
⊢ (x.sum fun g a ↦ ((fun g ↦ lsingle g.2 ∘ₗ A.ρ g.1⁻¹ - lsingle (g.1 * g.2) + lsingle g.1) g) a) = 0 ↔
    (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
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: case mem.inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : IsUnit z
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z

pp: case mem.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : Prime z
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z

Tactic:
· exact ⟨∅, by simpa using (associated_one_iff_isUnit.2 h).symm⟩

Goal state after:
case mem.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : Prime z
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
⊢ IsAdic ⊥ ↔ DiscreteTopology A

Tactic:
by
  rw [isAdic_iff]
  constructor
  · rintro ⟨h, _h'⟩
    rw [discreteTopology_iff_isOpen_singleton_zero]
    simpa using h 1
  · intros
    constructor
    · simp
    · intro U U_nhds
      use 1
      simp [mem_of_mem_nhds U_nhds]

Goal state after:
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
⊢ chainsMap f 0 = 0

Tactic:
by
  ext; simp [chainsMap_f, LinearMap.zero_apply (M₂ := B)]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (truncTotal n) (toAdicCompletionInv σ R f) - Quotient.out (↑f n) ∈ MvPolynomial.idealOfVars σ R ^ n • ⊤

Tactic:
simp only [smul_eq_mul, Ideal.mul_top, MvPolynomial.mem_pow_idealOfVars_iff',
    MvPolynomial.coeff_sub]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ ∀ (x : σ →₀ ℕ),
    degree x < n →
      MvPolynomial.coeff x ((truncTotal n) (toAdicCompletionInv σ R f)) - MvPolynomial.coeff x (Quotient.out (↑f n)) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ (MvPowerSeries.rename fun x ↦ i) (MvPowerSeries.X ()) = MvPowerSeries.X i

Tactic:
MvPowerSeries.rename_X

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ MvPowerSeries.X i = MvPowerSeries.X i
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_1
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 ψ).τ₁

pp: case refine_2
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:
all_goals
  { simp only [shortComplexH1]
    ext
    simp [Prod.map]}

Goal state after:
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
φ : A ⟶ res 1 B
x : ↑(ModuleCat.of k ↥(cycles₁ A))
⊢ (ModuleCat.Hom.hom (mapCycles₁ 1 φ ≫ H1π B)) x = (ModuleCat.Hom.hom 0) x

Tactic:
ModuleCat.hom_comp

Goal state after:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
φ : A ⟶ res 1 B
x : ↑(ModuleCat.of k ↥(cycles₁ A))
⊢ (ModuleCat.Hom.hom (H1π B) ∘ₗ ModuleCat.Hom.hom (mapCycles₁ 1 φ)) x = (ModuleCat.Hom.hom 0) x