mathlib-initiative/mathlib-tactics huggingface dataset:
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 α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ HasFiniteIntegral f ((η ∘ₖ κ) a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ (y : γ), ‖f y‖ ∂η x) (κ a)

Tactic:
rw [hasFiniteIntegral_congr hf.ae_eq_mk, hasFiniteIntegral_comp_iff hf.stronglyMeasurable_mk]
  refine and_congr (eventually_congr ?_) (hasFiniteIntegral_congr ?_)
  · filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using
      hasFiniteIntegral_congr hx
  · filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using
      integral_congr_ae (EventuallyEq.fun_comp hx _)

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) =
    ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν

Tactic:
rw [ofReal_integral_eq_lintegral_ofReal]

Goal state after:
case pos.hfi
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν

case pos.f_nn
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔ Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
⊢ 0 ≤ᵐ[ν] fun x ↦ klFun (μ.rnDeriv ν x).toReal
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique

Goal state before:
pp: case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ∞ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ∞
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | 0 ≤ g x} ∩ s, f x ∂μ ≤ ∫ (x : α) in {x | 0 ≤ f x} ∩ s, f x ∂μ

Tactic:
← Measure.restrict_restrict (hm _ h_meas_nonneg_g),

Goal state after:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ∞ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ∞
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | 0 ≤ g x}, f x ∂μ.restrict s ≤ ∫ (x : α) in {x | 0 ≤ f x} ∩ s, f x ∂μ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: case neg.refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := (ν univ)⁻¹ • ν
hμν' : μ ≪ ν'
⊢ Integrable (llr μ ν') μ

Tactic:
rw [integrable_congr (llr_smul_right hμν (ν univ)⁻¹ (by simp) (by simp [hν]))]

Goal state after:
case neg.refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := (ν univ)⁻¹ • ν
hμν' : μ ≪ ν'
⊢ Integrable (fun x ↦ llr μ ν x - log (ν univ)⁻¹.toReal) μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
⊢ ‖↑((condExpL2 E 𝕜 hm) f)‖ ≤ ‖f‖

Tactic:
Submodule.norm_coe

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
⊢ ‖(condExpL2 E 𝕜 hm) f‖ ≤ ‖f‖
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᵐ[ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ = ν

Tactic:
refine (Measure.rnDeriv_eq_one_iff_eq h_ne.1).mp ?_

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᵐ[ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ.rnDeriv ν =ᵐ[ν] 1
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: case h
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hp : 1 ≤ ∞
h'f : ∑' (n : ι), eLpNorm (f n) ∞ μ ≠ ∞
this : ∀ᵐ (x : X) ∂μ, ∀ (n : ι), ‖f n x‖ₑ ≤ eLpNorm (f n) ∞ μ
x : X
hx : ∀ (n : ι), ‖f n x‖ₑ ≤ eLpNorm (f n) ∞ μ
i : ι
⊢ ‖f i x‖ₑ ≤ eLpNorm (f i) ∞ μ

Tactic:
exact hx i

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: case inl
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Finite ι
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)

Tactic:
let : Fintype ι := Fintype.ofFinite ι

Goal state after:
case inl
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : CompleteSpace E
f : ι → ↥(Lp E p μ)
hf : ∑' (n : ι), ‖f n‖ₑ ≠ ∞
hι : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ ∀ᵐ (a : X) ∂μ, HasSum (fun n ↦ ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_2
α : 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 α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E'
⊢ ∫ (x : α) in s, ⟪c, ↑↑↑((condExpL2 E' 𝕜 hm) f) x⟫ - ⟪c, ↑↑f x⟫ ∂μ = 0

Tactic:
integral_sub
      ((integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs).const_inner c)
      ((integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs).const_inner c)

Goal state after:
case refine_2
α : 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 α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E'
⊢ ∫ (a : α) in s, ⟪c, ↑↑↑((condExpL2 E' 𝕜 hm) f) a⟫ ∂μ - ∫ (a : α) in s, ⟪c, ↑↑f a⟫ ∂μ = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
⊢ (condExpL1CLM F' hm μ) ↑f = ↑f

Tactic:
by
  let g := lpMeasToLpTrimLie F' ℝ 1 μ hm f
  have hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g := by
    simp only [g, LinearIsometryEquiv.symm_apply_apply]
  rw [hfg]
  refine @Lp.induction α F' m _ 1 (μ.trim hm) _ ENNReal.coe_ne_top (fun g : α →₁[μ.trim hm] F' =>
    condExpL1CLM F' hm μ ((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g : α →₁[μ] F') =
    ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g)) ?_ ?_ ?_ g
  · intro c s hs hμs
    rw [@Lp.simpleFunc.coe_indicatorConst _ _ m, lpMeasToLpTrimLie_symm_indicator hs hμs.ne c,
      condExpL1CLM_indicatorConstLp]
    exact condExpInd_of_measurable hs ((le_trim hm).trans_lt hμs).ne c
  · intro f g hf hg _ hf_eq hg_eq
    rw [LinearIsometryEquiv.map_add]
    push_cast
    rw [map_add, hf_eq, hg_eq]
  · refine isClosed_eq ?_ ?_
    · refine (condExpL1CLM F' hm μ).continuous.comp (continuous_induced_dom.comp ?_)
      exact LinearIsometryEquiv.continuous _
    · refine continuous_induced_dom.comp ?_
      exact LinearIsometryEquiv.continuous _

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

Goal state before:
pp: α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᵐ[μ] 0
⊢ Nontrivial ↥(Lp F' 1 μ)

Tactic:
apply nontrivial_of_ne (hf.toL1 f) 0

Goal state after:
α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : ¬f =ᵐ[μ] 0
⊢ Integrable.toL1 f hf ≠ 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : 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‖ₑ ∂μ ≠ ∞
⊢ μ[fun a ↦ ∑' (i : ι), f i a | m] =ᵐ[μ] fun a ↦ ∑' (i : ι), μ[f i | m] a

Tactic:
by_cases hm : m ≤ m₀; swap
  · simp only [condExp_of_not_le hm, Pi.zero_apply, tsum_zero]
    exact ae_eq_rfl
  by_cases hμm : SigmaFinite (μ.trim hm); swap
  · simp only [condExp_of_not_sigmaFinite hm hμm, Pi.zero_apply, tsum_zero]
    exact ae_eq_rfl
  grw [condExp_ae_eq_condExpL1 hm]
  have A : ∀ᵐ a ∂μ, ∀ i, μ[f i | m] a = condExpL1 hm μ (f i) a :=
    ae_all_iff.2 (fun i ↦ condExp_ae_eq_condExpL1 hm _)
  have B : ∑' (n : ι), ‖condExpL1 hm μ (f n)‖ₑ ≠ ∞ := by
    apply (lt_of_le_of_lt ?_ hf'.lt_top).ne
    gcongr with i
    exact (enorm_setToFun_le _ (by simp)).trans_eq (by simp)
  have C := coeFn_tsum (f := fun i ↦ condExpL1 hm μ (f i)) B
  filter_upwards [A, C] with a ha h'a
  simp_all [condExpL1, setToFun_tsum]

Goal state after:
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f g : V →ₗ[R] V
⊢ (f ∘ₗ g).fixedSubmodule ⊓ g.fixedSubmodule ≤ f.fixedSubmodule

Tactic:
by intro; aesop

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

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

Tactic:
tmul_smul,

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ 2 • (associatedHom A) (Q₁.tmul Q₂) =
    ⅟2 • (BilinForm.tensorDistrib R A) (2 • (2 • (associatedHom A) Q₁) ⊗ₜ[R] (associatedHom R) Q₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ (contractLeft d) ((ι Q) a * b) = d a • b - (ι Q) a * (contractLeft d) b

Tactic:
by
-- Porting note: Lean cannot figure out anymore the third argument
  refine foldr'_ι_mul _ _ ?_ _ _ _
  exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ ofQuaternion.comp toQuaternion = AlgHom.id R (CliffordAlgebra (Q c₁ c₂))

Tactic:
by
  ext : 2 <;> (ext; simp)

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

Goal state before:
pp: case neg
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 ↑ι
x y : ↑ι
⊢ (b.repr (b y + f (b y) • v)) x = Matrix.diagonal (Function.update 1 i (1 + f v)) x y

Tactic:
Matrix.diagonal

Goal state after:
case neg
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 ↑ι
x y : ↑ι
⊢ (b.repr (b y + f (b y) • v)) x = Matrix.of (fun i_1 j ↦ if i_1 = j then Function.update 1 i (1 + f v) i_1 else 0) x y
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
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ ⟨(CliffordAlgebra.ι Q) (x✝² • x✝¹) * (CliffordAlgebra.ι Q) x✝, ⋯⟩ =
    x✝² • ⟨(CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) x✝, ⋯⟩

Tactic:
simp only [map_smul, smul_mul_assoc]

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
A : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ ⟨x✝² • ((CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) x✝), ⋯⟩ =
    x✝² • ⟨(CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) x✝, ⋯⟩
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: case refine_2
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 * (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) m = ↑((algebraMap R ↥(even (Q' Q))) (Q m))

Tactic:
simp [← mul_assoc, v_sq_scalar]

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

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 b : M
inst✝¹ : Invertible ((ι Q) a)
inst✝ : Invertible (Q a)
⊢ (ι Q) (⅟(Q a) • (QuadraticMap.polar (⇑Q) a b • a - Q a • b)) = (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)

Tactic:
smul_sub,

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
a b : M
inst✝¹ : Invertible ((ι Q) a)
inst✝ : Invertible (Q a)
⊢ (ι Q) (⅟(Q a) • QuadraticMap.polar (⇑Q) a b • a - ⅟(Q a) • Q a • b) =
    (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: case refine_2
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)
m₁ : M × R
⊢ ∀ (m₂ m₃ : M × R),
    ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) * ((ι Q) m₂.1 - (algebraMap R (CliffordAlgebra Q)) m₂.2) *
        (((ι Q) m₂.1 + (algebraMap R (CliffordAlgebra Q)) m₂.2) *
          ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2)) =
      (Q' Q) m₂ •
        (((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
          ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2))

Tactic:
m₂

Goal state after:
case refine_2
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)
m₁ m₂ : M × R
⊢ ∀ (m₃ : M × R),
    ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) * ((ι Q) m₂.1 - (algebraMap R (CliffordAlgebra Q)) m₂.2) *
        (((ι Q) m₂.1 + (algebraMap R (CliffordAlgebra Q)) m₂.2) *
          ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2)) =
      (Q' Q) m₂ •
        (((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
          ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2))
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
⊢ 1 * (ι Q) m = (ι Q) m

Tactic:
one_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
⊢ (ι Q) m = (ι Q) m
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 ℬ
j₁ i₂ : ι
a₁ : ⨁ (i : ι), 𝒜 i
b₁ : ℬ j₁
a₂ : 𝒜 i₂
b₂ : ⨁ (i : ι), ℬ i
⊢ (map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)))
      ((TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm
        (a₁ ⊗ₜ[R]
          (↑↑((-1) ^ (i₂ * j₁)) •
            (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i))
              ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₁) b₁ ⊗ₜ[R] b₂)))) =
    ↑↑((-1) ^ (i₂ * j₁)) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)

Tactic:
tmul_smul,

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 ℬ
j₁ i₂ : ι
a₁ : ⨁ (i : ι), 𝒜 i
b₁ : ℬ j₁
a₂ : 𝒜 i₂
b₂ : ⨁ (i : ι), ℬ i
⊢ (map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)))
      ((TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm
        (↑↑((-1) ^ (i₂ * j₁)) •
          a₁ ⊗ₜ[R]
            (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i))
              ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] (lof R ι ℬ j₁) b₁ ⊗ₜ[R] b₂))) =
    ↑↑((-1) ^ (i₂ * j₁)) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: case e'_3
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 ℤˣ)
i₂ : ι
a₁ : A
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ b₂ = 1 * b₂

Tactic:
one_mul

Goal state after:
case e'_3
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 ℤˣ)
i₂ : ι
a₁ : A
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ b₂ = b₂
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: case e'_3.e'_17
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 ℤˣ)
a₁ : A
b₂ : B
⊢ b₂ = 1 * b₂

Tactic:
one_mul

Goal state after:
case e'_3.e'_17
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 ℤˣ)
a₁ : A
b₂ : B
⊢ b₂ = b₂
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: case e_f
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 ℤˣ)
a₁ a₂ : A
i : ι
⊢ (of R 𝒜 ℬ) ((a₁ * ↑(((decompose 𝒜) a₂) i)) ⊗ₜ[R] 1) = (a₁ * ↑(((decompose 𝒜) a₂) i)) ᵍ⊗ₜ[R] (1 * 1)

Tactic:
one_mul

Goal state after:
case e_f
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 ℤˣ)
a₁ a₂ : A
i : ι
⊢ (of R 𝒜 ℬ) ((a₁ * ↑(((decompose 𝒜) a₂) i)) ⊗ₜ[R] 1) = (a₁ * ↑(((decompose 𝒜) a₂) i)) ᵍ⊗ₜ[R] 1