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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
⊢ Indep (⨆ n, s n) (limsup s f) κ μα

Tactic:
suffices (⨆ a, ⨆ n ∈ ns a, s n) = ⨆ n, s n by
    rw [← this]
    exact indep_iSup_directed_limsup h_le h_indep hf hns hnsp
  rw [iSup_comm]
  refine iSup_congr fun n => ?_
  have h : ⨆ (i : β) (_ : n ∈ ns i), s n = ⨆ _ : ∃ i, n ∈ ns i, s n := by rw [iSup_exists]
  have : Nonempty (∃ i : β, n ∈ ns i) := ⟨hns_univ n⟩
  rw [h, iSup_const]

Goal state after:
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) ns

pp: case refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a

Tactic:
· exact Antitone.directed_le fun _ _ ↦ Set.Ici_subset_Ici.2

Goal state after:
case refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: case 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}
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
q : ℚ
hqa : ↑a < ↑q
hqI : 0 ≤ q ∧ ↑q ≤ 1
h : (κ e.1).real (Icc 0 ⟨↑q, ⋯⟩) < ↑e.2
⊢ a < ⟨↑q, ⋯⟩

Tactic:
change a.1 < q

Goal state after:
case 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}
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
q : ℚ
hqa : ↑a < ↑q
hqI : 0 ≤ q ∧ ↑q ≤ 1
h : (κ e.1).real (Icc 0 ⟨↑q, ⋯⟩) < ↑e.2
⊢ ↑a < ↑q
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (∫ (x : Ω) in s, g x ∂μ.tilted fun x ↦ t * X x) = ∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ

Tactic:
· simp_rw [setIntegral_tilted_mul_eq_mgf' _ hs, exp_sub, exp_cgf ht]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ Var[X; μ.tilted fun x ↦ t * X x] = iteratedDeriv 2 (cgf X μ) t

Tactic:
by
  rw [variance_eq_integral]
  swap; · exact (memLp_tilted_mul ht 1).aestronglyMeasurable.aemeasurable
  rw [integral_tilted_mul_self ht, iteratedDeriv_two_cgf_eq_integral ht, integral_tilted_mul_eq_mgf,
    ← integral_div]
  simp only [smul_eq_mul]
  congr with ω
  ring

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

Goal state before:
pp: case mpr
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
⊢ (∃ a, 0 < a ∧ ↑a ≤ X ω) → 0 < X ω

Tactic:
intro ⟨q, h1, h2⟩

Goal state after:
case mpr
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
q : ℚ
h1 : 0 < q
h2 : ↑q ≤ X ω
⊢ 0 < X ω
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
⊢ ∃ T, Tendsto T atTop atTop ∧ ∀ (n : ℕ), ∃ k, P {ω | σ n k ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n

Tactic:
obtain ⟨T, -, hT⟩ := Filter.exists_seq_monotone_tendsto_atTop_atTop ι

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
⊢ ∃ T, Tendsto T atTop atTop ∧ ∀ (n : ℕ), ∃ k, P {ω | σ n k ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
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 : ℚ
ω' : Ω'
⊢ (∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)) →
    Integrable (fun y ↦ rexp (↑q * X y)) (κ ω') →
      (∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)) →
        Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω') →
          mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') ↑q ≤ rexp (↑(c + cY) * ↑q ^ 2 / 2)

Tactic:
hX_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)
⊢ Integrable (fun y ↦ rexp (↑q * X y)) (κ ω') →
    (∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)) →
      Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω') →
        mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') ↑q ≤ rexp (↑(c + cY) * ↑q ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
r : ℝ
⊢ HasSubgaussianMGF (fun ω ↦ r * X ω) (⟨r ^ 2, ⋯⟩ * c) μ

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at h ⊢
  exact Kernel.HasSubgaussianMGF.const_mul h r

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
ht : 0 < t
⊢ mgf X μ t ≤ rexp ((↑‖b - a‖₊ / 2) ^ 2 * t ^ 2 / 2)

Tactic:
have hi (u : ℝ) : Integrable (fun ω ↦ exp (u * X ω)) μ := integrable_exp_mul_of_mem_Icc hm hb
  have hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ) := by simp [hi, integrableExpSet]
  obtain ⟨u, h1, h2⟩ := exists_cgf_eq_iteratedDeriv_two_cgf_mul ht hc hs
  rw [← exp_cgf (hi t), exp_le_exp, h2]
  gcongr
  calc
  _ = Var[X; μ.tilted (u * X ·)] := by
    rw [← variance_tilted_mul (hs (Set.mem_Icc_of_Ioo h1))]
  _ ≤ ((b - a) / 2) ^ 2 := by
    convert! variance_le_sq_of_bounded ((tilted_absolutelyContinuous μ (u * X ·)) hb) _
    · exact isProbabilityMeasure_tilted (hi u)
    · exact hm.mono_ac (tilted_absolutelyContinuous μ (u * X ·))
  _ = (‖b - a‖₊ / 2) ^ 2 := by simp [field]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
