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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((η ×ₖ Kernel.id ∘ₖ κ) a) (s ×ˢ t) = ((η ∘ₖ κ) a) s * (κ a) t

Tactic:
comp_apply' _ _ _ (hs.prod ht)

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ((η ×ₖ Kernel.id) b) (s ×ˢ t) ∂κ a = ((η ∘ₖ κ) a) s * (κ a) t
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: n : ℕ
p : ↑I
⊢ Bin(n, p) = ∑ k ≤ n, ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • dirac k

Tactic:
by
  refine ext_of_singleton fun k ↦ ?_
  rw [binomial_singleton, finsetSum_apply, Finset.sum_eq_single k]
  · simp
  · simp_all
  · simp_all [Nat.choose_eq_zero_of_lt]

Goal state after:
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ ∫ (t : ℝ) in Ioc 0 x, r * rexp (-(r * t)) ∂volume = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

Tactic:
← uIoc_of_le h,

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ ∫ (t : ℝ) in uIoc 0 x, r * rexp (-(r * t)) ∂volume = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
⊢ Function.Injective toMeasure

Tactic:
by
  intro p q h
  ext x
  rw [← p.toMeasure_apply_singleton x <| measurableSet_singleton x,
    ← q.toMeasure_apply_singleton x <| measurableSet_singleton x, h]

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

Goal state before:
pp: case pos
α : Type u_1
a : α
s : Set α
ha : a ∈ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 1

pp: case neg
α : Type u_1
a : α
s : Set α
ha : a ∉ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 0

Tactic:
· refine (tsum_congr fun b => ?_).trans (tsum_ite_eq a 1)
    exact ite_eq_left_iff.2 fun hb =>
      symm (ite_eq_right_iff.2 fun h => (hb <| h.symm ▸ ha).elim)

Goal state after:
case neg
α : Type u_1
a : α
s : Set α
ha : a ∉ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 0
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ μ[AEStronglyMeasurable.mk f ⋯ | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

Tactic:
refine (condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable hm
    hf_int.1.stronglyMeasurable_mk ?_).trans ?_

Goal state after:
case refine_1
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ Integrable (AEStronglyMeasurable.mk f ⋯) μ

case refine_2
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ (fun ω ↦ ∫ (y : Ω), AEStronglyMeasurable.mk f ⋯ y ∂(condExpKernel μ m) ω) =ᵐ[μ.trim hm] fun ω ↦
    ∫ (y : Ω), f y ∂(condExpKernel μ m) ω
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{?u.182 + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ { carrier := X.carrier × { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier,
      str := Prod.instMeasurableSpace } ≅
    X

Tactic:
refine ⟨⟨Kernel.id.map Prod.fst, by infer_instance⟩,
      ⟨Kernel.id.map f₁, by infer_instance⟩, ?_, ?_⟩

Goal state after:
case refine_1
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ { hom := Kernel.id.map Prod.fst, property := ⋯ } ≫ { hom := Kernel.id.map f₁, property := ⋯ } =
    𝟙
      { carrier := X.carrier × { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier,
        str := Prod.instMeasurableSpace }

case refine_2
X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{u + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
hf₂ : Measurable Prod.fst
⊢ { hom := Kernel.id.map f₁, property := ⋯ } ≫ { hom := Kernel.id.map Prod.fst, property := ⋯ } = 𝟙 X
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Z : Ω → G
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P
f : Unit → G →ᵇ ℝ
⊢ ∫ (ω : Ω) in A, ∏ s, (f s) (Z ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (Z ω) ∂P

Tactic:
convert! h (f ()) <;> simp

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

Goal state before:
pp: case neg.right
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (⇑κ ∘ₘ ν) < ∞

Tactic:
· rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp0) (by simp)]
    simp only [ENNReal.coe_toReal]
    have h' := (h.integrable_exp_mul (p * t)).2
    rw [hasFiniteIntegral_def] at h'
    convert! h' using 3 with ω
    rw [enorm_eq_ofReal (by positivity), enorm_eq_ofReal (by positivity),
      ENNReal.ofReal_rpow_of_nonneg (by positivity), ← exp_mul, mul_comm, ← mul_assoc]
    positivity

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
x : α
h1 : x ∈ Function.support fun a ↦ (p a).toReal
h2 : p x = 0
⊢ (fun a ↦ (p a).toReal) x = 0

Tactic:
by simp [h2]

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 : Ω → ℝ
hX : Measurable X
h : HasSubgaussianMGF X 0 κ ν
⊢ ∀ᵐ (y : Ω') ∂ν, ∀ᵐ (z : Ω) ∂κ y, X z = 0 z

Tactic:
exact h.ae_eq_zero_of_hasSubgaussianMGF_zero

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

Goal state before:
pp: case pos.inr.refine_1
Ω : 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
⊢ MemLp (fun ω ↦ rexp (t * X ω.1)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
have h := hX.memLp_exp_mul t 2

Goal state after:
case pos.inr.refine_1
Ω : 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
h : MemLp (fun ω ↦ rexp (t * X ω)) (↑2) (⇑κ ∘ₘ ν)
⊢ MemLp (fun ω ↦ rexp (t * X ω.1)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
k : ℕ
x✝ : k < N
⊢ IntervalIntegrable (fun x ↦ x + 1) ρ ↑k ↑(k + 1)

Tactic:
· exact (continuous_id.add continuous_const).intervalIntegrable _ _

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Tactic:
apply Set.Subset.antisymm _ _

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ {ω | X ω ∈ Set.Ioi ↑i} ⊆ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N} ⊆ {ω | X ω ∈ Set.Ioi ↑i}
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 only [pow_succ, coe_mul, show f ^ (n + 1) = f ^ n * f from rfl, ih]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : ModuleCat k[G]
f : X✝ ⟶ Y✝
g : G
⊢ { toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ } ∘ₗ (Representation.ofModule ↑X✝) g =
    (Representation.ofModule ↑Y✝) g ∘ₗ { toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ }

Tactic:
by ext; apply f.hom.map_smul

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
Ω : 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))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
have B : ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range n, (neg ∘ X i) ω) / n) atTop (𝓝 𝔼[neg ∘ X 0]) :=
    strong_law_aux7 _ hint.neg_part (fun i j hij => (hindep hij).comp negm negm)
      (fun i => (hident i).comp negm) fun i ω => le_max_right _ _

Goal state after:
case neg
Ω : 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))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
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✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := ⋯
s✝ : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s✝ b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : G → ↥S := ⋯
hmk : ∀ (s : ↥S) (g : G), Quotient.mk' (↑s * g) = Quotient.mk' g
s : ↥S
g : G
⊢ ↑(γ (↑s * g)) = ↑(s * γ g)

Tactic:
simp [mul_assoc, γ, hmk]

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Rep k G
Y : ModuleCat k
f : X ⟶ (trivialFunctor k G).obj Y
x✝ : ↑((forget₂ (Rep k G) (ModuleCat k)).obj X)
⊢ (ModuleCat.Hom.hom ((coinvariantsMk k G).app X ≫ ((coinvariantsAdjunction k G).homEquiv X Y).symm f)) x✝ =
    (ModuleCat.Hom.hom ((coinvariantsMk k G).app X ≫ desc f)) x✝

Tactic:
simp [coinvariantsAdjunction, Adjunction.homEquiv_symm_apply]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
⊢ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) p μ = 0

Tactic:
apply eLpNorm_eq_zero_of_ae_zero

Goal state after:
Ω : 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
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
⊢ (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) =ᵐ[μ] 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
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₁ g
⊢ (A.indToCoindAux g) a (↑s * g₁) = (A.ρ s) ((A.indToCoindAux g) a g₁)

Tactic:
rw [indToCoindAux_of_not_rel _ _ _ h, indToCoindAux_of_not_rel, map_zero]

Goal state after:
case inr.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
g g₁ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₁ g
⊢ ¬(QuotientGroup.rightRel S) (↑s * g₁) g
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : CommRing k
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommGroup A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommGroup B
inst✝ : Module k B
τ : Representation k G B
x✝³ x✝² x✝¹ : H
x✝ : A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * (x✝³ * x✝²)⁻¹),
                  isIntertwining' := ⋯ } ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝³⁻¹),
                    isIntertwining' := ⋯ } *
                Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝²⁻¹),
                    isIntertwining' := ⋯ }) ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝

Tactic:
simp [IndV, mul_assoc]

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
⊢ iCocycles A 0 = ((cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f) ≫ (cochainsIso₀ A).inv

Tactic:
Iso.eq_comp_inv,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ iCocycles A 0 ≫ (cochainsIso₀ A).hom = (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
⊢ span (m.leadingTerm '' B) ≤ span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B)

Tactic:
rw [Ideal.span_le, Set.image_subset_iff]

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
⊢ B ⊆ m.leadingTerm ⁻¹' ↑(span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B))
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
⊢ span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B) ≤ span (m.leadingTerm '' B)

Tactic:
rw [Ideal.span_le, Set.image_subset_iff]

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
⊢ B ⊆ (fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) ⁻¹' ↑(span (m.leadingTerm '' B))
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
k : Fin w✝¹
⊢ f k ∈ span {a} ⊔ I

Tactic:
sup_comm,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
k : Fin w✝¹
⊢ f k ∈ I ⊔ span {a}
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
⊢ CompleteSpace R

Tactic:
refine UniformSpace.complete_of_cauchySeq_tendsto fun u hu ↦ ?_

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
⊢ ∃ a, Filter.Tendsto u Filter.atTop (𝓝 a)
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
n : ℕ
hn : ↑(J ^ n) ⊆ s
⊢ s ∈ 𝓝 0

Tactic:
mem_nhds_iff

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
⊢ ∃ t ⊆ s, IsOpen[top] t ∧ 0 ∈ t
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 : ℕ
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) 0) = 0

Tactic:
by rw [map_zero, map_zero]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
f : A ⟶ B
⊢ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom = (H0Iso A).hom ≫ (coinvariantsFunctor k G).map f

Tactic:
rw [← cancel_epi (H0π A)]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
f : A ⟶ B
⊢ H0π A ≫ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom = H0π A ≫ (H0Iso A).hom ≫ (coinvariantsFunctor k G).map f
Module: Mathlib.RingTheory.AdicCompletion.Noetherian

Goal state before:
pp: case neg
R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
hf : f n ≡ f m [SMOD maximalIdeal A ^ n • ⊤]
h : ¬m ≤ n
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]

Tactic:
hn,

Goal state after:
case neg
R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
n : ℕ
hn : maximalIdeal A ^ n = 0
m : ℕ
hf : f n ≡ f m [SMOD 0 • ⊤]
h : ¬m ≤ n
⊢ f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
Module: Mathlib.RingTheory.AdicCompletion.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsNoetherianRing R
inst✝³ : Module.Finite R M
A : Type u_3
inst✝² : CommRing A
inst✝¹ : IsArtinianRing A
inst✝ : IsLocalRing A
f : ℕ → A
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD maximalIdeal A ^ m • ⊤]
⊢ ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD maximalIdeal A ^ n • ⊤]

Tactic:
by
    obtain ⟨n, hn⟩ := (isArtinianRing_iff_isNilpotent_maximalIdeal A).mp ‹_›
    use f n; intro m
    by_cases h : m ≤ n
    · exact hf h
    specialize hf (show n ≤ m by lia)
    rw [hn, zero_smul, Ideal.zero_eq_bot, SModEq.bot] at hf
    rw [hf]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
⊢ gaussNorm (v.intAdicAbv hb) 1 p ≤ 1

Tactic:
by
  by_cases hp0 : p = 0
  · simp [hp0]
  simp [gaussNorm, hp0, intAdicAbv_le_one]

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

Goal state before:
pp: R : Type u_1
A : Type u_3
M : Type u_8
N : Type u_9
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Bialgebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
x : A[M]
⊢ counit ((domCongr R A e) x) = counit x

Tactic:
by
  induction x using MonoidAlgebra.induction_linear <;> simp [*]

Goal state after: