awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
R : Type u_7
α : Type v
inst : DecidableEq n
inst_1 : Zero α
inst_2 : SMulZeroClass R α
r : R
d : n → α
i j : n
pos : ∀ (h : i = j), diagonal (r • d) i j = (r • diagonal d) i j
⊢ diagonal (r • d) i j = (r • diagonal d) i j
have neg : ∀ (h : ¬i = j), diagonal (r • d) i j = (r • diagonal d) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NegZeroClass α
d : n → α
⊢ -diagonal d = diagonal fun (i : n) ↦ -d i
have a : ∀ (i j : n), (-diagonal d) i j = diagonal (fun (i : n) ↦ -d i) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NegZeroClass α
d : n → α
i j : n
⊢ (-diagonal d) i j = diagonal (fun (i : n) ↦ -d i) i j
have pos : ∀ (h : i = j), (-diagonal d) i j = diagonal (fun (i : n) ↦ -d i) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : NegZeroClass α
d : n → α
i j : n
pos : ∀ (h : i = j), (-diagonal d) i j = diagonal (fun (i : n) ↦ -d i) i j
⊢ (-diagonal d) i j = diagonal (fun (i : n) ↦ -d i) i j
have neg : ∀ (h : ¬i = j), (-diagonal d) i j = diagonal (fun (i : n) ↦ -d i) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : SubNegZeroMonoid α
d₁ d₂ : n → α
⊢ diagonal d₁ - diagonal d₂ = diagonal fun (i : n) ↦ d₁ i - d₂ i
have a : ∀ (i j : n), (diagonal d₁ - diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i - d₂ i) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i - d₂ i) i j
have pos : ∀ (h : i = j), (diagonal d₁ - diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i - d₂ i) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
pos : ∀ (h : i = j), (diagonal d₁ - diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i - d₂ i) i j
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i - d₂ i) i j
have neg : ∀ (h : ¬i = j), (diagonal d₁ - diagonal d₂) i j = diagonal (fun (i : n) ↦ d₁ i - d₂ i) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
⊢ Membership.mem (γ := Set (Matrix n n α)) S.matrix (diagonal d) ↔ ∀ (i : n), d i ∈ S
have simp : (∀ (i j : n), (if i = j then d i else 0) ∈ S) ↔ ∀ (i : n), d i ∈ S
Tactic: simp only [Set.mem_matrix, diagonal, of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
i j : n
| (if i = j then d i else 0) ∈ S
have rw : (i = j → d i ∈ S) ∧ (¬i = j → 0 ∈ S)
Tactic: rw [ite_mem]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
⊢ (∀ (i j : n), (if i = j then d i else 0) ∈ S) ↔ ∀ (i : n), d i ∈ S
have conv_lhs : (∀ (i j : n), (i = j → d i ∈ S) ∧ (¬i = j → 0 ∈ S)) ↔ ∀ (i : n), d i ∈ S
Tactic: conv_lhs => intro _ _; rw [ite_mem]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : Zero β
f : α → β
h : f 0 = 0
d : n → α
⊢ (diagonal d).map f = diagonal fun (m : n) ↦ f (d m)
have a : ∀ (i j : n), (diagonal d).map f i j = diagonal (fun (m : n) ↦ f (d m)) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : Zero β
f : α → β
h : f 0 = 0
d : n → α
i j : n
⊢ (diagonal d).map f i j = diagonal (fun (m : n) ↦ f (d m)) i j
have a : f (if i = j then d i else 0) = if i = j then f (d i) else 0
Tactic: simp only [diagonal_apply, map_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : Zero β
f : α → β
h : f 0 = 0
d : n → α
i j : n
⊢ f (if i = j then d i else 0) = if i = j then f (d i) else 0
have pos : i = j → f (d i) = f (d i)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : Zero β
f : α → β
h : f 0 = 0
d : n → α
i j : n
pos : i = j → f (d i) = f (d i)
⊢ f (if i = j then d i else 0) = if i = j then f (d i) else 0
have neg : ¬i = j → f 0 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
i j : n
d : ℕ
⊢ Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (↑(if i = j then d else 0) : α)
have rw : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else (↑0 : α))
Tactic: rw [Nat.cast_ite, Nat.cast_zero, ← diagonal_natCast, diagonal_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
i j : n
d : ℕ
rw : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else (↑0 : α))
⊢ Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (↑(if i = j then d else 0) : α)
have rw₁ : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else 0)
Tactic: rw [Nat.cast_ite, Nat.cast_zero, ← diagonal_natCast, diagonal_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
i j : n
d : ℕ
rw : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else (↑0 : α))
rw₁ : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else 0)
⊢ Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (↑(if i = j then d else 0) : α)
have rw₂ : Eq.{v + 1} (α := α) (diagonal (fun (x : n) ↦ (↑d : α)) i j) (if i = j then (↑d : α) else 0)
Tactic: rw [Nat.cast_ite, Nat.cast_zero, ← diagonal_natCast, diagonal_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
i j : n
d : ℕ
rw : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else (↑0 : α))
rw₁ : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else 0)
rw₂ : Eq.{v + 1} (α := α) (diagonal (fun (x : n) ↦ (↑d : α)) i j) (if i = j then (↑d : α) else 0)
⊢ Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (↑(if i = j then d else 0) : α)
have rw₃ : Eq.{v + 1} (α := α) (if i = j then (↑d : α) else 0) (if i = j then (↑d : α) else 0)
Tactic: rw [Nat.cast_ite, Nat.cast_zero, ← diagonal_natCast, diagonal_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j : n
d : ℤ
⊢ Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (↑(if i = j then d else 0) : α)
have rw : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else (↑0 : α))
Tactic: rw [Int.cast_ite, Int.cast_zero, ← diagonal_intCast, diagonal_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j : n
d : ℤ
rw : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else (↑0 : α))
⊢ Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (↑(if i = j then d else 0) : α)
have rw₁ : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else 0)
Tactic: rw [Int.cast_ite, Int.cast_zero, ← diagonal_intCast, diagonal_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j : n
d : ℤ
rw : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else (↑0 : α))
rw₁ : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else 0)
⊢ Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (↑(if i = j then d else 0) : α)
have rw₂ : Eq.{v + 1} (α := α) (diagonal (fun (x : n) ↦ (↑d : α)) i j) (if i = j then (↑d : α) else 0)
Tactic: rw [Int.cast_ite, Int.cast_zero, ← diagonal_intCast, diagonal_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : AddGroupWithOne α
i j : n
d : ℤ
rw : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else (↑0 : α))
rw₁ : Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (if i = j then (↑d : α) else 0)
rw₂ : Eq.{v + 1} (α := α) (diagonal (fun (x : n) ↦ (↑d : α)) i j) (if i = j then (↑d : α) else 0)
⊢ Eq.{v + 1} (α := α) ((↑d : Matrix n n α) i j) (↑(if i = j then d else 0) : α)
have rw₃ : Eq.{v + 1} (α := α) (if i = j then (↑d : α) else 0) (if i = j then (↑d : α) else 0)
Tactic: rw [Int.cast_ite, Int.cast_zero, ← diagonal_intCast, diagonal_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
m : Type u_2
α : Type v
inst : Unique m
inst_1 : DecidableEq m
inst_2 : Zero α
d : m → α
⊢ diagonal d = (of : (a : m → m → α) → Matrix m m α) fun (x x_1 : m) ↦ d default
have a : ∀ (i j : m), diagonal d i j = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
m : Type u_2
α : Type v
inst : Unique m
inst_1 : DecidableEq m
inst_2 : Zero α
d : m → α
i j : m
⊢ diagonal d i j = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) i j
have a : diagonal d default j = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) default j
Tactic: rw [Subsingleton.elim i default, Subsingleton.elim j default, diagonal_apply_eq _ _, of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
m : Type u_2
α : Type v
inst : Unique m
inst_1 : DecidableEq m
inst_2 : Zero α
d : m → α
i j : m
a : diagonal d default j = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) default j
⊢ diagonal d i j = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) i j
have a₁ : diagonal d default default = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) default default
Tactic: rw [Subsingleton.elim i default, Subsingleton.elim j default, diagonal_apply_eq _ _, of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
m : Type u_2
α : Type v
inst : Unique m
inst_1 : DecidableEq m
inst_2 : Zero α
d : m → α
i j : m
a : diagonal d default j = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) default j
a₁ : diagonal d default default = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) default default
⊢ diagonal d i j = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) i j
have a₂ : d default = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) default default
Tactic: rw [Subsingleton.elim i default, Subsingleton.elim j default, diagonal_apply_eq _ _, of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
m : Type u_2
α : Type v
inst : Unique m
inst_1 : DecidableEq m
inst_2 : Zero α
d : m → α
i j : m
a : diagonal d default j = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) default j
a₁ : diagonal d default default = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) default default
a₂ : d default = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) default default
⊢ diagonal d i j = (of : (a : m → m → α) → Matrix m m α) (fun (x x_1 : m) ↦ d default) i j
have a₃ : d default = d default
Tactic: rw [Subsingleton.elim i default, Subsingleton.elim j default, diagonal_apply_eq _ _, of_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d : n → α
i : n
⊢ (diagonal d).col i = Pi.single (M := fun (j : n) ↦ α) i (d i)
have h : ∀ (x : n), (diagonal d).col i x = Pi.single (M := fun (j : n) ↦ α) i (d i) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
d : n → α
j : n
⊢ (diagonal d).row j = Pi.single (M := fun (j : n) ↦ α) j (d j)
have h : ∀ (x : n), (diagonal d).row j x = Pi.single (M := fun (j : n) ↦ α) j (d j) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Zero β
inst_4 : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
⊢ Eq (α := Matrix n n β) (map 1 f) 1
have a : ∀ (i j : n), map 1 f i j = 1 i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Zero β
inst_4 : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i j : n
⊢ map 1 f i j = 1 i j
have a : f (if i = j then 1 else 0) = if i = j then 1 else 0
Tactic: simp only [one_apply, map_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Zero β
inst_4 : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i j : n
⊢ f (if i = j then 1 else 0) = if i = j then 1 else 0
have pos : i = j → f 1 = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
β : Type w
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Zero β
inst_4 : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i j : n
pos : i = j → f 1 = 1
⊢ f (if i = j then 1 else 0) = if i = j then 1 else 0
have neg : ¬i = j → f 0 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
⊢ Eq (α := Matrix n n α) (diagonal fun (x : n) ↦ (↑0 : α)) 0
have rw : Eq (α := Matrix n n α) (diagonal fun (x : n) ↦ 0) 0
Tactic: rw [Nat.cast_zero, diagonal_zero]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : DecidableEq n
inst_1 : AddMonoidWithOne α
rw : Eq (α := Matrix n n α) (diagonal fun (x : n) ↦ 0) 0
⊢ Eq (α := Matrix n n α) (diagonal fun (x : n) ↦ (↑0 : α)) 0
have rw₁ : Eq (α := Matrix n n α) 0 0
Tactic: rw [Nat.cast_zero, diagonal_zero]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
n_1 : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : DecidableEq n_1
inst_1 : AddMonoidWithOne α
n : ℕ
⊢ (diagonal fun (x : n_1) ↦ (↑(n + 1) : α)) = HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1
have rw : (diagonal fun (x : n_1) ↦ HAdd.hAdd (α := α) (↑n : α) 1) =
  HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1
Tactic: rw [Nat.cast_succ, ← diagonal_add, diagonal_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
n_1 : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : DecidableEq n_1
inst_1 : AddMonoidWithOne α
n : ℕ
rw :
  (diagonal fun (x : n_1) ↦ HAdd.hAdd (α := α) (↑n : α) 1) =
    HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1
⊢ (diagonal fun (x : n_1) ↦ (↑(n + 1) : α)) = HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1
have rw₁ : HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) (diagonal fun (x : n_1) ↦ 1) =
  HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1
Tactic: rw [Nat.cast_succ, ← diagonal_add, diagonal_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
n_1 : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : DecidableEq n_1
inst_1 : AddMonoidWithOne α
n : ℕ
rw :
  (diagonal fun (x : n_1) ↦ HAdd.hAdd (α := α) (↑n : α) 1) =
    HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1
rw₁ :
  HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) (diagonal fun (x : n_1) ↦ 1) =
    HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1
⊢ (diagonal fun (x : n_1) ↦ (↑(n + 1) : α)) = HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1
have rw₂ : HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1 =
  HAdd.hAdd (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) 1
Tactic: rw [Nat.cast_succ, ← diagonal_add, diagonal_one]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
n_1 : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : DecidableEq n_1
inst_1 : AddGroupWithOne α
n : ℕ
⊢ Eq (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑(↑n : ℤ) : α)) (diagonal fun (x : n_1) ↦ (↑n : α))
have rw : Eq (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑n : α)) (diagonal fun (x : n_1) ↦ (↑n : α))
Tactic: rw [Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
n_1 : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : DecidableEq n_1
inst_1 : AddGroupWithOne α
n : ℕ
⊢ Eq (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑(Int.negSucc n) : α))
    (-diagonal fun (x : n_1) ↦ (↑(n + 1) : α))
