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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
⊢ klDiv μ (c • ν) = ↑c * klDiv (c⁻¹ • μ) ν

Tactic:
by
  have hc' : (c : ℝ≥0∞) ≠ 0 := by simpa
  have hμ_smul : μ = c • (c⁻¹ • μ) := by rw [smul_smul, mul_inv_cancel₀ hc, one_smul]
  have hν_smul : ν = c⁻¹ • (c • ν) := by rw [smul_smul, inv_mul_cancel₀ hc, one_smul]
  by_cases hμν : μ ≪ ν
  swap
  · rw [klDiv_of_not_ac, klDiv_of_not_ac, ENNReal.mul_top hc']
    · refine fun h_contra ↦ hμν ?_
      rw [hμ_smul]
      exact h_contra.smul_left _
    · refine fun h_contra ↦ hμν ?_
      rw [hν_smul]
      exact h_contra.smul_right (by simpa)
  have hμν_right := hμν.smul_right hc'
  simp only [Measure.coe_nnreal_smul] at hμν_right
  by_cases h_int : Integrable (llr μ ν) μ
  swap
  · rw [klDiv_of_not_integrable, klDiv_of_not_integrable, ENNReal.mul_top hc']
    · refine fun h_contra ↦ h_int ?_
      rw [hμ_smul]
      refine Integrable.smul_measure_nnreal ?_
      rw [integrable_congr (llr_smul_nnreal_left (hμν.smul_left _) c hc)]
      fun_prop
    · refine fun h_contra ↦ h_int ?_
      rw [hν_smul]
      have : IsFiniteMeasure ((c : ℝ≥0∞) • ν) := by
        simp only [Measure.coe_nnreal_smul]
        infer_instance
      have h := llr_smul_nnreal_right (hμν.smul_right hc') c⁻¹ (by simpa)
      simp only [Measure.coe_nnreal_smul, NNReal.coe_inv, log_inv, sub_neg_eq_add] at h
      rw [integrable_congr h]
      fun_prop
  have h_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ) := by
    refine Integrable.smul_measure_nnreal ?_
    rw [integrable_congr (llr_smul_nnreal_left hμν c⁻¹ (by simpa))]
    fun_prop
  have h_int_right : Integrable (llr μ (c • ν)) μ := by
    rw [integrable_congr (llr_smul_nnreal_right hμν c (by simpa))]
    fun_prop
  rw [← ENNReal.ofReal_toReal (klDiv_ne_top hμν_right h_int_right),
    toReal_klDiv_smul_right_eq_smul_left hμν h_int c]
  simp only [NNReal.zero_le_coe, ENNReal.ofReal_mul, ENNReal.ofReal_coe_nnreal]
  rw [ENNReal.ofReal_toReal]
  exact klDiv_ne_top (hμν.smul_left _) h_int_left

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)
inst✝ : CompleteSpace F
hm : m ≤ m0
⊢ IsComplete {f | AEStronglyMeasurable (↑↑f) μ}

Tactic:
← completeSpace_coe_iff_isComplete

Goal state after:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
inst✝ : CompleteSpace F
hm : m ≤ m0
⊢ CompleteSpace ↑{f | AEStronglyMeasurable (↑↑f) μ}
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν

Tactic:
rw [← ENNReal.ofReal_toReal (a := klDiv μ ν)]

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤
    ENNReal.ofReal (klDiv μ ν).toReal

case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ klDiv μ ν ≠ ∞
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 α
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 μ),
    StronglyMeasurable f →
      StronglyMeasurable 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 g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᵐ[μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᵐ[μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᵐ[μ] ∅
f' : α → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
⊢ s_f \ ∅ =ᵐ[μ] s_f

Tactic:
rw [Set.sdiff_empty]

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 α
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 μ),
    StronglyMeasurable f →
      StronglyMeasurable 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 g : α → F
hf : MemLp f p μ
hg : MemLp g p μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
h_disj : Disjoint (Function.support f) (Function.support g)
hPf : P (MemLp.toLp f hf)
hPg : P (MemLp.toLp g hg)
s_f : Set α := Function.support (AEStronglyMeasurable.mk f hfm)
hs_f : MeasurableSet s_f
hs_f_eq : s_f =ᵐ[μ] Function.support f
s_g : Set α := Function.support (AEStronglyMeasurable.mk g hgm)
hs_g : MeasurableSet s_g
hs_g_eq : s_g =ᵐ[μ] Function.support g
h_inter_empty : s_f ∩ s_g =ᵐ[μ] ∅
f' : α → F := (s_f \ s_g).indicator (AEStronglyMeasurable.mk f hfm)
hff' : f =ᵐ[μ] f'
hf'_meas : StronglyMeasurable f'
hf'_Lp : MemLp f' p μ
g' : α → F := (s_g \ s_f).indicator (AEStronglyMeasurable.mk g hgm)
⊢ s_g \ ∅ =ᵐ[μ] s_g

Tactic:
rw [Set.sdiff_empty]

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

Goal state before:
pp: case refine_3
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
h_coe : ↑↑(T.compLp ↑((condExpL2 E' 𝕜 hm) f)) =ᵐ[μ] fun a ↦ T (↑↑↑((condExpL2 E' 𝕜 hm) f) a)
⊢ AEStronglyMeasurable (↑↑(T.compLp ↑((condExpL2 E' 𝕜 hm) f))) μ

Tactic:
refine AEStronglyMeasurable.congr ?_ h_coe.symm

Goal state after:
case refine_3
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
inst✝⁶ : CompleteSpace E'
inst✝⁵ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst✝⁴ : RCLike 𝕜'
inst✝³ : NormedAddCommGroup E''
inst✝² : InnerProductSpace 𝕜' E''
inst✝¹ : CompleteSpace E''
inst✝ : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
h_coe : ↑↑(T.compLp ↑((condExpL2 E' 𝕜 hm) f)) =ᵐ[μ] fun a ↦ T (↑↑↑((condExpL2 E' 𝕜 hm) f) a)
⊢ AEStronglyMeasurable (fun a ↦ T (↑↑↑((condExpL2 E' 𝕜 hm) f) a)) μ
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 κ
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ κ
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν

Tactic:
klDiv_eq_lintegral_klFun_of_ac h_ac,

Goal state after:
case pos
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsMarkovKernel κ
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ κ
⊢ ∫⁻ (x : 𝓧 × 𝓨), ENNReal.ofReal (klFun ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) x).toReal) ∂ν ⊗ₘ κ = klDiv μ ν
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
⊢ Measurable P⁻[X | mΩ]

Tactic:
by_cases hm : mΩ ≤ mΩ₀
  · exact (measurable_condLExp _ _ _).mono hm (le_refl _)
  · simp [condLExp_of_not_le hm, measurable_zero]

Goal state after:
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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs✝ : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᵐ[μ] fX
a : α
ha : f a ∈ Y
hs : f a ∈ s
⊢ fY a ∈ ⇑Y.subtypeL ⁻¹' s

Tactic:
simpa [fY, ha]

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

Goal state before:
pp: case neg
α : 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)
hs_m₂ : MeasurableSet s
hf_int : ¬Integrable f μ
⊢ s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[f | m₂]

pp: case pos
α : 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)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
⊢ s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[f | m₂]

Tactic:
· simp_rw [condExp_of_not_integrable hf_int]; rfl

Goal state after:
case pos
α : 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)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
⊢ s.indicator μ[f | m] =ᵐ[μ] s.indicator μ[f | m₂]
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
V : Type u_2
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : Algebra A R
inst✝¹ : Module A V
inst✝ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := ⋯
⊢ Function.Bijective ⇑(Finsupp.linearCombination R ⇑b ∘ₗ ↑j)

Tactic:
LinearMap.coe_comp,

Goal state after:
case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
V : Type u_2
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : Algebra A R
inst✝¹ : Module A V
inst✝ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
j : R ⊗[A] (ι →₀ A) ≃ₗ[R] ι →₀ R := finsuppScalarRight A R R ι
⊢ Function.Bijective (⇑(Finsupp.linearCombination R ⇑b) ∘ ⇑↑j)
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁷ : CommSemiring R
V : Type u_2
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Module R V
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Algebra A R
inst✝² : Module A V
inst✝¹ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst✝ : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := ⋯
⊢ Function.Bijective ⇑(Fintype.linearCombination R ⇑b ∘ₗ ↑j)

Tactic:
LinearMap.coe_comp,

Goal state after:
case refine_1
R : Type u_1
inst✝⁷ : CommSemiring R
V : Type u_2
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Module R V
A : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Algebra A R
inst✝² : Module A V
inst✝¹ : IsScalarTower A R V
ι : Type u_4
b : Module.Basis ι R V
inst✝ : Fintype ι
this : DecidableEq ι
j : R ⊗[A] (ι → A) ≃ₗ[R] ι → R := piScalarRight A R R ι
⊢ Function.Bijective (⇑(Fintype.linearCombination R ⇑b) ∘ ⇑↑j)
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
  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.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
⊢ (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) m = e0 Q * (v Q) m

Tactic:
LinearMap.coe_comp,

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
⊢ (⇑(LinearMap.mulLeft R (e0 Q)) ∘ ⇑(v Q)) m = e0 Q * (v Q) m
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
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (f x) y =
      ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q)) r) x
⊢ ↥(even (Q' Q)) →ₐ[R] CliffordAlgebra Q

Tactic:
haveI hm :
    ∀ m : M × R,
      ι Q m.1 * ι Q m.1 - algebraMap R _ m.2 * algebraMap R _ m.2 = algebraMap R _ (Q' Q m) := by
    intro m
    rw [ι_sq_scalar, ← map_mul, ← map_sub, sub_eq_add_neg, Q'_apply, sub_eq_add_neg]

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
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (f x) y =
      ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    (ι Q) m.1 * (ι Q) m.1 - (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
      (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
⊢ ↥(even (Q' Q)) →ₐ[R] CliffordAlgebra Q
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

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
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m₁ m₂ : M
⊢ (aux f) (((ι Q).bilin m₁) m₂) = (f.bilin m₁) m₂

Tactic:
rw [CliffordAlgebra.even.lift.aux_apply]
  refine (congr_arg Prod.fst (foldr_mul Q (fFold f) _ _ _ _)).trans ?_
  rw [foldr_ι, foldr_ι]
  exact mul_one _

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

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
i : Fin n
⊢ (⇑γ ∘ vM) i = b.equivFun v i

Tactic:
simp only [vM, γ, Function.comp_apply]

Goal state after:
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
i : Fin n
⊢ ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v)) (MvPolynomial.X (Sum.inr i)) = b.equivFun v i
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
⊢ (gradedComm R 𝒜 ℬ) (((gradedMul R 𝒜 ℬ) x) y) = ((gradedMul R ℬ 𝒜) ((gradedComm R 𝒜 ℬ) x)) ((gradedComm R 𝒜 ℬ) y)

Tactic:
suffices (gradedMul R 𝒜 ℬ).compr₂ (gradedComm R 𝒜 ℬ).toLinearMap
      = (gradedMul R ℬ 𝒜 ∘ₗ (gradedComm R 𝒜 ℬ).toLinearMap).compl₂
        (gradedComm R 𝒜 ℬ).toLinearMap from
    LinearMap.congr_fun₂ this x y

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
⊢ (gradedMul R 𝒜 ℬ).compr₂ ↑(gradedComm R 𝒜 ℬ) = (gradedMul R ℬ 𝒜 ∘ₗ ↑(gradedComm R 𝒜 ℬ)).compl₂ ↑(gradedComm R 𝒜 ℬ)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
⊢ ↑x ∈ pinGroup Q ↔ x ∈ lipschitzGroup Q ∧ ↑x ∈ unitary (CliffordAlgebra Q)

Tactic:
mem_iff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
⊢ ↑x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ∧
      ↑x ∈ unitary (CliffordAlgebra Q) ↔
    x ∈ lipschitzGroup Q ∧ ↑x ∈ unitary (CliffordAlgebra Q)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: 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
m : M₁ × M₂
⊢ (((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
            (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯)
          m.1 +
        ((GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
            (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯)
          m.2) *
      (((GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
            (evenOdd Q₁ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯)
          m.1 +
        ((GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘ₗ
            (evenOdd Q₂ 1).subtype ∘ₗ LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯)
          m.2) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) ((QuadraticMap.prod Q₁ Q₂) m)

Tactic:
LinearMap.coe_comp,

Goal state after:
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
m : M₁ × M₂
⊢ ((⇑(GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘
            ⇑(evenOdd Q₁ 1).subtype ∘ ⇑(LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯))
          m.1 +
        (⇑(GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘
            ⇑(evenOdd Q₂ 1).subtype ∘ ⇑(LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯))
          m.2) *
      ((⇑(GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘
            ⇑(evenOdd Q₁ 1).subtype ∘ ⇑(LinearMap.codRestrict (evenOdd Q₁ 1) (ι Q₁) ⋯))
          m.1 +
        (⇑(GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂)).toLinearMap ∘
            ⇑(evenOdd Q₂ 1).subtype ∘ ⇑(LinearMap.codRestrict (evenOdd Q₂ 1) (ι Q₂) ⋯))
          m.2) =
    (algebraMap R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)) ((QuadraticMap.prod Q₁ Q₂) m)