mathlib-initiative/mathlib-tactics huggingface dataset:
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
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
h : H
w : NormalWord d
⊢ (base φ) h • w = h • w

Tactic:
by
  rw [base_smul_def, base_smul_def']

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (xa i) = 2 ^ 2

Tactic:
have : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two

Goal state after:
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ orderOf (xa i) = 2 ^ 2
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a 1 ^ orderOf (a 1) = 1
⊢ False

Tactic:
rw [a_one_pow] at h1

Goal state after:
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a ↑(orderOf (a 1)) = 1
⊢ False
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∫⁻ (a : α), f a ∂Kernel.id a = f a

Tactic:
by
  rw [id_apply, lintegral_dirac' _ hf]

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
i : ι
I : Finset ι
hi_notMem_I : i ∉ I
h_ind : (∀ i ∈ I, IsSFiniteKernel (κs i)) → IsSFiniteKernel (∑ i ∈ I, κs i)
h : ∀ i_1 ∈ insert i I, IsSFiniteKernel (κs i_1)
this✝ : IsSFiniteKernel (κs i)
this : IsSFiniteKernel (∑ x ∈ I, κs x)
⊢ IsSFiniteKernel (κs i + ∑ x ∈ I, κs x)

Tactic:
exact IsSFiniteKernel.add _ _

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y : Hamming β), ↑(hammingDist (ofHamming x) (ofHamming y)) = ↑(hammingDist (ofHamming y) (ofHamming x))

Tactic:
exact mod_cast hammingDist_comm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
ac : α × γ
g : β × δ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (bd : β × δ), g bd ∂(κ ∥ₖ η) ac = ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂η ac.2 ∂κ ac.1

Tactic:
rw [parallelComp_apply, MeasureTheory.lintegral_prod _ hg.aemeasurable]

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 (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ (((Measure.dirac (a, a).1).prod (κ (a, a).2)).bind
        ⇑(swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β)))
      s =
    ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a

Tactic:
Measure.bind_apply hs (by fun_prop),

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ ∫⁻ (a : α × β),
      ((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β)) a)
        s ∂(Measure.dirac (a, a).1).prod (κ (a, a).2) =
    ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
⊢ (((η ((a, b), b).1).prod (Measure.dirac ((a, b), b).2)).bind ⇑(swap γ β)) s = (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
Measure.bind_apply hs (by fun_prop),

Goal state after:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
⊢ ∫⁻ (a : γ × β), ((swap γ β) a) s ∂(η ((a, b), b).1).prod (Measure.dirac ((a, b), b).2) = (η (a, b)) (Prod.mk b ⁻¹' s)
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:
rw [prod_apply' _ _ _ hs, lintegral_deterministic']

Goal state after:
case hf
α : 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
⊢ Measurable fun b ↦ (κ a) (Prod.mk b ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.Prod

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 δ
κ : Kernel α β
h : IsZeroOrMarkovKernel κ
η : Kernel α γ
inst✝ : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel (κ ×ₖ η)

Tactic:
by
  rcases eq_zero_or_isMarkovKernel κ with rfl | h
  · simp only [prod]; infer_instance
  rcases eq_zero_or_isMarkovKernel η with rfl | h'
  · simp only [prod]; infer_instance
  infer_instance

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

Goal state before:
pp: case pos.e_f
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
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
d : T
⊢ ∫⁻ (x : Y), (Prod.mk d ⁻¹' s).indicator (1 ∘ Prod.mk d) x ∂κ ac.1 = (κ ac.1) (Prod.mk d ⁻¹' s)

Tactic:
lintegral_indicator (measurable_prodMk_left hs)

Goal state after:
case pos.e_f
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
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
ac : X × Z
s : Set (T × Y)
hs : MeasurableSet s
d : T
⊢ ∫⁻ (a : Y) in Prod.mk d ⁻¹' s, (1 ∘ Prod.mk d) a ∂κ ac.1 = (κ ac.1) (Prod.mk d ⁻¹' s)
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
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f ((κ ⊗ₖ η) a)
hg : Integrable g ((κ ⊗ₖ η) a)
⊢ ∫ (x : β), F (∫ (y : γ), f (x, y) + g (x, y) ∂η (a, x)) ∂κ a =
    ∫ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) + ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a

Tactic:
by
  refine integral_congr_ae ?_
  filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g
  simp [integral_add h2f h2g]

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

Goal state before:
pp: case h0
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ 0 < ∫ (x : α), rexp (f x) ∂μ

Tactic:
exact integral_exp_pos hf

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ (fun x ↦ rexp (llr μ ν x)) =ᵐ[μ] fun x ↦ (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [hμν.ae_le (exp_llr μ ν), Measure.rnDeriv_pos hμν] with x hx_eq hx_pos
  rw [hx_eq, if_neg hx_pos.ne']

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ (-llr μ ν) x = llr ν μ x

Tactic:
rw [Pi.neg_apply, llr, llr, ← log_inv, ← ENNReal.toReal_inv]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ log (μ.rnDeriv ν x)⁻¹.toReal = log (ν.rnDeriv μ x).toReal
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log c.toReal

Tactic:
simp only [llr, llr_def]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ (fun x ↦ log ((c • μ).rnDeriv ν x).toReal) =ᵐ[μ] fun x ↦ log (μ.rnDeriv ν x).toReal + log c.toReal
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log c.toReal

Tactic:
simp only [llr, llr_def]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ (fun x ↦ log (μ.rnDeriv (c • ν) x).toReal) =ᵐ[μ] fun x ↦ log (μ.rnDeriv ν x).toReal - log c.toReal
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ≠ 0

Tactic:
filter_upwards
      simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]
      exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0

Tactic:
filter_upwards
      simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]
      exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x ↦ rexp (f x)) ν
