awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
i : m
hi : ¬Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) ((g : (a : m) → Option n) i : Option n)
h :
  ∀ (hf : Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) (none : Option n)),
    ∃ (x : n),
      ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) none x then 1 else 0)
          (if Membership.mem (γ := Option n) ((g : (a : m) → Option n) i : Option n) x then 1 else 0)
h₁ :
  ∀ (fi : n) (hf : (f : (a : m) → Option n) i = some fi),
    ∃ (x : n),
      ¬Eq.{u_5 + 1} (α := α) (if x ∈ some fi then 1 else 0)
          (if Membership.mem (γ := Option n) ((g : (a : m) → Option n) i : Option n) x then 1 else 0)
⊢ ∃ (x : n),
    ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) ((f : (a : m) → Option n) i : Option n) x then 1 else 0)
        (if Membership.mem (γ := Option n) ((g : (a : m) → Option n) i : Option n) x then 1 else 0)

Tactic:
rcases hf : f i with - | fi

Premises used: DFunLike.coe
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
i : m
hi : ¬Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) ((g : (a : m) → Option n) i : Option n)
hf : Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) (none : Option n)
h :
  ∀ (hg : Eq.{u_4 + 1} (α := Option n) ((g : (a : m) → Option n) i : Option n) (none : Option n)),
    ∃ (x : n),
      ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) none x then 1 else 0)
          (if Membership.mem (γ := Option n) none x then 1 else 0)
h₁ :
  ∀ (gi : n) (hg : (g : (a : m) → Option n) i = some gi),
    ∃ (x : n),
      ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) none x then 1 else 0) (if x ∈ some gi then 1 else 0)
⊢ ∃ (x : n),
    ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) none x then 1 else 0)
        (if Membership.mem (γ := Option n) ((g : (a : m) → Option n) i : Option n) x then 1 else 0)

Tactic:
rcases hg : g i with - | gi

Premises used: DFunLike.coe
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
i : m
hi : ¬Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) ((g : (a : m) → Option n) i : Option n)
hf : Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) (none : Option n)
hg : Eq.{u_4 + 1} (α := Option n) ((g : (a : m) → Option n) i : Option n) (none : Option n)
⊢ ¬Eq.{u_4 + 1} (α := Option n) none none

Tactic:
rw [hf, hg] at hi
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
i : m
hi : ¬Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) ((g : (a : m) → Option n) i : Option n)
hf : Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) (none : Option n)
hg : Eq.{u_4 + 1} (α := Option n) ((g : (a : m) → Option n) i : Option n) (none : Option n)
hi₁ : ¬Eq.{u_4 + 1} (α := Option n) none none
⊢ Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) (none : Option n)

Tactic:
rw [hf, hg] at hi
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
i : m
hi : ¬Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) ((g : (a : m) → Option n) i : Option n)
hf : Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) (none : Option n)
hg : Eq.{u_4 + 1} (α := Option n) ((g : (a : m) → Option n) i : Option n) (none : Option n)
hi₁ : ¬Eq.{u_4 + 1} (α := Option n) none none
hf₁ : Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) (none : Option n)
⊢ Eq.{u_4 + 1} (α := Option n) ((g : (a : m) → Option n) i : Option n) (none : Option n)

Tactic:
rw [hf, hg] at hi
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
i : m
hi : ¬Eq.{u_4 + 1} (α := Option n) none none
hf : Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) (none : Option n)
hg : Eq.{u_4 + 1} (α := Option n) ((g : (a : m) → Option n) i : Option n) (none : Option n)
⊢ ∃ (x : n),
    ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) none x then 1 else 0)
        (if Membership.mem (γ := Option n) none x then 1 else 0)

Tactic:
(hi rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
i : m
hi : ¬Eq.{u_4 + 1} (α := Option n) none none
hf : Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) (none : Option n)
hg : Eq.{u_4 + 1} (α := Option n) ((g : (a : m) → Option n) i : Option n) (none : Option n)
⊢ ∃ (x : n),
    ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) none x then 1 else 0)
        (if Membership.mem (γ := Option n) none x then 1 else 0)

Tactic:
exact (hi rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
i : m
hi : ¬Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) ((g : (a : m) → Option n) i : Option n)
hf : Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) (none : Option n)
gi : n
hg : (g : (a : m) → Option n) i = some gi
h : ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) none gi then 1 else 0) (if gi ∈ some gi then 1 else 0)
⊢ ∃ (x : n),
    ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) none x then 1 else 0) (if x ∈ some gi then 1 else 0)

