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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Nonempty α
h : IsMarkovKernel 0
x : α := ⋯.some
⊢ False

Tactic:
have h1 : (0 : Measure β) .univ = 1 := (h.isProbabilityMeasure x).measure_univ

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Nonempty α
h : IsMarkovKernel 0
x : α := ⋯.some
h1 : 0 Set.univ = 1
⊢ False
Module: Mathlib.InformationTheory.Hamming

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

Tactic:
iff_not_comm,

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = 0 ↔ ¬0 < hammingDist x y
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
s t : Set β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hs : MeasurableSet s
⊢ IsSFiniteKernel (κ.restrict hs)

Tactic:
by
  refine ⟨⟨fun n => Kernel.restrict (seq κ n) hs, inferInstance, ?_⟩⟩
  ext1 a
  simp_rw [sum_apply, restrict_apply, ← Measure.restrict_sum _ hs, ← sum_apply, kernel_sum_seq]

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

Goal state before:
pp: case pos
α : 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✝ : IsFiniteKernel κ
f : β → γ
a : α
hf : Measurable f
⊢ ((κ.map f) a) Set.univ ≤ κ.bound

Tactic:
rw [map_apply' κ hf a MeasurableSet.univ]
    exact measure_le_bound κ a _

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 γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ.fst a) s = (κ a) {p | p.1 ∈ s}

Tactic:
rw [fst_apply, Measure.map_apply measurable_fst hs]; rfl

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 γ
inst✝ : Nonempty γ
κ : Kernel α β
⊢ IsSFiniteKernel (prodMkLeft γ κ) ↔ IsSFiniteKernel κ

Tactic:
by
  inhabit γ
  refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
  rw [← sectR_prodMkLeft γ κ default]
  infer_instance

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 γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
b : β
⊢ (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = s.indicator (fun b ↦ (η (a, b)) ({c | (b, c) ∈ u} ∩ t)) b

Tactic:
classical
    rw [Set.indicator_apply]
    split_ifs with h
    · simp only [h, true_and, Set.inter_def, Set.mem_ofPred]
    · simp only [h, false_and, and_false, Set.ofPred_false, measure_empty]

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

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ
s : Set α
hf : ¬Integrable (fun x ↦ rexp (f x)) μ
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Tactic:
simp [tilted_of_not_integrable hf, integral_undef 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 α
hp : Fact (1 ≤ p)
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ‖lpMeasSubgroupToLpTrim F p μ hm f‖ = ‖f‖

Tactic:
rw [Lp.norm_def, eLpNorm_trim hm (Lp.stronglyMeasurable _),
    eLpNorm_congr_ae (lpMeasSubgroupToLpTrim_ae_eq hm _), ← Lp.norm_def]

Goal state after:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ‖↑f‖ = ‖f‖
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x y : G
⊢ ↑↑(condExpIndL1Fin hm hs hμs (x + y)) =ᵐ[μ] ↑↑(condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm hs hμs y)

Tactic:
unfold condExpIndL1Fin Integrable.toL1

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x y : G
⊢ ↑↑(MemLp.toLp ↑↑(condExpIndSMul hm hs hμs (x + y)) ⋯) =ᵐ[μ]
    ↑↑(MemLp.toLp ↑↑(condExpIndSMul hm hs hμs x) ⋯ + MemLp.toLp ↑↑(condExpIndSMul hm hs hμs y) ⋯)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : G
⊢ (fun a ↦ ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 ⋯ hμs 1)) a • c) =ᵐ[μ] s.indicator fun x ↦ c

Tactic:
condExpL2_indicator_of_measurable hm hs hμs (1 : ℝ)

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : G
⊢ (fun a ↦ ↑↑(indicatorConstLp 2 ⋯ hμs 1) a • c) =ᵐ[μ] s.indicator fun x ↦ c
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp) + (condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) x ∂μ

Tactic:
setIntegral_congr_ae (hm s hs) ((Lp.coeFn_add (condExpL1CLM F' hm μ (hf_Lp.toLp f))
      (condExpL1CLM F' hm μ (hg_Lp.toLp g))).mono fun x hx _ => hx)

Goal state after:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s,
      (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) + ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp))) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) x ∂μ
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
hf : ¬Integrable f μ
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ (if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯ else 0) = 0