⊢ μ.rnDeriv (ν.tilted f) =ᵐ[ν] fun x ↦ ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x

Tactic:
cases eq_zero_or_neZero ν with
  | inl h => simp_rw [h, ae_zero, Filter.EventuallyEq]; exact Filter.eventually_bot
  | inr h0 =>
    refine (Measure.rnDeriv_withDensity_right μ ν ?_ ?_ ?_).trans ?_
    · exact (hf.1.aemeasurable.div_const _).ennreal_ofReal
    · filter_upwards
      simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]
      exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)
    · refine ae_of_all _ (by simp)
    · filter_upwards with x
      congr
      rw [← ENNReal.ofReal_inv_of_pos, inv_div', ← exp_neg, div_eq_mul_inv, inv_inv]
      exact div_pos (exp_pos _) (integral_exp_pos hf)

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

Goal state before:
pp: α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
⊢ lpMeasSubgroupToLpTrim F p μ hm (f - g) = lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g

Tactic:
by
  rw [sub_eq_add_neg, sub_eq_add_neg, lpMeasSubgroupToLpTrim_add,
    lpMeasSubgroupToLpTrim_neg]

Goal state after:
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 : ∀ᵐ (a : X) ∂μ, ∑' (n : ι), ‖f n a‖ₑ < ∞
⊢ ∀ᵐ (a : X) ∂μ, Summable fun n ↦ ‖f n a‖

Tactic:
by
    filter_upwards [H] with x hx using tsum_enorm_ne_top_iff_summable_norm.1 hx.ne

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

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f' : ↥(lpMeas F ℝ m p μ) := ⟨f✝, hf✝⟩
g✝ : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'
hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g✝
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
⊢ P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf)) →
    P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp g hg)) →
      P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg))

Tactic:
hfP

Goal state after:
case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f' : ↥(lpMeas F ℝ m p μ) := ⟨f✝, hf✝⟩
g✝ : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'
hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g✝
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf))
⊢ P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp g hg)) →
    P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun x ↦ c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → MemLp f p μ → P f → P g
f✝ : α → F
hf : MemLp f✝ p μ
hfm✝ : AEStronglyMeasurable f✝ μ
f_Lp : ↥(Lp F p μ) := toLp f✝ hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
⊢ P ↑↑(toLp f hf_mem) → P ↑↑(toLp g hg_mem) → P ↑↑(toLp f hf_mem + toLp g hg_mem)

Tactic:
hfP

