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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
⊢ Nontrivial (Subgroup ↥(alternatingGroup α))

Tactic:
Subgroup.nontrivial_iff,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
⊢ Nontrivial ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
⊢ ∀ (a : QuaternionGroup n), 1 * a = a

Tactic:
by
    rintro (i | i)
    · exact congr_arg a (zero_add i)
    · exact congr_arg xa (sub_zero i)

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

Goal state before:
pp: n : ℕ
⊢ ∀ (x y : QuaternionGroup 0),
    (match x * y with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) =
      (match x with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j) *
        match y with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j

Tactic:
by rintro (k | k) (l | l) <;> simp

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

Goal state before:
pp: case inr.a
n : ℕ
hn : NeZero n
⊢ lcm (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
apply lcm_dvd

Goal state after:
case inr.a.hab
n : ℕ
hn : NeZero n
⊢ 2 * n ∣ Monoid.exponent (QuaternionGroup n)

case hcb
n : ℕ
hn : NeZero n
⊢ 4 ∣ Monoid.exponent (QuaternionGroup n)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
⊢ ⨆ s, Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s) = ⊤

Tactic:
by
    rw [eq_top_iff, ← closure_cycleType_eq_two_two_eq_top h5, Subgroup.closure_le]
    intro g hg
    simp only [Set.mem_ofPred_eq] at hg
    apply Subgroup.mem_iSup_of_mem ⟨(g : Perm α).support, by simp [← sum_cycleType, hg]⟩
    rw [mem_map_kleinFour_ofSubtype] <;> simp [hg, ← sum_cycleType]

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
⊢ N = ⊤

Tactic:
have : IsPreprimitive (alternatingGroup α) (Set.powersetCard α 4) := by
    apply Set.powersetCard.isPreprimitive_alternatingGroup (by norm_num) <;> grind

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
this : IsPreprimitive ↥(alternatingGroup α) ↑(Set.powersetCard α 4)
⊢ N = ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hα' : ¬Nat.card α = 6
⊢ N = ⊥ ∨ N = ⊤

Tactic:
apply normal_subgroup_eq_bot_or_eq_top_of_card_ne_six hα hα'

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
⊢ (base φ).range ≤ (of i).range

Tactic:
rw [← of_comp_eq_base i]

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
⊢ ((of i).comp (φ i)).range ≤ (of i).range
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (n : ι), (0 a) s = (0 a) s

Tactic:
simp only [zero_apply, Measure.coe_zero, Pi.zero_apply, tsum_zero]

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
H : x = y
⊢ hammingDist x y = 0

Tactic:
rw [H]
    exact hammingDist_self _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((κ a).bind ⇑η) s = ∫⁻ (b : β), (η b) s ∂κ a

Tactic:
Measure.bind_apply hs (Kernel.aemeasurable _)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : β), (η a) s ∂κ a = ∫⁻ (b : β), (η b) s ∂κ a
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
⊢ ((η ∘ₖ κ) a) Set.univ ≤ (κ a) Set.univ * η.bound

Tactic:
rw [comp_apply' _ _ _ .univ]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
⊢ ∫⁻ (b : β), (η b) Set.univ ∂κ a ≤ (κ a) Set.univ * η.bound
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' f i)
a : α
⊢ ∀ (i : ℕ), MeasurableSet (Prod.mk a ⁻¹' f i)

Tactic:
exact fun i ↦ measurable_prodMk_left (hf_meas i)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
f : β → γ
⊢ IsZeroOrMarkovKernel (κ.map f)

Tactic:
by_cases hf : Measurable f
  · rcases eq_zero_or_isMarkovKernel κ with rfl | h
    · simp only [map_zero]; infer_instance
    · have := IsMarkovKernel.map κ hf; infer_instance
  · simp only [map_of_not_measurable _ hf]; infer_instance

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (κ + η)) () =
    (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () + (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η) ()

Tactic:
Kernel.prodMkLeft_add,

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ (Kernel.const Unit μ ⊗ₖ (Kernel.prodMkLeft Unit κ + Kernel.prodMkLeft Unit η)) () =
    (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () + (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η) ()
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel κ.swapLeft

Tactic:
Kernel.swapLeft

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap Prod.swap ⋯)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel κ.swapLeft

Tactic:
Kernel.swapLeft

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap Prod.swap ⋯)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel κ.swapLeft

Tactic:
Kernel.swapLeft

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap Prod.swap ⋯)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ ⊗ₘ κ ⟂ₘ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η
⊢ μ ⊗ₘ η ≪ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η

pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
⊢ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ≪ μ ⊗ₘ η

Tactic:
· exact (absolutelyContinuous_withDensity_rnDeriv hμν).compProd_left _

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η
⊢ μ.withDensity (ν.rnDeriv μ) ⊗ₘ η ≪ μ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) (f ⁻¹' s) ∂μ = (⇑(κ.map f) ∘ₘ μ) s

Tactic:
Measure.bind_apply hs (Kernel.aemeasurable _)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) (f ⁻¹' s) ∂μ = ∫⁻ (a : α), ((κ.map f) a) s ∂μ
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
π : Measure Bool
s : Set α
hs : MeasurableSet s
⊢ (⇑(Kernel.boolKernel μ ν) ∘ₘ π) s = (π {true} • ν + π {false} • μ) s

Tactic:
Measure.bind_apply hs (Kernel.aemeasurable _)

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
π : Measure Bool
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : Bool), ((Kernel.boolKernel μ ν) a) s ∂π = (π {true} • ν + π {false} • μ) s
Module: Mathlib.Probability.Kernel.Composition.RadonNikodym

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α β
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
x✝ : (ν ⊗ₘ κ) s < ∞
h_key :
  ∀ (t₁ : Set α) (t₂ : Set β),
    MeasurableSet t₁ →
      MeasurableSet t₂ →
        ∫⁻ (x : α × β) in t₁ ×ˢ t₂, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
          ∫⁻ (x : α × β) in t₁ ×ˢ t₂, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ
⊢ ∀ (f : ℕ → Set (α × β)),
    Pairwise (Function.onFun Disjoint f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ),
            ∫⁻ (x : α × β) in f i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
              ∫⁻ (x : α × β) in f i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ) →
          ∫⁻ (x : α × β) in ⋃ i, f i, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ κ) x ∂ν ⊗ₘ κ =
            ∫⁻ (x : α × β) in ⋃ i, f i, μ.rnDeriv ν x.1 ∂ν ⊗ₘ κ

Tactic:
intro f' hf_disj hf_meas hf_eq
    rw [lintegral_iUnion hf_meas hf_disj, lintegral_iUnion hf_meas hf_disj]
    congr with i
    exact hf_eq i

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
h2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η] 0
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η]
    (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)