X : ModuleCat k
Y : Rep k G
f : (trivialFunctor k G).obj X ⟶ Y
⊢ ∀ (c : ↑((trivialFunctor k G).obj X)), (Hom.hom f).toLinearMap c ∈ Y.ρ.invariants

Tactic:
intro _ _

Goal state after:
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
X : ModuleCat k
Y : Rep k G
f : (trivialFunctor k G).obj X ⟶ Y
c✝ : ↑((trivialFunctor k G).obj X)
g✝ : G
⊢ (Y.ρ g✝) ((Hom.hom f).toLinearMap c✝) = (Hom.hom f).toLinearMap c✝
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
f : ρ.IntertwiningMap σ
inst✝ : ρ.IsIrreducible
⊢ Injective ⇑f ∨ f = 0

Tactic:
rw [← 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
f : ρ.IntertwiningMap σ
inst✝ : ρ.IsIrreducible
⊢ Injective ⇑f ∨ (equivLinearMapAsModule ρ σ) f = 0
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
f : ρ.IntertwiningMap σ
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
⊢ Bijective ⇑f ∨ f = 0

Tactic:
rw [← 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
f : ρ.IntertwiningMap σ
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
⊢ Bijective ⇑f ∨ (equivLinearMapAsModule ρ σ) f = 0
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
g : G
v : W
⊢ ∑ g_1, MonoidAlgebra.single g_1⁻¹ 1 • π (MonoidAlgebra.single g_1 1 • MonoidAlgebra.single g 1 • v) =
    ∑ x, MonoidAlgebra.single g 1 • MonoidAlgebra.single x⁻¹ 1 • π (MonoidAlgebra.single x 1 • v)

Tactic:
refine Fintype.sum_bijective (· * g) (Group.mulRight_bijective g) _ _ fun i ↦ ?_

Goal state after:
k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i✝ : V →ₗ[k[G]] W
inst✝ : Fintype G
g : G
v : W
i : G
⊢ MonoidAlgebra.single i⁻¹ 1 • π (MonoidAlgebra.single i 1 • MonoidAlgebra.single g 1 • v) =
    MonoidAlgebra.single g 1 • MonoidAlgebra.single (i * g)⁻¹ 1 • π (MonoidAlgebra.single (i * g) 1 • v)
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:
indToCoindAux_of_not_rel (h := h),

Goal state after:
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₂ = 0
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₃ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) (g₂ * g₃⁻¹) g₁
⊢ (A.indToCoindAux g₁) a (g₂ * g₃⁻¹) = (A.indToCoindAux (g₁ * g₃)) a g₂

Tactic:
indToCoindAux_of_not_rel (h := h),

Goal state after:
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₃ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) (g₂ * g₃⁻¹) g₁
⊢ 0 = (A.indToCoindAux (g₁ * g₃)) a g₂
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ ((HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).map
      (forget₂ (Rep k G) (ModuleCat k))).Exact

Tactic:
rw [ShortComplex.moduleCat_exact_iff_range_eq_ker]

Goal state after:
case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ (ModuleCat.Hom.hom
        ((HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).map
            (forget₂ (Rep k G) (ModuleCat k))).f).range =
    (ModuleCat.Hom.hom
        ((HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).map
            (forget₂ (Rep k G) (ModuleCat k))).g).ker
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
⊢ (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨⟨ContinuousMap.const G x, ⋯⟩, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨σ, hσ⟩ => ⟨↑σ 1, ⋯⟩)
        ⟨⟨x, hx'⟩, hx⟩) =
    ⟨⟨x, hx'⟩, hx⟩

Tactic:
by
    ext g
    rw [LinearMap.mem_ker, Subtype.ext_iff, ContinuousLinearMap.coe_coe,
      homogeneousCochains.d_apply] at hx
    simp only [Nat.reduceAdd, d_succ, d_zero, ConcreteCategory.hom_ofHom, hom_sub,
      ContIntertwiningMap.sub_apply, coind₁ι_toFun, coind₁Map_toFun, ZeroMemClass.coe_zero,
      sub_eq_zero, ContinuousMap.const_apply] at hx ⊢
    simpa using DFunLike.ext_iff.1 (DFunLike.ext_iff.1 hx g) 1

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)
α : (G → k) →ₗ[k] G → k := Hom.hom (η.hom.hom.app rightFDRep).hom
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (η.inv.hom.app rightFDRep).hom
⊢ α 1 = 1

Tactic:
suffices α (α_inv 1) = (1 : G → k) by
    have h := this
    rwa [← one_mul (α_inv 1), map_mul_toRightFDRepComp, h, mul_one] at this

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (η.hom.hom.app rightFDRep).hom
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (η.inv.hom.app rightFDRep).hom
⊢ α (α_inv 1) = 1
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 : σ
⊢ x ∉ ⋃ i ∈ ↑d.support, f ⁻¹' {i} → x ∉ {s | (coeff d) ((X ∘ f) s) ≠ 0}

