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

Goal state before:
pp: case tmul
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i : ι₁
x : M₁ i
y : M₂'
⊢ (directSumLeft R S M₁ M₂').symm ((of (fun i ↦ M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)) =
    (rTensor M₂' (lof R ι₁ M₁ i)) (x ⊗ₜ[R] y)

Tactic:
← lof_eq_of S,

Goal state after:
case tmul
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i : ι₁
x : M₁ i
y : M₂'
⊢ (directSumLeft R S M₁ M₂').symm ((lof S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)) =
    (rTensor M₂' (lof R ι₁ M₁ i)) (x ⊗ₜ[R] y)
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: case single.single
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n)) (i, k) =
    (Finsupp.single i' m) i ⊗ₜ[R] (Finsupp.single k' n) k

Tactic:
[

Goal state after:
case single.single
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n)) (i, k) =
    (Finsupp.single i' m) i ⊗ₜ[R] (Finsupp.single k' n) k
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y z : R
⊢ SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z

Tactic:
[

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y z : R
⊢ SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommGroupWithZero R
inst✝ : StarMul R
x y : R
⊢ op (star (x / y)) = op (star x / star y)

Tactic:
division_def,

Goal state after:
R : Type u
inst✝¹ : CommGroupWithZero R
inst✝ : StarMul R
x y : R
⊢ op (star (x * y⁻¹)) = op (star x / star y)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : StarAddMonoid R
x : R
inst✝ : IsStarNormal x
⊢ star (-x) * -x = -x * star (-x)

Tactic:
[

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : NonUnitalNonAssocRing R
inst✝¹ : StarAddMonoid R
x : R
inst✝ : IsStarNormal x
⊢ star (-x) * -x = -x * star (-x)
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
⊢ ⅟2 • (x + star x) ∈ selfAdjoint A

Tactic:
by
      rw [selfAdjoint.mem_iff, star_smul, star_trivial, star_add, star_star, add_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : m
r : n → α
e : l ≃ m
f : o ≃ n
⊢ (A.updateRow i r).submatrix ⇑e ⇑f = (A.updateRow (e (e.symm i)) fun j ↦ r (f (f.symm j))).submatrix ⇑e ⇑f

Tactic:
[

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : m
r : n → α
e : l ≃ m
f : o ≃ n
⊢ (A.updateRow i r).submatrix ⇑e ⇑f = (A.updateRow (e (e.symm i)) fun j ↦ r (f (f.symm j))).submatrix ⇑e ⇑f
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq o
inst✝ : DecidableEq n
A : Matrix m n α
j : n
c : m → α
e : l ≃ m
f : o ≃ n
⊢ (A.updateCol j c).submatrix ⇑e ⇑f = (A.updateCol (f (f.symm j)) fun i ↦ c (e (e.symm i))).submatrix ⇑e ⇑f

Tactic:
[

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq o
inst✝ : DecidableEq n
A : Matrix m n α
j : n
c : m → α
e : l ≃ m
f : o ≃ n
⊢ (A.updateCol j c).submatrix ⇑e ⇑f = (A.updateCol (f (f.symm j)) fun i ↦ c (e (e.symm i))).submatrix ⇑e ⇑f
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ diagonal d (i, k) (j, k) = 0

Tactic:
diagonal_apply_ne _ (mt _ hij)

Goal state after:
case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ 0 = 0

m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (i, k) = (j, k) → i = j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 2
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) j = !![1, 0; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «0».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 2
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) j = !![1, 0; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «1».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «0».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «0».«2»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «1».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«2»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «2»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ 1 ((fun i ↦ i) ⟨2, ⋯⟩) j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨2, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «2».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «2».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «2».«2»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 2
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) j = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «0».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 2
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) j = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «1».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 3
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «0».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «0».«2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 3
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «1».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 3
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «2».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «2».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «2».«2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: F : Type u_1
R✝ : Type u_2
A✝ : Type u_3
B✝ : Type u_4
C : Type u_5
inst✝¹⁸ : Add A✝
inst✝¹⁷ : Add B✝
inst✝¹⁶ : Mul A✝
inst✝¹⁵ : Mul B✝
inst✝¹⁴ : SMul R✝ A✝
inst✝¹³ : SMul R✝ B✝
inst✝¹² : Star A✝
inst✝¹¹ : Star B✝
inst✝¹⁰ : Add C
inst✝⁹ : Mul C
inst✝⁸ : SMul R✝ C
inst✝⁷ : Star C
R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Star A
inst✝ : Star B
f : A ≃⋆ₐ[R] B
r : R
⊢ f.toFun ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
[

Goal state after:
F : Type u_1
R✝ : Type u_2
A✝ : Type u_3
B✝ : Type u_4
C : Type u_5
inst✝¹⁸ : Add A✝
inst✝¹⁷ : Add B✝
inst✝¹⁶ : Mul A✝
inst✝¹⁵ : Mul B✝
inst✝¹⁴ : SMul R✝ A✝
inst✝¹³ : SMul R✝ B✝
inst✝¹² : Star A✝
inst✝¹¹ : Star B✝
inst✝¹⁰ : Add C
inst✝⁹ : Mul C
inst✝⁸ : SMul R✝ C
inst✝⁷ : Star C
R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Star A
inst✝ : Star B
f : A ≃⋆ₐ[R] B
r : R
⊢ f.toFun ((algebraMap R A) r) = (algebraMap R B) r
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) j = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «0».«0»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map (f₁ + f₂) g)) x✝¹) x✝ = ((curry (map f₁ g + map f₂ g)) x✝¹) x✝

Tactic:
[

Goal state after:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map (f₁ + f₂) g)) x✝¹) x✝ = ((curry (map f₁ g + map f₂ g)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) j = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «1».«0»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map f (g₁ + g₂))) x✝¹) x✝ = ((curry (map f g₁ + map f g₂)) x✝¹) x✝

Tactic:
[

Goal state after:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map f (g₁ + g₂))) x✝¹) x✝ = ((curry (map f g₁ + map f g₂)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) j = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «0».«0»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «0».«2»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map f (r • g))) x✝¹) x✝ = ((curry (r • map f g)) x✝¹) x✝

Tactic:
[

Goal state after:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map f (r • g))) x✝¹) x✝ = ((curry (r • map f g)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) j = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «1».«0»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«2»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «2»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ A ((fun i ↦ i) ⟨2, ⋯⟩) j = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨2, ⋯⟩) j

Tactic:
fin_cases j

Goal state after:
case «2».«0»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «2».«1»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «2».«2»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : Semiring A
inst✝¹⁷ : Semiring B
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra R B
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : Module A M
inst✝¹¹ : IsScalarTower R A M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : IsScalarTower R A P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map (b • f) g)) x✝¹) x✝ = ((curry (b • map f g)) x✝¹) x✝

Tactic:
[

Goal state after:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : Semiring A
inst✝¹⁷ : Semiring B
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra R B
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : Module A M
inst✝¹¹ : IsScalarTower R A M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : IsScalarTower R A P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map (b • f) g)) x✝¹) x✝ = ((curry (b • map f g)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ I = Ideal.span {x}

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ I = Ideal.span {x}
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0»
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
j : Fin 2
⊢ (!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂]) ((fun i ↦ i) ⟨0, ⋯⟩) j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] ((fun i ↦ i) ⟨0, ⋯⟩)
      j

Tactic:
fin_cases j

Goal state after:
case «0».«0»
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ (!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂]) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ (!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂]) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨1, ⋯⟩)