Tactic:
use gi
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
i : m
hi : ¬Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) ((g : (a : m) → Option n) i : Option n)
hf : Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) (none : Option n)
gi : n
hg : (g : (a : m) → Option n) i = some gi
⊢ ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) none gi then 1 else 0) (if gi ∈ some gi then 1 else 0)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
i : m
hi : ¬Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) ((g : (a : m) → Option n) i : Option n)
fi : n
hf : (f : (a : m) → Option n) i = some fi
h :
  ¬Eq.{u_5 + 1} (α := α) (if fi ∈ some fi then 1 else 0)
      (if Membership.mem (γ := Option n) ((g : (a : m) → Option n) i : Option n) fi then 1 else 0)
⊢ ∃ (x : n),
    ¬Eq.{u_5 + 1} (α := α) (if x ∈ some fi then 1 else 0)
        (if Membership.mem (γ := Option n) ((g : (a : m) → Option n) i : Option n) x then 1 else 0)

Tactic:
use fi
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
m : Type u_3
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : MulZeroOneClass α
inst_2 : Nontrivial α
f g : m ≃. n
i : m
hi : ¬Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) i : Option n) ((g : (a : m) → Option n) i : Option n)
fi : n
hf : (f : (a : m) → Option n) i = some fi
⊢ ¬Eq.{u_5 + 1} (α := α) (if fi ∈ some fi then 1 else 0)
      (if Membership.mem (γ := Option n) ((g : (a : m) → Option n) i : Option n) fi then 1 else 0)

Tactic:
simp [hf.symm, Ne.symm hi]