Tactic:
intro _ _

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.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

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

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p : MvPowerSeries (Option σ) R
n : ℕ
x : σ →₀ ℕ
⊢ (coeff x) ((PowerSeries.coeff n) (PowerSeries.mk fun n x ↦ (coeff (optionElim n x)) p)) = (coeff (optionElim n x)) p

Tactic:
PowerSeries.coeff_mk

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p : MvPowerSeries (Option σ) R
n : ℕ
x : σ →₀ ℕ
⊢ ((coeff x) fun x ↦ (coeff (optionElim n x)) p) = (coeff (optionElim n x)) p
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff (Finsupp.cons k x)) (X j.succ) = (coeff x) ((PowerSeries.coeff k) (PowerSeries.C (X j)))

Tactic:
PowerSeries.coeff_C,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff (Finsupp.cons k x)) (X j.succ) = (coeff x) (if k = 0 then X j else 0)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff (Finsupp.cons k x)) (C r) = (coeff x) ((PowerSeries.coeff k) (PowerSeries.C (C r)))

Tactic:
PowerSeries.coeff_C,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff (Finsupp.cons k x)) (C r) = (coeff x) (if k = 0 then C r else 0)
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
inst✝ : IsAdicComplete I S
F : R →+* S
hF : ∀ (n : ℕ), (Ideal.Quotient.mk (I ^ a n)).comp F = f n
⊢ ⇑F = ⇑(liftRingHom I ha f ⋯)

Tactic:
apply IsHausdorff.StrictMono.funext' I ha

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
inst✝ : IsAdicComplete I S
F : R →+* S
hF : ∀ (n : ℕ), (Ideal.Quotient.mk (I ^ a n)).comp F = f n
⊢ ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ a n)) (F r) = (Ideal.Quotient.mk (I ^ a n)) ((liftRingHom I ha f ⋯) r)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
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
n : ℕ
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ (A.quotientToCoinvariants S))
y : ↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S)))
hy : (ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) ((A.toCoinvariants S).resOfQuotientIso S).inv)) y = x
Y : G →₀ ↑A
hY : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Y = ↑y
this : (ConcreteCategory.hom (d₁₀ A)) Y ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)
Z : ↥S →₀ ↑A
hZ : (ConcreteCategory.hom (chains₁ToCoinvariantsKer (res S.subtype A))) Z = ⟨(ConcreteCategory.hom (d₁₀ A)) Y, this⟩
H : (ConcreteCategory.hom (d₁₀ A)) (Y - mapDomain (⇑S.subtype) Z) = 0
⊢ ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S)))
          ⟨Y - mapDomain Subtype.val Z, ⋯⟩) -
      ↑x ∈
    boundaries₁ (A.quotientToCoinvariants S)

Tactic:
simpa [← hy, mapCycles₁_hom, map_sub, Rep.hom_id (res _ _), ← mapDomain_comp,
    ← mapDomain_mapRange, hY, Function.comp_def, (QuotientGroup.eq_one_iff <| Subtype.val _).2
    (Subtype.prop _)] using! Submodule.finsuppSum_mem _ _ _ _ fun _ _ ↦ single_one_mem_boundaries₁ _

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

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_8
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Bialgebra R A
inst✝ : CommMonoid M
f g : WithConv (R[M] →ₐc[R] A)
x : M
⊢ (f * g).ofConv (single x 1) = f.ofConv (single x 1) * g.ofConv (single x 1)

Tactic:
by
  simp only [BialgHom.convMul_def, BialgHom.coe_comp, Function.comp_apply]
  change mulBialgHom R A (Bialgebra.TensorProduct.map f.ofConv g.ofConv (comul (single x 1))) = _
  simp [Bialgebra.TensorProduct.map_tmul]

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

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
⊢ x ∈ Set.range fun x ↦ single x 1

Tactic:
by_contra h
    have : LinearIndepOn R id (insert x <| .range (single · 1)) :=
      linearIndepOn_isGroupLikeElem.mono <| by simp [Set.subset_def, hx]
    have : x.coeff.sum single ∉ span R (.range (single · 1)) := by
      simpa using this.notMem_span_of_insert h
    refine this <| sum_mem fun g hg ↦ ?_
    rw [← mul_one (x.coeff g), ← smul_eq_mul, ← smul_single]
    exact smul_mem _ _ <| subset_span <| Set.mem_range_self _

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

Goal state before:
pp: case add
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
x y : DividedPowerAlgebra R M
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hy : y ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ x + y ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
exact Submodule.add_mem _ hx hy

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

Goal state before:
pp: case dp.mem.add
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x✝ : DividedPowerAlgebra R M
k : ℕ
i : ι
x y : DividedPowerAlgebra R M
hxmem : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hymem : y ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hx : x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hy : y * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ x * dp R k (v i) + y * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
exact Submodule.add_mem _ hx hy

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

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
n : ℕ
r : R
m : M
⊢ hI.dpow n (g (r • m)) = r ^ n • hI.dpow n (g m)

Tactic:
LinearMap.map_smulₛₗ,

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
n : ℕ
r : R
m : M
⊢ hI.dpow n ((RingHom.id R) r • g m) = r ^ n • hI.dpow n (g m)