have rw : Eq (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ -(↑(n + 1) : α)) (-diagonal fun (x : n_1) ↦ (↑(n + 1) : α))
Tactic: rw [Int.cast_negSucc, diagonal_neg]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
n_1 : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst : DecidableEq n_1
inst_1 : AddGroupWithOne α
n : ℕ
rw : Eq (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ -(↑(n + 1) : α)) (-diagonal fun (x : n_1) ↦ (↑(n + 1) : α))
⊢ Eq (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ (↑(Int.negSucc n) : α))
    (-diagonal fun (x : n_1) ↦ (↑(n + 1) : α))
have rw₁ : Eq (α := Matrix n_1 n_1 α) (diagonal fun (x : n_1) ↦ -(↑(n + 1) : α)) (diagonal fun (i : n_1) ↦ -(↑(n + 1) : α))
Tactic: rw [Int.cast_negSucc, diagonal_neg]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
M : Matrix n n α
v : n → α
⊢ M = (diagonal v)ᵀ ↔ M = diagonal v
have rw : M = diagonal v ↔ M = diagonal v
Tactic: rw [diagonal_transpose]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
⊢ (diagonal d).submatrix e e i j = diagonal (d ∘ e) i j
have rw : diagonal d (e i) (e j) = diagonal (d ∘ e) i j
Tactic: rw [submatrix_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
have pos : ∀ (h : i = j), diagonal d (e i) (e j) = diagonal (d ∘ e) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
pos : ∀ (h : i = j), diagonal d (e i) (e j) = diagonal (d ∘ e) i j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
have neg : ∀ (h : ¬i = j), diagonal d (e i) (e j) = diagonal (d ∘ e) i j
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
have pos : diagonal d (e j) (e j) = diagonal (d ∘ e) j j
Tactic: rw [h, diagonal_apply_eq, diagonal_apply_eq, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
pos : diagonal d (e j) (e j) = diagonal (d ∘ e) j j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
have pos₁ : d (e j) = diagonal (d ∘ e) j j
Tactic: rw [h, diagonal_apply_eq, diagonal_apply_eq, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
pos : diagonal d (e j) (e j) = diagonal (d ∘ e) j j
pos₁ : d (e j) = diagonal (d ∘ e) j j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
have pos₂ : d (e j) = (d ∘ e) j
Tactic: rw [h, diagonal_apply_eq, diagonal_apply_eq, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
pos : diagonal d (e j) (e j) = diagonal (d ∘ e) j j
pos₁ : d (e j) = diagonal (d ∘ e) j j
pos₂ : d (e j) = (d ∘ e) j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
have pos₃ : d (e j) = d (e j)
Tactic: rw [h, diagonal_apply_eq, diagonal_apply_eq, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : ¬i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
have neg : diagonal d (e i) (e j) = 0
Tactic: rw [diagonal_apply_ne _ h, diagonal_apply_ne _ (he.ne h)]
-- Lean 4 proof step from Mathlib.Data.Matrix.Diagonal (goal)
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : Zero α
inst_1 : DecidableEq m
inst_2 : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : ¬i = j
neg : diagonal d (e i) (e j) = 0
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j
have neg₁ : Eq.{v + 1} (α := α) 0 0
Tactic: rw [diagonal_apply_ne _ h, diagonal_apply_ne _ (he.ne h)]