mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsFiniteMeasure μ
hm : m ≤ m₀
hf_int : Integrable f μ
T : E →L[ℝ] F
a : F
⊢ (fun x ↦ T (μ[f | m] x) + a) =ᵐ[μ] μ[fun y ↦ T (f y) + a | m]

Tactic:
have hp : (fun x ↦ T (μ[f | m] x) + a) =ᵐ[μ] μ[T ∘ f | m] + μ[(fun y ↦ a) | m] := by
    filter_upwards [T.comp_condExp_comm hf_int] with b hb
    simpa [condExp_const hm a]

Goal state after:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ F
inst✝ : IsFiniteMeasure μ
hm : m ≤ m₀
hf_int : Integrable f μ
T : E →L[ℝ] F
a : F
hp : (fun x ↦ T (μ[f | m] x) + a) =ᵐ[μ] μ[⇑T ∘ f | m] + μ[fun y ↦ a | m]
⊢ (fun x ↦ T (μ[f | m] x) + a) =ᵐ[μ] μ[fun y ↦ T (f y) + a | m]
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
inst✝ : NeZero P
X : Ω → ℝ≥0∞
hP : ¬IsFiniteMeasure P
⊢ ¬SigmaFinite (P.trim ⋯)

Tactic:
rwa [sigmaFinite_trim_bot_iff]

Goal state after:
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
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : 0 ≤ᵐ[μ] f
hfint : ¬Integrable f μ
⊢ 0 ≤ᵐ[μ] μ[f | m]

Tactic:
condExp_of_not_integrable hfint

Goal state after:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : 0 ≤ᵐ[μ] f
hfint : ¬Integrable f μ
⊢ 0 ≤ᵐ[μ] 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
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : f ≤ᵐ[μ] 0
hfint : ¬Integrable f μ
⊢ μ[f | m] ≤ᵐ[μ] 0

Tactic:
condExp_of_not_integrable hfint

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

Goal state before:
pp: case refine_3
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) μ
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
φY : ↥Y → ℝ := φ ∘ ⇑Y.subtypeL
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
hfY_int : Integrable fY μ
lem2 : μ[f | m] =ᵐ[μ] ⇑Y.subtypeL ∘ μ[fY | m]
lem3 : φ ∘ f =ᵐ[μ] φY ∘ fY
⊢ IsClosed (⇑Y.subtypeL ⁻¹' s)

Tactic:
exact hs.preimage Y.subtypeL.continuous

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 ε
i : ι
pf✝³ : RingHomInvPair (RingHom.id S) (RingHom.id S)
pf✝² : SMulCommClass R S S
pf✝¹ : IsScalarTower R S S
pf✝ : IsScalarTower R S (ι →₀ S)
ibcRA : IsBaseChange S (Finsupp.mapRange.linearMap (Algebra.linearMap R S))
⊢ ibcRA.equiv.symm (Finsupp.single i 1) = 1 ⊗ₜ[R] Finsupp.single i 1

Tactic:
simp [LinearEquiv.symm_apply_eq, IsBaseChange.equiv_tmul]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
h : AffineIndependent k p
i : ι
w : ι → k
hw : ∑ i, w i = 1
c : k
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) c ↔ w i = 1 - c

Tactic:
refine ⟨?_, fun h ↦ by simpa [h] using affineCombination_mem_shift p i hw⟩
  obtain ⟨j, hj⟩ := exists_ne i
  rw [shift_eq ⟨p j, mem_affineSpan k <| Set.mem_image_of_mem _ hj⟩]
  suffices ∀ q ∈ affineSpan k (p '' {i}ᶜ),
    (1 - c) • (p i -ᵥ p j) +ᵥ q = affineCombination k univ p w → w i = 1 - c by simpa
  intro q hqmem heq
  obtain ⟨t, w', ht, hw', rfl⟩ := eq_affineCombination_of_mem_affineSpan_image hqmem
  have ht : (t : Set ι).indicator w' i = 0 := Set.indicator_of_notMem (by simpa using ht) w'
  rw [affineCombination_indicator_subset _ _ t.subset_univ,
    ← affineCombination_piSingle k _ p (mem_univ i),
    ← affineCombination_piSingle k _ p (mem_univ j), affineCombination_vsub, ← map_smul,
    weightedVSub_vadd_affineCombination, h.affineCombination_eq_iff_eq ?_ hw] at heq
  · simpa [hj.symm, ht] using (heq i (mem_univ i)).symm
  · simp [sum_add_distrib, sum_indicator_subset, ← mul_sum, hw']

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : IsOrderedAddMonoid k
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Module k V
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x < 0 ∨ 1 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hleft : (affineCombination k univ s.points) w ∈ s.closedInterior
hright : w i = 1 - x
⊢ False

Tactic:
rw [affineCombination_mem_closedInterior_iff hw] at hleft

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : IsOrderedAddMonoid k
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Module k V
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x < 0 ∨ 1 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hleft : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hright : w i = 1 - x
⊢ False
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
V : Type u_2
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
W : Type u_3
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module R W
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A W
inst✝² : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst✝¹ : Free R V
inst✝ : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A ((Algebra.linearMap R A).compLeft ι)
⊢ ibc.toDualBaseChangeAux =
    ↑(LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (b.constr R).symm ≪≫ₗ ibc_pow.equiv ≪≫ₗ (basis b ibc).constr A)

Tactic:
ext f w

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
V : Type u_2
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
W : Type u_3
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module R W
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A W
inst✝² : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst✝¹ : Free R V
inst✝ : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A ((Algebra.linearMap R A).compLeft ι)
f : Dual R V
w : W
⊢ (((AlgebraTensorModule.curry ibc.toDualBaseChangeAux) 1) f) w =
    (((AlgebraTensorModule.curry
            ↑(LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (b.constr R).symm ≪≫ₗ ibc_pow.equiv ≪≫ₗ
                (basis b ibc).constr A))
          1)
        f)
      w
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: case tmul
R : Type u_1
inst✝¹⁰ : CommSemiring R
V : Type u_2
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
W : Type u_3
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module R W
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A W
inst✝² : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst✝¹ : Free R V
inst✝ : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A ((Algebra.linearMap R A).compLeft ι)
f : Dual R V
v : V
⊢ (ibc.toDualBaseChangeAux (1 ⊗ₜ[R] f)) (j v) =
    (((basis b ibc).constr A)
        (ibc_pow.equiv ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (b.constr R).symm) (1 ⊗ₜ[R] f))))
      (j v)