Premises used: Ne.symm, Eq.symm
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j : n
a :
  ∀ (i_1 j_1 : n),
    (Equiv.toPEquiv (Equiv.swap i j)).toMatrix i_1 j_1 =
      HAdd.hAdd (β := Matrix n n α)
        (HSub.hSub (α := Matrix n n α) 1 (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix)
        (single j i).toMatrix i_1 j_1
⊢ (Equiv.toPEquiv (Equiv.swap i j)).toMatrix =
    HSub.hSub (α := Matrix n n α) 1 (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix +
      (single j i).toMatrix

Tactic:
ext
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
a :
  (if j_1 ∈ some (if i_1 = i then j else if i_1 = j then i else i_1) then 1 else 0) =
    ((HSub.hSub (α := α) (if i_1 = j_1 then 1 else 0) (if j_1 ∈ if i_1 = i then some i else none then 1 else 0) -
          if j_1 ∈ if i_1 = j then some j else none then 1 else 0) +
        if j_1 ∈ if i_1 = i then some j else none then 1 else 0) +
      if j_1 ∈ if i_1 = j then some i else none then 1 else 0
⊢ (Equiv.toPEquiv (Equiv.swap i j)).toMatrix i_1 j_1 =
    HAdd.hAdd (β := Matrix n n α)
      (HSub.hSub (α := Matrix n n α) 1 (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix)
      (single j i).toMatrix i_1 j_1

Tactic:
dsimp [toMatrix, single, Equiv.swap_apply_def, Equiv.toPEquiv, one_apply]

Premises used: PEquiv.single, Matrix.one_apply, Equiv.toPEquiv, Equiv.swap_apply_def, PEquiv.toMatrix
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∈ some j
h_2 : i_1 = j_1
h_3 : j_1 ∈ some i
h_4 : i_1 = j
⊢ 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∈ some j
h_2 : i_1 = j_1
h_3 : j_1 ∈ some i
h_4 : ¬i_1 = j
h_5 : Membership.mem (γ := Option n) none j_1
⊢ 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∈ some j
h_2 : i_1 = j_1
h_3 : j_1 ∈ some i
h_4 : ¬i_1 = j
h_5 : j_1 ∉ none
⊢ 1 = HSub.hSub (α := α) 1 1 - 0 + 1 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∈ some j
h_2 : i_1 = j_1
h_3 : j_1 ∉ some i
h_4 : i_1 = j
⊢ 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∈ some j
h_2 : i_1 = j_1
h_3 : j_1 ∉ some i
h_4 : ¬i_1 = j
h_5 : Membership.mem (γ := Option n) none j_1
⊢ 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∈ some j
h_2 : i_1 = j_1
h_3 : j_1 ∉ some i
h_4 : ¬i_1 = j
h_5 : j_1 ∉ none
⊢ 1 = HSub.hSub (α := α) 1 0 - 0 + 1 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∈ some j
h_2 : ¬i_1 = j_1
h_3 : j_1 ∈ some i
h_4 : i_1 = j
⊢ 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∈ some j
h_2 : ¬i_1 = j_1
h_3 : j_1 ∈ some i
h_4 : ¬i_1 = j
h_5 : Membership.mem (γ := Option n) none j_1
⊢ 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∈ some j
h_2 : ¬i_1 = j_1
h_3 : j_1 ∈ some i
h_4 : ¬i_1 = j
h_5 : j_1 ∉ none
⊢ 1 = HSub.hSub (α := α) 0 1 - 0 + 1 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∈ some j
h_2 : ¬i_1 = j_1
h_3 : j_1 ∉ some i
h_4 : i_1 = j
⊢ 1 = HSub.hSub (α := α) 0 0 - 1 + 1 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∈ some j
h_2 : ¬i_1 = j_1
h_3 : j_1 ∉ some i
h_4 : ¬i_1 = j
h_5 : Membership.mem (γ := Option n) none j_1
⊢ 1 = HSub.hSub (α := α) 0 0 - 1 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∈ some j
h_2 : ¬i_1 = j_1
h_3 : j_1 ∉ some i
h_4 : ¬i_1 = j
h_5 : j_1 ∉ none
⊢ 1 = HSub.hSub (α := α) 0 0 - 0 + 1 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∉ some j
h_2 : i_1 = j_1
h_3 : j_1 ∈ some i
h_4 : i_1 = j
⊢ 0 = HSub.hSub (α := α) 1 1 - 0 + 0 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∉ some j
h_2 : i_1 = j_1
h_3 : j_1 ∈ some i
h_4 : ¬i_1 = j
h_5 : Membership.mem (γ := Option n) none j_1
⊢ 0 = HSub.hSub (α := α) 1 1 - 1 + 0 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∉ some j
h_2 : i_1 = j_1
h_3 : j_1 ∈ some i
h_4 : ¬i_1 = j
h_5 : j_1 ∉ none
⊢ 0 = HSub.hSub (α := α) 1 1 - 0 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∉ some j
h_2 : i_1 = j_1
h_3 : j_1 ∉ some i
h_4 : i_1 = j
⊢ 0 = HSub.hSub (α := α) 1 0 - 0 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∉ some j
h_2 : i_1 = j_1
h_3 : j_1 ∉ some i
h_4 : ¬i_1 = j
h_5 : Membership.mem (γ := Option n) none j_1
⊢ 0 = HSub.hSub (α := α) 1 0 - 1 + 0 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∉ some j
h_2 : i_1 = j_1
h_3 : j_1 ∉ some i
h_4 : ¬i_1 = j
h_5 : j_1 ∉ none
⊢ 0 = HSub.hSub (α := α) 1 0 - 0 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∉ some j
h_2 : ¬i_1 = j_1
h_3 : j_1 ∈ some i
h_4 : i_1 = j
⊢ 0 = HSub.hSub (α := α) 0 1 - 0 + 0 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∉ some j
h_2 : ¬i_1 = j_1
h_3 : j_1 ∈ some i
h_4 : ¬i_1 = j
h_5 : Membership.mem (γ := Option n) none j_1
⊢ 0 = HSub.hSub (α := α) 0 1 - 1 + 0 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∉ some j
h_2 : ¬i_1 = j_1
h_3 : j_1 ∈ some i
h_4 : ¬i_1 = j
h_5 : j_1 ∉ none
⊢ 0 = HSub.hSub (α := α) 0 1 - 0 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∉ some j
h_2 : ¬i_1 = j_1
h_3 : j_1 ∉ some i
h_4 : i_1 = j
⊢ 0 = HSub.hSub (α := α) 0 0 - 0 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∉ some j
h_2 : ¬i_1 = j_1
h_3 : j_1 ∉ some i
h_4 : ¬i_1 = j
h_5 : Membership.mem (γ := Option n) none j_1
⊢ 0 = HSub.hSub (α := α) 0 0 - 1 + 0 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : i_1 = i
h_1 : j_1 ∉ some j
h_2 : ¬i_1 = j_1
h_3 : j_1 ∉ some i
h_4 : ¬i_1 = j
h_5 : j_1 ∉ none
⊢ 0 = HSub.hSub (α := α) 0 0 - 0 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∈ some i
h_3 : i_1 = j_1
h_4 : Membership.mem (γ := Option n) none j_1
h_5 : j_1 ∈ some j
⊢ 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∈ some i
h_3 : i_1 = j_1
h_4 : Membership.mem (γ := Option n) none j_1
h_5 : j_1 ∉ some j
⊢ 1 = HSub.hSub (α := α) 1 1 - 0 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∈ some i
h_3 : i_1 = j_1
h_4 : j_1 ∉ none
h_5 : j_1 ∈ some j
⊢ 1 = HSub.hSub (α := α) 1 0 - 1 + 0 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∈ some i
h_3 : i_1 = j_1
h_4 : j_1 ∉ none
h_5 : j_1 ∉ some j
⊢ 1 = HSub.hSub (α := α) 1 0 - 0 + 0 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∈ some i
h_3 : ¬i_1 = j_1
h_4 : Membership.mem (γ := Option n) none j_1
h_5 : j_1 ∈ some j
⊢ 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∈ some i
h_3 : ¬i_1 = j_1
h_4 : Membership.mem (γ := Option n) none j_1
h_5 : j_1 ∉ some j
⊢ 1 = HSub.hSub (α := α) 0 1 - 0 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∈ some i
h_3 : ¬i_1 = j_1
h_4 : j_1 ∉ none
h_5 : j_1 ∈ some j
⊢ 1 = HSub.hSub (α := α) 0 0 - 1 + 0 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∈ some i
h_3 : ¬i_1 = j_1
h_4 : j_1 ∉ none
h_5 : j_1 ∉ some j
⊢ 1 = HSub.hSub (α := α) 0 0 - 0 + 0 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∉ some i
h_3 : i_1 = j_1
h_4 : Membership.mem (γ := Option n) none j_1
h_5 : j_1 ∈ some j
⊢ 0 = HSub.hSub (α := α) 1 1 - 1 + 1 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∉ some i
h_3 : i_1 = j_1
h_4 : Membership.mem (γ := Option n) none j_1
h_5 : j_1 ∉ some j
⊢ 0 = HSub.hSub (α := α) 1 1 - 0 + 1 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∉ some i
h_3 : i_1 = j_1
h_4 : j_1 ∉ none
h_5 : j_1 ∈ some j
⊢ 0 = HSub.hSub (α := α) 1 0 - 1 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∉ some i
h_3 : i_1 = j_1
h_4 : j_1 ∉ none
h_5 : j_1 ∉ some j
⊢ 0 = HSub.hSub (α := α) 1 0 - 0 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∉ some i
h_3 : ¬i_1 = j_1
h_4 : Membership.mem (γ := Option n) none j_1
h_5 : j_1 ∈ some j
⊢ 0 = HSub.hSub (α := α) 0 1 - 1 + 1 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∉ some i
h_3 : ¬i_1 = j_1
h_4 : Membership.mem (γ := Option n) none j_1
h_5 : j_1 ∉ some j
⊢ 0 = HSub.hSub (α := α) 0 1 - 0 + 1 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∉ some i
h_3 : ¬i_1 = j_1
h_4 : j_1 ∉ none
h_5 : j_1 ∈ some j
⊢ 0 = HSub.hSub (α := α) 0 0 - 1 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : i_1 = j
h_2 : j_1 ∉ some i
h_3 : ¬i_1 = j_1
h_4 : j_1 ∉ none
h_5 : j_1 ∉ some j
⊢ 0 = HSub.hSub (α := α) 0 0 - 0 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : ¬i_1 = j
h_2 : j_1 ∈ some i_1
h_3 : i_1 = j_1
h_4 : Membership.mem (γ := Option n) none j_1
⊢ 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : ¬i_1 = j
h_2 : j_1 ∈ some i_1
h_3 : i_1 = j_1
h_4 : j_1 ∉ none
⊢ 1 = HSub.hSub (α := α) 1 0 - 0 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : ¬i_1 = j
h_2 : j_1 ∈ some i_1
h_3 : ¬i_1 = j_1
h_4 : Membership.mem (γ := Option n) none j_1
⊢ 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : ¬i_1 = j
h_2 : j_1 ∈ some i_1
h_3 : ¬i_1 = j_1
h_4 : j_1 ∉ none
⊢ 1 = HSub.hSub (α := α) 0 0 - 0 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : ¬i_1 = j
h_2 : j_1 ∉ some i_1
h_3 : i_1 = j_1
h_4 : Membership.mem (γ := Option n) none j_1
⊢ 0 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : ¬i_1 = j
h_2 : j_1 ∉ some i_1
h_3 : i_1 = j_1
h_4 : j_1 ∉ none
⊢ 0 = HSub.hSub (α := α) 1 0 - 0 + 0 + 0

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : ¬i_1 = j
h_2 : j_1 ∉ some i_1
h_3 : ¬i_1 = j_1
h_4 : Membership.mem (γ := Option n) none j_1
⊢ 0 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.PEquiv
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
h : ¬i_1 = i
h_1 : ¬i_1 = j
h_2 : j_1 ∉ some i_1
h_3 : ¬i_1 = j_1
h_4 : j_1 ∉ none
⊢ 0 = HSub.hSub (α := α) 0 0 - 0 + 0 + 0

Tactic:
simp_all
-- 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 k
inst_2 : DecidableEq m
inst_3 : DecidableEq n
inst_4 : NonAssocSemiring α
a : m
b : n
c : k
rw : Eq (α := Matrix m k α) ((single a b).trans (single b c)).toMatrix (single a c).toMatrix
rw₁ rw₂ : Eq (α := Matrix m k α) (single a c).toMatrix (single a c).toMatrix
⊢ HMul.hMul (α := Matrix m n α) (β := Matrix n k α) (single a b).toMatrix (single b c).toMatrix = (single a c).toMatrix

Tactic:
rw [← toMatrix_trans, single_trans_single]

Premises used: PEquiv.single_trans_single, PEquiv.toMatrix_trans