mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)
a : A
m : M₂
⊢ Q₁ ((a • 1) ⊗ₜ[R] m) = Q₂ ((a • 1) ⊗ₜ[R] m)

Tactic:
← smul_tmul',

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)
a : A
m : M₂
⊢ Q₁ (a • 1 ⊗ₜ[R] m) = Q₂ (a • 1 ⊗ₜ[R] m)
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: 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 = ⊥
⊢ finrank K V = 1 + finrank K ↥(ker f)

Tactic:
rw [← f.finrank_ker_add_one_of_ne_zero, add_comm]

Goal state after:
case hf
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 = ⊥
⊢ f ≠ 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
v : M
x fx : CliffordAlgebra Q
⊢ d v • ((ι Q) v * x) - ((ι Q) v * d v • x - (ι Q) v * (ι Q) v * fx) = Q v • fx

Tactic:
ι_sq_scalar,

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
v : M
x fx : CliffordAlgebra Q
⊢ d v • ((ι Q) v * x) - ((ι Q) v * d v • x - (algebraMap R (CliffordAlgebra Q)) (Q v) * fx) = Q v • fx
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case pos
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
hv : v = 0
⊢ LinearMap.det (transvection f v) = 1 + f v

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
hv : ¬v = 0
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
· simp [hv]

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
hv : ¬v = 0
⊢ LinearMap.det (transvection f v) = 1 + f v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (ι (Q c₁ c₂)) (1, 0) * (ι (Q c₁ c₂)) (1, 0) = c₁ • 1 + 0 • (ι (Q c₁ c₂)) (1, 0)

Tactic:
ι_sq_scalar,

Goal state after:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) ((Q c₁ c₂) (1, 0)) = c₁ • 1 + 0 • (ι (Q c₁ c₂)) (1, 0)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (ι (Q c₁ c₂)) (0, 1) * (ι (Q c₁ c₂)) (0, 1) = c₂ • 1

Tactic:
ι_sq_scalar,

Goal state after:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) ((Q c₁ c₂) (0, 1)) = c₂ • 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r₁ r₂ : R
⊢ (r₁ * r₂) • ((ι 0) 1 * (ι 0) 1) = 0

Tactic:
ι_sq_scalar,

Goal state after:
R : Type u_1
inst✝ : CommRing R
r₁ r₂ : R
⊢ (r₁ * r₂) • (algebraMap R (CliffordAlgebra 0)) (0 1) = 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
B : BilinForm R M
v : M
x : CliffordAlgebra Q
⊢ (ι Q) v * (ι Q) v * x - (ι Q) v * (contractLeft (B v)) x -
      (contractLeft (B v)) ((ι Q) v * x - (contractLeft (B v)) x) =
    (Q v - (B v) v) • x

Tactic:
ι_sq_scalar,

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
B : BilinForm R M
v : M
x : CliffordAlgebra Q
⊢ (algebraMap R (CliffordAlgebra Q)) (Q v) * x - (ι Q) v * (contractLeft (B v)) x -
      (contractLeft (B v)) ((ι Q) v * x - (contractLeft (B v)) x) =
    (Q v - (B v) v) • x
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
m₁ m₂ m₃ : M
⊢ (CliffordAlgebra.ι Q) m₁ * ((CliffordAlgebra.ι Q) m₂ * (CliffordAlgebra.ι Q) m₂ * (CliffordAlgebra.ι Q) m₃) =
    (algebraMap R (CliffordAlgebra Q)) (Q m₂) * ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₃)

Tactic:
ι_sq_scalar,

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
m₁ m₂ m₃ : M
⊢ (CliffordAlgebra.ι Q) m₁ * ((algebraMap R (CliffordAlgebra Q)) (Q m₂) * (CliffordAlgebra.ι Q) m₃) =
    (algebraMap R (CliffordAlgebra Q)) (Q m₂) * ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι 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
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)

Tactic:
ι_sq_scalar,

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
m : M × R
⊢ (algebraMap R (CliffordAlgebra Q)) (Q m.1) -
      (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
    (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: case snd.refine_4
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
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
⊢ ∀ (a : R),
    ∀ x ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)},
      (f.bilin m₁) m * x m = Q m • x m₁ → (f.bilin m₁) m * (a • x) m = Q m • (a • x) m₁

Tactic:
rintro x hx _c ihx

Goal state after:
case snd.refine_4
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
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
x : R
hx : M →ₗ[R] A
_c : hx ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
ihx : (f.bilin m₁) m * hx m = Q m • hx m₁
⊢ (f.bilin m₁) m * (x • hx) m = Q m • (x • hx) m₁
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
m : M
inst✝ : Invertible (Q m)
⊢ ⅟(Q m) • ((ι Q) m * (ι Q) m) = 1

Tactic:
ι_sq_scalar,

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
inst✝ : Invertible (Q m)
⊢ ⅟(Q m) • (algebraMap R (CliffordAlgebra Q)) (Q m) = 1
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
m : M
inst✝ : Invertible (Q m)
⊢ (ι Q) (⅟(Q m) • m) * (ι Q) m = 1

Tactic:
by
    rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]

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

Goal state before:
pp: case add
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₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
x✝ y✝ : CliffordAlgebra Q₁
hx✝ : x✝ ∈ ⨆ i, (ι Q₁).range ^ ↑i
hy✝ : y✝ ∈ ⨆ i, (ι Q₁).range ^ ↑i
ihx : (map f₁) x✝ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) x✝)
ihy : (map f₁) y✝ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) y✝)
⊢ (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) x✝) + (map f₁) y✝ * (map f₂) m₂ =
    (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) x✝ + (map f₂) m₂ * (map f₁) y✝)

Tactic:
ihy,

Goal state after:
case add
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₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
x✝ y✝ : CliffordAlgebra Q₁
hx✝ : x✝ ∈ ⨆ i, (ι Q₁).range ^ ↑i
hy✝ : y✝ ∈ ⨆ i, (ι Q₁).range ^ ↑i
ihx : (map f₁) x✝ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) x✝)
ihy : (map f₁) y✝ * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) y✝)
⊢ (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) x✝) + (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) y✝) =
    (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) x✝ + (map f₂) m₂ * (map f₁) y✝)
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]
          (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i))
            ((↑↑((-1) ^ (i₂ * j₁)) • (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:
← smul_tmul',

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
        (a₁ ⊗ₜ[R]
          (TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i))
            (↑↑((-1) ^ (i₂ * j₁)) • (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.CliffordAlgebra.Prod

Goal state before:
pp: case mem.add
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 : ℕ
x✝ y✝ : CliffordAlgebra Q₁
i✝ : ℕ
hx✝ : x✝ ∈ (ι Q₁).range ^ i✝
hy✝ : y✝ ∈ (ι Q₁).range ^ i✝
ihx : (map f₁) x✝ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) x✝)
ihy : (map f₁) y✝ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) y✝)
⊢ (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) x✝) + (map f₁) y✝ * (map f₂) m₂ =
    (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) x✝ + (map f₂) m₂ * (map f₁) y✝)

Tactic:
ihy,

Goal state after:
case mem.add
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 : ℕ
x✝ y✝ : CliffordAlgebra Q₁
i✝ : ℕ
hx✝ : x✝ ∈ (ι Q₁).range ^ i✝
hy✝ : y✝ ∈ (ι Q₁).range ^ i✝
ihx : (map f₁) x✝ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) x✝)
ihy : (map f₁) y✝ * (map f₂) m₂ = (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) y✝)
⊢ (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) x✝) + (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) y✝) =
    (-1) ^ (i₂ * ↑i✝) • ((map f₂) m₂ * (map f₁) x✝ + (map f₂) m₂ * (map f₁) y✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.mem_mul.e_a.e_a.add
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
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
x✝ y✝ : CliffordAlgebra Q₂
hx✝ : x✝ ∈ ⨆ i, (ι Q₂).range ^ ↑i
hy✝ : y✝ ∈ ⨆ i, (ι Q₂).range ^ ↑i
ihx : (ι Qₙ) (f₁ v₁) * (map f₂) x✝ = (-1) ^ i₂ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁))
ihy : (ι Qₙ) (f₁ v₁) * (map f₂) y✝ = (-1) ^ i₂ • ((map f₂) y✝ * (ι Qₙ) (f₁ v₁))
⊢ (-1) ^ i₂ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁)) + (ι Qₙ) (f₁ v₁) * (map f₂) y✝ =
    (-1) ^ i₂ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁) + (map f₂) y✝ * (ι Qₙ) (f₁ v₁))

Tactic:
ihy,