Tactic:
simp only [toDualBaseChangeAux_tmul, one_mul]

Goal state after:
case tmul
R : Type u_1
inst✝¹⁰ : CommSemiring R
V : Type u_2
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
W : Type u_3
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module R W
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A W
inst✝² : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst✝¹ : Free R V
inst✝ : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A ((Algebra.linearMap R A).compLeft ι)
f : Dual R V
v : V
⊢ (algebraMap R A) (f v) =
    (((basis b ibc).constr A)
        (ibc_pow.equiv ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (b.constr R).symm) (1 ⊗ₜ[R] f))))
      (j v)
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
⊢ ((algebraMap R S).mapMatrix ((toMatrix b b) f)).det = (algebraMap R S) ((toMatrix b b) f).det

Tactic:
← RingHom.map_det

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) ((toMatrix b b) f).det = (algebraMap R S) ((toMatrix b b) f).det
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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
feq : ∀ (i j : ι), f (b j) = (b.coord i) (f (b i)) • b j
i : ι := Classical.ofNonempty
ha : ∀ (r : R), Commute ((b.coord i) (f (b i))) r
⊢ ∃ a, f = a • 1

Tactic:
refine ⟨⟨b.coord i (f (b i)), ?_⟩, ?_⟩

Goal state after:
case refine_1
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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
feq : ∀ (i j : ι), f (b j) = (b.coord i) (f (b i)) • b j
i : ι := Classical.ofNonempty
ha : ∀ (r : R), Commute ((b.coord i) (f (b i))) r
⊢ (b.coord i) (f (b i)) ∈ Subring.center R

case refine_2
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
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
feq : ∀ (i j : ι), f (b j) = (b.coord i) (f (b i)) • b j
i : ι := Classical.ofNonempty
ha : ∀ (r : R), Commute ((b.coord i) (f (b i))) r
⊢ f = ⟨(b.coord i) (f (b i)), ?refine_1⟩ • 1
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case refine_1.right
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 ∈ transvections K V
f : Dual K V
v : V
hfv : f v = 0
he : e = transvection hfv
⊢ e.fixedReduce = 1

Tactic:
one_eq_refl,

Goal state after:
case refine_1.right
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 ∈ transvections K V
f : Dual K V
v : V
hfv : f v = 0
he : e = transvection hfv
⊢ e.fixedReduce = refl K (V ⧸ (↑e).fixedSubmodule)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case algebraMap
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
r✝ : R
⊢ r✝ • 0 = r✝ • 0 + r✝ • 0

Tactic:
smul_zero,

Goal state after:
case algebraMap
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
r✝ : R
⊢ 0 = 0 + 0
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 : CliffordAlgebra Q
r : R
⊢ (algebraMap R (CliffordAlgebra Q)) r * (contractLeft d) a = (contractLeft d) a * (algebraMap R (CliffordAlgebra Q)) r

Tactic:
Algebra.commutes

Goal state after:
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 : CliffordAlgebra Q
r : R
⊢ (contractLeft d) a * (algebraMap R (CliffordAlgebra Q)) r = (contractLeft d) a * (algebraMap R (CliffordAlgebra Q)) r
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 : CliffordAlgebra Q
r : R
⊢ (algebraMap R (CliffordAlgebra Q)) r * (contractRight a) d =
    (contractRight a) d * (algebraMap R (CliffordAlgebra Q)) r

