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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
⊢ AEStronglyMeasurable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ

Tactic:
refine StronglyMeasurable.aestronglyMeasurable ?_

Goal state after:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
⊢ StronglyMeasurable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ))
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
⊢ μ[stoppedValue f τ | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
have h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ := by
        apply condExp_of_stronglyMeasurable hτ.measurableSpace_le
        · exact Measurable.stronglyMeasurable <|
            measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ
        · exact integrable_stoppedValue ι hτ h.integrable hτ_le
      rw [h1]
      exact (condExp_stoppedValue_stopping_time_ae_eq_restrict_le h hτ hσ hτ_le).symm

Goal state after:
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 κ ν
r t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * r * X ω)) (⇑κ ∘ₘ ν)

Tactic:
exact h.integrable_exp_mul (t * r)

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
H : f x ∉ Set.Ioc (-A) A
⊢ 0 = f x

Tactic:
apply H.elim

Goal state after:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
H : f x ∉ Set.Ioc (-A) A
⊢ f x ∈ Set.Ioc (-A) A
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case succ
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : ρ.IntertwiningMap ρ
n : ℕ
ih : (f ^ n).toLinearMap = f.toLinearMap ^ n
⊢ (f ^ (n + 1)).toLinearMap = f.toLinearMap ^ (n + 1)

Tactic:
simp [ih, pow_succ]

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
z : A[G]
hz : z ∈ Submonoid.center A[G]
x✝ : G
⊢ ρ.asAlgebraHom z * ρ.asAlgebraHom ((MonoidAlgebra.of A G) x✝) =
    ρ.asAlgebraHom ((MonoidAlgebra.of A G) x✝) * ρ.asAlgebraHom z

Tactic:
← map_mul,

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
z : A[G]
hz : z ∈ Submonoid.center A[G]
x✝ : G
⊢ ρ.asAlgebraHom (z * (MonoidAlgebra.of A G) x✝) = ρ.asAlgebraHom ((MonoidAlgebra.of A G) x✝ * z)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N : ℕ
⊢ ∑ x ∈ range N, ε⁻¹ ^ 2 * ((↑(u x))⁻¹ ^ 2 * Var[S (u x); ℙ]) ≤ ε⁻¹ ^ 2 * C

Tactic:
← mul_sum

Goal state after:
Ω : 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)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N : ℕ
⊢ ε⁻¹ ^ 2 * ∑ i ∈ range N, (↑(u i))⁻¹ ^ 2 * Var[S (u i); ℙ] ≤ ε⁻¹ ^ 2 * 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:
← 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:
← 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.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.RepresentationTheory.Semisimple

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Field k
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module k[G] M
⊢ ComplementedLattice (Submodule k[G] M) ↔ (ofModule M).IsSemisimpleRepresentation

Tactic:
exact OrderIso.complementedLattice_iff Subrepresentation.submoduleSubrepresentationOrderIso

Goal state after:
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
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ (equivariantProjection G π) (i v) = v

Tactic:
rw [equivariantProjection_apply]
  simp only [conjugate_i π i h]
  rw [Finset.sum_const, Finset.card_univ, ← Nat.cast_smul_eq_nsmul k, smul_smul,
    Fintype.card_eq_nat_card, Ring.inverse_mul_cancel _ hcard, one_smul]

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
b : Quotient (QuotientGroup.rightRel S)
a✝ : b ∈ Finset.univ
⊢ b ≠ ⟦g⟧ → b.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0

Tactic:
hb

Goal state after:
case h₀
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
b : Quotient (QuotientGroup.rightRel S)
a✝ : b ∈ Finset.univ
hb : b ≠ ⟦g⟧
⊢ b.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀
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 : ↑(coind.{u, v, v, w} S.subtype A)
a : G
b : Quotient (QuotientGroup.rightRel S)
a✝ : b ∈ Finset.univ
⊢ b ≠ ⟦a⟧ → ↑(A.indToCoind (b.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0

Tactic:
hb

Goal state after:
case h₀
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 : ↑(coind.{u, v, v, w} S.subtype A)
a : G
b : Quotient (QuotientGroup.rightRel S)
a✝ : b ∈ Finset.univ
hb : b ≠ ⟦a⟧
⊢ ↑(A.indToCoind (b.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case refine_1
k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_4
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
g : G
inst✝ : Finite G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
α : V
i : ℕ
⊢ (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) i, α) ∈ ↑(ρ g - LinearMap.id).range

Tactic:
induction i with | zero => exact ⟨0, by simp⟩ | succ n _ =>
    use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))
    simpa using ρ.apply_sub_id_partialSum_eq _ _ _

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
x : ↑(ModuleCat.of k ↑A)
⊢ x ∈ (ModuleCat.Hom.hom (d₀₁ A)).ker ↔ x ∈ A.ρ.invariants

Tactic:
simp only [LinearMap.mem_ker, mem_invariants, ← @sub_eq_zero _ _ _ x, funext_iff]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑(ModuleCat.of k ↑A)
⊢ (∀ (x_1 : G), (ModuleCat.Hom.hom (d₀₁ A)) x x_1 = 0 x_1) ↔ ∀ (g : G), (A.ρ g) x - x = 0
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 : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ Mono (H1InfRes A S).f

Tactic:
rw [ModuleCat.mono_iff_injective, injective_iff_map_eq_zero]

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
n : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ ∀ (a : ↑(H1InfRes A S).X₁), (ConcreteCategory.hom (H1InfRes A S).f) a = 0 → a = 0
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fintype G
X : FDRep k G
v : ↑X.V
x✝¹ x✝ : G → k
⊢ ∑ s, (x✝¹ + x✝) s • (X.ρ s⁻¹) v = ∑ s, x✝¹ s • (X.ρ s⁻¹) v + ∑ s, x✝ s • (X.ρ s⁻¹) v

Tactic:
by simp [add_smul, sum_add_distrib]

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

Goal state before:
pp: A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
d : MvPolynomial σ A
⊢ (Ideal.Quotient.mkₐ A I) d = eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) (fun d ↦ (Ideal.Quotient.mkₐ A I) (X d)) d

Tactic:
mkₐ_eq_aeval,

Goal state after:
A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
d : MvPolynomial σ A
⊢ (aeval fun d ↦ (Ideal.Quotient.mk I) (X d)) d =
    eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) (fun d ↦ (aeval fun d ↦ (Ideal.Quotient.mk I) (X d)) (X d)) d
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ (MvPolynomial.monomial (m.degree p)) 1 =
    MvPolynomial.C ↑⋯.unit⁻¹ * MvPolynomial.C (m.leadingCoeff p) * (MvPolynomial.monomial (m.degree p)) 1

Tactic:
← map_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ (MvPolynomial.monomial (m.degree p)) 1 =
    MvPolynomial.C (↑⋯.unit⁻¹ * m.leadingCoeff p) * (MvPolynomial.monomial (m.degree p)) 1
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (t : Set R), t ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ t

Tactic:
by
    intro U
    rw [I.ringFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
    constructor
    · rintro ⟨-, ⟨i, rfl⟩, h⟩
      replace h : ↑(I ^ i) ⊆ U := by simpa using h
      exact ⟨i, trivial, h⟩
    · rintro ⟨i, -, h⟩
      exact ⟨(I ^ i : Ideal R), ⟨i, by simp⟩, h⟩

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

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p q : MvPowerSeries σ R
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) (p * q)) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) p) *
      (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) q)

Tactic:
← map_mul,

Goal state after:
σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p q : MvPowerSeries σ R
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) (p * q)) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) p * (truncTotal n) q)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ Quotient.out (↑((toAdicCompletion σ R) p) n) - (truncTotal n) p ∈ MvPolynomial.idealOfVars σ R ^ n

Tactic:
rw [toAdicCompletion_apply_eq_mk_truncTotal, smul_eq_mul]
    nth_rw 1 [← Ideal.mul_top (MvPolynomial.idealOfVars σ R ^ n), ← Ideal.Quotient.eq,
      Ideal.Quotient.mk_out]

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

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ (degree x + 1) • ⊤)) (Quotient.out (↑f (degree x + 1))) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ (degree x + 1) • ⊤)) (Quotient.out (↑f n))

Tactic:
simp only [Submodule.mapQ_eq_factor, Submodule.factor_eq_factor, Ideal.Quotient.mk_out]

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ ↑f (degree x + 1) = (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ (degree x + 1) • ⊤)) (Quotient.out (↑f n))
Module: Mathlib.RingTheory.Flat.Domain

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁴ : AddCommGroup P
inst✝³ : Module R P
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst✝ : Module.Flat R Q
hf : Injective ⇑f
hg : Injective ⇑g
K : Type u_1 := FractionRing R
H₁ : Injective ⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g))
H₂ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm
⊢ Injective (⇑((mk R K (M ⊗[R] N)) 1) ∘ ⇑(map f g))

Tactic:
have H₃ := (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N).injective

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁴ : AddCommGroup P
inst✝³ : Module R P
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst✝ : Module.Flat R Q
hf : Injective ⇑f
hg : Injective ⇑g
K : Type u_1 := FractionRing R
H₁ : Injective ⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g))
H₂ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm
H₃ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N)
⊢ Injective (⇑((mk R K (M ⊗[R] N)) 1) ∘ ⇑(map f g))
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
I : Submodule R C
⊢ ((∀ ⦃x : C⦄, x ∈ I → counit x = 0) ∧ ∀ ⦃x : C⦄, x ∈ I → (TensorProduct.map I.mkQ I.mkQ) (comul x) = 0) ↔
    (∀ ⦃x : C⦄, x ∈ I → counit x = 0) ∧ ∀ x ∈ I, comul x ∈ (lTensor C I.subtype).range ⊔ (rTensor C I.subtype).range

Tactic:
← LinearMap.mem_ker,

Goal state after:
R : Type u_1
C : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
I : Submodule R C
⊢ ((∀ ⦃x : C⦄, x ∈ I → x ∈ counit.ker) ∧ ∀ ⦃x : C⦄, x ∈ I → comul x ∈ (TensorProduct.map I.mkQ I.mkQ).ker) ↔
    (∀ ⦃x : C⦄, x ∈ I → x ∈ counit.ker) ∧ ∀ x ∈ I, comul x ∈ (lTensor C I.subtype).range ⊔ (rTensor C I.subtype).range
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))
⊢ ∃ a, (ConcreteCategory.hom (H1CoresCoinf A S).g) a = (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S))) x

Tactic:
rcases (ModuleCat.epi_iff_surjective _).1
    (mapCycles₁_quotientGroupMk'_epi (A.toCoinvariants S) S) x with ⟨y, hy⟩
/- We know `C₁(G, A) ⟶ C₁(G, A_S)` is surjective, so pick `Y` in the preimage of `y`. -/
  rcases mapRange_surjective _ (map_zero _)
    (Coinvariants.mk_surjective (A.ρ.comp S.subtype)) y.1 with ⟨Y, hY⟩
/- Then `d(Y) ∈ I(S)A,` since `d(y) = 0`. -/
  have : d₁₀ _ Y ∈ Coinvariants.ker (A.ρ.comp S.subtype) := by
    have h' := congr($((mapShortComplexH1 (B := toCoinvariants A S)
      (MonoidHom.id G) (toCoinvariantsMkQ A S)).comm₂₃) Y)
    simp_all [shortComplexH1, ← Coinvariants.mk_eq_zero]
  /- Thus we can pick a representation of `d(Y)` as a sum `∑ ρ(sᵢ⁻¹)(aᵢ) - aᵢ`, `sᵢ ∈ S, aᵢ ∈ A`,
and `Y - ∑ aᵢ·sᵢ` is a cycle. -/
  rcases chains₁ToCoinvariantsKer_surjective
    (res S.subtype A) ⟨d₁₀ A Y, this⟩ with ⟨(Z : S →₀ A), hZ⟩
  have H : d₁₀ A (Y - mapDomain S.subtype Z) = 0 := by
    simpa [map_sub, sub_eq_zero, chains₁ToCoinvariantsKer, -LinearMap.sub_apply, d₁₀,
      sum_mapDomain_index_inj] using! Subtype.ext_iff.1 hZ.symm
  use H1π A ⟨Y - mapDomain S.subtype Z, H⟩
  simp only [H1CoresCoinf_X₃, H1CoresCoinf_X₂, H1CoresCoinf_g,
    Subgroup.coe_subtype, H1π_comp_map_apply]
/- Moreover, the image of `Y - ∑ aᵢ·sᵢ` in `Z₁(G ⧸ S, A_S)` is `x - ∑ aᵢ·1`, and hence differs from
`x` by a boundary, since `aᵢ·1 = d(aᵢ·(1, 1))`. -/
  refine (H1π_eq_iff _ _).2 ?_
  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.Polynomial.ContentIdeal

Goal state before:
pp: case mp
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ p.contentIdeal ≤ span {r} → C r ∣ p

Tactic:
rw [← p.contentIdeal.span_singleton_generator]

Goal state after:
case mp
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ span {Submodule.IsPrincipal.generator p.contentIdeal} ≤ span {r} → C r ∣ p