mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ ∑' (i : ι), eLpNorm (f i) p (μ.restrict s) < ∞

pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ (μ.restrict s) Set.univ ^ (1 / ENNReal.toReal 1 - 1 / p.toReal) < ∞

Tactic:
· apply lt_of_le_of_lt ?_ h'f.lt_top
        gcongr
        exact Measure.restrict_le_self

Goal state after:
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ (μ.restrict s) Set.univ ^ (1 / ENNReal.toReal 1 - 1 / p.toReal) < ∞
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
hf : ¬Integrable f μ
hm : ¬m ≤ m₀
⊢ μ[f | m] = 0

pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
⊢ μ[f | m] = 0

Tactic:
· rw [condExp_of_not_le hm]

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : ¬m ≤ m₀
⊢ μ[0 | m] = 0

pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ m₀
⊢ μ[0 | m] = 0

Tactic:
· rw [condExp_of_not_le hm]

Goal state after:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ m₀
⊢ μ[0 | m] = 0
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 : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
h_zero1 : ¬((∂μ/∂ν) p.1).toReal = 0
h_zero2 : ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
simp [h_zero2]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
⊢ μ[f | ⊥] =ᵐ[μ] fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ
  · rw [ae_zero]; exact eventually_bot
  · exact Eventually.of_forall <| congr_fun (condExp_bot' f)

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

Goal state before:
pp: case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f
hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g
⊢ ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 (μ.trim hm)) (hg : MemLp g 1 (μ.trim hm)),
    Disjoint (Function.support f) (Function.support g) →
      (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) =
          ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) →
        (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) =
            ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) →
          (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg)) =
            ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg))

Tactic:
intro f g hf hg _ hf_eq hg_eq

Goal state after:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
f✝ : ↥(lpMeas F' ℝ m 1 μ)
g✝ : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm) f✝
hfg : f✝ = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g✝
f g : α → F'
hf : MemLp f 1 (μ.trim hm)
hg : MemLp g 1 (μ.trim hm)
a✝ : Disjoint (Function.support f) (Function.support g)
hf_eq :
  (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf)) =
    ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf))
hg_eq :
  (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg)) =
    ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp g hg))
⊢ (condExpL1CLM F' hm μ) ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg)) =
    ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm (MemLp.toLp f hf + MemLp.toLp g hg))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
A : μ[fun x ↦ (ENNReal.ofReal (f x)).toReal | m] =ᵐ[μ] μ[f | m]
B : 0 ≤ᵐ[μ] μ[f | m]
g : 𝓧 → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (f x)
⊢ ∫⁻ (x : 𝓧), g x ∂μ = ∫⁻ (x : 𝓧), ‖f x‖ₑ ∂μ

Tactic:
apply lintegral_congr_ae

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
A : μ[fun x ↦ (ENNReal.ofReal (f x)).toReal | m] =ᵐ[μ] μ[f | m]
B : 0 ≤ᵐ[μ] μ[f | m]
g : 𝓧 → ℝ≥0∞ := ⋯
⊢ g =ᵐ[μ] fun a ↦ ‖f a‖ₑ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
hm : m ≤ m𝓧
μ : Measure 𝓧
inst✝ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ ∫⁻ (a : 𝓧), ‖μ[s.indicator 1 | m] a‖ₑ ∂μ = ∫⁻ (a : 𝓧), μ⁻[fun x ↦ ‖s.indicator 1 x‖ₑ | m] a ∂μ

Tactic:
apply lintegral_congr_ae

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
hm : m ≤ m𝓧
μ : Measure 𝓧
inst✝ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ (fun a ↦ ‖μ[s.indicator 1 | m] a‖ₑ) =ᵐ[μ] μ⁻[fun x ↦ ‖s.indicator 1 x‖ₑ | m]
Module: Mathlib.LinearAlgebra.Basis.Flag

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
n : ℕ
inst✝ : Nontrivial R
b : Basis (Fin n) R M
k : Fin (n + 1)
l : Fin n
⊢ b.flag k ≤ (b.coord l).ker ↔ k ≤ l.castSucc

Tactic:
by
  simp [flag_le_iff, Finsupp.single_apply_eq_zero, imp_false, imp_not_comm]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
V : Type u_3
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module R V
W : Type u_4
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module S W
inst✝ : IsScalarTower R S W
ι : Type u_5
ε : V →ₗ[R] W
b : Module.Basis ι R V
ibc : IsBaseChange S ε
v : V
⊢ (basis b ibc).repr (ε v) = (Finsupp.mapRange.linearMap (Algebra.linearMap R S)) (b.repr v)

Tactic:
ext i
  simp [basis_repr_comp_apply]

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
j : ι
hj : j ≠ i
t : Finset ι
w' : ι → k
ht✝ : ↑t ⊆ {i}ᶜ
hw' : ∑ i ∈ t, w' i = 1
hqmem : (affineCombination k t p) w' ∈ affineSpan k (p '' {i}ᶜ)
heq : (1 - c) • (p i -ᵥ p j) +ᵥ (affineCombination k t p) w' = (affineCombination k univ p) w
ht : (↑t).indicator w' i = 0
⊢ w i = 1 - c

Tactic:
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