Goal state after:
case mem.mem_mul.e_a.e_a.add
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
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
x✝ y✝ : CliffordAlgebra Q₂
hx✝ : x✝ ∈ ⨆ i, (ι Q₂).range ^ ↑i
hy✝ : y✝ ∈ ⨆ i, (ι Q₂).range ^ ↑i
ihx : (ι Qₙ) (f₁ v₁) * (map f₂) x✝ = (-1) ^ i₂ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁))
ihy : (ι Qₙ) (f₁ v₁) * (map f₂) y✝ = (-1) ^ i₂ • ((map f₂) y✝ * (ι Qₙ) (f₁ v₁))
⊢ (-1) ^ i₂ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁)) + (-1) ^ i₂ • ((map f₂) y✝ * (ι Qₙ) (f₁ v₁)) =
    (-1) ^ i₂ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁) + (map f₂) y✝ * (ι Qₙ) (f₁ v₁))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem.mem_mul.e_a.e_a.mem.add
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 : ℕ
x✝ y✝ : CliffordAlgebra Q₂
i✝ : ℕ
hx✝ : x✝ ∈ (ι Q₂).range ^ i✝
hy✝ : y✝ ∈ (ι Q₂).range ^ i✝
ihx : (ι Qₙ) (f₁ v₁) * (map f₂) x✝ = (-1) ^ ↑i✝ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁))
ihy : (ι Qₙ) (f₁ v₁) * (map f₂) y✝ = (-1) ^ ↑i✝ • ((map f₂) y✝ * (ι Qₙ) (f₁ v₁))
⊢ (-1) ^ ↑i✝ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁)) + (ι Qₙ) (f₁ v₁) * (map f₂) y✝ =
    (-1) ^ ↑i✝ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁) + (map f₂) y✝ * (ι Qₙ) (f₁ v₁))

Tactic:
ihy,

Goal state after:
case mem.mem_mul.e_a.e_a.mem.add
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 : ℕ
x✝ y✝ : CliffordAlgebra Q₂
i✝ : ℕ
hx✝ : x✝ ∈ (ι Q₂).range ^ i✝
hy✝ : y✝ ∈ (ι Q₂).range ^ i✝
ihx : (ι Qₙ) (f₁ v₁) * (map f₂) x✝ = (-1) ^ ↑i✝ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁))
ihy : (ι Qₙ) (f₁ v₁) * (map f₂) y✝ = (-1) ^ ↑i✝ • ((map f₂) y✝ * (ι Qₙ) (f₁ v₁))
⊢ (-1) ^ ↑i✝ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁)) + (-1) ^ ↑i✝ • ((map f₂) y✝ * (ι Qₙ) (f₁ v₁)) =
    (-1) ^ ↑i✝ • ((map f₂) x✝ * (ι Qₙ) (f₁ v₁) + (map f₂) y✝ * (ι Qₙ) (f₁ v₁))
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₂
⊢ ((ι Q₁) m.1 * (ι Q₁) m.1) ᵍ⊗ₜ[R] 1 + (ι Q₁) m.1 ᵍ⊗ₜ[R] (ι Q₂) m.2 +
      (-(ι Q₁) m.1 ᵍ⊗ₜ[R] ((ι Q₂) m.2 * 1) + 1 ᵍ⊗ₜ[R] ((ι Q₂) m.2 * (ι Q₂) m.2)) =
    (algebraMap R (CliffordAlgebra Q₁)) (Q₁ m.1) ᵍ⊗ₜ[R] 1 + (algebraMap R (CliffordAlgebra Q₁)) (Q₂ m.2) ᵍ⊗ₜ[R] 1

Tactic:
ι_sq_scalar,

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₂
⊢ (algebraMap R (CliffordAlgebra Q₁)) (Q₁ m.1) ᵍ⊗ₜ[R] 1 + (ι Q₁) m.1 ᵍ⊗ₜ[R] (ι Q₂) m.2 +
      (-(ι Q₁) m.1 ᵍ⊗ₜ[R] ((ι Q₂) m.2 * 1) + 1 ᵍ⊗ₜ[R] (algebraMap R (CliffordAlgebra Q₂)) (Q₂ m.2)) =
    (algebraMap R (CliffordAlgebra Q₁)) (Q₁ m.1) ᵍ⊗ₜ[R] 1 + (algebraMap R (CliffordAlgebra Q₁)) (Q₂ m.2) ᵍ⊗ₜ[R] 1
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

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

Tactic:
ihy,

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x x✝ y✝ : ExteriorAlgebra R M
i✝ : ℕ
hx✝ : x✝ ∈ (ι R).range ^ i✝
hy✝ : y✝ ∈ (ι R).range ^ i✝
ihx : (liftι R M) x✝ = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩
ihy : (liftι R M) y✝ = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨y✝, hy✝⟩
⊢ (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝, hx✝⟩ + (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨y✝, hy✝⟩ =
    (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i✝) ⟨x✝ + y✝, ⋯⟩
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
⊢ Basis ι (ZMod n) (ModN G n)

Tactic:
set φ : G →ₗ[ℤ] H := nG.mkQ

Goal state after:
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
⊢ Basis ι (ZMod n) (ModN G n)
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (ι' R A) ((DirectSum.lof R I A i) 1) = 1

Tactic:
exact identify_one R A i

Goal state after: