awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq m
A : Matrix m n R
rw : IsTotallyUnimodular (m := n ⊕ m) (A.fromCols 1)ᵀ ↔ A.IsTotallyUnimodular
rw₁ : IsTotallyUnimodular (m := n ⊕ m) (Aᵀ.fromRows 1ᵀ) ↔ A.IsTotallyUnimodular
rw₂ : IsTotallyUnimodular (m := n ⊕ m) (Aᵀ.fromRows 1) ↔ A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (n := n ⊕ m) (A.fromCols 1) ↔ A.IsTotallyUnimodular
have rw₃ : Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
    fromRows_one_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq m
A : Matrix m n R
rw : IsTotallyUnimodular (m := n ⊕ m) (A.fromCols 1)ᵀ ↔ A.IsTotallyUnimodular
rw₁ : IsTotallyUnimodular (m := n ⊕ m) (Aᵀ.fromRows 1ᵀ) ↔ A.IsTotallyUnimodular
rw₂ : IsTotallyUnimodular (m := n ⊕ m) (Aᵀ.fromRows 1) ↔ A.IsTotallyUnimodular
rw₃ : Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (n := n ⊕ m) (A.fromCols 1) ↔ A.IsTotallyUnimodular
have rw₄ : A.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
    fromRows_one_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq m
A : Matrix m n R
⊢ IsTotallyUnimodular (n := m ⊕ n) (fromCols 1 A) ↔ A.IsTotallyUnimodular
have rw : IsTotallyUnimodular (m := m ⊕ n) (fromCols 1 A)ᵀ ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
    one_fromRows_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq m
A : Matrix m n R
rw : IsTotallyUnimodular (m := m ⊕ n) (fromCols 1 A)ᵀ ↔ A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (n := m ⊕ n) (fromCols 1 A) ↔ A.IsTotallyUnimodular
have rw₁ : IsTotallyUnimodular (m := m ⊕ n) (fromRows 1ᵀ Aᵀ) ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
    one_fromRows_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq m
A : Matrix m n R
rw : IsTotallyUnimodular (m := m ⊕ n) (fromCols 1 A)ᵀ ↔ A.IsTotallyUnimodular
rw₁ : IsTotallyUnimodular (m := m ⊕ n) (fromRows 1ᵀ Aᵀ) ↔ A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (n := m ⊕ n) (fromCols 1 A) ↔ A.IsTotallyUnimodular
have rw₂ : IsTotallyUnimodular (m := m ⊕ n) (fromRows 1 Aᵀ) ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
    one_fromRows_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq m
A : Matrix m n R
rw : IsTotallyUnimodular (m := m ⊕ n) (fromCols 1 A)ᵀ ↔ A.IsTotallyUnimodular
rw₁ : IsTotallyUnimodular (m := m ⊕ n) (fromRows 1ᵀ Aᵀ) ↔ A.IsTotallyUnimodular
rw₂ : IsTotallyUnimodular (m := m ⊕ n) (fromRows 1 Aᵀ) ↔ A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (n := m ⊕ n) (fromCols 1 A) ↔ A.IsTotallyUnimodular
have rw₃ : Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
    one_fromRows_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
R : Type u_5
inst : CommRing R
inst_1 : DecidableEq m
A : Matrix m n R
rw : IsTotallyUnimodular (m := m ⊕ n) (fromCols 1 A)ᵀ ↔ A.IsTotallyUnimodular
rw₁ : IsTotallyUnimodular (m := m ⊕ n) (fromRows 1ᵀ Aᵀ) ↔ A.IsTotallyUnimodular
rw₂ : IsTotallyUnimodular (m := m ⊕ n) (fromRows 1 Aᵀ) ↔ A.IsTotallyUnimodular
rw₃ : Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
⊢ IsTotallyUnimodular (n := m ⊕ n) (fromCols 1 A) ↔ A.IsTotallyUnimodular
have rw₄ : A.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
    one_fromRows_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