Tactic:
if_neg hf

Goal state after:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

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

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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ Integrable μ[f | m] μ

Tactic:
· rw [condExp_of_not_sigmaFinite hm hμm]; exact integrable_zero _ _ _

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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ Integrable μ[f | m] μ
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)

Tactic:
rw [klDiv_of_not_ac h_ac]

Goal state after:
case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : ¬μ ⊗ₘ κ ≪ ν ⊗ₘ η
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Goal state before:
pp: case hf
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
s : Set ℝ≥0∞
hs : MeasurableSet s
⊢ MeasurableSet ((fun a ↦ (Measure.map g μ).rnDeriv (Measure.map g ν) (g a)) ⁻¹' s)

Tactic:
exact ⟨((μ.map g).rnDeriv (ν.map g)) ⁻¹' s, hs.preimage (by fun_prop), by grind⟩

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

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable (fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal) (ν.trim hm)

Tactic:
refine integrable_of_le_of_le (f := fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal)
    (g₁ := fun x ↦ c * ((∂μ.trim hm/∂ν.trim hm) x).toReal + c')
    (g₂ := fun x ↦ (ν[fun x ↦ f (μ.rnDeriv ν x).toReal | m]) x)
    ?_ ?_ ?_ ?_ ?_

Goal state after:
case refine_1
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ AEStronglyMeasurable (fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal) (ν.trim hm)

case refine_2
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ (fun x ↦ c * ((∂μ.trim hm/∂ν.trim hm) x).toReal + c') ≤ᵐ[ν.trim hm] fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal

case refine_3
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ (fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal) ≤ᵐ[ν.trim hm] fun x ↦ ν[fun x ↦ f ((∂μ/∂ν) x).toReal | m] x

case refine_4
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable (fun x ↦ c * ((∂μ.trim hm/∂ν.trim hm) x).toReal + c') (ν.trim hm)

case refine_5
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable (fun x ↦ ν[fun x ↦ f ((∂μ/∂ν) x).toReal | m] x) (ν.trim hm)
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: case h.refine_2
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hf : StronglyMeasurable klFun
hf_cont : ContinuousWithinAt klFun (Ici 0) 0
h_int' : Integrable (fun x ↦ klFun ((∂μ/∂ν) x).toReal) ν
⊢ (fun x ↦ klFun (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x)) ≤ᵐ[ν]
    ν[fun x ↦ klFun ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨]

Tactic:
· refine ae_of_ae_trim hg.comap_le ?_
    exact convexOn_klFun.map_condExp_rnDeriv_le hg.comap_le hf hf_cont h_int'

Goal state after:
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 (ε ((Finsupp.linearCombination R ⇑b) (b.repr v)))) i

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
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 (ε ((b.repr v).sum fun i a ↦ a • b i))) i
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: case inr
R : Type u_6
inst✝¹⁰ : CommRing R
S : Type u_7
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_8
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
P : Type u_9
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
hR : Nontrivial R
b : Basis (Fin (finrank R M)) R M := finBasis R M
⊢ (((toMatrix b b) f).map ⇑(algebraMap R S)).det = (algebraMap R S) ((toMatrix b b) f).det

Tactic:
← RingHom.mapMatrix_apply,

Goal state after:
case inr
R : Type u_6
inst✝¹⁰ : CommRing R
S : Type u_7
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_8
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
P : Type u_9
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
hR : Nontrivial R
b : Basis (Fin (finrank R M)) R M := finBasis R M
⊢ ((algebraMap R S).mapMatrix ((toMatrix b b) f)).det = (algebraMap R S) ((toMatrix b b) f).det
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
i j : ι
h✝ : ∀ (v : V), ∃ x x_1, ∃ (_ : x • v + x_1 • f v = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
hj : ¬i = j
this : t = 0 ∨ (b.repr (f (b i))) j = 0
h' : t = 0
h : s • b i = 0
⊢ s = 0

Tactic:
contrapose hj

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
i j : ι
h✝ : ∀ (v : V), ∃ x x_1, ∃ (_ : x • v + x_1 • f v = 0), ¬(x = 0 ∧ x_1 = 0)
s t : R
this : t = 0 ∨ (b.repr (f (b i))) j = 0
h' : t = 0
h : s • b i = 0
hj : ¬s = 0
⊢ i = j
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
hx : x = b i + r • b j
this : s + t * (b.repr (f (b i))) i = -(t * r * (b.repr (f (b j))) i)
⊢ -(t * r * (b.repr ((b.coord j) (f (b j)) • b j)) i) = 0

Tactic:
simp [single_eq_of_ne hij]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Free R V
f : V →ₗ[R] V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
⊢ ∃ a, f = a • 1

Tactic:
by_cases hV1 : finrank R V = 1
  · rw [finrank_eq_one_iff Unit] at hV1
    let b : Basis Unit R V := Classical.ofNonempty
    use b.coord () (f (b ()))
    apply b.ext
    intro i
    nth_rewrite 1 [← b.linearCombination_repr (f (b i))]
    simp [linearCombination_unique]
  obtain ⟨a, rfl⟩ := exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent hV1 h
  refine ⟨a, by simp [Subring.smul_def]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
this : ↑(u.rangeRestrict x) = u x
⊢ (Finsupp.linearCombination K ⇑b) (b.repr (u.rangeRestrict x)) = (b.repr (u.rangeRestrict x)) default • b default

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
hu : u + LinearMap.id = ↑e
hr : 1 ≤ Module.rank K ↥u.range
b : Basis Unit K ↥u.range
x : V
this : ↑(u.rangeRestrict x) = u x
⊢ ((b.repr (u.rangeRestrict x)).sum fun i a ↦ a • b i) = (b.repr (u.rangeRestrict x)) default • b default
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case hle
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
this : finrank K (V ⧸ ker f) = 1
⊢ (↑e).fixedSubmodule ≤ ker f

Tactic:
intro x
          rw [mem_ker, ← Submodule.mem_bot K, ← hf]
          exact mem_map_of_mem

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

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
⊢ (toBaseChange A Q).comp involute = (Algebra.TensorProduct.map (AlgHom.id A A) involute).comp (toBaseChange A Q)

Tactic:
by
  ext v
  change toBaseChange A Q (involute (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))
    = (Algebra.TensorProduct.map (AlgHom.id _ _) involute :
        A ⊗[R] CliffordAlgebra Q →ₐ[A] _)
      (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))
  rw [toBaseChange_ι, involute_ι, map_neg (toBaseChange A Q), toBaseChange_ι,
    Algebra.TensorProduct.map_tmul, AlgHom.id_apply, involute_ι, TensorProduct.tmul_neg]

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this✝ : Fintype ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.diagonal (Function.update 1 i (1 + f v))
⊢ (Matrix.diagonal (Function.update 1 i (1 + f v))).det = 1 + f v

Tactic:
simp only [Matrix.det_diagonal]

Goal state after:
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this✝ : Fintype ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.diagonal (Function.update 1 i (1 + f v))
⊢ ∏ i_1, Function.update 1 i (1 + f v) i_1 = 1 + f v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm ⋯) x✝ -
      ((contractLeft (B' m✝)) ((changeForm ⋯) x✝) + (contractLeft (B m✝)) ((changeForm ⋯) x✝)) =
    (ι Q'') m✝ * (changeForm ⋯) x✝ -
      ((contractLeft (B m✝)) ((changeForm ⋯) x✝) + (contractLeft (B' m✝)) ((changeForm ⋯) x✝))

Tactic:
add_comm (_ : CliffordAlgebra Q'')

Goal state after:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm ⋯) x✝ -
      ((contractLeft (B m✝)) ((changeForm ⋯) x✝) + (contractLeft (B' m✝)) ((changeForm ⋯) x✝)) =
    (ι Q'') m✝ * (changeForm ⋯) x✝ -
      ((contractLeft (B m✝)) ((changeForm ⋯) x✝) + (contractLeft (B' m✝)) ((changeForm ⋯) x✝))