awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : NonAssocSemiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
a :
  Eq.{u_5 + 1} (α := α)
    (if Membership.mem (γ := Option n) (Option.bind.{u_3, u_4} (α := m) none (⇑g : (a : m) → Option n)) j then 1
      else 0 :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0
        (fun (val : m) ↦ if Membership.mem (γ := Option n) ((g : (a : m) → Option n) val : Option n) j then 1 else 0)
        none :
      α)
⊢ Eq.{u_5 + 1} (α := α)
    (if
          Membership.mem (γ := Option n)
            (Option.bind.{u_3, u_4} (α := m) ((f : (a : l) → Option m) i) (⇑g : (a : m) → Option n)) j then
        1
      else 0 :
      α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0
        (fun (val : m) ↦ if Membership.mem (γ := Option n) ((g : (a : m) → Option n) val : Option n) j then 1 else 0)
        ((f : (a : l) → Option m) i) :
      α)
have a₁ : ∀ (val : m),
  Eq.{u_5 + 1} (α := α)
    (if Membership.mem (γ := Option n) ((some val).bind (⇑g : (a : m) → Option n)) j then 1 else 0 : α)
    (Option.rec (motive := fun (x : Option m) ↦ α) 0
        (fun (val : m) ↦ if Membership.mem (γ := Option n) ((g : (a : m) → Option n) val : Option n) j then 1 else 0)
        (some val) :
      α)
Tactic: cases f i
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
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
⊢ Eq (α := Matrix m n α) f.toMatrix g.toMatrix → f = g
have refine : ¬f = g → ¬Eq (α := Matrix m n α) f.toMatrix g.toMatrix
Tactic: refine not_imp_not.1 ?_
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
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
⊢ ¬f = g → ¬Eq (α := Matrix m n α) f.toMatrix g.toMatrix
have simp : ∀ (x : m),
  ¬Eq.{u_4 + 1} (α := Option n) ((f : (a : m) → Option n) x : Option n) ((g : (a : m) → Option n) x : Option n) →
    ∃ (x : m) (x_1 : n),
      ¬Eq.{u_5 + 1} (α := α)
          (if Membership.mem (γ := Option n) ((f : (a : m) → Option n) x : Option n) x_1 then 1 else 0)
          (if Membership.mem (γ := Option n) ((g : (a : m) → Option n) x : Option n) x_1 then 1 else 0)
Tactic: simp only [Matrix.ext_iff.symm, toMatrix_apply, PEquiv.ext_iff, not_forall, exists_imp]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
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)
⊢ ∃ (x : m) (x_1 : n),
    ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) ((f : (a : m) → Option n) x : Option n) x_1 then 1 else 0)
        (if Membership.mem (γ := Option n) ((g : (a : m) → Option n) x : Option n) x_1 then 1 else 0)
have h : ∃ (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: use i
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases hf : f i with - | fi
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases hf : f i with - | fi
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases hg : g i with - | gi
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases hg : g i with - | gi
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (hypothesis)
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)
⊢ ∃ (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)
have hi₁ : ¬Eq.{u_4 + 1} (α := Option n) none none
Tactic: rw [hf, hg] at hi
Cleared hypotheses: hi, hf, hg
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
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
⊢ ∃ (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)
have h : ¬Eq.{u_5 + 1} (α := α) (if Membership.mem (γ := Option n) none gi then 1 else 0) (if gi ∈ some gi then 1 else 0)
Tactic: use gi
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use fi
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j : n
⊢ (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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j 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
have 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
Tactic: dsimp [toMatrix, single, Equiv.swap_apply_def, Equiv.toPEquiv, one_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
⊢ (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
have pos : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
pos : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
⊢ (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
have pos₁ : i_1 = i →
  j_1 ∈ some j →
    i_1 = j_1 →
      j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
pos : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
pos₁ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
⊢ (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
have neg : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 1 - 0 + 1 + 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
pos : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
pos₁ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
neg : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 1 - 0 + 1 + 0
⊢ (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
have pos₂ : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
pos : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
pos₁ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
neg : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 1 - 0 + 1 + 0
pos₂ : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 0
⊢ (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
have pos₃ : i_1 = i →
  j_1 ∈ some j →
    i_1 = j_1 →
      j_1 ∉ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
pos : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
pos₁ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
neg : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 1 - 0 + 1 + 0
pos₂ : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 0
pos₃ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∉ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 1
⊢ (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
have neg₁ : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 0 - 0 + 1 + 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
pos : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
pos₁ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
neg : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 1 - 0 + 1 + 0
pos₂ : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 0
pos₃ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∉ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 1
neg₁ :
  i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 0 - 0 + 1 + 0
⊢ (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
have pos₄ : i_1 = i → j_1 ∈ some j → ¬i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
pos : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
pos₁ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
neg : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 1 - 0 + 1 + 0
pos₂ : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 0
pos₃ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∉ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 1
neg₁ :
  i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 0 - 0 + 1 + 0
pos₄ : i_1 = i → j_1 ∈ some j → ¬i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1
⊢ (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
have pos₅ : i_1 = i →
  j_1 ∈ some j →
    ¬i_1 = j_1 →
      j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
pos : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
pos₁ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
neg : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 1 - 0 + 1 + 0
pos₂ : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 0
pos₃ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∉ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 1
neg₁ :
  i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 0 - 0 + 1 + 0
pos₄ : i_1 = i → j_1 ∈ some j → ¬i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1
pos₅ :
  i_1 = i →
    j_1 ∈ some j →
      ¬i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1
⊢ (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
have neg₂ : i_1 = i → j_1 ∈ some j → ¬i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 0 1 - 0 + 1 + 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.PEquiv (goal)
Goal:
n : Type u_4
α : Type u_5
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j i_1 j_1 : n
pos : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
pos₁ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 1 - 1 + 1 + 1
neg : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 1 - 0 + 1 + 0
pos₂ : i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → i_1 = j → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 0
pos₃ :
  i_1 = i →
    j_1 ∈ some j →
      i_1 = j_1 →
        j_1 ∉ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 1 0 - 1 + 1 + 1
neg₁ :
  i_1 = i → j_1 ∈ some j → i_1 = j_1 → j_1 ∉ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 1 0 - 0 + 1 + 0
pos₄ : i_1 = i → j_1 ∈ some j → ¬i_1 = j_1 → j_1 ∈ some i → i_1 = j → 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1
pos₅ :
  i_1 = i →
    j_1 ∈ some j →
      ¬i_1 = j_1 →
        j_1 ∈ some i → ¬i_1 = j → Membership.mem (γ := Option n) none j_1 → 1 = HSub.hSub (α := α) 0 1 - 1 + 1 + 1
neg₂ :
  i_1 = i → j_1 ∈ some j → ¬i_1 = j_1 → j_1 ∈ some i → ¬i_1 = j → j_1 ∉ none → 1 = HSub.hSub (α := α) 0 1 - 0 + 1 + 0
⊢ (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
have pos₆ : i_1 = i → j_1 ∈ some j → ¬i_1 = j_1 → j_1 ∉ some i → i_1 = j → 1 = HSub.hSub (α := α) 0 0 - 1 + 1 + 0
Tactic: split_ifs