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

Goal state before:
pp: case h₀
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
i i' : ι
⊢ (b.repr v) i' ≠ 0 → i' ≠ i → ((basis b ibc).repr ((b.repr v) i' • ε (b i'))) i = 0

Tactic:
_

Goal state after:
case h₀
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
i i' : ι
a✝ : (b.repr v) i' ≠ 0
⊢ i' ≠ i → ((basis b ibc).repr ((b.repr v) i' • ε (b i'))) i = 0
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case inr
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
h_allEq : ∀ (i j : ι), (b.coord i) (f (b i)) = (b.coord j) (f (b j))
hcomm : ∀ (i : ι) (r : R), r • f (b i) = (b.coord i) (f (b i)) • r • b i
i : ι := Classical.ofNonempty
x : V
j : ι
⊢ j ∈ (b.repr x).support → f ((b.repr x) j • b j) = ⟨(b.coord i) (f (b i)), ⋯⟩ • (b.repr x) j • b j

Tactic:
_

Goal state after:
case inr
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
h_allEq : ∀ (i j : ι), (b.coord i) (f (b i)) = (b.coord j) (f (b j))
hcomm : ∀ (i : ι) (r : R), r • f (b i) = (b.coord i) (f (b i)) • r • b i
i : ι := Classical.ofNonempty
x : V
j : ι
a✝ : j ∈ (b.repr x).support
⊢ f ((b.repr x) j • b j) = ⟨(b.coord i) (f (b i)), ⋯⟩ • (b.repr x) j • b j
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
⊢ transvection 0 v = id

Tactic:
ext
  simp [transvection]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : Dual R V
⊢ transvection f 0 = id

Tactic:
ext
  simp [transvection]

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

Goal state before:
pp: case «1»
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
⊢ transvection f v = id

Tactic:
let b := finBasis R V

Goal state after:
case «1»
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
⊢ transvection f v = id
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case «1»
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
⊢ (transvection f v) x = id x

Tactic:
suffices f x • v = 0 by
      simp [apply, this]

Goal state after:
case «1»
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
⊢ f x • v = 0
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case inr.inl
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : StrongRankCondition R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
hV : Nontrivial V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V := Free.chooseBasis R V
hι : Subsingleton ι
this✝ : Nonempty ι
this : Fintype ι
⊢ ∃ a, f = a • 1

Tactic:
simp_all [finrank_eq_card_basis b, ← Nat.card_eq_fintype_card]

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
⊢ AlgHom.op.symm
      ((algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯).comp (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯))) =
    AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ)

Tactic:
by ext <;> 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
⊢ (AlgHom.opComm (algHomOfLinearMapTensorProduct ↑e₂ ⋯ ⋯)).comp (algHomOfLinearMapTensorProduct ↑e₁ ⋯ ⋯) =
    AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)

Tactic:
by ext <;> rfl

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

Goal state before:
pp: case tmul
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 x : V
⊢ (ibc.endHom (LinearMap.transvection f v)) (ε x) = (LinearMap.transvection (ibc.toDual f) (ε v)) (ε x)

Tactic:
simp [LinearMap.transvection.apply, endHom_comp_apply, toDual_comp_apply]

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

Goal state before:
pp: 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
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this✝ : Fintype ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.transvection i j 1
⊢ ((toMatrix b b) (transvection f v)).det = 1 + f v

Tactic:
rw [this, Matrix.det_transvection_of_ne i j hi 1, hfv, add_zero]

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

Goal state before:
pp: r : ℝ
⊢ (LinearMap.toSpanSingleton ℝ ℂ Complex.I) r * (LinearMap.toSpanSingleton ℝ ℂ Complex.I) r = (algebraMap ℝ ℂ) (Q r)

Tactic:
dsimp [LinearMap.toSpanSingleton, LinearMap.id]
      rw [mul_mul_mul_comm]
      simp

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

Goal state before:
pp: case h₀
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 ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.diagonal (Function.update 1 i (1 + f v))
j : ↑ι
⊢ j ∈ Finset.univ → j ≠ i → Function.update 1 i (1 + f v) j = 1

Tactic:
_

Goal state after:
case h₀
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 ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.diagonal (Function.update 1 i (1 + f v))
j : ↑ι
a✝ : j ∈ Finset.univ
⊢ j ≠ i → Function.update 1 i (1 + f v) j = 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 : ↑ι
⊢ (Finsupp.single y 1) x + f (b y) * (Finsupp.single i 1) x = if x = y then if x = i then 1 + f (b i) else 1 x else 0

Tactic:
Pi.one_apply,

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 : ↑ι
⊢ (Finsupp.single y 1) x + f (b y) * (Finsupp.single i 1) x = if x = y then if x = i then 1 + f (b i) else 1 else 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
let b := finBasis R V

Goal state after:
case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
b : Basis (Fin (finrank R V)) R V := finBasis R V
⊢ LinearMap.det (transvection f v) = 1 + f v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case inv_mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x✝ : (CliffordAlgebra Q)ˣ
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ ⅟↑x * (ι Q) m * ↑x⁻¹⁻¹ ∈ (ι Q).range

Tactic:
inv_inv,

Goal state after:
case inv_mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x✝ : (CliffordAlgebra Q)ˣ
inst✝ : Invertible 2
x : (CliffordAlgebra Q)ˣ
m a : M
ha : (ι Q) a = ↑x
this✝¹ : Invertible ↑x := x.invertible
this✝ : Invertible ((ι Q) a) := ⋯.mpr this✝¹
this : Invertible (Q a) := invertibleOfInvertibleι Q a
⊢ ⅟↑x * (ι Q) m * ↑x ∈ (ι Q).range
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case mul
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
inst✝ : Invertible 2
y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (m : M), ↑y * (ι Q) m * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (m : M), ↑z * (ι Q) m * ↑z⁻¹ ∈ (ι Q).range
m : M
⊢ ↑(y * z) * (ι Q) m * ↑(y * z)⁻¹ ∈ (ι Q).range

Tactic:
simp_rw [mul_inv_rev, Units.val_mul]
    suffices ↑y * (↑z * ι Q m * ↑z⁻¹) * ↑y⁻¹ ∈ _ by
      simpa only [mul_assoc] using this
    obtain ⟨z', hz'⟩ := hz m
    obtain ⟨y', hy'⟩ := hy z'
    simp_rw [← hz', ← hy', LinearMap.mem_range_self]

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

Goal state before:
pp: case inv_mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this✝³ : Invertible ↑x := x.invertible
this✝² : Invertible ((ι Q) a) := ⋯.mpr this✝³
this✝¹ : Invertible (Q a) := invertibleOfInvertibleι Q a
this✝ : Invertible (-(ι Q) a) := invertibleNeg ((ι Q) a)
this : Invertible (involute ((ι Q) a)) := Invertible.map involute ((ι Q) a)
⊢ involute ⅟↑x * (ι Q) b * ↑x⁻¹⁻¹ ∈ (ι Q).range

Tactic:
inv_inv,

Goal state after:
case inv_mem
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x✝ x : (CliffordAlgebra Q)ˣ
b a : M
ha : (ι Q) a = ↑x
this✝³ : Invertible ↑x := x.invertible
this✝² : Invertible ((ι Q) a) := ⋯.mpr this✝³
this✝¹ : Invertible (Q a) := invertibleOfInvertibleι Q a
this✝ : Invertible (-(ι Q) a) := invertibleNeg ((ι Q) a)
this : Invertible (involute ((ι Q) a)) := Invertible.map involute ((ι Q) a)
⊢ involute ⅟↑x * (ι Q) b * ↑x ∈ (ι Q).range
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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
a₁ : A
j₁ : ι
⊢ (AlgebraTensorModule.curry
          ((LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ)).compr₂
              (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) ∘ₗ
            ↑(of R 𝒜 ℬ)))
        a₁ ∘ₗ
      (ℬ j₁).subtype =
    (AlgebraTensorModule.curry
          ((LinearMap.mul R C ∘ₗ
                  LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm).compl₂
              (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) ∘ₗ
            ↑(of R 𝒜 ℬ)))
        a₁ ∘ₗ
      (ℬ j₁).subtype

Tactic:
ext b₁ : 3

Goal state after:
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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
a₁ : A
j₁ : ι
b₁ : ↥(ℬ j₁)
⊢ AlgebraTensorModule.curry
      (((AlgebraTensorModule.curry
                ((LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ)).compr₂
                    (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) ∘ₗ
                  ↑(of R 𝒜 ℬ)))
              a₁ ∘ₗ
            (ℬ j₁).subtype)
          b₁ ∘ₗ
        ↑(of R 𝒜 ℬ)) =
    AlgebraTensorModule.curry
      (((AlgebraTensorModule.curry
                ((LinearMap.mul R C ∘ₗ
                        LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm).compl₂
                    (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) ∘ₗ
                  ↑(of R 𝒜 ℬ)))
              a₁ ∘ₗ
            (ℬ j₁).subtype)
          b₁ ∘ₗ
        ↑(of R 𝒜 ℬ))
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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ F (↑a ᵍ⊗ₜ[R] 1 * 1 ᵍ⊗ₜ[R] ↑b) = (-1) ^ (j * i) • (F (1 ᵍ⊗ₜ[R] ↑b) * F (↑a ᵍ⊗ₜ[R] 1))

Tactic:
← map_mul F,

Goal state after:
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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ F (↑a ᵍ⊗ₜ[R] 1 * 1 ᵍ⊗ₜ[R] ↑b) = (-1) ^ (j * i) • F (1 ᵍ⊗ₜ[R] ↑b * ↑a ᵍ⊗ₜ[R] 1)
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ toTensorAlgebra (GradedMonoid.GMul.mul a b) = toTensorAlgebra a * toTensorAlgebra b

Tactic:
rw [TensorPower.gMul_eq_coe_linearMap, ← LinearMap.compr₂_apply, ← @LinearMap.mul_apply' R, ←
    LinearMap.compl₂_apply, ← LinearMap.comp_apply]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ ((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra) a) b =
    (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra) a) b
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: case refine_1
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
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
x : G
hx : ∀ (b : ι), ↑n ∣ (f x) b
⊢ nG.mkQ x = 0

Tactic:
simp only [Submodule.mkQ_apply]

Goal state after:
case refine_1
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
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
x : G
hx : ∀ (b : ι), ↑n ∣ (f x) b
⊢ Submodule.Quotient.mk x = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
h : LinearIndependent R v
this✝ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
this : Injective ⇑(Pi.algebraMap ι' R K)
⊢ LinearIndependent R (⇑(Pi.algebraMap ι' R K) ∘ v)

Tactic:
rwa [LinearMap.linearIndependent_iff_of_injOn _ this.injOn]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
⊢ ∀ (f : Fin k✝ → m) (g : Fin k✝ → n),
    Function.Injective f → Function.Injective g → (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
_

Goal state after:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → m
⊢ ∀ (g : Fin k✝ → n), Function.Injective f✝ → Function.Injective g → (A.submatrix f✝ g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → m
⊢ ∀ (g : Fin k✝ → n), Function.Injective f✝ → Function.Injective g → (A.submatrix f✝ g).det ∈ Set.range SignType.cast

Tactic:
_

Goal state after:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → m
g✝ : Fin k✝ → n
⊢ Function.Injective f✝ → Function.Injective g✝ → (A.submatrix f✝ g✝).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → m
g✝ : Fin k✝ → n
⊢ Function.Injective f✝ → Function.Injective g✝ → (A.submatrix f✝ g✝).det ∈ Set.range SignType.cast

Tactic:
_

Goal state after:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → m
g✝ : Fin k✝ → n
a✝ : Function.Injective f✝
⊢ Function.Injective g✝ → (A.submatrix f✝ g✝).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → m
g✝ : Fin k✝ → n
a✝ : Function.Injective f✝
⊢ Function.Injective g✝ → (A.submatrix f✝ g✝).det ∈ Set.range SignType.cast

Tactic:
_

Goal state after:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → m
g✝ : Fin k✝ → n
a✝¹ : Function.Injective f✝
a✝ : Function.Injective g✝
⊢ (A.submatrix f✝ g✝).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
ι : Type w
⊢ ∀ [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n), (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
_

Goal state after:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
ι : Type w
inst✝ : Fintype ι
⊢ ∀ [inst : DecidableEq ι] (f : ι → m) (g : ι → n), (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
ι : Type w
inst✝ : Fintype ι
⊢ ∀ [inst : DecidableEq ι] (f : ι → m) (g : ι → n), (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
_

Goal state after:
case mp
m : Type u_1
n : Type u_3
R : Type u_5
inst✝² : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ∀ (f : ι → m) (g : ι → n), (A.submatrix f g).det ∈ Set.range SignType.cast