mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

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

Tactic:
have ⟨h_int_μν, h_int_κη⟩ := (integrable_llr_compProd_iff h_ac).mp h_int

Goal state after:
case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:

Tactic:
s.indicator (μ[s.indicator f + sᶜ.indicator f | m]) =ᵐ[μ]
        s.indicator (μ[s.indicator f | m] + μ[sᶜ.indicator f | m]) := by
      filter_upwards [condExp_add (hf_int.indicator (hm _ hs)) (hf_int.indicator (hm _ hs.compl)) m]
        with x hx
      classical rw [Set.indicator_apply, Set.indicator_apply, hx]
    _ = s.indicator (μ[s.indicator f | m]) + s.indicator (μ[sᶜ.indicator f | m]) :=
      (s.indicator_add' _ _)
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) +
        s.indicator (sᶜ.indicator (μ[sᶜ.indicator f | m])) := by
      refine Filter.EventuallyEq.rfl.add ?_
      have : sᶜ.indicator (μ[sᶜ.indicator f | m]) =ᵐ[μ] μ[sᶜ.indicator f | m] := by
        refine (condExp_indicator_aux hs.compl ?_).symm.trans ?_
        · exact indicator_ae_eq_restrict_compl (hm _ hs.compl)
        · rw [Set.indicator_indicator, Set.inter_self]
      filter_upwards [this] with x hx
      by_cases hxs : x ∈ s
      · simp only [hx, hxs, Set.indicator_of_mem]
      · simp only [hxs, Set.indicator_of_notMem, not_false_iff]
    _ =ᵐ[μ] s.indicator (μ[s.indicator f | m]) := by
      rw [Set.indicator_indicator, Set.inter_compl_self, Set.indicator_empty', add_zero]
    _ =ᵐ[μ] μ[s.indicator f | m] := by
      refine (condExp_indicator_aux hs ?_).symm.trans ?_
      · exact indicator_ae_eq_restrict_compl (hm _ hs)
      · rw [Set.indicator_indicator, Set.inter_self]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
⊢ (μ.restrict s)[f | m] =ᵐ[μ.restrict s] μ[f | m]

Tactic:
ae_eq_restrict_iff_indicator_ae_eq (hm _ hs_m)

Goal state after:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs_m : MeasurableSet s
hf_int : Integrable f μ
this : SigmaFinite ((μ.restrict s).trim hm)
⊢ s.indicator (μ.restrict s)[f | m] =ᵐ[μ] s.indicator μ[f | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
⊢ μ[f | m] =ᵐ[μ.restrict s] μ[f | m₂]

Tactic:
ae_eq_restrict_iff_indicator_ae_eq (hm _ hs_m)

Goal state after:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
⊢ s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[f | m₂]
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case h12
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
hY : AEMeasurable Y (P.trim hm)
hXY : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
s : Set Ω
hs : MeasurableSet s
a✝ : (P.trim hm) s < ∞
⊢ ∫⁻ (x : Ω) in s, Y x ∂P.trim hm = ∫⁻ (x : Ω) in s, P⁻[X | mΩ] x ∂P.trim hm

Tactic:
setLIntegral_trim_ae hm hY hs,

Goal state after:
case h12
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
hY : AEMeasurable Y (P.trim hm)
hXY : ∀ (s : Set Ω), MeasurableSet s → ∫⁻ (ω : Ω) in s, Y ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
s : Set Ω
hs : MeasurableSet s
a✝ : (P.trim hm) s < ∞
⊢ ∫⁻ (x : Ω) in s, Y x ∂P = ∫⁻ (x : Ω) in s, P⁻[X | mΩ] x ∂P.trim hm
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]

Tactic:
by
  borelize E
  obtain ⟨t, ht, htt⟩ := hf_int.aestronglyMeasurable.isSeparable_ae_range
  let Y := (Submodule.span ℝ t).topologicalClosure
  have : CompleteSpace Y := (Submodule.isClosed_topologicalClosure _).completeSpace_coe
  have : SecondCountableTopology Y := ht.span.closure.secondCountableTopology
  let φY := φ ∘ Y.subtypeL
  classical
  let fY : α → Y := fun a => if h : f a ∈ Y then ⟨f a, h⟩ else 0
  let fX : α → E := Y.subtypeL ∘ fY
  have lem0 : ∀ᵐ a ∂μ, f a ∈ Y := by
    filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)
  have lem1 : f =ᵐ[μ] fX := by
    filter_upwards [lem0] with a ha
    simp_all [fX, fY]
  have hfY_int : Integrable fY μ := by
    refine (hf_int.congr lem1).mono ?_ (by simp [fX])
    obtain ⟨g, hg1, hg2, hg3⟩ := hf_int.1.exists_stronglyMeasurable_range_subset
      ((Submodule.isClosed_topologicalClosure _).measurableSet) Nonempty.of_subtype lem0
    refine ⟨codRestrict g Y hg2, (hg1.measurable.codRestrict hg2).stronglyMeasurable, ?_⟩
    filter_upwards [hg3] with a ha
    have : g a ∈ Y := hg2 a
    simp_all [fY, codRestrict]
  have lem2 : μ[f | m] =ᵐ[μ] Y.subtypeL ∘ μ[fY | m] := calc
    _ =ᵐ[μ] μ[fX | m] := condExp_congr_ae lem1
    _ =ᵐ[μ] _ := (Y.subtypeL.comp_condExp_comm hfY_int).symm
  have lem3 : φ ∘ f =ᵐ[μ] φY ∘ fY := by filter_upwards [lem1] with a ha; simp [φY, ha, fX]
  calc
    φ ∘ μ[f | m]
      =ᵐ[μ] φY ∘ μ[fY | m] := by filter_upwards [lem2] with a ha; simp [φY, ha]
    _ ≤ᵐ[μ] μ[φY ∘ fY | m] := by
      refine (hφ_cvx.comp_linearMap Y.subtype).map_condExp_le_of_hereditarilyLindelofSpace
        (s := Y.subtypeL ⁻¹' s) hm ?_ ?_ ?_ hfY_int (Integrable.congr hφ_int lem3)
      · exact hφ_cont.comp (by fun_prop) fun x => by
          #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
          (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
          goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem
          in the new canonicalizer; a minimization would help. The original proof was: `grind` -/
          simp
      · filter_upwards [lem0, hf] with a ha hb
        simp_all [fY]
      · exact hs.preimage Y.subtypeL.continuous
    _ =ᵐ[μ] μ[φ ∘ f | m] := condExp_congr_ae lem3.symm

Goal state after:
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 μ ν) μ
⊢ Integrable (fun x ↦ klFun ((∂μ/∂ν) x).toReal) ν

Tactic:
integrable_klFun_rnDeriv_iff hμν

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
h_int : Integrable (llr μ ν) μ
⊢ Integrable (llr μ ν) μ
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: case neg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ klDiv (Measure.map g μ) (Measure.map g ν) ≤ klDiv μ ν

pp: case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ klDiv (Measure.map g μ) (Measure.map g ν) ≤ klDiv μ ν

Tactic:
· simp [klDiv_of_not_integrable h_int]

Goal state after:
case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ klDiv (Measure.map g μ) (Measure.map g ν) ≤ klDiv μ ν
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 : 𝓧 → 𝓨
hg : Measurable g
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hf : StronglyMeasurable klFun
hf_cont : ContinuousWithinAt klFun (Ici 0) 0
⊢ Integrable (fun x ↦ klFun ((∂μ/∂ν) x).toReal) ν

Tactic:
integrable_klFun_rnDeriv_iff hμν

Goal state after:
𝓧 : 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
⊢ Integrable (llr μ ν) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hφ_cont : UpperSemicontinuous φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ μ[φ ∘ f | m] ≤ᵐ[μ] φ ∘ μ[f | m]

Tactic:
filter_upwards [hφ_cvx.neg.map_condExp_le_univ hm hφ_cont.neg hf_int hφ_int.neg,
    condExp_neg (φ ∘ f) m] with a h ha
  simp_all [Pi.neg_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Isometry

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
g : B₂ →bᵢ B₃
f : B₁ →bᵢ B₂
x y : M₁
⊢ (B₃ (g (f x))) (g (f y)) = (B₂ (f x)) (f y)

Tactic:
← g.map_app

Goal state after:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
g : B₂ →bᵢ B₃
f : B₁ →bᵢ B₂
x y : M₁
⊢ (B₃ (g (f x))) (g (f y)) = (B₃ (g (f x))) (g (f y))
Module: Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
g : B₂.IsometryEquiv B₃
n m : M₁
⊢ (B₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun n)) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) =
    (B₂ (f n)) (f m)

