awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
m : Type u_2
inst_2 : Semiring R
inst_3 : StarRing R
inst_4 : Fintype m
inst_5 : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : Membership.mem (γ := Submonoid (Matrix n n R)) (unitary (Matrix n n R)) U₁
hU₂ : Membership.mem (γ := Submonoid (Matrix m m R)) (unitary (Matrix m m R)) U₂
i j : n × m
left : Eq.{u_1 + 1} (α := R) (∑ x : m, (∑ i_1 : n, star U₂ i.2 x * (star U₁ i.1 i_1 * U₁ i_1 j.1)) * U₂ x j.2) (1 i j)
left₁ : Eq.{u_1 + 1} (α := R) (∑ x : m, (star U₂ i.2 x * ∑ i_1 : n, star U₁ i.1 i_1 * U₁ i_1 j.1) * U₂ x j.2) (1 i j)
left₂ : Eq.{u_1 + 1} (α := R) (∑ x : m, star U₂ i.2 x * (star U₁ * U₁) i.1 j.1 * U₂ x j.2) (1 i j)
left₃ : Eq.{u_1 + 1} (α := R) (∑ x : m, star U₂ i.2 x * 1 i.1 j.1 * U₂ x j.2) (1 i j)
left₄ :
  Eq.{u_1 + 1} (α := R) (∑ x : m, (star U₂ i.2 x * if i.1 = j.1 then 1 else 0) * U₂ x j.2) (if i = j then 1 else 0)
left₅ : Eq.{u_1 + 1} (α := R) (∑ x : m, (if i.1 = j.1 then star U₂ i.2 x else 0) * U₂ x j.2) (if i = j then 1 else 0)
left₆ :
  Eq.{u_1 + 1} (α := R) (∑ x : m, if i.1 = j.1 then star U₂ i.2 x * U₂ x j.2 else 0 * U₂ x j.2) (if i = j then 1 else 0)
left₇ : Eq.{u_1 + 1} (α := R) (∑ x : m, if i.1 = j.1 then star U₂ i.2 x * U₂ x j.2 else 0) (if i = j then 1 else 0)
left₈ :
  Eq.{u_1 + 1} (α := R) (if i.1 = j.1 then ∑ x : m, star U₂ i.2 x * U₂ x j.2 else ∑ x : m, 0) (if i = j then 1 else 0)
left₉ : (if i.1 = j.1 then (star U₂ * U₂) i.2 j.2 else ∑ x : m, 0) = if i = j then 1 else 0
left₁₀ : Eq.{u_1 + 1} (α := R) (if i.1 = j.1 then 1 i.2 j.2 else ∑ x : m, 0) (if i = j then 1 else 0)
left₁₁ : Eq.{u_1 + 1} (α := R) (if i.1 = j.1 then if i.2 = j.2 then 1 else 0 else ∑ x : m, 0) (if i = j then 1 else 0)
left₁₂ : Eq.{u_1 + 1} (α := R) (if i.1 = j.1 then if i.2 = j.2 then 1 else 0 else 0) (if i = j then 1 else 0)
⊢ Eq.{u_1 + 1} (α := R) (∑ y : m, ∑ x : n, star U₂ i.2 y * (star U₁ i.1 x * U₁ x j.1) * U₂ y j.2) (1 i j)
have left₁₃ : Eq.{u_1 + 1} (α := R) (if i.1 = j.1 ∧ i.2 = j.2 then 1 else 0) (if i = j then 1 else 0)
Tactic: simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ← Matrix.mul_apply, hU₁.1, Matrix.one_apply,
      mul_boole, ite_mul, zero_mul, Finset.sum_ite_irrel, ← Matrix.mul_apply, hU₂.1,
      Matrix.one_apply, Finset.sum_const_zero, ← ite_and, Prod.eq_iff_fst_eq_snd_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (hypothesis)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