Tactic:
Algebra.commutes

Goal state after:
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 : CliffordAlgebra Q
r : R
⊢ (contractRight a) d * (algebraMap R (CliffordAlgebra Q)) r =
    (contractRight a) d * (algebraMap R (CliffordAlgebra 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 : QuadraticForm R M
m : M
r : R
⊢ (ι (Q' Q)) (m, r) = (ι (Q' Q)) (m, 0) + (ι (Q' Q)) (r • 0, r • 1)

Tactic:
smul_zero,

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
r : R
⊢ (ι (Q' Q)) (m, r) = (ι (Q' Q)) (m, 0) + (ι (Q' Q)) (0, r • 1)
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 : ↑ι
⊢ (toMatrix b b) (transvection f v) x y = Matrix.diagonal (Function.update 1 i (1 + f v)) x y

Tactic:
rw [toMatrix_apply, transvection.apply, 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.EvenEquiv

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ M →ₗ[R] ↥(even (Q' Q))

Tactic:
refine LinearMap.codRestrict _ ?_ fun m => Submodule.mem_iSup_of_mem ⟨2, rfl⟩ ?_
    · exact (LinearMap.mulLeft R <| e0 Q).comp (v Q)
    rw [Subtype.coe_mk, pow_two]
    exact Submodule.mul_mem_mul (LinearMap.mem_range_self _ _) (LinearMap.mem_range_self _ _)

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
⊢ ↑((toEven Q) ((ι Q) m)) = e0 Q * (v Q) m

Tactic:
simp only [toEven, CliffordAlgebra.lift_ι_apply, ← even_toSubmodule]
  rw [LinearMap.codRestrict_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.mulLeft_apply]

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
f : Dual R V
v : V
hfv : f v = 0
⊢ LinearEquiv.det (LinearEquiv.transvection hfv) = 1

Tactic:
← Units.val_inj,

Goal state after:
R : Type u_3
V : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
hfv : f v = 0
⊢ ↑(LinearEquiv.det (LinearEquiv.transvection hfv)) = ↑1
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₂ 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:
· intro m₁ m₂ m₃
    rw [← mul_smul_comm, ← mul_assoc, mul_assoc (_ + _), ← (hc _ _).symm.mul_self_sub_mul_self_eq',
      Algebra.smul_def, ← mul_assoc, hm]

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

Goal state before:
pp: case mem.algebraMap
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 : ℕ
r✝ : R
⊢ (algebraMap R (CliffordAlgebra Qₙ)) r✝ * (map f₂) m₂ = (map f₂) m₂ * (algebraMap R (CliffordAlgebra Qₙ)) r✝

Tactic:
Algebra.commutes

Goal state after:
case mem.algebraMap
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 : ℕ
r✝ : R
⊢ (map f₂) m₂ * (algebraMap R (CliffordAlgebra Qₙ)) r✝ = (map f₂) m₂ * (algebraMap R (CliffordAlgebra Qₙ)) r✝
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 : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
i✝¹ : ι
x✝¹ : 𝒜 i✝¹
i✝ : ι
x✝ : ℬ i✝
⊢ ((lof R ι 𝒜 i✝¹) x✝¹ * (lof R ι 𝒜 0) (DirectSum.GAlgebra.toFun r)) ⊗ₜ[R] (lof R ι ℬ i✝) x✝ =
    ((algebraMap R (⨁ (i : ι), 𝒜 i)) r * (lof R ι 𝒜 i✝¹) x✝¹) ⊗ₜ[R] (lof R ι ℬ i✝) x✝

Tactic:
Algebra.commutes

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 : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
i✝¹ : ι
x✝¹ : 𝒜 i✝¹
i✝ : ι
x✝ : ℬ i✝
⊢ ((lof R ι 𝒜 i✝¹) x✝¹ * (lof R ι 𝒜 0) (DirectSum.GAlgebra.toFun r)) ⊗ₜ[R] (lof R ι ℬ i✝) x✝ =
    ((lof R ι 𝒜 i✝¹) x✝¹ * (algebraMap R (⨁ (i : ι), 𝒜 i)) r) ⊗ₜ[R] (lof R ι ℬ i✝) x✝
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.mem_mul.e_a.e_a.mem.algebraMap
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 : ℕ
r✝ : R
⊢ (ι Qₙ) (f₁ v₁) * (algebraMap R (CliffordAlgebra Qₙ)) r✝ = (algebraMap R (CliffordAlgebra Qₙ)) r✝ * (ι Qₙ) (f₁ v₁)

Tactic:
Algebra.commutes

Goal state after:
case mem.mem_mul.e_a.e_a.mem.algebraMap
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 : ℕ
r✝ : R
⊢ (ι Qₙ) (f₁ v₁) * (algebraMap R (CliffordAlgebra Qₙ)) r✝ = (ι Qₙ) (f₁ v₁) * (algebraMap R (CliffordAlgebra Qₙ)) r✝