Goal state after:
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
j : ι
hj : j ≠ i
t : Finset ι
w' : ι → k
ht✝ : ↑t ⊆ {i}ᶜ
hw' : ∑ i ∈ t, w' i = 1
hqmem : (affineCombination k t p) w' ∈ affineSpan k (p '' {i}ᶜ)
heq : ∀ i_1 ∈ univ, ((1 - c) • (Pi.single i 1 - Pi.single j 1) + (↑t).indicator w') i_1 = w i_1
ht : (↑t).indicator w' i = 0
⊢ w i = 1 - c

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
j : ι
hj : j ≠ i
t : Finset ι
w' : ι → k
ht✝ : ↑t ⊆ {i}ᶜ
hw' : ∑ i ∈ t, w' i = 1
hqmem : (affineCombination k t p) w' ∈ affineSpan k (p '' {i}ᶜ)
heq :
  (affineCombination k univ p) ((1 - c) • (Pi.single i 1 - Pi.single j 1) + (↑t).indicator w') =
    (affineCombination k univ p) w
ht : (↑t).indicator w' i = 0
⊢ ∑ i_1, ((1 - c) • (Pi.single i 1 - Pi.single j 1) + (↑t).indicator w') i_1 = 1
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, e y = y
x✝ : v ∈ map (↑e) W
w : V
hv : w ∈ ↑W
hv' : ↑e w = v
⊢ v ∈ W

Tactic:
simp only [SetLike.mem_coe, coe_coe] at hv hv'

Goal state after:
case refine_1
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, e y = y
x✝ : v ∈ map (↑e) W
w : V
hv' : e w = v
hv : w ∈ W
⊢ v ∈ W
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ f x * ↑(-h.unit⁻¹) + (f x + f x * ↑(-h.unit⁻¹) * f v) = 0

Tactic:
← mul_one (f x)

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ f x * ↑(-h.unit⁻¹) + (f x * 1 + f x * ↑(-h.unit⁻¹) * f v) = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case h
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = ↑e
hr : Module.rank K ↥u.range = 0
x : V
⊢ u x = 0

Tactic:
rw [rank_zero_iff] at hr

Goal state after:
case h
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u + LinearMap.id = ↑e
hr : Subsingleton ↥u.range
x : V
⊢ u x = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case refine_1.left
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 ∈ dilatransvections K V

Tactic:
he

Goal state after:
case refine_1.left
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
⊢ transvection hfv ∈ dilatransvections K V
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
⊢ ∀ (v : V), e v - v ∈ (↑e).fixedSubmodule

Tactic:
he

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
⊢ ∀ (v_1 : V), (transvection hfv) v_1 - v_1 ∈ (↑(transvection hfv)).fixedSubmodule
Module: Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ (↑R (ι (QuadraticForm.baseChange A Q)) ∘ₗ (TensorProduct.mk R A V) 1) v *
      (↑R (ι (QuadraticForm.baseChange A Q)) ∘ₗ (TensorProduct.mk R A V) 1) v =
    (algebraMap R (CliffordAlgebra (QuadraticForm.baseChange A Q))) (Q v)

Tactic:
refine (CliffordAlgebra.ι_sq_scalar (Q.baseChange A) (1 ⊗ₜ v)).trans ?_

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) ((QuadraticForm.baseChange A Q) (1 ⊗ₜ[R] v)) =
    (algebraMap R (CliffordAlgebra (QuadraticForm.baseChange A Q))) (Q v)
Module: Mathlib.LinearAlgebra.Transvection.Basic

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

Tactic:
← Nat.add_le_add_iff_right,

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

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

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ (toBaseChange A Q) (-(ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)) =
    (Algebra.TensorProduct.map (AlgHom.id A A) involute) (1 ⊗ₜ[R] (ι Q) v)

Tactic:
map_neg (toBaseChange A Q),

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
v : V
⊢ -(toBaseChange A Q) ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)) =
    (Algebra.TensorProduct.map (AlgHom.id A A) involute) (1 ⊗ₜ[R] (ι Q) v)
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case smul
R : Type u_3
V : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
A : Type u_5
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
W : Type u_6
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module A W
inst✝ : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
a : A
w : W
hw : (ibc.endHom (LinearMap.transvection f v)) w = (LinearMap.transvection (ibc.toDual f) (ε v)) w
⊢ (ibc.endHom (LinearMap.transvection f v)) (a • w) = (LinearMap.transvection (ibc.toDual f) (ε v)) (a • w)

Tactic:
simp [hw]

Goal state after:
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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x : CliffordAlgebra Q'
⊢ (changeForm h) ((changeForm ⋯) x) = x

Tactic:
exact (changeForm_changeForm _ _ x).trans <|
        by simp_rw [(neg_add_cancel B), changeForm_self_apply]

Goal state after:
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 × 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))

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₃ : 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.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 ℤˣ)
a₁ : A
b₂ : B
⊢ a₁ ᵍ⊗ₜ[R] 1 * 1 ᵍ⊗ₜ[R] b₂ = a₁ ᵍ⊗ₜ[R] b₂

Tactic:
convert!
    tmul_coe_mul_zero_coe_tmul 𝒜 ℬ a₁ (GradedMonoid.GOne.one (A := (ℬ ·)))
      (GradedMonoid.GOne.one (A := (𝒜 ·))) b₂

Goal state after:
case e'_3.e'_16
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
⊢ a₁ = a₁ * ↑GradedMonoid.GOne.one

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₂ = ↑GradedMonoid.GOne.one * b₂
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x ↦ a.elim0)) []).prod =
    GradedMonoid.mk 0 ((PiTensorProduct.tprod R) Fin.elim0)

Tactic:
List.map_nil,

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ [].prod = GradedMonoid.mk 0 ((PiTensorProduct.tprod R) Fin.elim0)