A : Type u_2
B : Type u_3
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : StarRing A
inst_8 : StarRing B
inst_9 : StarRing R
inst_10 : StarModule R A
inst_11 : StarModule R B
m : Type u_4
inst_12 : Fintype m
inst_13 : DecidableEq m
U : Matrix m m A
V : Matrix n n B
hU : Membership.mem (γ := Submonoid (Matrix m m A)) (unitary (Matrix m m A)) U
hV : Membership.mem (γ := Submonoid (Matrix n n B)) (unitary (Matrix n n B)) V
⊢ Membership.mem (γ := Submonoid (Matrix (m × n) (m × n) (A ⊗[R] B))) (unitary (Matrix (m × n) (m × n) (A ⊗[R] B)))
    (U ⊗ₖₜ[R] V)
have hU₁ : Uᴴ * U = 1 ∧ U * Uᴴ = 1
Tactic: simp_rw [Unitary.mem_iff, star_eq_conjTranspose] at hU hV ⊢
Cleared hypotheses: hU, hV
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (hypothesis)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
A : Type u_2
B : Type u_3
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : StarRing A
inst_8 : StarRing B
inst_9 : StarRing R
inst_10 : StarModule R A
inst_11 : StarModule R B
m : Type u_4
inst_12 : Fintype m
inst_13 : DecidableEq m
U : Matrix m m A
V : Matrix n n B
hU : Membership.mem (γ := Submonoid (Matrix m m A)) (unitary (Matrix m m A)) U
hV : Membership.mem (γ := Submonoid (Matrix n n B)) (unitary (Matrix n n B)) V
hU₁ : Uᴴ * U = 1 ∧ U * Uᴴ = 1
⊢ Membership.mem (γ := Submonoid (Matrix (m × n) (m × n) (A ⊗[R] B))) (unitary (Matrix (m × n) (m × n) (A ⊗[R] B)))
    (U ⊗ₖₜ[R] V)
