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

Goal state before:
pp: case mp
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := ⋯
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
⊢ (∃ a_1, ∃ (h : 0 ≤ a_1 ∧ a_1 ≤ 1), (κ e.1).real (Icc 0 ⟨a_1, ⋯⟩) < ↑e.2 ∧ a < ⟨a_1, ⋯⟩) →
    ∃ i, ↑a < ↑i ∧ ∃ (x : 0 ≤ i ∧ ↑i ≤ 1), (κ e.1).real (Icc 0 ⟨↑i, ⋯⟩) < ↑e.2

pp: case mpr
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := ⋯
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
⊢ (∃ i, ↑a < ↑i ∧ ∃ (x : 0 ≤ i ∧ ↑i ≤ 1), (κ e.1).real (Icc 0 ⟨↑i, ⋯⟩) < ↑e.2) →
    ∃ a_2, ∃ (h : 0 ≤ a_2 ∧ a_2 ≤ 1), (κ e.1).real (Icc 0 ⟨a_2, ⋯⟩) < ↑e.2 ∧ a < ⟨a_2, ⋯⟩

Tactic:
· rintro ⟨y, hyI, y_mem, (hy : a.1 < y)⟩
        obtain ⟨q, hqa, hqy⟩ := exists_rat_btwn hy
        refine ⟨q, hqa, ⟨?_, hqy.le.trans hyI.2⟩, lt_of_lt_of_le' y_mem (h_monotone e.1 hqy.le)⟩
        simp [← Rat.cast_nonneg (K := ℝ), a.2.1.trans hqa.le]

Goal state after:
case mpr
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := ⋯
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
⊢ (∃ i, ↑a < ↑i ∧ ∃ (x : 0 ≤ i ∧ ↑i ≤ 1), (κ e.1).real (Icc 0 ⟨↑i, ⋯⟩) < ↑e.2) →
    ∃ a_2, ∃ (h : 0 ≤ a_2 ∧ a_2 ≤ 1), (κ e.1).real (Icc 0 ⟨a_2, ⋯⟩) < ↑e.2 ∧ a < ⟨a_2, ⋯⟩
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.discard X.carrier ∥ₖ Kernel.discard Y.carrier)

Tactic:
rw [Kernel.id_map (by fun_prop), Kernel.deterministic_comp_eq_map]

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

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / rexp (cgf X μ t) ∂μ)

Tactic:
rwa [exp_cgf]

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

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst✝ : SFinite μ
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / rexp (cgf X μ t) ∂μ)

Tactic:
rwa [exp_cgf]

Goal state after:
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
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ = ∫ (ω : Ω), (rexp (t * X ω) / rexp (cgf X μ t)) • g ω ∂μ

Tactic:
rwa [exp_cgf]

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 μ)
⊢ (∫ (x : Ω), X x ∂μ.tilted fun x ↦ t * X x) = deriv (cgf X μ) t

Tactic:
by
  simp_rw [integral_tilted_mul_eq_mgf, deriv_cgf ht, ← integral_div, smul_eq_mul]
  congr with ω
  ring

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

Goal state before:
pp: case e_f
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSingletonClass α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Fintype α
p : PMF α
f : α → E
x : α
⊢ p.toMeasure.real {x} • f x = (p x).toReal • f x

Tactic:
rw [measureReal_def]

