mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Module S P
inst✝ : IsScalarTower R S P
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
p : P
⊢ (j.endHom f) p = ((liftBaseChangeEquiv S) (α ∘ₗ f)) (j.equiv.symm p)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_4.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ Perm.sign a✝ • (MultilinearMap.domDomCongr a✝ (c • MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝ =
    Perm.sign a✝ • c • (MultilinearMap.domDomCongr a✝ (MultilinearMap.domCoprod' (↑m ⊗ₜ[R'] ↑n))) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ ∑ x, ∑ x_1, domCoprod' (Perm.sign x • Perm.sign x_1 • domDomCongr x a ⊗ₜ[R'] domDomCongr x_1 b) =
    ∑ σa, ∑ σb, Perm.sign σa • Perm.sign σb • domCoprod' (domDomCongr σa a ⊗ₜ[R'] domDomCongr σb b)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
hfv : f v = 0
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x✝ : V
i : Fin (finrank R V) := ⟨0, ⋯⟩
x : V
this : x = ∑ i, (b.repr x) i • b i
⊢ ∀ b_1 ∈ Finset.univ, b_1 ≠ i → (b.repr x) b_1 • b b_1 = 0

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
a₁ a₂ : Aᵐᵒᵖ
b₁ b₂ : Bᵐᵒᵖ
⊢ unop (↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂))) = unop (↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑e₁ (a₂ ⊗ₜ[R] b₂))

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
a₁ a₂ : A
b₁ b₂ : B
⊢ unop (↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂))) = unop (↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑e₂ (a₂ ⊗ₜ[R] b₂))

Tactic:
rfl

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

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
x✝ : A
⊢ ((AlgHom.op.symm
            ((algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯).comp
              (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)))).comp
        includeLeft)
      x✝ =
    ((AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ)).comp includeLeft) x✝

Tactic:
rfl

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

Goal state before:
pp: case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
x✝ : B
⊢ ((AlgHom.restrictScalars R
            (AlgHom.op.symm
              ((algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯).comp
                (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯))))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ))).comp includeRight) x✝

Tactic:
rfl

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₂
x✝³ : M₁
x✝² : M₂
x✝¹ : M₁
x✝ : M₂
⊢ ⅟2 * ((Q₁.tmul Q₂) (x✝³ ⊗ₜ[R] x✝² + x✝¹ ⊗ₜ[R] x✝) - Q₂ x✝² • Q₁ x✝³ - Q₂ x✝ • Q₁ x✝¹) =
    ⅟2 *
      ((AlgebraTensorModule.rid R A A) ((QuadraticMap.tmul Q₁ Q₂) (x✝³ ⊗ₜ[R] x✝² + x✝¹ ⊗ₜ[R] x✝)) - Q₂ x✝² • Q₁ x✝³ -
        Q₂ x✝ • Q₁ x✝¹)

Tactic:
rfl

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

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
x✝ : Aᵐᵒᵖ
⊢ (((AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)).comp (algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯)).comp
        includeLeft)
      x✝ =
    ((AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)).comp includeLeft) x✝

Tactic:
rfl

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

Goal state before:
pp: case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S).symm (opLinearEquiv R).symm ≪≫ₗ opLinearEquiv S
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) ≪≫ₗ opLinearEquiv S
x✝ : Bᵐᵒᵖ
⊢ ((AlgHom.restrictScalars R
            ((AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)).comp
              (algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ))).comp includeRight) x✝

Tactic:
rfl

Goal state after:
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
⊢ op (1 ⊗ₜ[R] (ι Q) v) = op (unop (↑(AlgEquiv.toOpposite A A) 1) ⊗ₜ[R] unop (op ((ι Q) v)))

Tactic:
rfl

Goal state after:
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
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
⊢ (TensorProduct.AlgebraTensorModule.map (↑(LinearEquiv.refl A A)) (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap))
      ((toBaseChange A Q) x) =
    (TensorProduct.map LinearMap.id (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x)

Tactic:
rfl

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' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q
⊢ ((changeFormAux Q' B) m) (((foldr Q (changeFormAux Q' B) ⋯) 1) x) =
    (ι Q') m * (changeForm h) x - (contractLeft (B m)) ((changeForm h) x)

Tactic:
rfl

Goal state after:
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✝² x✝¹ x✝ : M
⊢ ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝ + (CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) x✝, ⋯⟩ =
    ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝, ⋯⟩ +
      ⟨(CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) x✝, ⋯⟩

Tactic:
rfl

Goal state after:
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
⊢ ⟨x✝² • ((CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) x✝), ⋯⟩ =
    x✝² • ⟨(CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) x✝, ⋯⟩

Tactic:
rfl

Goal state after:
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✝² x✝¹ x✝ : M
⊢ ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝¹ + (CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝, ⋯⟩ =
    ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝¹, ⋯⟩ +
      ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case ι_mul_ι_mul
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 g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
x✝ : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
ih : f ⟨x, hx⟩ = g ⟨x, hx⟩
⊢ f ⟨(CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x, ⋯⟩ =
    g ⟨(CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x, ⋯⟩

Tactic:
have := congr_arg₂ (· * ·) (LinearMap.congr_fun (LinearMap.congr_fun h m₁) m₂) ih
    exact (map_mul f _ _).trans (this.trans <| (map_mul g _ _).symm)

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 : ↑ι
hxy : x = y
hxi : ¬x = i
⊢ (Finsupp.single y 1) x + f v * (Finsupp.single y 1) i * 0 = 1

Tactic:
simp [hxy]

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

Goal state before:
pp: case snd
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
⊢ (f.bilin m₁) m * g m = Q m • g m₁

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hg

Goal state after:
case snd.refine_1
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 ∈ {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₁

case snd.refine_2
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
⊢ (f.bilin m₁) m * 0 m = Q m • 0 m₁

case snd.refine_3
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 y : M →ₗ[R] A),
    x ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)} →
      y ∈ 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 * y m = Q m • y m₁ → (f.bilin m₁) m * (x + y) m = Q m • (x + y) m₁

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₁
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)
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)

Tactic:
rfl

Goal state after:
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)
⊢ (gradedComm R 𝒜 ℬ).symm = gradedComm R ℬ 𝒜

Tactic:
rfl

Goal state after:
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
⊢ ((gradedMul R 𝒜 ℬ) (a₁ ⊗ₜ[R] (lof R ι ℬ j₁) b₁)) ((lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] b₂) =
    (-1) ^ (j₁ * i₂) • (a₁ * (lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((lof R ι ℬ j₁) b₁ * b₂)

Tactic:
by
  rw [gradedMul]
  dsimp only [curry_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, assoc_tmul,
    map_tmul, LinearMap.id_coe, id_eq, assoc_symm_tmul, LinearMap.rTensor_tmul,
    LinearMap.lTensor_tmul]
  rw [mul_comm j₁ i₂, gradedComm_of_tmul_of]
  -- the tower smul lemmas elaborate too slowly
  rw [Units.smul_def, Units.smul_def, ← Int.cast_smul_eq_zsmul R, ← Int.cast_smul_eq_zsmul R]
  -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specialize `map_smul` to avoid timeouts.
  rw [← smul_tmul', LinearEquiv.map_smul, tmul_smul, LinearEquiv.map_smul, map_smul]
  dsimp

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

Goal state before:
pp: case mem
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 : ℕ
hm₁ : m₁' ∈ (ι Q₁).range ^ ↑⟨i₁n, ⋯⟩
⊢ (map f₁) m₁' * (map f₂) m₂ = (-1) ^ (i₂ * ↑i₁n) • ((map f₂) m₂ * (map f₁) m₁')

Tactic:
dsimp only at *

Goal state after:
case mem
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 : ℕ
hm₁ : m₁' ∈ (ι Q₁).range ^ i₁n
⊢ (map f₁) m₁' * (map f₂) m₂ = (-1) ^ (i₂ * ↑i₁n) • ((map f₂) m₂ * (map f₁) 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 ℬ
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✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ((gradedMul R 𝒜 ℬ)
        (((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 ixa) xa ⊗ₜ[R] (lof R ι ℬ ixb) xb))
          ((lof R ι 𝒜 iya) ya ⊗ₜ[R] (lof R ι ℬ iyb) yb)))
      ((lof R ι 𝒜 iza) za ⊗ₜ[R] (lof R ι ℬ izb) zb) =
    ((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 ixa) xa ⊗ₜ[R] (lof R ι ℬ ixb) xb))
      (((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 iya) ya ⊗ₜ[R] (lof R ι ℬ iyb) yb)) ((lof R ι 𝒜 iza) za ⊗ₜ[R] (lof R ι ℬ izb) zb))

Tactic:
tmul_of_gradedMul_of_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 ℬ
x y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
mA : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ →ₗ[R] DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ :=
  gradedMul R 𝒜 ℬ
ixa : ι
xa : 𝒜 ixa
ixb : ι
xb : ℬ ixb
iya : ι
ya : 𝒜 iya
iyb : ι
yb : ℬ iyb
iza : ι
za : 𝒜 iza
izb : ι
zb : ℬ izb
⊢ ((gradedMul R 𝒜 ℬ)
        ((-1) ^ (ixb * iya) •
          ((lof R ι 𝒜 ixa) xa * (lof R ι 𝒜 iya) ya) ⊗ₜ[R] ((lof R ι ℬ ixb) xb * (lof R ι ℬ iyb) yb)))
      ((lof R ι 𝒜 iza) za ⊗ₜ[R] (lof R ι ℬ izb) zb) =
    ((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 ixa) xa ⊗ₜ[R] (lof R ι ℬ ixb) xb))
      ((-1) ^ (iyb * iza) • ((lof R ι 𝒜 iya) ya * (lof R ι 𝒜 iza) za) ⊗ₜ[R] ((lof R ι ℬ iyb) yb * (lof R ι ℬ izb) zb))