Tactic:
← g.map_app

Goal state after:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
g : B₂.IsometryEquiv B₃
n m : M₁
⊢ (B₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun n)) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) =
    (B₃ (g (f n))) (g (f m))
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr.mp.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : (1 - r) • (c -ᵥ ↑h.some) +ᵥ x = p
⊢ t • (x -ᵥ ↑h.some) +ᵥ ↑h.some ∈ s

Tactic:
refine vadd_mem_of_mem_direction ?_ h.some.prop

Goal state after:
case inr.mp.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : (1 - r) • (c -ᵥ ↑h.some) +ᵥ x = p
⊢ t • (x -ᵥ ↑h.some) ∈ s.direction
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr.mpr.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : r • (x -ᵥ c) +ᵥ c = p
⊢ r • (x -ᵥ ↑h.some) +ᵥ ↑h.some ∈ s

Tactic:
refine vadd_mem_of_mem_direction ?_ h.some.prop

Goal state after:
case inr.mpr.refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : r • (x -ᵥ c) +ᵥ c = p
⊢ r • (x -ᵥ ↑h.some) ∈ s.direction
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: case tmul
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Module S P
inst✝ : IsScalarTower R S P
α : M →ₗ[R] P
j : IsBaseChange S α
m : M
⊢ (j.endHom 1) (α m) = 1 (α m)