⊢ (A.fromRows (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
have refine : Nonempty n →
  ∀ (x : m'),
    ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
Tactic: refine fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
h : Nonempty n
x : m'
⊢ ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
have inhabit : ∀ (inhabited_h : Inhabited n),
  ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
Tactic: inhabit n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
h : Nonempty n
x : m'
inhabited_h : Inhabited n
⊢ ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
have refine : Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) default (↑0 : R))
Tactic: refine ⟨default, 0, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
h : Nonempty n
x : m'
inhabited_h : Inhabited n
⊢ Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) default (↑0 : R))
have h : ∀ (x_1 : n),
  Eq.{u_5 + 1} (α := R) (replicateRow m' 0 x x_1 : R) (Pi.single (M := fun (j : n) ↦ R) default (↑0 : R) x_1 : R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
⊢ (A.fromRows (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
have refine : Nonempty n →
  ∀ (x : m'),
    ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
Tactic: classical
  refine fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_
  inhabit n
  refine ⟨default, 0, ?_⟩
  ext x
  simp [Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
refine :
  Nonempty n →
    ∀ (x : m'),
      ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
⊢ (A.fromRows (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
have refine₁ : Nonempty n →
  ∀ (x : m') (inhabited_h : Inhabited n),
    ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
Tactic: classical
  refine fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_
  inhabit n
  refine ⟨default, 0, ?_⟩
  ext x
  simp [Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
refine :
  Nonempty n →
    ∀ (x : m'),
      ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
refine₁ :
  Nonempty n →
    ∀ (x : m') (inhabited_h : Inhabited n),
      ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
⊢ (A.fromRows (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
have refine₂ : Nonempty n →
  ∀ (x : m') (inhabited_h : Inhabited n),
    Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) default (↑0 : R))
Tactic: classical
  refine fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_
  inhabit n
  refine ⟨default, 0, ?_⟩
  ext x
  simp [Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst : CommRing R
A : Matrix m n R
refine :
  Nonempty n →
    ∀ (x : m'),
      ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
refine₁ :
  Nonempty n →
    ∀ (x : m') (inhabited_h : Inhabited n),
      ∃ (j : n) (s : SignType), Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) j (↑s : R))
refine₂ :
  Nonempty n →
    ∀ (x : m') (inhabited_h : Inhabited n),
      Eq (α := n → R) (replicateRow m' 0 x) (Pi.single (M := fun (j : n) ↦ R) default (↑0 : R))
⊢ (A.fromRows (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
have h : Nonempty n →
  ∀ (x : m') (inhabited_h : Inhabited n) (x_1 : n),
    Eq.{u_5 + 1} (α := R) (replicateRow m' 0 x x_1 : R) (Pi.single (M := fun (j : n) ↦ R) default (↑0 : R) x_1 : R)
Tactic: classical
  refine fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_
  inhabit n
  refine ⟨default, 0, ?_⟩
  ext x
  simp [Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst : CommRing R
A : Matrix m n R
⊢ (A.fromCols (replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
have rw : (A.fromCols (replicateCol n' 0))ᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_replicateCol,
    fromRows_replicateRow0_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst : CommRing R
A : Matrix m n R
rw : (A.fromCols (replicateCol n' 0))ᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
⊢ (A.fromCols (replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
have rw₁ : (Aᵀ.fromRows (replicateCol n' 0)ᵀ).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_replicateCol,
    fromRows_replicateRow0_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst : CommRing R
A : Matrix m n R
rw : (A.fromCols (replicateCol n' 0))ᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
rw₁ : (Aᵀ.fromRows (replicateCol n' 0)ᵀ).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
⊢ (A.fromCols (replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
have rw₂ : (Aᵀ.fromRows (replicateRow n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_replicateCol,
    fromRows_replicateRow0_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst : CommRing R
A : Matrix m n R
rw : (A.fromCols (replicateCol n' 0))ᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
rw₁ : (Aᵀ.fromRows (replicateCol n' 0)ᵀ).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
rw₂ : (Aᵀ.fromRows (replicateRow n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
⊢ (A.fromCols (replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
have rw₃ : Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_replicateCol,
    fromRows_replicateRow0_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular (goal)
Goal:
m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst : CommRing R
A : Matrix m n R
rw : (A.fromCols (replicateCol n' 0))ᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
rw₁ : (Aᵀ.fromRows (replicateCol n' 0)ᵀ).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
rw₂ : (Aᵀ.fromRows (replicateRow n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
rw₃ : Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
⊢ (A.fromCols (replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular
have rw₄ : A.IsTotallyUnimodular ↔ A.IsTotallyUnimodular
Tactic: rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_replicateCol,
    fromRows_replicateRow0_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
⊢ Eq (α := Submodule K (m → K))
    (ker (R₂ := K) (M₂ := m → K) (τ₁₂ := RingHom.id K)
      ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)))
    (⨆ (i : m),
      ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
have rw : Eq (α := Submodule K (m → K))
  (⨅ (i : m),
    comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
      ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
  (⨆ (i : m),
    ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
Tactic: rw [← comap_bot, ← iInf_ker_proj, comap_iInf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (hypothesis)
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
⊢ Eq (α := Submodule K (m → K))
    (⨅ (i : m),
      comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
    (⨆ (i : m),
      ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
have this : ∀ (i : m),
  Eq (α := Submodule K (m → K))
    (ker (M₂ := K)
      (proj (φ := fun (a : m) ↦ K) i ∘ₗ (toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) :
        (m → K) →ₗ[K] K))
    (comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
      ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
Tactic: have := fun i : m => ker_comp (toLin' (diagonal w)) (proj i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
this :
  ∀ (i : m),
    Eq (α := Submodule K (m → K))
      (ker (M₂ := K)
        (proj (φ := fun (a : m) ↦ K) i ∘ₗ (toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) :
          (m → K) →ₗ[K] K))
      (comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
⊢ Eq (α := Submodule K (m → K))
    (⨅ (i : m),
      comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
    (⨆ (i : m),
      ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
have simp : Eq (α := Submodule K (m → K)) (⨅ (i : m), ⨅ (_ : w i ≠ 0), ker (proj (φ := fun (a : m) ↦ K) i))
  (⨆ (i : m),
    ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
Tactic: simp only [← this, proj_diagonal, ker_smul']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
this :
  ∀ (i : m),
    Eq (α := Submodule K (m → K))
      (ker (M₂ := K)
        (proj (φ := fun (a : m) ↦ K) i ∘ₗ (toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) :
          (m → K) →ₗ[K] K))
      (comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
⊢ Subset.{u_1} (α := Set m) univ ({i : m | w i = 0} ∪ {i : m | w i = 0}ᶜ)
have rw : Subset.{u_1} (α := Set m) univ univ
Tactic: rw [Set.union_compl_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (hypothesis)
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
this :
  ∀ (i : m),
    Eq (α := Submodule K (m → K))
      (ker (M₂ := K)
        (proj (φ := fun (a : m) ↦ K) i ∘ₗ (toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) :
          (m → K) →ₗ[K] K))
      (comap (R₂ := K) (M₂ := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)) (ker (proj (φ := fun (a : m) ↦ K) i)))
⊢ Eq (α := Submodule K (m → K)) (⨅ (i : m), ⨅ (_ : w i ≠ 0), ker (proj (φ := fun (a : m) ↦ K) i))
    (⨆ (i : m),
      ⨆ (_ : Membership.mem (γ := Set m) {i : m | w i = 0} i), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
have this₁ : Subset.{u_1} (α := Set m) univ ({i : m | w i = 0} ∪ {i : m | w i = 0}ᶜ)
Tactic: have : univ ⊆ { i : m | w i = 0 } ∪ { i : m | w i = 0 }ᶜ := by rw [Set.union_compl_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
⊢ Eq (α := Submodule K (m → K))
    (LinearMap.range (R := K) (M := m → K) (τ₁₂ := RingHom.id K)
      ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w)))
    (⨆ (i : m), ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
have rw : Eq (α := Submodule K (m → K))
  (⨆ (i : m),
    Submodule.map (M := m → K) (σ₁₂ := RingHom.id K) ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
      (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
  (⨆ (i : m), ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
Tactic: rw [← Submodule.map_top, ← iSup_range_single, Submodule.map_iSup]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
⊢ Eq (α := Submodule K (m → K))
    (⨆ (i : m),
      Submodule.map (M := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
        (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
    (⨆ (i : m), ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
have e_s : Eq (α := m → Submodule K (m → K))
  (fun (i : m) ↦
    Submodule.map (M := m → K) (σ₁₂ := RingHom.id K) ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
      (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
  fun (i : m) ↦ ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i)
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
⊢ Eq (α := m → Submodule K (m → K))
    (fun (i : m) ↦
      Submodule.map (M := m → K) (σ₁₂ := RingHom.id K)
        ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
        (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
    fun (i : m) ↦ ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i)
have e_s : ∀ (i : m),
  Eq (α := Submodule K (m → K))
    (Submodule.map (M := m → K) (σ₁₂ := RingHom.id K) ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
      (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
    (⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
Tactic: funext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
i : m
⊢ Eq (α := Submodule K (m → K))
    (Submodule.map (M := m → K) (σ₁₂ := RingHom.id K) ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
      (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
    (⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
have e_s : Eq (α := Submodule K (m → K))
  (LinearMap.range (M := K)
    ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) ∘ₗ LinearMap.single K (fun (a : m) ↦ K) i :
      K →ₗ[K] m → K))
  (⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
Tactic: rw [← LinearMap.range_comp, diagonal_comp_single, ← range_smul']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
i : m
e_s :
  Eq (α := Submodule K (m → K))
    (LinearMap.range (M := K)
      ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) ∘ₗ LinearMap.single K (fun (a : m) ↦ K) i :
        K →ₗ[K] m → K))
    (⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
⊢ Eq (α := Submodule K (m → K))
    (Submodule.map (M := m → K) (σ₁₂ := RingHom.id K) ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
      (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
    (⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
have e_s₁ : (HSMul.hSMul (β := K →ₗ[K] (i : m) → K) (w i) (LinearMap.single K (fun (x : m) ↦ K) i : K →ₗ[K] (i : m) → K)).range =
  ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i)
Tactic: rw [← LinearMap.range_comp, diagonal_comp_single, ← range_smul']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Semifield K
inst_2 : DecidableEq m
w : m → K
i : m
e_s :
  Eq (α := Submodule K (m → K))
    (LinearMap.range (M := K)
      ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w) ∘ₗ LinearMap.single K (fun (a : m) ↦ K) i :
        K →ₗ[K] m → K))
    (⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
e_s₁ :
  (HSMul.hSMul (β := K →ₗ[K] (i : m) → K) (w i) (LinearMap.single K (fun (x : m) ↦ K) i : K →ₗ[K] (i : m) → K)).range =
    ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i)
⊢ Eq (α := Submodule K (m → K))
    (Submodule.map (M := m → K) (σ₁₂ := RingHom.id K) ((toLin' : (a : Matrix m m K) → (m → K) →ₗ[K] m → K) (diagonal w))
      (LinearMap.range (LinearMap.single K (fun (a : m) ↦ K) i)))
    (⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.single K (fun (x : m) ↦ K) i))
have e_s₂ : (HSMul.hSMul (β := K →ₗ[K] (i : m) → K) (w i) (LinearMap.single K (fun (x : m) ↦ K) i : K →ₗ[K] (i : m) → K)).range =
  (HSMul.hSMul (β := K →ₗ[K] (i : m) → K) (w i) (LinearMap.single K (fun (x : m) ↦ K) i : K →ₗ[K] (i : m) → K)).range
Tactic: rw [← LinearMap.range_comp, diagonal_comp_single, ← range_smul']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Diagonal (goal)
Goal:
m : Type u_1
inst : Fintype m
K : Type u
inst_1 : Field K
inst_2 : DecidableEq m
inst_3 : DecidableEq K
w : m → K
⊢ Subset.{u_1} (α := Set m) univ ({i : m | w i = 0}ᶜ ∪ {i : m | w i = 0})
have rw : Subset.{u_1} (α := Set m) univ univ
Tactic: rw [Set.compl_union_self]