Goal state after:
case e_f
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSingletonClass α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Fintype α
p : PMF α
f : α → E
x : α
⊢ (p.toMeasure {x}).toReal • f x = (p x).toReal • f x
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
⊢ ∀ᵐ (ω' : Ω') ∂ν, (κ ω') {ω | 0 < X ω} = 0

Tactic:
have hb (ε : ℚ) : ∀ᵐ ω' ∂ν, 0 < ε → (κ ω') {ω | ε ≤ X ω} = 0 := by
    filter_upwards [h.measure_ge_le_exp_add ε, h.isFiniteMeasure] with ω' hm _ hε
    simp only [neg_mul, NNReal.coe_zero, zero_mul, zero_div, add_zero] at hm
    suffices (κ ω').real {ω | ε ≤ X ω} = 0 by simpa [Measure.real, ENNReal.toReal_eq_zero_iff]
    have hl : Filter.Tendsto (fun t ↦ rexp (-(t * ε))) Filter.atTop (𝓝 0) := by
      apply tendsto_exp_neg_atTop_nhds_zero.comp
      exact Filter.Tendsto.atTop_mul_const (ε.cast_pos.2 hε) (fun _ a ↦ a)
    apply le_antisymm
    · exact ge_of_tendsto hl (Filter.eventually_atTop.2 ⟨0, hm⟩)
    · exact measureReal_nonneg

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
hb : ∀ (ε : ℚ), ∀ᵐ (ω' : Ω') ∂ν, 0 < ε → (κ ω') {ω | ↑ε ≤ X ω} = 0
⊢ ∀ᵐ (ω' : Ω') ∂ν, (κ ω') {ω | 0 < X ω} = 0
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h.hs
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ MeasurableSet (Set.Ioc ↑i ↑(i + 1))

pp: case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ ∀ x ∈ Set.Ioc ↑i ↑(i + 1), (↑i + 1) * 1 ≤ x + 1

Tactic:
· exact measurableSet_Ioc

Goal state after:
case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ ∀ x ∈ Set.Ioc ↑i ↑(i + 1), (↑i + 1) * 1 ≤ x + 1
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:

Tactic:
mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') q
  _ = ∫ x, exp (q * X x) * ∫ y, exp (q * Y y) ∂(η (ω', x)) ∂(κ ω') := by
    simp_rw [mgf, mul_add, exp_add] at h_int_mul ⊢
    simp_rw [integral_compProd h_int_mul, integral_const_mul]
  _ ≤ ∫ x, exp (q * X x) * exp (cY * q ^ 2 / 2) ∂(κ ω') := by
    refine integral_mono_of_nonneg ?_ (hX_int.mul_const _) ?_
    · exact ae_of_all _ fun ω ↦ mul_nonneg (by positivity)
        (integral_nonneg (fun _ ↦ by positivity))
    · filter_upwards [all_ae_of hY_mgf q] with ω hY_mgf
      gcongr
      exact hY_mgf
  _ ≤ exp (↑(c + cY) * q ^ 2 / 2) := by
    rw [integral_mul_const, NNReal.coe_add, add_mul, add_div, exp_add]
    gcongr
    exact hX_mgf q

Goal state after:
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 : ℝ
⊢ StronglyMeasurable fun ω ↦ rexp (t * X ω)

Tactic:
exact Measurable.stronglyMeasurable <| by fun_prop

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

Goal state before:
pp: case hf
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ StronglyMeasurable fun ω ↦ rexp (t * X ω)

Tactic:
exact Measurable.stronglyMeasurable <| by fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * (X ω + Y ω))) μ

Tactic:
simp_rw [mul_add, exp_add]
    convert! MemLp.integrable_mul (hX.memLp_exp_mul t 2) (hY.memLp_exp_mul t 2)
    norm_cast
    infer_instance

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
X✝ Y✝ : Rep k G
x✝² : X✝ ⟶ Y✝
x✝¹ : ↑((coindFunctor k φ).obj X✝)
x✝ : H
⊢ (Hom.hom ((Hom.hom ((coindFunctor k φ).map x✝² ≫ (coindIso φ Y✝).hom)).toLinearMap x✝¹)).toLinearMap
      (MonoidAlgebra.single x✝ 1) =
    (Hom.hom ((Hom.hom ((coindIso φ X✝).hom ≫ (coindFunctor' k φ).map x✝²)).toLinearMap x✝¹)).toLinearMap
      (MonoidAlgebra.single x✝ 1)

Tactic:
simp [coindIso, coindMap']

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
⊢ Tendsto (fun n ↦ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ) atTop (𝓝 0)

Tactic:
have hint : Integrable (X 0) μ := hℒp.integrable hp

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
⊢ Tendsto (fun n ↦ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ) atTop (𝓝 0)
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₂ g₃ : G
a : ↑A
⊢ (A.indToCoindAux g₁) a (g₂ * g₃⁻¹) = (A.indToCoindAux (g₁ * g₃)) a g₂

Tactic:
by
  rcases em ((QuotientGroup.rightRel S).r (g₂ * g₃⁻¹) g₁) with ⟨s, hs⟩ | h
  · simp [S.1.smul_def, mul_assoc, ← eq_mul_inv_iff_mul_eq.1 hs]
  · rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]
    exact mt (fun ⟨s, hs⟩ => ⟨s, by simpa [S.1.smul_def, eq_mul_inv_iff_mul_eq, mul_assoc]⟩) h

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 B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ g₂ : G
a : ↑A
⊢ (B.indToCoindAux g₁) ((Hom.hom f) a) g₂ = (Hom.hom f) ((A.indToCoindAux g₁) a g₂)

Tactic:
by
  rcases em ((QuotientGroup.rightRel S).r g₂ g₁) with ⟨s, rfl⟩ | h
  · simp [S.1.smul_def, hom_comm_apply]
  · simp [indToCoindAux_of_not_rel (h := h)]

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

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

Tactic:
by
  ext i : 1
  rw [cochainsMap_f, resolutionMap_id]
  ext v
  rfl

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

Goal state before:
pp: case refine_1
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 : ℕ
inst✝ : DecidableEq G
⊢ (i : ℕ) → (inhomogeneousChains A).X i ≅ (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X i

Tactic:
intro i
    apply (coinvariantsTensorFreeLEquiv A (Fin i → G)).toModuleIso.symm

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : ↥(cocycles₁ A)
g h : G
⊢ f (g * h) = f g + f h

Tactic:
by
  rw [(mem_cocycles₁_iff f).1 f.2, isTrivial_apply A.ρ g (f h), add_comm]

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

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Monoid G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
⊢ f (g, 1) = g • f (1, 1)

Tactic:
simpa only [mul_one, add_left_inj] using hf g 1 1

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
x : ↑((inhomogeneousCochains A).X 2)
g : G × G
⊢ (ModuleCat.Hom.hom ((cochainsMap f φ).f 2 ≫ (cochainsIso₂ B).hom)) x g =
    (ModuleCat.Hom.hom ((cochainsIso₂ A).hom ≫ cochainsMap₂ f φ)) x g

Tactic:
change φ.hom (x _) = φ.hom (x _)

Goal state after:
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
x : ↑((inhomogeneousCochains A).X 2)
g : G × G
⊢ (Hom.hom φ) (x ((fun x ↦ ⇑f ∘ x) ((piFinTwoEquiv fun x ↦ G).symm g))) =
    (Hom.hom φ) (x ((piFinTwoEquiv fun x ↦ H).symm (Prod.map (⇑f) (⇑f) g)))
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
x : ↑((inhomogeneousCochains A).X 3)
g : G × G × G
⊢ (ModuleCat.Hom.hom ((cochainsMap f φ).f 3 ≫ (cochainsIso₃ B).hom)) x g =
    (ModuleCat.Hom.hom ((cochainsIso₃ A).hom ≫ cochainsMap₃ f φ)) x g

Tactic:
change φ.hom (x _) = φ.hom (x _)

Goal state after:
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
x : ↑((inhomogeneousCochains A).X 3)
g : G × G × G
⊢ (Hom.hom φ)
      (x
        ((fun x ↦ ⇑f ∘ x)
          (((Fin.consEquiv fun a ↦ G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G))).symm g))) =
    (Hom.hom φ)
      (x
        (((Fin.consEquiv fun a ↦ H).symm.trans ((Equiv.refl H).prodCongr (piFinTwoEquiv fun x ↦ H))).symm
          (Prod.map (⇑f) (Prod.map ⇑f ⇑f) g)))
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
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
x✝ : Fin 0 → G
⊢ ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) ((ConcreteCategory.hom (chainsIso₀ X.X₁).inv) x)) x✝ =
    ((ConcreteCategory.hom ((inhomogeneousChains X.X₂).d 1 0)) ((ConcreteCategory.hom (chainsIso₁ X.X₂).inv) y)) x✝

Tactic:
conv_rhs => rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, 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 : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
x✝ : Fin 0 → G
⊢ ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) ((ConcreteCategory.hom (chainsIso₀ X.X₁).inv) x)) x✝ =
    ((ModuleCat.Hom.hom (d₁₀ X.X₂ ≫ (chainsIso₀ X.X₂).inv)) y) x✝
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
x✝¹ : ↑(ModuleCat.of R ↑M)
x✝ : G
⊢ (ModuleCat.Hom.hom (Hom.toModuleCatHom M.norm ≫ d₀₁ M)) x✝¹ x✝ = (ModuleCat.Hom.hom 0) x✝¹ x✝

Tactic:
simp [Pi.zero_apply _]

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)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
this : Fintype G
X : FDRep k G
v : ↑((forget k G).obj X).obj
h1 : (forget k G).map (ofRightFDRep X v) ≫ η₁.hom.hom.app X = (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X
h2 :
  (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X =
    η₂.hom.hom.app rightFDRep ≫ (forget k G).map (ofRightFDRep X v)
⊢ (Hom.hom (η₁.hom.hom.app X).hom) v = (Hom.hom (η₂.hom.hom.app X).hom) v

Tactic:
simpa using congr(($h1).hom (single 1 1))

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
⊢ {p | p.1 ∈ Finset.antidiagonal x ∧ p.2 ∈ ⋯.toFinset ×ˢ ⋯.toFinset}.Finite

Tactic:
by
  classical
  apply Set.Finite.subset (s := ↑((Finset.antidiagonal x).sup (fun q ↦ Finset.product {q}
    ((TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) q.1).toFinset ×ˢ
      (TendstoCofinite.finite_preimage_singleton (Finsupp.mapDomain f) q.2).toFinset))))
  · exact Finset.finite_toSet ..
  · intro; simp
    grind

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
p q : MvPowerSeries σ R
⊢ renameFun f (p * q) = renameFun f p * renameFun f q

Tactic:
by
  classical
  ext x
  simp only [coeff_renameFun, coeff_mul, sum_mul_sum, ← sum_product']
  rw [← sum_finset_product' (renameFunAux f x).toFinset _ _ (by simp),
    ← sum_finset_product' (renameFunAux' f x).toFinset _ _ (by simp),
    ← renameFunAuxImage f x, sum_image fun _ ↦ by simp; grind]

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

Goal state before:
pp: case h₂.zero
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
hy : (ModuleCat.Hom.hom (d₁₀ A)) 0 = x
⊢ x ∈ Submodule.span k (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2)

Tactic:
simp [← hy]

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

Goal state before:
pp: case mpr.h.mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n ↦ J ^ n • ⊤ := Ideal.adic_basis J
H : ∃ i, True ∧ ↑(J ^ i) ⊆ s
⊢ s ∈ 𝓝 0

Tactic:
rcases H with ⟨n, -, hn⟩

Goal state after:
case mpr.h.mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n ↦ J ^ n • ⊤ := Ideal.adic_basis J
n : ℕ
hn : ↑(J ^ n) ⊆ s
⊢ s ∈ 𝓝 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case h
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
t : Option σ
⊢ (optionElim m u + optionElim n v) t = (optionElim k x) t

Tactic:
cases t <;> simp_all [Finsupp.ext_iff]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
a : Option σ
⊢ (optionElim 0 (single i 1)) a = (single (Option.some i) 1) a

Tactic:
cases a <;> simp [single_apply]

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
φ : A ⟶ res f B
n : ℕ
a✝ : G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom (chainsMap₁ f φ ≫ d₁₀ B) ∘ₗ lsingle a✝) x✝ =
    (ModuleCat.Hom.hom (d₁₀ A ≫ Hom.toModuleCatHom φ) ∘ₗ lsingle a✝) x✝

Tactic:
simpa [← map_inv, d₁₀] using (hom_comm_apply φ _ _).symm

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

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

Tactic:
MvPowerSeries.rename_C

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
⊢ MvPowerSeries.C r = MvPowerSeries.C r
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
⊢ LinearIndepOn R id {a | IsGroupLikeElem R a}

Tactic:
rw [linearIndepOn_iff_linearIndepOn_finset]
  rintro s hs
  -- For this, we do induction on `s`.
  induction s using Finset.cons_induction with
  -- The case `s = ∅` is trivial.
  | empty => simp
  -- Let's deal with the `s ∪ {a}` case.
  | cons a s has ih =>
  simp only [Finset.cons_eq_insert, Finset.coe_insert, Set.subset_def, Set.mem_insert_iff,
    Finset.mem_coe, Set.mem_ofPred_eq, forall_eq_or_imp] at hs
  obtain ⟨ha, hs⟩ := hs
  specialize ih hs
  -- Assume that there is some `c : A → R` and `d : R` such that `∑ x ∈ s, c x • x = d • a`.
  -- We want to prove `d = 0` and `∀ x ∈ s, c x = 0`.
  rw [Finset.coe_cons]
  refine ih.id_insert' ?_
  simp only [mem_span_finset, forall_exists_index, and_imp]
  rintro d c - hc
  -- `x ⊗ y` over `x, y ∈ s` are linearly independent since `s` is linearly independent and
  -- `R` is a domain.
  replace ih := ih.tmul_of_isDomain ih
  simp_rw [← Finset.coe_product, linearIndepOn_finset_iffₛ, id] at ih
  -- Tensoring the equality `∑ x ∈ s, c x • x = d • a` with itself, we get by linear independence
  -- that `c x ^ 2 = d * c x` and `c x * c y = 0` for `x ≠ y`.
  have key := calc
        ∑ x ∈ s, ∑ y ∈ s, (if x = y then d * c x else 0) • x ⊗ₜ[R] y
    _ = d • ∑ x ∈ s, c x • x ⊗ₜ[R] x := by simp [Finset.smul_sum, mul_smul]
    _ = d • comul (d • a) := by rw [← hc]; simp +contextual [(hs _ _).comul_eq_tmul_self]
    _ = (d • a) ⊗ₜ (d • a) := by simp [ha.comul_eq_tmul_self, smul_tmul, tmul_smul, -neg_smul]
    _ = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y := by
      simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]
  simp_rw [← Finset.sum_product'] at key
  apply ih at key
  -- Therefore, `c x = 0` for all `x ∈ s`.
  replace key x (hx : x ∈ s) : c x = 0 := by
    -- Otherwise, we deduce from `key` that `c y = 0` for any `y ≠ x` with `y ∈ s`.
    by_contra! hcx
    have hcy (y) (hys : y ∈ s) (hyx : y ≠ x) : c y = 0 := by
      simpa [*] using (key (y, x) (by simp [*])).symm
    -- Then substitute this into `hc` to get `c x • x = d • a`.
    rw [Finset.sum_eq_single x (by simp +contextual [hcy]) (by simp [hx])] at hc
    -- But `key` also says that `c x = d`.
    have hcxa : d = c x := mul_left_injective₀ hcx (by simpa using (key (x, x) (by simp [*])))
    -- So `x = a`...
    obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc
    -- ... which contradicts `x ∈ s` and `a ∉ s`.
    contradiction
  -- We are now done, since `d • a = ∑ x ∈ s, c x • x = 0`
  simp_all [ha.ne_zero, eq_comm]

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
⊢ (toPrincipalIdeal A (FractionRing A)).range ≤
    Subgroup.comap (Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B))
      (toPrincipalIdeal B (FractionRing B)).range

Tactic:
rintro _ ⟨α, rfl⟩
      refine ⟨Units.mk0 (IsFractionRing.map (j := algebraMap A B)
        (FaithfulSMul.algebraMap_injective _ _) (α : FractionRing A))
        (by simp [α.ne_zero]), ?_⟩
      simpa [coe_toPrincipalIdeal, Units.coe_map, Units.val_mk0] using!
        (FractionalIdeal.extendedHom_spanSingleton (FractionRing B) B _).symm

Goal state after: