mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
⊢ sign ↑k = -1

Tactic:
sign_of_cycleType,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
⊢ (-1) ^ ((↑k).cycleType.sum + (↑k).cycleType.card) = -1
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ Fintype.card { x // x ∈ Finset.univ ∧ x.cycleType = g.cycleType } = Fintype.card { h // IsConj g h }

Tactic:
Finset.mem_univ,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ Fintype.card { x // True ∧ x.cycleType = g.cycleType } = Fintype.card { h // IsConj g h }
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i✝ : ι
p : Pair d i✝
n : ↑↑(φ i✝).range × ↑(d.set i✝) := ⋯.equiv p.head
w : Word G :=
  (Word.equivPair i✝).symm
    (let __src := p.toPair;
    { head := ↑n.2, tail := __src.tail, fstIdx_ne := ⋯ })
i : ι
g : G i
hg : ⟨i, g⟩ ∈ ((Word.equivPair i✝).symm { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }).toList
⊢ g ∈ d.set i

Tactic:
Word.equivPair_symm,

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i✝ : ι
p : Pair d i✝
n : ↑↑(φ i✝).range × ↑(d.set i✝) := ⋯.equiv p.head
w : Word G :=
  (Word.equivPair i✝).symm
    (let __src := p.toPair;
    { head := ↑n.2, tail := __src.tail, fstIdx_ne := ⋯ })
i : ι
g : G i
hg : ⟨i, g⟩ ∈ (Word.rcons { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }).toList
⊢ g ∈ d.set i
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count :
  ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
c : ↥g.cycleFactorsFinset
⊢ ↑(((toPermHom g) ⟨x, ⋯⟩) c) = ↑(1 c)

Tactic:
exact h_count _ (by simp) _ c.prop (mem_range_toPermHom_iff.mp (by simp) c)

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
⊢ Nat.card ↥(alternatingGroup α) = 12

Tactic:
by
  have : Nontrivial α := by
    rw [← Finite.one_lt_card_iff_nontrivial, hα4]
    simp
  rw [nat_card_alternatingGroup, hα4]
  decide

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hG' : IsCyclic ↥↑Q
hQ : Subgroup.comap f ↑Q = ↑P
⊢ IsCyclic ↥↑P

Tactic:
have h : Subgroup.map f P ≤ Q := hQ ▸ Subgroup.map_comap_le f ↑Q

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hG' : IsCyclic ↥↑Q
hQ : Subgroup.comap f ↑Q = ↑P
h : Subgroup.map f ↑P ≤ ↑Q
⊢ IsCyclic ↥↑P
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
h : commutator ↥(commutator ↥H) ≤ Subgroup.center ↥(commutator ↥H)
⊢ IsCyclic ↥(commutator ↥H)

Tactic:
by
      rw [← Abelianization.ker_of (commutator H)] at h
      let _ := commGroupOfCyclicCenterQuotient Abelianization.of h
      infer_instance

Goal state after:
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst✝ : MeasurableSingletonClass β
⊢ ∫⁻ (x : β), f x ∂Measure.dirac (g a) = f (g a)

Tactic:
lintegral_dirac (g a) f

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst✝ : MeasurableSingletonClass β
⊢ f (g a) = f (g a)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (copy α)

Tactic:
copy

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsMarkovKernel (deterministic Function.diag ⋯)
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝ : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
⊢ IsSFiniteKernel (Kernel.sum κs)

Tactic:
by
  cases fintypeOrInfinite ι
  · rw [sum_fintype]
    exact IsSFiniteKernel.finsetSum Finset.univ fun i _ => hκs i
  cases nonempty_denumerable ι
  exact isSFiniteKernel_sum_of_denumerable hκs

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
h : UniquelyDecodable ↑S
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
⊢ w₁ = w₂

Tactic:
funext i

Goal state after:
α : Type u_1
S : Finset (List α)
h : UniquelyDecodable ↑S
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
i : Fin r
⊢ w₁ i = w₂ i
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
a : α
⊢ ((Kernel.piecewise hs κ η) a) Set.univ = 1

Tactic:
piecewise_apply',

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
a : α
⊢ (if a ∈ s then (κ a) Set.univ else (η a) Set.univ) = 1
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable fun a ↦ c * (κ a) (Prod.mk a ⁻¹' t)

Tactic:
exact Measurable.const_mul (measurable_kernel_prodMk_left ht) c

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
⊢ κ ∘ₖ deterministic g hg = κ.comap g hg

Tactic:
ext a s hs
  simp_rw [comap_apply' _ _ _ s, comp_apply' _ _ _ hs, deterministic_apply hg a,
    lintegral_dirac' _ (Kernel.measurable_coe κ hs)]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((deterministic f mf ×ₖ κ) a) s = (κ a) (Prod.mk (f a) ⁻¹' s)

Tactic:
by
  rw [prod_apply' _ _ _ hs, lintegral_deterministic']
  exact measurable_measure_prodMk_left hs

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
⊢ ((κ ⊗ₖ deterministic f hf) x) s = (κ x) {b | (b, f (x, b)) ∈ s}

Tactic:
simp only [deterministic_apply, Measure.dirac_apply,
    Set.indicator_apply, Pi.one_apply, compProd_apply hs]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
⊢ ∫⁻ (b : β), if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0 ∂κ x = (κ x) {b | (b, f (x, b)) ∈ s}
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
⊢ ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂κ x +
      ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂κ x =
    (κ x) {b | (b, f (x, b)) ∈ s}

Tactic:
convert! add_zero _

Goal state after:
case e'_2.e'_6
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
⊢ ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂κ x = 0

case e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
x : α
t : Set β := {b | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
⊢ (κ x) {b | (b, f (x, b)) ∈ s} = ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂κ x
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
h : ∀ᵐ (ω : β) ∂⇑κ ∘ₘ μ, p ω
⊢ ∀ᵐ (ω' : α) ∂μ, ∀ᵐ (ω : β) ∂κ ω', p ω

Tactic:
rw [comp_eq_comp_const_apply] at h
  exact Kernel.ae_ae_of_ae_comp h

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.KernelLemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
η : Kernel Z T
inst✝ : IsSFiniteKernel κ
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ κ

Tactic:
by
  rw [parallelComp_id_left_comp_parallelComp]
  congr
  exact comp_id κ

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ Tendsto (fun i ↦ ∫⁻ (x : β), ‖∫ (y : γ), ↑↑i (x, y) ∂η (a, x) - ∫ (y : γ), ↑↑g (x, y) ∂η (a, x)‖ₑ ∂κ a) (𝓝 g) (𝓝 0)

Tactic:
simp_rw [← lintegral_fn_integral_sub (‖·‖ₑ) (L1.integrable_coeFn _) (L1.integrable_coeFn g)]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ Tendsto (fun i ↦ ∫⁻ (x : β), ‖∫ (y : γ), ↑↑i (x, y) - ↑↑g (x, y) ∂η (a, x)‖ₑ ∂κ a) (𝓝 g) (𝓝 0)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
η : Kernel (α × β) γ
⊢ κ ⊗ₖ η = Kernel.sum fun n ↦ κ.seq n ⊗ₖ η

Tactic:
simp_rw [compProd_def]
  rw [← comp_sum_left, ← comp_sum_right, ← parallelComp_sum_right, kernel_sum_seq]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = ∑' (n : ℕ) (m : ℕ), ((κ.seq n ⊗ₖ η.seq m) a) s

Tactic:
rw [compProd_eq_sum_compProd]
  simp_rw [sum_apply' _ _ hs]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_5
β : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ ∫ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ

Tactic:
rw [Measure.compProd, ProbabilityTheory.setIntegral_compProd hs ht hf]
  simp

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

Tactic:
rw [klDiv_eq_integral_klFun, if_pos ⟨h, h_int⟩, ENNReal.toReal_ofReal]

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ 0 ≤ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ p.toReal⁻¹ ≤ 1

Tactic:
apply inv_le_one_of_one_le₀

Goal state after:
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ 1 ≤ p.toReal
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
s : ι → Set X
s_meas : ∀ (n : ι), MeasurableSet (s n)
hs : ∀ (n : ι), f n =ᵐ[μ.restrict (s n)ᶜ] 0
h's : ∀ (n : ι), SigmaFinite (μ.restrict (s n))
n : ι
i : ℕ
⊢ (μ.restrict (s n)) (spanningSets (μ.restrict (s n)) i) ≠ ∞

Tactic:
exact (measure_spanningSets_lt_top _ _).ne

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_1
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ Integrable (↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) (μ.restrict s)

Tactic:
rw [integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub (↑(condExpL2 E' 𝕜 hm f)) f).symm)]

Goal state after:
case refine_1
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ Integrable (↑↑(↑((condExpL2 E' 𝕜 hm) f) - f)) (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst✝ : SigmaFinite (μ.trim hm₂)
hμm₁ : ¬SigmaFinite (μ.trim ⋯)
⊢ μ[μ[f | m₂] | m₁] =ᵐ[μ] μ[f | m₁]

Tactic:
condExp_of_not_sigmaFinite (hm₁₂.trans hm₂) hμm₁

Goal state after:
case neg
α : Type u_1
E : Type u_3
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst✝ : SigmaFinite (μ.trim hm₂)
hμm₁ : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 =ᵐ[μ] 0
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
i : ι
⊢ ((basis b ibc).repr (ε v)) i = ((Finsupp.mapRange.linearMap (Algebra.linearMap R S)) (b.repr v)) i

Tactic:
simp [basis_repr_comp_apply]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
V : Type u_2
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Module R V
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Algebra A R
inst✝² : Module A V
inst✝¹ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst✝ : Fintype ι
a : ι → A
v : V
⊢ (Fintype.linearCombination A ⇑b) a = v ↔ b.equivFun.symm (⇑(algebraMap A R) ∘ a) = v

Tactic:
Fintype.linearCombination_apply,

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
V : Type u_2
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Module R V
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Algebra A R
inst✝² : Module A V
inst✝¹ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst✝ : Fintype ι
a : ι → A
v : V
⊢ ∑ i, a i • b i = v ↔ b.equivFun.symm (⇑(algebraMap A R) ∘ a) = v
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case h.inl.inl
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
σ : Perm (ιa ⊕ ιb)
hσ✝ : swap i j • Quotient.mk'' σ = Quotient.mk'' σ
sl : Perm ιa
sr : Perm ιb
hσ : (Perm.sumCongrHom ιa ιb) (sl, sr) = ((fun x ↦ swap i j • x) σ)⁻¹ * σ
i' : ιa
hi : i = σ (Sum.inl i')
j' : ιa
hj : j = σ (Sum.inl j')
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0

Tactic:
subst hi hj

Goal state after:
case h.inl.inl
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' j' : ιa
hv : v (σ (Sum.inl i')) = v (σ (Sum.inl j'))
hij : σ (Sum.inl i') ≠ σ (Sum.inl j')
hσ✝ : swap (σ (Sum.inl i')) (σ (Sum.inl j')) • Quotient.mk'' σ = Quotient.mk'' σ
hσ : (Perm.sumCongrHom ιa ιb) (sl, sr) = ((fun x ↦ swap (σ (Sum.inl i')) (σ (Sum.inl j')) • x) σ)⁻¹ * σ
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case h.inl.inr
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
σ : Perm (ιa ⊕ ιb)
hσ✝ : swap i j • Quotient.mk'' σ = Quotient.mk'' σ
sl : Perm ιa
sr : Perm ιb
hσ : (Perm.sumCongrHom ιa ιb) (sl, sr) = ((fun x ↦ swap i j • x) σ)⁻¹ * σ
i' : ιa
hi : i = σ (Sum.inl i')
j' : ιb
hj : j = σ (Sum.inr j')
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0

Tactic:
subst hi hj

Goal state after:
case h.inl.inr
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' : ιa
j' : ιb
hv : v (σ (Sum.inl i')) = v (σ (Sum.inr j'))
hij : σ (Sum.inl i') ≠ σ (Sum.inr j')
hσ✝ : swap (σ (Sum.inl i')) (σ (Sum.inr j')) • Quotient.mk'' σ = Quotient.mk'' σ
hσ : (Perm.sumCongrHom ιa ιb) (sl, sr) = ((fun x ↦ swap (σ (Sum.inl i')) (σ (Sum.inr j')) • x) σ)⁻¹ * σ
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0