Tactic:
filter_upwards [h, h2] with x hx hx2

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
h2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η] 0
x : α × β
hx :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x =
    ((μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) x
hx2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x = 0 x
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x =
    (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∀ (i : ι), AEMeasurable (fun b ↦ ((η i) (a, b)) (Prod.mk b ⁻¹' s)) (κ a)

Tactic:
exact fun _ ↦ (measurable_kernel_prodMk_left' hs a).aemeasurable

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ Integrable (fun x ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ ↔
    Integrable (fun x ↦ (∫ (a : α), rexp (f a) ∂μ)⁻¹ • rexp (f x) • g x) μ

Tactic:
congr! 2 with a
    rw [smul_smul, div_eq_inv_mul]

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

Goal state before:
pp: α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
⊢ f =ᵐ[μ] g

Tactic:
← ae_eq_trim_iff_of_aestronglyMeasurable hm hfm hgm

Goal state after:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable.mk f hfm =ᵐ[μ.trim hm] AEStronglyMeasurable.mk g hgm
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : StronglyMeasurable f
⊢ (if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯) =ᵐ[μ] ↑↑(condExpL1 hm μ f)

Tactic:
rw [if_pos hfm]

Goal state after:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : StronglyMeasurable f
⊢ f =ᵐ[μ] ↑↑(condExpL1 hm μ f)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : StronglyMeasurable f
⊢ f =ᵐ[μ] ↑↑(condExpL1 hm μ f)

Tactic:
exact (condExpL1_of_aestronglyMeasurable' hfm.aestronglyMeasurable hfi).symm

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

Goal state before:
pp: α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
⊢ AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

Tactic:
by_cases hF' : CompleteSpace (Lp F' 1 μ); swap
  · simp only [condExpL1, setToFun, hF', ↓reduceDIte, ZeroMemClass.coe_zero]
    apply stronglyMeasurable_zero.aestronglyMeasurable.congr
    exact (coeFn_zero _ 1 _).symm
  by_cases hf : Integrable f μ; swap
  · rw [condExpL1_undef hf]
    exact stronglyMeasurable_zero.aestronglyMeasurable.congr (coeFn_zero ..).symm
  by_cases hf' : f =ᵐ[μ] 0
  · apply stronglyMeasurable_zero.aestronglyMeasurable.congr
    simp only [condExpL1_congr_ae hm hf', condExpL1_zero, ZeroMemClass.coe_zero]
    exact (coeFn_zero _ 1 _).symm
  have : CompleteSpace F' := by
    have : Nontrivial (Lp F' 1 μ) := by
      apply nontrivial_of_ne (hf.toL1 f) 0
      grw [ne_eq, Lp.ext_iff, Integrable.coeFn_toL1, coeFn_zero]
      exact hf'
    exact completeSpace_of_completeSpace_Lp F' 1 μ
  rw [condExpL1_eq hf]
  exact aestronglyMeasurable_condExpL1CLM _

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

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst✝ : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (Measure.map id ν)
h :
  (fun a ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) a).toReal) =ᵐ[Measure.map id ν]
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | m]
⊢ (fun x ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) x).toReal) =ᵐ[Measure.map id ν]
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]

Tactic:
convert! h <;> rw [MeasurableSpace.comap_id]

Goal state after:
Module: Mathlib.Lean.Thunk

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
a : Thunk α
⊢ (b : Thunk α) → Decidable (a = b)

Tactic:
b

Goal state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : Thunk α
⊢ Decidable (a = b)
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ associated (Q₁.tmul Q₂) = BilinForm.tmul (associated Q₁) (associated Q₂)

Tactic:
rw [BilinForm.tmul, BilinForm.tensorDistrib, LinearMap.comp_apply, ← BilinMap.tmul,
    ← QuadraticMap.associated_tmul Q₁ Q₂, LinearEquiv.coe_coe, LinearEquiv.congrRight₂_apply]

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ associated (Q₁.tmul Q₂) = LinearMap.compr₂ (associated (QuadraticMap.tmul Q₁ Q₂)) ↑(AlgebraTensorModule.rid R A A)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : CliffordAlgebra 0
⊢ x * y = y * x

Tactic:
induction x using CliffordAlgebra.induction with
    | algebraMap r => apply Algebra.commutes
    | ι x => simp
    | add x₁ x₂ hx₁ hx₂ => rw [mul_add, add_mul, hx₁, hx₂]
    | mul x₁ x₂ hx₁ hx₂ => rw [mul_assoc, hx₂, ← mul_assoc, hx₁, ← mul_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ -(e0 Q * (v Q) m) = (v Q) m * e0 Q

Tactic:
refine neg_eq_of_add_eq_zero_right ((ι_mul_ι_add_swap _ _).trans ?_)
  simp [QuadraticMap.polar]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: case mk.algebraMap
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
r : R
⊢ (((foldr Q (fFold f) ⋯) (((foldr Q (fFold f) ⋯) (1, 0)) val✝)) ((algebraMap R (CliffordAlgebra Q)) r)).1 =
    (aux f) ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩ * (aux f) ⟨val✝, property✝⟩

Tactic:
generalize_proofs at ⊢

Goal state after:
case mk.algebraMap
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
x val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
r : R
pf✝⁴ : SMulCommClass R R A
pf✝³ : SMulCommClass R R A
pf✝² : SMulCommClass R R (A × ↥(S f))
pf✝¹ : ∀ (m : M) (x : A × ↥(S f)), ((fFold f) m) (((fFold f) m) x) = Q m • x
pf✝ : (algebraMap R (CliffordAlgebra Q)) r ∈ even Q
⊢ (((foldr Q (fFold f) pf✝¹) (((foldr Q (fFold f) pf✝¹) (1, 0)) val✝)) ((algebraMap R (CliffordAlgebra Q)) r)).1 =
    (aux f) ⟨(algebraMap R (CliffordAlgebra Q)) r, pf✝⟩ * (aux f) ⟨val✝, property✝⟩
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
x : 𝒜 ᵍ⊗[R] ℬ
⊢ 1 * x = x

Tactic:
by
    rw [mul_def, mulHom_apply, auxEquiv_one, one_gradedMul, LinearEquiv.symm_apply_apply]

Goal state after: