awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
k : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : DecidableEq k
inst_3 : DecidableEq m
inst_4 : NonAssocSemiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
rw : Eq (α := Matrix m k α) ((single a b₁).trans (single b₂ c)).toMatrix 0
rw₁ : Eq (α := Matrix m k α) (toMatrix ⊥) 0
rw₂ rw₃ : Eq (α := Matrix m k α) 0 0
⊢ HMul.hMul (α := Matrix m n α) (β := Matrix n k α) (single a b₁).toMatrix (single b₂ c).toMatrix = 0

Tactic:
rw [← toMatrix_trans, single_trans_single_of_ne hb, toMatrix_bot]

Premises used: PEquiv.toMatrix_bot, PEquiv.single_trans_single_of_ne, PEquiv.toMatrix_trans
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype n
inst_1 : Fintype k
inst_2 : DecidableEq n
inst_3 : DecidableEq k
inst_4 : DecidableEq m
inst_5 : Semiring α
a : m
b : n
c : k
M : Matrix k l α
rw :
  HMul.hMul (α := Matrix m n α) (β := Matrix n k α) (single a b).toMatrix (single b c).toMatrix * M =
    HMul.hMul (α := Matrix m k α) (single a c).toMatrix M
rw₁ rw₂ : HMul.hMul (α := Matrix m k α) (single a c).toMatrix M = HMul.hMul (α := Matrix m k α) (single a c).toMatrix M
⊢ HMul.hMul (α := Matrix m n α) (single a b).toMatrix (HMul.hMul (α := Matrix n k α) (single b c).toMatrix M) =
    HMul.hMul (α := Matrix m k α) (single a c).toMatrix M

Tactic:
rw [← Matrix.mul_assoc, single_mul_single]

Premises used: Matrix.mul_assoc, PEquiv.single_mul_single
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
σ : Equiv.Perm n
⊢ Eq (α := Matrix n n α) (Equiv.toPEquiv σ).toMatrix (submatrix (m := n) 1 (⇑σ : (a : n) → n) id)

Tactic:
Matrix.ext fun _ _ => if_congr Option.some_inj rfl rfl

Premises used: if_congr, Matrix.ext, Option.some_inj, rfl
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : NonAssocSemiring β
f : α →+* β
σ : m ≃. n
a :
  ∀ (i : m) (j : n),
    Eq.{u_6 + 1} (α := β) (map.{u_5, u_6, u_3, u_4} (α := α) σ.toMatrix (⇑f : (a : α) → β) i j) (σ.toMatrix i j)
⊢ Eq (α := Matrix m n β) (map.{u_5, u_6, u_3, u_4} (α := α) σ.toMatrix (⇑f : (a : α) → β)) σ.toMatrix

Tactic:
ext i j
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
inst : DecidableEq n
inst_1 : NonAssocSemiring α
inst_2 : NonAssocSemiring β
f : α →+* β
σ : m ≃. n
i : m
j : n
⊢ Eq.{u_6 + 1} (α := β) (map.{u_5, u_6, u_3, u_4} (α := α) σ.toMatrix (⇑f : (a : α) → β) i j) (σ.toMatrix i j)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
simp :
  (∀ (x : Fin n → α) (x_1 : Matrix (Fin m) (Fin n) α),
      P ((of : (a : Fin (m + 1) → Fin n → α) → Matrix (Fin (m + 1)) (Fin n) α) (vecCons x x_1))) ↔
    ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
⊢ Forall P ↔ ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x

Tactic:
simp only [Forall, FinVec.forall_iff, forall_iff]

Premises used: FinVec.forall_iff, Matrix.Forall
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∀ (x : Fin n → α) (x_1 : Matrix (Fin m) (Fin n) α),
      P ((of : (a : Fin (m + 1) → Fin n → α) → Matrix (Fin (m + 1)) (Fin n) α) (vecCons x x_1))) ↔
    ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x

Tactic:
Iff.symm Fin.forall_fin_succ_pi

Premises used: Fin.forall_fin_succ_pi, Iff.symm
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∀ (x : Fin n → α) (x_1 : Matrix (Fin m) (Fin n) α),
      P ((of : (a : Fin (m + 1) → Fin n → α) → Matrix (Fin (m + 1)) (Fin n) α) (vecCons x x_1))) ↔
    ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x

Tactic:
exact Iff.symm Fin.forall_fin_succ_pi

Premises used: Fin.forall_fin_succ_pi, Iff.symm
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m n : ℕ
α : Type u_1
P : Matrix (Fin 2) (Fin 3) α → Prop
⊢ (∀ (x : Matrix (Fin 2) (Fin 3) α), P x) ↔ ∀ (a b c d e f : α), P !![a, b, c; d, e, f]

Tactic:
(forall_iff _).symm

Premises used: Matrix.forall_iff, FinVec.Forall, Fin.cons, absurd, Fin.induction, Matrix.vecEmpty, Fin.cases, Matrix.vecCons, Iff.symm, Matrix.Forall, Fin.elim0
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
simp :
  (∃ (r : Fin n → α) (A : Matrix (Fin m) (Fin n) α),
      P ((of : (a : Fin (m + 1) → Fin n → α) → Matrix (Fin (m + 1)) (Fin n) α) (vecCons r A))) ↔
    ∃ (x : Matrix (Fin (m + 1)) (Fin n) α), P x
⊢ Exists P ↔ ∃ (x : Matrix (Fin (m + 1)) (Fin n) α), P x

Tactic:
simp only [Exists, FinVec.exists_iff, exists_iff]

Premises used: FinVec.exists_iff, Matrix.Exists
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∃ (r : Fin n → α) (A : Matrix (Fin m) (Fin n) α),
      P ((of : (a : Fin (m + 1) → Fin n → α) → Matrix (Fin (m + 1)) (Fin n) α) (vecCons r A))) ↔
    ∃ (x : Matrix (Fin (m + 1)) (Fin n) α), P x

Tactic:
Iff.symm Fin.exists_fin_succ_pi

Premises used: Fin.exists_fin_succ_pi, Iff.symm
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∃ (r : Fin n → α) (A : Matrix (Fin m) (Fin n) α),
      P ((of : (a : Fin (m + 1) → Fin n → α) → Matrix (Fin (m + 1)) (Fin n) α) (vecCons r A))) ↔
    ∃ (x : Matrix (Fin (m + 1)) (Fin n) α), P x

Tactic:
exact Iff.symm Fin.exists_fin_succ_pi

Premises used: Fin.exists_fin_succ_pi, Iff.symm
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m n : ℕ
α : Type u_1
P : Matrix (Fin 2) (Fin 3) α → Prop
⊢ (∃ (x : Matrix (Fin 2) (Fin 3) α), P x) ↔ ∃ (a : α) (b : α) (c : α) (d : α) (e : α) (f : α), P !![a, b, c; d, e, f]

Tactic:
(exists_iff _).symm