Goal state after:
case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : (α → F) → Prop
h_ind : ∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun x ↦ c)
h_add :
  ∀ ⦃f g : α → F⦄,
    Disjoint (Function.support f) (Function.support g) →
      MemLp f p μ → MemLp g p μ → StronglyMeasurable f → StronglyMeasurable g → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑↑f}
h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → MemLp f p μ → P f → P g
f✝ : α → F
hf : MemLp f✝ p μ
hfm✝ : AEStronglyMeasurable f✝ μ
f_Lp : ↥(Lp F p μ) := toLp f✝ hf
hfm_Lp : AEStronglyMeasurable (↑↑f_Lp) μ
f g : α → F
hf_mem : MemLp f p μ
hg_mem : MemLp g p μ
hfm : StronglyMeasurable f
hgm : StronglyMeasurable g
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P ↑↑(toLp f hf_mem)
⊢ P ↑↑(toLp g hg_mem) → P ↑↑(toLp f hf_mem + toLp g hg_mem)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

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

Tactic:
exact (coeFn_add _ _).trans
    ((condExp_ae_eq_condExpL1 hm _).symm.add (condExp_ae_eq_condExpL1 hm _).symm)

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

Goal state before:
pp: case pos.refine_3
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : (μ.restrict s) t < ∞
⊢ ∫ (x : α) in t, f x ∂μ.restrict s = ∫ (x : α) in t, 0 x ∂μ.restrict s

Tactic:
refine setIntegral_congr_ae (hm _ ht) ?_

Goal state after:
case pos.refine_3
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᵐ[μ.restrict s] 0
hm : m ≤ m0
hμm this✝ : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : (μ.restrict s) t < ∞
⊢ ∀ᵐ (x : α) ∂μ.restrict s, x ∈ t → f x = 0 x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ι : Type u_5
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[fun a ↦ ∑' (i : ι), f i a | m] =ᵐ[μ] fun a ↦ ∑' (i : ι), μ[f i | m] a

Tactic:
simp only [condExp_of_not_sigmaFinite hm hμm, Pi.zero_apply, tsum_zero]

Goal state after:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
ι : Type u_5
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᵐ[μ] fun a ↦ 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : 0 ≤ᵐ[μ] f
hfint : Integrable f μ
⊢ 0 ≤ᵐ[μ] μ[f | m]

Tactic:
rw [(condExp_zero.symm : (0 : α → E) = μ[0 | m])]

Goal state after:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : 0 ≤ᵐ[μ] f
hfint : Integrable f μ
⊢ μ[0 | m] ≤ᵐ[μ] μ[f | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : f ≤ᵐ[μ] 0
hfint : Integrable f μ
⊢ μ[f | m] ≤ᵐ[μ] 0

Tactic:
rw [(condExp_zero.symm : (0 : α → E) = μ[0 | m])]

Goal state after:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : f ≤ᵐ[μ] 0
hfint : Integrable f μ
⊢ μ[f | m] ≤ᵐ[μ] μ[0 | m]
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
h_int : Integrable (llr μ ν) μ
⊢ klDiv (Measure.map g μ) (Measure.map g ν) =
    ENNReal.ofReal (∫ (x : 𝓧), klFun (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν)

Tactic:
rw [klDiv_eq_integral_klFun, if_pos ⟨hμν.map hg, integrable_llr_map hμν hg h_int⟩]
  congr
  rw [← toReal_klDiv_eq_integral_klFun (hμν.map hg), toReal_klDiv_map_of_ac hμν hg]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
V : Type u_2
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
W : Type u_3
inst✝⁵ : AddCommMonoid W
inst✝⁴ : Module R W
A : Type u_4
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : Module A W
inst✝ : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
f : Dual R V
⊢ ibc.toDual f = (Dual.congr ibc.equiv) ((Dual.baseChange A) f)

Tactic:
apply ibc.algHom_ext

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
V : Type u_2
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
W : Type u_3
inst✝⁵ : AddCommMonoid W
inst✝⁴ : Module R W
A : Type u_4
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : Module A W
inst✝ : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
f : Dual R V
⊢ ∀ (x : V), (ibc.toDual f) (j x) = ((Dual.congr ibc.equiv) ((Dual.baseChange A) f)) (j x)