have hV₁ : Vᴴ * V = 1 ∧ V * Vᴴ = 1
Tactic: simp_rw [Unitary.mem_iff, star_eq_conjTranspose] at hU hV ⊢
Cleared hypotheses: hU, hV
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
⊢ Eq (α := n → α) ((toLin' A⁻¹ ∘ₗ toLin' A : (a : n → α) → n → α) x : n → α)
    ((toLin' (A⁻¹ * A) : (a : n → α) → n → α) x : n → α)
have rw : Eq (α := n → α) ((toLin' (A⁻¹ * A) : (a : n → α) → n → α) x : n → α)
  ((toLin' (A⁻¹ * A) : (a : n → α) → n → α) x : n → α)
Tactic: rw [← toLin'_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
⊢ (toLin' (A⁻¹ * A) : (a : n → α) → n → α) x = x
have rw : (toLin' 1 : (a : n → α) → n → α) x = x
Tactic: rw [inv_mul_cancel, toLin'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
rw : (toLin' 1 : (a : n → α) → n → α) x = x
⊢ (toLin' (A⁻¹ * A) : (a : n → α) → n → α) x = x
have rw₁ : (LinearMap.id : (a : n → α) → n → α) x = x
Tactic: rw [inv_mul_cancel, toLin'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
rw : (toLin' 1 : (a : n → α) → n → α) x = x
rw₁ : (LinearMap.id : (a : n → α) → n → α) x = x
⊢ (toLin' (A⁻¹ * A) : (a : n → α) → n → α) x = x
have rw₂ : x = x
Tactic: rw [inv_mul_cancel, toLin'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
⊢ Eq (α := n → α) ((toLin' A ∘ₗ toLin' A⁻¹ : (a : n → α) → n → α) x : n → α)
    ((toLin' (A * A⁻¹) : (a : n → α) → n → α) x : n → α)
have rw : Eq (α := n → α) ((toLin' (A * A⁻¹) : (a : n → α) → n → α) x : n → α)
  ((toLin' (A * A⁻¹) : (a : n → α) → n → α) x : n → α)
Tactic: rw [← toLin'_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
⊢ (toLin' (A * A⁻¹) : (a : n → α) → n → α) x = x
have rw : (toLin' 1 : (a : n → α) → n → α) x = x
Tactic: rw [mul_inv_cancel, toLin'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
rw : (toLin' 1 : (a : n → α) → n → α) x = x
⊢ (toLin' (A * A⁻¹) : (a : n → α) → n → α) x = x
have rw₁ : (LinearMap.id : (a : n → α) → n → α) x = x
Tactic: rw [mul_inv_cancel, toLin'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
rw : (toLin' 1 : (a : n → α) → n → α) x = x
rw₁ : (LinearMap.id : (a : n → α) → n → α) x = x
⊢ (toLin' (A * A⁻¹) : (a : n → α) → n → α) x = x
have rw₂ : x = x
Tactic: rw [mul_inv_cancel, toLin'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
⊢ Eq (α := (n → α) →ₗ[α] n → α) (↑(toGL 1) : (n → α) →ₗ[α] n → α) (↑1 : (n → α) →ₗ[α] n → α)
have simp : Eq (α := (n → α) →ₗ[α] n → α) LinearMap.id (↑1 : (n → α) →ₗ[α] n → α)
Tactic: simp only [coe_toGL, toLin'_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A B : ↥(unitaryGroup n α)
⊢ (↑(toGL (A * B)) : (n → α) →ₗ[α] n → α) = (↑(toGL A * toGL B) : (n → α) →ₗ[α] n → α)
have simp : toLin' A ∘ₗ toLin' B = (↑(toGL A * toGL B) : (n → α) →ₗ[α] n → α)
Tactic: simp only [coe_toGL, toLin'_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : Matrix n n α
| Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) U
have rw : star U * U = 1
Tactic: rw [mem_unitaryGroup_iff']
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : Matrix n n α
⊢ Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) Uᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) U
have conv_rhs : Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) Uᵀ ↔ star U * U = 1
Tactic: conv_rhs => rw [mem_unitaryGroup_iff']
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : Matrix n n α
⊢ Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) Uᵀ ↔ star U * U = 1
have rw : (star U * U)ᵀᵀ = 1ᵀ ↔ star U * U = 1
Tactic: rw [mem_unitaryGroup_iff, show star Uᵀ = (star U)ᵀ by rfl, ← transpose_mul, ← transpose_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : ↥(unitaryGroup n α)
⊢ (map_star U)⁻¹ = transpose U
have a : ∀ (i j : n), (↑(map_star U)⁻¹ : Matrix n n α) i j = (↑(transpose U) : Matrix n n α) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (hypothesis)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(specialUnitaryGroup n α)
⊢ star (↑A : Matrix n n α) ∈ (↑(MonoidHom.mker (F := Matrix n n α →* α) detMonoidHom) : Set (Matrix n n α))
have this : (↑A : Matrix n n α) ∈ (↑(MonoidHom.mker (F := Matrix n n α →* α) detMonoidHom) : Set (Matrix n n α))
Tactic: have := A.prop.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
R : Type v
inst : CommRing R
a b c d : R
⊢ Membership.mem (α := Matrix (Fin 2) (Fin 2) R) (γ := Submonoid (Matrix (Fin 2) (Fin 2) R))
      (specialOrthogonalGroup (Fin 2) R) (!![a, b; c, d] : Matrix (Fin 2) (Fin 2) R) ↔
    a = d ∧ b = -c ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 1
have trans : Membership.mem (α := Matrix (Fin 2) (Fin 2) R) (γ := Submonoid (Matrix (Fin 2) (Fin 2) R))
    (specialOrthogonalGroup (Fin 2) R) (!![a, b; c, d] : Matrix (Fin 2) (Fin 2) R) ↔
  ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
Tactic: trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧
    c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
R : Type v
inst : CommRing R
a b c d : R
trans :
  Membership.mem (α := Matrix (Fin 2) (Fin 2) R) (γ := Submonoid (Matrix (Fin 2) (Fin 2) R))
      (specialOrthogonalGroup (Fin 2) R) (!![a, b; c, d] : Matrix (Fin 2) (Fin 2) R) ↔
    ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
⊢ Membership.mem (α := Matrix (Fin 2) (Fin 2) R) (γ := Submonoid (Matrix (Fin 2) (Fin 2) R))
      (specialOrthogonalGroup (Fin 2) R) (!![a, b; c, d] : Matrix (Fin 2) (Fin 2) R) ↔
    a = d ∧ b = -c ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 1
have trans₁ : ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1 ↔
  a = d ∧ b = -c ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 1
Tactic: trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧
    c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
R : Type v
inst : CommRing R
M : Matrix (Fin 2) (Fin 2) R
⊢ Membership.mem (γ := Submonoid (Matrix (Fin 2) (Fin 2) R)) (specialOrthogonalGroup (Fin 2) R) M ↔
    M 0 0 = M 1 1 ∧ M 0 1 = -M 1 0 ∧ HPow.hPow (β := ℕ) (M 0 0) 2 + HPow.hPow (β := ℕ) (M 0 1) 2 = 1
have rw : Membership.mem (γ := Submonoid (Matrix (Fin 2) (Fin 2) R)) (specialOrthogonalGroup (Fin 2) R) M.etaExpand ↔
  M.etaExpand 0 0 = M.etaExpand 1 1 ∧
    M.etaExpand 0 1 = -M.etaExpand 1 0 ∧
      HPow.hPow (β := ℕ) (M.etaExpand 0 0) 2 + HPow.hPow (β := ℕ) (M.etaExpand 0 1) 2 = 1
Tactic: rw [← M.etaExpand_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v0 : R
v : Fin n → R
⊢ Eq.{u_1 + 1} (α := Matrix (Fin (n + 1)) (Fin (n + 1)) R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v))
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ)) fun (i : Fin n) ↦
      Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j)
have a : ∀ (i j : Fin (n + 1)),
  Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) i j : R)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
        (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j) i j :
      R)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i j : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) i j : R)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
        (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j) i j :
      R)
have a : ∀ (i : Fin n),
  Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) i.succ j : R)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
        (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j) i.succ
        j :
      R)
Tactic: refine Fin.cases (by simp) (fun i => ?_) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i_1 j : Fin (n + 1)
i : Fin n
⊢ Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) i.succ j : R)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
        (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j) i.succ
        j :
      R)
have a : ∀ (j : Fin n),
  Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) i.succ j.succ : R)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
        (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j) i.succ
        j.succ :
      R)
Tactic: refine Fin.cases (by simp) (fun j => ?_) j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n.succ → R
| vandermonde v
have rw : Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v 0 ^ (↑j : ℕ)) fun (i : Fin n) ↦
  Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦
    tail (α := fun (i : Fin (n + 1)) ↦ R) v i * vandermonde (tail (α := fun (i : Fin (n + 1)) ↦ R) v) i j
Tactic: rw [← Fin.cons_self_tail v, vandermonde_cons]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n.succ → R
⊢ vandermonde v =
    (of :
        (a : (Fin n.succ → R) → ((i : Fin n) → Fin n.succ → R) → (i : Fin (n + 1)) → Fin n.succ → R) →
          Matrix (Fin n.succ → R) ((i : Fin n) → Fin n.succ → R) ((i : Fin (n + 1)) → Fin n.succ → R))
      (Fin.cons (α := fun (a : Fin n.succ) ↦ Fin n.succ → R) :
        (x : Fin n.succ → R) → (p : (i : Fin n) → Fin n.succ → R) → (i : Fin (n + 1)) → Fin n.succ → R)
      (fun (j : Fin n.succ) ↦ v 0 ^ (↑j : ℕ)) fun (i : Fin n) ↦
      Fin.cons (α := fun (a : Fin n.succ) ↦ R) 1 fun (j : Fin n) ↦
        v i.succ * vandermonde (tail (α := fun (i : Fin (n + 1)) ↦ R) v) i j
have conv_lhs : Eq.{u_1 + 1} (α := Matrix (Fin n.succ) (Fin n.succ) R)
  (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v 0 ^ (↑j : ℕ)) fun (i : Fin n) ↦
    Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦
      tail (α := fun (i : Fin (n + 1)) ↦ R) v i * vandermonde (tail (α := fun (i : Fin (n + 1)) ↦ R) v) i j)
  ((of :
      (a : (Fin n.succ → R) → ((i : Fin n) → Fin n.succ → R) → (i : Fin (n + 1)) → Fin n.succ → R) →
        Matrix (Fin n.succ → R) ((i : Fin n) → Fin n.succ → R) ((i : Fin (n + 1)) → Fin n.succ → R))
    (Fin.cons (α := fun (a : Fin n.succ) ↦ Fin n.succ → R) :
      (x : Fin n.succ → R) → (p : (i : Fin n) → Fin n.succ → R) → (i : Fin (n + 1)) → Fin n.succ → R)
    (fun (j : Fin n.succ) ↦ v 0 ^ (↑j : ℕ)) fun (i : Fin n) ↦
    Fin.cons (α := fun (a : Fin n.succ) ↦ R) 1 fun (j : Fin n) ↦
      v i.succ * vandermonde (tail (α := fun (i : Fin (n + 1)) ↦ R) v) i j)
Tactic: conv_lhs => rw [← Fin.cons_self_tail v, vandermonde_cons]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
⊢ rectVandermonde v w (n + 1) i = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n)
have h : ∀ (j : Fin (n + 1)), rectVandermonde v w (n + 1) i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
j : Fin (n + 1)
⊢ rectVandermonde v w (n + 1) i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
have h : rectVandermonde v w (n + 1) i (last n) = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) (last n)
Tactic: obtain rfl | hlt := j.le_last.eq_or_lt
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
j : Fin (n + 1)
h : rectVandermonde v w (n + 1) i (last n) = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) (last n)
⊢ rectVandermonde v w (n + 1) i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
have h₁ : ∀ (hlt : j < last n), rectVandermonde v w (n + 1) i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
Tactic: obtain rfl | hlt := j.le_last.eq_or_lt
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
hw : w i = 0
j : Fin (n + 1)
hlt : j < last n
⊢ rectVandermonde v w (n + 1) i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
have h : (↑j.rev : ℕ) ≠ 0
Tactic: rw [rectVandermonde_apply, Pi.single_eq_of_ne hlt.ne, hw, zero_pow, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n : ℕ
v w : Fin (n + 1) → K
i j : Fin (n + 1)
hw : w i ≠ 0
⊢ projVandermonde v w i j = v i ^ (↑j : ℕ) * w i ^ n / w i ^ (↑j : ℕ)
have rw : v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ) = v i ^ (↑j : ℕ) * w i ^ n / w i ^ (↑j : ℕ)
Tactic: rw [projVandermonde_apply, eq_div_iff (by simp [hw]), mul_assoc, ← pow_add, rev_add_cast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n : ℕ
v w : Fin (n + 1) → K
i j : Fin (n + 1)
hw : w i ≠ 0
rw : v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ) = v i ^ (↑j : ℕ) * w i ^ n / w i ^ (↑j : ℕ)
⊢ projVandermonde v w i j = v i ^ (↑j : ℕ) * w i ^ n / w i ^ (↑j : ℕ)
have rw₁ : v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ) * w i ^ (↑j : ℕ) = v i ^ (↑j : ℕ) * w i ^ n
Tactic: rw [projVandermonde_apply, eq_div_iff (by simp [hw]), mul_assoc, ← pow_add, rev_add_cast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n : ℕ
v w : Fin (n + 1) → K
i j : Fin (n + 1)
hw : w i ≠ 0
rw : v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ) = v i ^ (↑j : ℕ) * w i ^ n / w i ^ (↑j : ℕ)
rw₁ : v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ) * w i ^ (↑j : ℕ) = v i ^ (↑j : ℕ) * w i ^ n
⊢ projVandermonde v w i j = v i ^ (↑j : ℕ) * w i ^ n / w i ^ (↑j : ℕ)
have rw₂ : v i ^ (↑j : ℕ) * (w i ^ (↑j.rev : ℕ) * w i ^ (↑j : ℕ)) = v i ^ (↑j : ℕ) * w i ^ n
Tactic: rw [projVandermonde_apply, eq_div_iff (by simp [hw]), mul_assoc, ← pow_add, rev_add_cast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n : ℕ
v w : Fin (n + 1) → K
i j : Fin (n + 1)
hw : w i ≠ 0
rw : v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ) = v i ^ (↑j : ℕ) * w i ^ n / w i ^ (↑j : ℕ)
rw₁ : v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ) * w i ^ (↑j : ℕ) = v i ^ (↑j : ℕ) * w i ^ n
rw₂ : v i ^ (↑j : ℕ) * (w i ^ (↑j.rev : ℕ) * w i ^ (↑j : ℕ)) = v i ^ (↑j : ℕ) * w i ^ n
⊢ projVandermonde v w i j = v i ^ (↑j : ℕ) * w i ^ n / w i ^ (↑j : ℕ)
have rw₃ : v i ^ (↑j : ℕ) * w i ^ ((↑j.rev : ℕ) + (↑j : ℕ)) = v i ^ (↑j : ℕ) * w i ^ n
Tactic: rw [projVandermonde_apply, eq_div_iff (by simp [hw]), mul_assoc, ← pow_add, rev_add_cast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
K : Type u_2
inst : Field K
n : ℕ
v w : Fin (n + 1) → K
i j : Fin (n + 1)
hw : w i ≠ 0
rw : v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ) = v i ^ (↑j : ℕ) * w i ^ n / w i ^ (↑j : ℕ)
rw₁ : v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ) * w i ^ (↑j : ℕ) = v i ^ (↑j : ℕ) * w i ^ n
rw₂ : v i ^ (↑j : ℕ) * (w i ^ (↑j.rev : ℕ) * w i ^ (↑j : ℕ)) = v i ^ (↑j : ℕ) * w i ^ n
rw₃ : v i ^ (↑j : ℕ) * w i ^ ((↑j.rev : ℕ) + (↑j : ℕ)) = v i ^ (↑j : ℕ) * w i ^ n
⊢ projVandermonde v w i j = v i ^ (↑j : ℕ) * w i ^ n / w i ^ (↑j : ℕ)
have rw₄ : v i ^ (↑j : ℕ) * w i ^ n = v i ^ (↑j : ℕ) * w i ^ n
Tactic: rw [projVandermonde_apply, eq_div_iff (by simp [hw]), mul_assoc, ← pow_add, rev_add_cast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
⊢ projVandermonde v w i = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n)
have h : ∀ (j : Fin (n + 1)), projVandermonde v w i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
j : Fin (n + 1)
⊢ projVandermonde v w i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
have h : projVandermonde v w i (last n) = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) (last n)
Tactic: obtain rfl | hlt := j.le_last.eq_or_lt
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
j : Fin (n + 1)
h : projVandermonde v w i (last n) = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) (last n)
⊢ projVandermonde v w i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
have h₁ : ∀ (hlt : j < last n), projVandermonde v w i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
Tactic: obtain rfl | hlt := j.le_last.eq_or_lt
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin (n + 1) → R
i : Fin (n + 1)
hw : w i = 0
j : Fin (n + 1)
hlt : j < last n
⊢ projVandermonde v w i j = Pi.single (M := fun (j : Fin (n + 1)) ↦ R) (last n) (v i ^ n) j
have h : (↑j.rev : ℕ) ≠ 0
Tactic: rw [projVandermonde_apply, Pi.single_eq_of_ne hlt.ne, hw, zero_pow, mul_zero]