Premises used: Fin.cons, absurd, Fin.induction, FinVec.Exists, Matrix.vecEmpty, Fin.cases, Matrix.Exists, Matrix.vecCons, Matrix.exists_iff, Iff.symm, Fin.elim0
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
simp_rw :
  (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
      (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i j =
    Aᵀ i j
⊢ A.transposeᵣ i j = Aᵀ i j

Tactic:
simp_rw [transposeᵣ, transposeᵣ_eq]

Premises used: Matrix.transposeᵣ
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
      (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i j =
    Aᵀ i j

Tactic:
i.cases ?_ fun i => ?_

Premises used: Fin.cases
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
refine_1 :
  (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
      (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) 0 j =
    Aᵀ 0 j
refine_2 :
  ∀ (i : Fin n),
    (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
        (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i.succ j =
      Aᵀ i.succ j
⊢ (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
      (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i j =
    Aᵀ i j

Tactic:
refine i.cases ?_ fun i => ?_
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
refine_1 : FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A j = A j 0
⊢ (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
      (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) 0 j =
    Aᵀ 0 j

Tactic:
dsimp
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
refine_1 : ((fun (v : Fin (n + 1) → α) ↦ v 0) ∘ A) j = A j 0
refine_1₁ refine_1₂ : A j 0 = A j 0
⊢ FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A j = A j 0

Tactic:
rw [FinVec.map_eq, Function.comp_apply]

Premises used: FinVec.map_eq, Function.comp_apply
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i_1 : Fin (n + 1)
j : Fin m
i : Fin n
refine_2 : (A.submatrix id Fin.succ)ᵀ i j = Aᵀ i.succ j
⊢ (of : (a : Fin (n + 1) → Fin m → α) → Matrix (Fin (n + 1)) (Fin m) α)
      (vecCons (FinVec.map (fun (v : Fin (n + 1) → α) ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i.succ j =
    Aᵀ i.succ j

Tactic:
simp only [of_apply, Matrix.cons_val_succ]

Premises used: Matrix.cons_val_succ, Matrix.of_apply
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i_1 : Fin (n + 1)
j : Fin m
i : Fin n
⊢ (A.submatrix id Fin.succ)ᵀ i j = Aᵀ i.succ j

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m n : ℕ
α : Type u_1
a b c d : α
⊢ Eq.{u_1 + 1} (α := Matrix (Fin 2) (Fin 2) α) !![a, b; c, d]ᵀ !![a, c; b, d]

Tactic:
(transposeᵣ_eq _).symm

Premises used: Eq.mpr, FinVec.map, Matrix.submatrix, Fin.cons, Fin.induction.go, absurd, Fin.induction, Matrix.vecEmpty, Matrix.transposeᵣ_eq, Fin.cases, FinVec.seq, Eq.symm, Matrix.vecTail, Matrix.vecCons, Fin.elim0, Matrix.transposeᵣ
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddCommMonoid α
m : ℕ
a b : Fin m → α
simp_rw : FinVec.sum (FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b) = a ⬝ᵥ b
simp_rw₁ : Eq (α := α) (FinVec.sum (FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b)) (∑ i : Fin m, a i * b i)
simp_rw₂ :
  Eq.{u_1 + 1} (α := α) (∑ i : Fin m, FinVec.seq (FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a) b i)
    (∑ i : Fin m, a i * b i)
simp_rw₃ :
  Eq.{u_1 + 1} (α := α) (∑ x : Fin m, FinVec.map (fun (x1 x2 : α) ↦ x1 * x2) a x (b x)) (∑ i : Fin m, a i * b i)
simp_rw₄ : Eq.{u_1 + 1} (α := α) (∑ x : Fin m, ((fun (x1 x2 : α) ↦ x1 * x2) ∘ a) x (b x)) (∑ i : Fin m, a i * b i)
⊢ dotProductᵣ a b = a ⬝ᵥ b

Tactic:
simp_rw [dotProductᵣ, dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq,
      Function.comp_apply]

Premises used: dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq, Function.comp_apply, Matrix.dotProductᵣ
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m n : ℕ
α : Type u_1
a b c d : α
inst : Mul α
inst_1 : AddCommMonoid α
⊢ ![a, b] ⬝ᵥ ![c, d] = a * c + b * d

Tactic:
(dotProductᵣ_eq _ _).symm

Premises used: Eq.mpr, FinVec.map, Fin.cons, Fin.induction.go, FinVec.sum, Fin.induction, Fin.cases, FinVec.seq, Eq.symm, Matrix.vecTail, Matrix.vecCons, Matrix.dotProductᵣ_eq, Matrix.dotProductᵣ
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m n : ℕ
α : Type u_1
inst : Mul α
inst_1 : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
simp :
  (of : (a : Fin l → Fin n → α) → Matrix (Fin l) (Fin n) α)
      ((fun (v₁ : Fin m → α) ↦
          (fun (v₂ : Fin m → α) ↦ v₁ ⬝ᵥ v₂) ∘
            (of : (a : Fin n → Fin m → α) → Matrix (Fin n) (Fin m) α) fun (x : Fin n) (y : Fin m) ↦ B y x) ∘
        A) =
    A * B
⊢ A.mulᵣ B = A * B

Tactic:
simp [mulᵣ, Matrix.transpose]

Premises used: Matrix.mulᵣ, Matrix.transpose
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m n : ℕ
α : Type u_1
inst : Mul α
inst_1 : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ (of : (a : Fin l → Fin n → α) → Matrix (Fin l) (Fin n) α)
      ((fun (v₁ : Fin m → α) ↦
          (fun (v₂ : Fin m → α) ↦ v₁ ⬝ᵥ v₂) ∘
            (of : (a : Fin n → Fin m → α) → Matrix (Fin n) (Fin m) α) fun (x : Fin n) (y : Fin m) ↦ B y x) ∘
        A) =
    A * B

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m n : ℕ
α : Type u_1
inst : AddCommMonoid α
inst_1 : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ HMul.hMul (α := Matrix (Fin 2) (Fin 2) α) (β := Matrix (Fin 2) (Fin 2) α)
      (!![a₁₁, a₁₂; a₂₁, a₂₂] : Matrix (Fin 2) (Fin 2) α) (!![b₁₁, b₁₂; b₂₁, b₂₂] : Matrix (Fin 2) (Fin 2) α) =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]

Tactic:
(mulᵣ_eq _ _).symm

Premises used: Eq.mpr, FinVec.map, Matrix.mulᵣ_eq, Fin.cons, Matrix.mulᵣ, Fin.induction.go, FinVec.sum, Fin.induction, Matrix.transpose, Fin.cases, FinVec.seq, Eq.symm, Matrix.vecTail, Matrix.vecCons, Matrix.dotProductᵣ
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m : ℕ
α : Type u_1
inst : NonUnitalNonAssocSemiring α
A : Matrix (Fin l) (Fin m) α
v : Fin m → α
simp : (fun (a : Fin m → α) ↦ a ⬝ᵥ v) ∘ A = A *ᵥ v
⊢ A.mulVecᵣ v = A *ᵥ v

Tactic:
simp [mulVecᵣ]

Premises used: Matrix.mulVecᵣ
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m : ℕ
α : Type u_1
inst : NonUnitalNonAssocSemiring α
A : Matrix (Fin l) (Fin m) α
v : Fin m → α
⊢ (fun (a : Fin m → α) ↦ a ⬝ᵥ v) ∘ A = A *ᵥ v

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m n : ℕ
α : Type u_1
inst : NonUnitalNonAssocSemiring α
a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α
⊢ !![a₁₁, a₁₂; a₂₁, a₂₂] *ᵥ ![b₁, b₂] = ![a₁₁ * b₁ + a₁₂ * b₂, a₂₁ * b₁ + a₂₂ * b₂]

Tactic:
(mulVecᵣ_eq _ _).symm

Premises used: Eq.mpr, FinVec.map, Matrix.mulVecᵣ_eq, Fin.cons, Fin.induction.go, FinVec.sum, Fin.induction, Matrix.mulVecᵣ, Fin.cases, FinVec.seq, Eq.symm, Matrix.vecTail, Matrix.vecCons, Matrix.dotProductᵣ
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m : ℕ
α : Type u_1
inst : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
simp : (fun (a : Fin l → α) ↦ v ⬝ᵥ a) ∘ Aᵀ = v ᵥ* A
⊢ vecMulᵣ v A = v ᵥ* A

Tactic:
simp [vecMulᵣ]

Premises used: Matrix.vecMulᵣ
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m : ℕ
α : Type u_1
inst : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ (fun (a : Fin l → α) ↦ v ⬝ᵥ a) ∘ Aᵀ = v ᵥ* A

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m n : ℕ
α : Type u_1
inst : NonUnitalNonAssocSemiring α
a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α
⊢ ![b₁, b₂] ᵥ* !![a₁₁, a₁₂; a₂₁, a₂₂] = ![b₁ * a₁₁ + b₂ * a₂₁, b₁ * a₁₂ + b₂ * a₂₂]

Tactic:
(vecMulᵣ_eq _ _).symm

Premises used: Eq.mpr, FinVec.map, Fin.cons, Fin.induction.go, Matrix.vecMulᵣ, FinVec.sum, Fin.induction, Matrix.transpose, Matrix.vecMulᵣ_eq, Fin.cases, FinVec.seq, Eq.symm, Matrix.vecTail, Matrix.vecCons, Matrix.dotProductᵣ
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin n) α
simp_rw :
  ((Equiv.refl (Fin m → Fin n → α) : (a : Fin m → Fin n → α) → Matrix (Fin m) (Fin n) α) fun (i : Fin m) (j : Fin n) ↦
      A i j) =
    A
⊢ A.etaExpand = A

Tactic:
simp_rw [etaExpand, FinVec.etaExpand_eq, Matrix.of]

Premises used: FinVec.etaExpand_eq, Matrix.of, Matrix.etaExpand
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin n) α
⊢ ((Equiv.refl (Fin m → Fin n → α) : (a : Fin m → Fin n → α) → Matrix (Fin m) (Fin n) α) fun (i : Fin m) (j : Fin n) ↦
      A i j) =
    A

Tactic:
rfl
-- Module: Mathlib.Data.Matrix.Reflection
Goal:
l m n : ℕ
α : Type u_1
A : Matrix (Fin 2) (Fin 2) α
⊢ A = !![A 0 0, A 0 1; A 1 0, A 1 1]

Tactic:
(etaExpand_eq _).symm

Premises used: FinVec.etaExpand, FinVec.map, Fin.succ, Matrix.etaExpand, Fin.cons, Fin.ofNat, Fin.induction, Fin.cases, Matrix.etaExpand_eq, FinVec.seq, Eq.symm, Matrix.vecTail, Matrix.vecCons
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t : List α
⊢ (↑s : Multiset α) + (↑t : Multiset α) = (↑(s ++ t) : Multiset α)

Tactic:
rfl

Premises used: Multiset.add, Multiset.ofList, rfl
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
a : α
s : Multiset α
⊢ {a} + s = a ::ₘ s

Tactic:
rfl

Premises used: Multiset.add, Multiset.cons, List.append, rfl
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t u : Multiset α
⊢ s + t ≤ s + u ↔ t ≤ u

Tactic:
Quotient.inductionOn₃ s t u fun _ _ _ => subperm_append_left _

Premises used: Quotient.inductionOn₃
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t u : Multiset α
⊢ s + u ≤ t + u ↔ s ≤ t

Tactic:
Quotient.inductionOn₃ s t u fun _ _ _ => subperm_append_right _

Premises used: Quotient.inductionOn₃
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t : Multiset α
⊢ s + t = t + s

Tactic:
Quotient.inductionOn₂ s t fun _ _ ↦ Quot.sound perm_append_comm

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t u : Multiset α
⊢ s + t + u = s + (t + u)

Tactic:
Quotient.inductionOn₃ s t u fun _ _ _ ↦ congr_arg _ <| append_assoc ..

Premises used: Quotient.inductionOn₃
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s : Multiset α
⊢ 0 + s = s

Tactic:
Quotient.inductionOn s fun _ ↦ rfl

Premises used: Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s : Multiset α
⊢ s + 0 = s

Tactic:
Quotient.inductionOn s fun l ↦ congr_arg _ <| append_nil l

Premises used: Quotient.inductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t : Multiset α
⊢ s ≤ s + t

Tactic:
simpa using Multiset.add_le_add_left (zero_le t)

Premises used: Multiset.add_le_add_left, Multiset.zero_le
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t : Multiset α
⊢ s ≤ t + s

Tactic:
simpa using Multiset.add_le_add_right (zero_le t)

Premises used: Multiset.add_le_add_right, Multiset.zero_le
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t : Multiset α
⊢ s ⊆ s + t

Tactic:
subset_of_le <| le_add_right s t

Premises used: Multiset.subset_of_le, Multiset.le_add_right
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t : Multiset α
⊢ s ⊆ t + s

Tactic:
subset_of_le <| le_add_left s t

Premises used: Multiset.subset_of_le, Multiset.le_add_left
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t : Multiset α
⊢ s ≤ t ↔ ∃ (u : Multiset α), t = s + u

Tactic:
⟨fun h =>
    leInductionOn h fun s =>
      let ⟨l, p⟩ := s.exists_perm_append
      ⟨l, Quot.sound p⟩,
    fun ⟨_u, e⟩ => e.symm ▸ le_add_right _ _⟩

Premises used: Multiset.leInductionOn, _private.0.Multiset.le_iff_exists_add.match_2, Eq.rec, LE.le, Iff.intro, Multiset.le_add_right, Eq.symm
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
a : α
s t : Multiset α
rw : {a} + s + t = a ::ₘ (s + t)
rw₁ : {a} + s + t = {a} + (s + t)
rw₂ rw₃ : {a} + (s + t) = {a} + (s + t)
⊢ a ::ₘ s + t = a ::ₘ (s + t)

Tactic:
rw [← singleton_add, ← singleton_add, Multiset.add_assoc]

Premises used: Multiset.singleton_add, Multiset.add_assoc
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
a : α
s t : Multiset α
rw : a ::ₘ t + s = a ::ₘ (s + t)
rw₁ : a ::ₘ (t + s) = a ::ₘ (s + t)
rw₂ rw₃ : a ::ₘ (s + t) = a ::ₘ (s + t)
⊢ s + a ::ₘ t = a ::ₘ (s + t)

Tactic:
rw [Multiset.add_comm, cons_add, Multiset.add_comm]

Premises used: Multiset.add_comm, Multiset.cons_add
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
a : α
s t : Multiset α
⊢ a ∈ s + t ↔ a ∈ s ∨ a ∈ t

Tactic:
Quotient.inductionOn₂ s t fun _l₁ _l₂ => mem_append

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s t : Multiset α
⊢ countP p (s + t) = countP p s + countP p t

Tactic:
Quotient.inductionOn₂ s t fun _ _ => countP_append

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ ∀ (s t : Multiset α), count a (s + t) = count a s + count a t

Tactic:
countP_add _

Premises used: Multiset.count, Multiset.countP_add
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t u : Multiset α
⊢ s + u = t + u ↔ s = t

Tactic:
simp [Multiset.ext]

Premises used: Multiset.ext
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t u : Multiset α
⊢ s + u = t + u ↔ s = t

Tactic:
classical simp [Multiset.ext]

Premises used: Multiset.ext
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t u : Multiset α
⊢ s + t = s + u ↔ t = u

Tactic:
simp [Multiset.ext]

Premises used: Multiset.ext
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t u : Multiset α
⊢ s + t = s + u ↔ t = u

Tactic:
classical simp [Multiset.ext]

Premises used: Multiset.ext
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
s t : Multiset α
⊢ (s + t).card = s.card + t.card

Tactic:
Quotient.inductionOn₂ s t fun _ _ => length_append

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
⊢ (↑l : Multiset α).erase a = (↑(l.erase a) : Multiset α)

Tactic:
rfl

Premises used: Multiset.erase, rfl
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ erase 0 a = 0

Tactic:
rfl

Premises used: Multiset.zero, Multiset.ofList, List.erase, Multiset.erase, rfl
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ (a ::ₘ s).erase a = s

Tactic:
Quot.inductionOn s fun l => congr_arg _ <| List.erase_cons_head a l

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Multiset α
h : b ≠ a
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a

Tactic:
Quot.inductionOn s fun _ => congr_arg _ <| List.erase_cons_tail (not_beq_of_ne h)

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ erase {a} a = 0

Tactic:
erase_cons_head a 0

Premises used: Multiset.erase_cons_head, OfNat.ofNat
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Multiset α
⊢ ¬a ∈ s → s.erase a = s

Tactic:
Quot.inductionOn s fun _l h => congr_arg _ <| List.erase_of_not_mem h

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ a ∈ s → a ::ₘ s.erase a = s

Tactic:
Quot.inductionOn s fun _l h => Quot.sound (perm_cons_erase h).symm

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
inl : (a ::ₘ s).erase a = a ::ₘ s.erase a
inr : ∀ (hab : a ≠ b), (b ::ₘ s).erase a = b ::ₘ s.erase a
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a

Tactic:
rcases eq_or_ne a b with rfl | hab

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ (a ::ₘ s).erase a = a ::ₘ s.erase a

Tactic:
simp [cons_erase h]

Premises used: Multiset.cons_erase
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
hab : a ≠ b
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a

Tactic:
s.erase_cons_tail hab.symm

Premises used: Ne.symm, Multiset.erase_cons_tail
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
hab : a ≠ b
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a

Tactic:
exact s.erase_cons_tail hab.symm

Premises used: Ne.symm, Multiset.erase_cons_tail
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
rw : s ≤ a ::ₘ s
⊢ s ≤ a ::ₘ s.erase a

Tactic:
rw [erase_of_notMem h]

Premises used: Multiset.erase_of_notMem
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s

Tactic:
apply le_cons_self

Premises used: Multiset.le_cons_self
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
rw : a ::ₘ s = t ↔ a ∈ t ∧ s = t.erase a
⊢ s + {a} = t ↔ a ∈ t ∧ s = t.erase a

Tactic:
rw [Multiset.add_comm, singleton_add]

Premises used: Multiset.singleton_add, Multiset.add_comm
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
a : α
mp : a ::ₘ s = t → a ∈ t ∧ s = t.erase a
mpr : a ∈ t ∧ s = t.erase a → a ::ₘ s = t
⊢ a ::ₘ s = t ↔ a ∈ t ∧ s = t.erase a

Tactic:
constructor
-- Module: Mathlib.Data.Multiset.AddSub
Goal:
α : Type u_1
inst : DecidableEq α
s : Multiset α
a : α
⊢ a ∈ a ::ₘ s ∧ s = (a ::ₘ s).erase a

Tactic:
⟨s.mem_cons_self a, (s.erase_cons_head a).symm⟩

Premises used: Multiset.erase_cons_head, And.intro, Multiset.mem_cons_self, Eq.symm