Tactic:
| tmul m =>

Goal state after:
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 : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
⊢ (d₁ + d₂) m✝ • x✝ - (ι Q) m✝ * ((foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝) =
    d₁ m✝ • x✝ - (ι Q) m✝ * (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ +
      (d₂ m✝ • x✝ - (ι Q) m✝ * (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝)

Tactic:
rw [sub_add_sub_comm, mul_add, LinearMap.add_apply, add_smul]

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

Goal state before:
pp: x y : CliffordAlgebra Q
⊢ CliffordAlgebraComplex.equiv (x * y) = CliffordAlgebraComplex.equiv (y * x)

Tactic:
map_mul,

Goal state after:
x y : CliffordAlgebra Q
⊢ CliffordAlgebraComplex.equiv x * CliffordAlgebraComplex.equiv y = CliffordAlgebraComplex.equiv (y * x)
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₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ ↑((toEven Q)
        (((ι Q) (m₁, r₁).1 + (algebraMap R (CliffordAlgebra Q)) (m₁, r₁).2) *
          ((ι Q) (m₂, r₂).1 - (algebraMap R (CliffordAlgebra Q)) (m₂, r₂).2))) =
    (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) *
      (e0 Q * (v Q) m₂ - (algebraMap R (CliffordAlgebra (Q' Q))) r₂)

Tactic:
map_mul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ ↑((toEven Q) ((ι Q) (m₁, r₁).1 + (algebraMap R (CliffordAlgebra Q)) (m₁, r₁).2) *
        (toEven Q) ((ι Q) (m₂, r₂).1 - (algebraMap R (CliffordAlgebra Q)) (m₂, r₂).2)) =
    (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) *
      (e0 Q * (v Q) m₂ - (algebraMap R (CliffordAlgebra (Q' Q))) r₂)
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 Q' : QuadraticForm R M
h : Q' = -Q
m₁ m₂ m₃ : M
⊢ -Q m₂ • ((even.ι Q').bilin m₁) m₃ = Q m₂ • -((even.ι Q').bilin m₁) m₃

Tactic:
smul_neg,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
h : Q' = -Q
m₁ m₂ m₃ : M
⊢ -Q m₂ • ((even.ι Q').bilin m₁) m₃ = -(Q m₂ • ((even.ι Q').bilin m₁) m₃)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.mem_mul
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
ih₁ : (map f₁) x₁ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i) • ((map f₂) m₂ * (map f₁) x₁)
v₁ : M₁
⊢ (map f₁) ((ι Q₁) v₁ * x₁) * (map f₂) m₂ = (-1) ^ (i₂ * ↑i.succ) • ((map f₂) m₂ * (map f₁) ((ι Q₁) v₁ * x₁))

Tactic:
map_mul,

Goal state after:
case mem.mem_mul
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
ih₁ : (map f₁) x₁ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i) • ((map f₂) m₂ * (map f₁) x₁)
v₁ : M₁
⊢ (map f₁) ((ι Q₁) v₁) * (map f₁) x₁ * (map f₂) m₂ =
    (-1) ^ (i₂ * ↑i.succ) • ((map f₂) m₂ * ((map f₁) ((ι Q₁) v₁) * (map f₁) x₁))
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] ℬ
⊢ x * 1 = x

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

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

Goal state before:
pp: case mem.mem_mul.e_a.e_a.mem.mem_mul
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ m₁' : CliffordAlgebra Q₁
i₁n i✝ : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i✝
v₁ : M₁
m₂' : CliffordAlgebra Q₂
i₂n i : ℕ
x₂ : CliffordAlgebra Q₂
_hx₂ : x₂ ∈ (ι Q₂).range ^ i
ih₂ : (ι Qₙ) (f₁ v₁) * (map f₂) x₂ = (-1) ^ ↑i • ((map f₂) x₂ * (ι Qₙ) (f₁ v₁))
v₂ : M₂
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) ((ι Q₂) v₂ * x₂) = (-1) ^ ↑i.succ • ((map f₂) ((ι Q₂) v₂ * x₂) * (ι Qₙ) (f₁ v₁))

Tactic:
map_mul,

Goal state after:
case mem.mem_mul.e_a.e_a.mem.mem_mul
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ m₁' : CliffordAlgebra Q₁
i₁n i✝ : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i✝
v₁ : M₁
m₂' : CliffordAlgebra Q₂
i₂n i : ℕ
x₂ : CliffordAlgebra Q₂
_hx₂ : x₂ ∈ (ι Q₂).range ^ i
ih₂ : (ι Qₙ) (f₁ v₁) * (map f₂) x₂ = (-1) ^ ↑i • ((map f₂) x₂ * (ι Qₙ) (f₁ v₁))
v₂ : M₂
⊢ (ι Qₙ) (f₁ v₁) * ((map f₂) ((ι Q₂) v₂) * (map f₂) x₂) =
    (-1) ^ ↑i.succ • ((map f₂) ((ι Q₂) v₂) * (map f₂) x₂ * (ι Qₙ) (f₁ v₁))
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: case mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ (ι R).range ^ i✝
ih : (liftι R M) x✝ = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
w✝ : M
⊢ (liftι R M) ((ι R) w✝ * x✝) = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝.succ) ⟨(ι R) w✝ * x✝, ⋯⟩

Tactic:
map_mul,

Goal state after:
case mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ (ι R).range ^ i✝
ih : (liftι R M) x✝ = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
w✝ : M
⊢ (liftι R M) ((ι R) w✝) * (liftι R M) x✝ = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝.succ) ⟨(ι R) w✝ * x✝, ⋯⟩