awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsOrderedRing R
m : Type u_3
inst_5 : Fintype m
inst_6 : DecidableEq m
M : Matrix n n R
e₁ e₂ : n ≃ m
rw :
  Membership.mem (γ := Submonoid (Matrix m m R)) (colStochastic R m)
      ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M)ᵀᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
rw₁ :
  Membership.mem (γ := Submonoid (Matrix m m R)) (colStochastic R m)
      ((reindex e₂ e₁ : (a : Matrix n n R) → Matrix m m R) Mᵀ)ᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
rw₂ :
  Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (rowStochastic R m)
      ((reindex e₂ e₁ : (a : Matrix n n R) → Matrix m m R) Mᵀ : Matrix m m R) ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
rw₃ :
  Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) Mᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
rw₄ :
  Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) Mᵀᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
⊢ Membership.mem (α := Matrix m m R) (γ := Submonoid (Matrix m m R)) (colStochastic R m)
      ((reindex e₁ e₂ : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R) ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
have rw₅ : Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M ↔
  Membership.mem (γ := Submonoid (Matrix n n R)) (colStochastic R n) M
Tactic: rw [← transpose_transpose (reindex e₁ e₂ M), transpose_reindex,
    transpose_mem_colStochastic_iff_mem_rowStochastic, reindex_mem_rowStochastic_iff,
    ← transpose_mem_colStochastic_iff_mem_rowStochastic, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Swap (goal)
Goal:
R : Type u_1
n : Type u_2
m : Type u_3
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a : m
g : Matrix n m R
⊢ (swap R i j * g) j a = g i a
have rw : (swap R j i * g) j a = g i a
Tactic: rw [swap_comm, swap_mul_apply_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Swap (goal)
Goal:
R : Type u_1
n : Type u_2
m : Type u_3
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a : m
g : Matrix n m R
rw : (swap R j i * g) j a = g i a
⊢ (swap R i j * g) j a = g i a
have rw₁ : g i a = g i a
Tactic: rw [swap_comm, swap_mul_apply_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Swap (goal)
Goal:
R : Type u_1
n : Type u_2
m : Type u_3
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a : m
g : Matrix m n R
⊢ (g * swap R i j) a j = g a i
have rw : (g * swap R j i) a j = g a i
Tactic: rw [swap_comm, mul_swap_apply_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Swap (goal)
Goal:
R : Type u_1
n : Type u_2
m : Type u_3
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a : m
g : Matrix m n R
rw : (g * swap R j i) a j = g a i
⊢ (g * swap R i j) a j = g a i
have rw₁ : g a i = g a i
Tactic: rw [swap_comm, mul_swap_apply_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Swap (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
⊢ swap R i j * swap R i j = 1
have simp : Equiv.Perm.permMatrix R (Equiv.swap i j) * Equiv.Perm.permMatrix R (Equiv.swap i j) = 1
Tactic: simp only [swap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Swap (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Semiring R
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
⊢ Equiv.Perm.permMatrix R (Equiv.swap i j) * Equiv.Perm.permMatrix R (Equiv.swap i j) = 1
have rw : Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) * Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) = 1
Tactic: rw [← Equiv.swap_inv, Equiv.Perm.inv_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Swap (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
S : Type u_3
inst_3 : CommRing S
f : R →+* S
i j : n
⊢ Eq (α := GL n S) ((map f : (a : GL n R) → GL n S) (swap R i j) : GL n S) (swap S i j : GL n S)
have huv : (↑((map f : (a : GL n R) → GL n S) (swap R i j)) : Matrix n n S) = (↑(swap S i j) : Matrix n n S)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
inst : CommSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n α
h : A.IsSymm
k : ℕ
⊢ (A ^ k).IsSymm
have rw : (A ^ k)ᵀ = A ^ k
Tactic: rw [IsSymm, transpose_pow, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
inst : CommSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n α
h : A.IsSymm
k : ℕ
rw : (A ^ k)ᵀ = A ^ k
⊢ (A ^ k).IsSymm
have rw₁ : Aᵀ ^ k = A ^ k
Tactic: rw [IsSymm, transpose_pow, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
inst : CommSemiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n α
h : A.IsSymm
k : ℕ
rw : (A ^ k)ᵀ = A ^ k
rw₁ : Aᵀ ^ k = A ^ k
⊢ (A ^ k).IsSymm
have rw₂ : A ^ k = A ^ k
Tactic: rw [IsSymm, transpose_pow, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
h : A.IsSymm
f : α → β
⊢ (A.map f).IsSymm
have rw : (A.map f)ᵀ = A.map f
Tactic: rw [IsSymm, ← transpose_map, h.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
h : A.IsSymm
f : α → β
rw : (A.map f)ᵀ = A.map f
⊢ (A.map f).IsSymm
have rw₁ : Aᵀ.map f = A.map f
Tactic: rw [IsSymm, ← transpose_map, h.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
h : A.IsSymm
f : α → β
rw : (A.map f)ᵀ = A.map f
rw₁ : Aᵀ.map f = A.map f
⊢ (A.map f).IsSymm
have rw₂ : A.map f = A.map f
Tactic: rw [IsSymm, ← transpose_map, h.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
⊢ (A.map f).IsSymm ↔ A.IsSymm
have rw : (A.map f)ᵀ = A.map f ↔ A.IsSymm
Tactic: rw [IsSymm, IsSymm, ← transpose_map, map_injective hf |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
rw : (A.map f)ᵀ = A.map f ↔ A.IsSymm
⊢ (A.map f).IsSymm ↔ A.IsSymm
have rw₁ : (A.map f)ᵀ = A.map f ↔ Aᵀ = A
Tactic: rw [IsSymm, IsSymm, ← transpose_map, map_injective hf |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
rw : (A.map f)ᵀ = A.map f ↔ A.IsSymm
rw₁ : (A.map f)ᵀ = A.map f ↔ Aᵀ = A
⊢ (A.map f).IsSymm ↔ A.IsSymm
have rw₂ : Aᵀ.map f = A.map f ↔ Aᵀ = A
Tactic: rw [IsSymm, IsSymm, ← transpose_map, map_injective hf |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
rw : (A.map f)ᵀ = A.map f ↔ A.IsSymm
rw₁ : (A.map f)ᵀ = A.map f ↔ Aᵀ = A
rw₂ : Aᵀ.map f = A.map f ↔ Aᵀ = A
⊢ (A.map f).IsSymm ↔ A.IsSymm
have rw₃ : Aᵀ = A ↔ Aᵀ = A
Tactic: rw [IsSymm, IsSymm, ← transpose_map, map_injective hf |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
A : Matrix n n α
⊢ Aᵀ.IsSymm ↔ A.IsSymm
have refine : ∀ (h : Aᵀ.IsSymm), A.IsSymm
Tactic: refine ⟨fun h ↦ ?_, (·.transpose)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
A : Matrix n n α
h : Aᵀ.IsSymm
⊢ A.IsSymm
have rw : Aᵀᵀ.IsSymm
Tactic: rw [← A.transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveStar α
A : Matrix n n α
⊢ Aᴴ.IsSymm ↔ A.IsSymm
have refine : ∀ (h : Aᴴ.IsSymm), A.IsSymm
Tactic: refine ⟨fun h ↦ ?_, (·.conjTranspose)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveStar α
A : Matrix n n α
h : Aᴴ.IsSymm
⊢ A.IsSymm
have rw : Aᴴᴴ.IsSymm
Tactic: rw [← A.conjTranspose_conjTranspose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveNeg α
A : Matrix n n α
⊢ (-A).IsSymm ↔ A.IsSymm
have refine : ∀ (h : (-A).IsSymm), A.IsSymm
Tactic: refine ⟨fun h ↦ ?_, (·.neg)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
inst : InvolutiveNeg α
A : Matrix n n α
h : (-A).IsSymm
⊢ A.IsSymm
have rw : (- -A).IsSymm
Tactic: rw [← neg_neg A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
R : Type u_5
inst : Monoid R
inst_1 : MulAction R α
A : Matrix n n α
k : R
inst_2 : Invertible k
⊢ (k • A).IsSymm ↔ A.IsSymm
have refine : ∀ (h : (k • A).IsSymm), A.IsSymm
Tactic: refine ⟨fun h ↦ ?_, (·.smul k)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
R : Type u_5
inst : Monoid R
inst_1 : MulAction R α
A : Matrix n n α
k : R
inst_2 : Invertible k
h : (k • A).IsSymm
⊢ A.IsSymm
have rw : (@Invertible.invOf _ MulOne.toMul MulOne.toOne k _ • k • A).IsSymm
Tactic: rw [← invOf_smul_smul k A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix n n α
h : A.IsSymm
f : n ≃ m
⊢ IsSymm.{u_1, u_4} (α := α) (n := m) ((Matrix.reindex f f : (a : Matrix n n α) → Matrix m m α) A)
have rw : IsSymm.{u_1, u_4} (n := m) (A.submatrix (⇑f.symm : (a : m) → n) (⇑f.symm : (a : m) → n))
Tactic: rw [reindex_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix n n α
f : n ≃ m
⊢ IsSymm.{u_1, u_4} (α := α) (n := m) ((reindex f f : (a : Matrix n n α) → Matrix m m α) A) ↔ A.IsSymm
have refine : ∀ (h : IsSymm.{u_1, u_4} (α := α) (n := m) ((reindex f f : (a : Matrix n n α) → Matrix m m α) A)), A.IsSymm
Tactic: refine ⟨fun h ↦ ?_, (·.reindex f)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ Cᵀ = B
have rw : Bᵀᵀ = B
Tactic: rw [← hBC]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (hypothesis)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ (Matrix.fromBlocks A B C D).IsSymm
have hCB : Cᵀ = B
Tactic: have hCB : Cᵀ = B := by
    rw [← hBC]
    simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D
have rw : Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
Tactic: rw [fromBlocks_transpose, hA, hCB, hBC, hD]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
rw : Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D
have rw₁ : Matrix.fromBlocks A Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
Tactic: rw [fromBlocks_transpose, hA, hCB, hBC, hD]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
rw : Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
rw₁ : Matrix.fromBlocks A Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D
have rw₂ : Matrix.fromBlocks A B Bᵀ Dᵀ = Matrix.fromBlocks A B C D
Tactic: rw [fromBlocks_transpose, hA, hCB, hBC, hD]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
rw : Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
rw₁ : Matrix.fromBlocks A Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
rw₂ : Matrix.fromBlocks A B Bᵀ Dᵀ = Matrix.fromBlocks A B C D
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D
have rw₃ : Matrix.fromBlocks A B C Dᵀ = Matrix.fromBlocks A B C D
Tactic: rw [fromBlocks_transpose, hA, hCB, hBC, hD]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
rw : Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
rw₁ : Matrix.fromBlocks A Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
rw₂ : Matrix.fromBlocks A B Bᵀ Dᵀ = Matrix.fromBlocks A B C D
rw₃ : Matrix.fromBlocks A B C Dᵀ = Matrix.fromBlocks A B C D
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D
have rw₄ : Matrix.fromBlocks A B C D = Matrix.fromBlocks A B C D
Tactic: rw [fromBlocks_transpose, hA, hCB, hBC, hD]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
⊢ IsSymm (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
have rw : Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᵀ
    ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
  Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
Tactic: rw [IsSymm, transpose_comp, transpose_map, comp .. |>.injective.eq_iff, eq_comm,
    transpose_involutive _ _ |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
rw :
  Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᵀ
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
⊢ IsSymm (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
have rw₁ : Eq (α := Matrix (m × n) (m × n) α)
    ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α)
        (Aᵀ.map fun (x : Matrix n n α) ↦ xᵀ) :
      Matrix (m × n) (m × n) α)
    ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
  Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
Tactic: rw [IsSymm, transpose_comp, transpose_map, comp .. |>.injective.eq_iff, eq_comm,
    transpose_involutive _ _ |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
rw :
  Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᵀ
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₁ :
  Eq (α := Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α)
          (Aᵀ.map fun (x : Matrix n n α) ↦ xᵀ) :
        Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
⊢ IsSymm (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
have rw₂ : Eq (α := Matrix (m × n) (m × n) α)
    ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α)
        (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ :
      Matrix (m × n) (m × n) α)
    ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
  Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
Tactic: rw [IsSymm, transpose_comp, transpose_map, comp .. |>.injective.eq_iff, eq_comm,
    transpose_involutive _ _ |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
rw :
  Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᵀ
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₁ :
  Eq (α := Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α)
          (Aᵀ.map fun (x : Matrix n n α) ↦ xᵀ) :
        Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₂ :
  Eq (α := Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α)
          (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ :
        Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
⊢ IsSymm (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
have rw₃ : (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ = A ↔ Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
Tactic: rw [IsSymm, transpose_comp, transpose_map, comp .. |>.injective.eq_iff, eq_comm,
    transpose_involutive _ _ |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
rw :
  Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᵀ
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₁ :
  Eq (α := Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α)
          (Aᵀ.map fun (x : Matrix n n α) ↦ xᵀ) :
        Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₂ :
  Eq (α := Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α)
          (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ :
        Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₃ : (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ = A ↔ Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
⊢ IsSymm (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
have rw₄ : A = (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ ↔ Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
Tactic: rw [IsSymm, transpose_comp, transpose_map, comp .. |>.injective.eq_iff, eq_comm,
    transpose_involutive _ _ |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
rw :
  Eq (α := Matrix (m × n) (m × n) α) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A)ᵀ
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₁ :
  Eq (α := Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α)
          (Aᵀ.map fun (x : Matrix n n α) ↦ xᵀ) :
        Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₂ :
  Eq (α := Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α)
          (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ :
        Matrix (m × n) (m × n) α)
      ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A : Matrix (m × n) (m × n) α) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₃ : (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ = A ↔ Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
rw₄ : A = (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ ↔ Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
⊢ IsSymm (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    Aᵀ = A.map fun (x : Matrix n n α) ↦ xᵀ
have rw₅ : A = (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ ↔ A = (A.map fun (x : Matrix n n α) ↦ xᵀ)ᵀ
Tactic: rw [IsSymm, transpose_comp, transpose_map, comp .. |>.injective.eq_iff, eq_comm,
    transpose_involutive _ _ |>.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Symmetric (goal)
Goal:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
⊢ IsSymm (α := α) (n := m × n) ((comp m m n n α : (a : Matrix m m (Matrix n n α)) → Matrix (m × n) (m × n) α) A) ↔
    ∀ (i j : m) (i' j' : n), A j i j' i' = A i j i' j'
have simp : (∀ (a : m) (b : n) (a_1 : m) (b_1 : n), A a_1 a b_1 b = A a a_1 b b_1) ↔
  ∀ (i j : m) (i' j' : n), A j i j' i' = A i j i' j'
Tactic: simp [IsSymm.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ Eq (α := Submodule R (n → R)) (LinearMap.range M.vecMulLinear) (span R (Set.range M.row))
have simp_rw : Eq (α := Submodule R (n → R)) (span R (Set.range fun (x : m) ↦ Pi.single (M := fun (i : m) ↦ R) x 1 ᵥ* M))
  (span R (Set.range fun (i : m) ↦ M i))
Tactic: simp_rw [range_eq_map, ← iSup_range_single, Submodule.map_iSup, range_eq_map, ←
    Ideal.span_singleton_one, Ideal.span, Submodule.map_span, image_image, image_singleton,
    Matrix.vecMulLinear_apply, iSup_span, range_eq_iUnion, iUnion_singleton_eq_range,
    LinearMap.single, LinearMap.coe_mk, AddHom.coe_mk, row_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
simp_rw simp_rw₁ :
  Eq (α := Submodule R (n → R))
    (span R (Set.range fun (x : m) (x_1 : n) ↦ Pi.single (M := fun (i : m) ↦ R) x 1 ⬝ᵥ fun (i : m) ↦ M i x_1))
    (span R (Set.range fun (i : m) ↦ M i))
⊢ Eq (α := Submodule R (n → R))
    (span R
      (Set.range fun (x : m) (x_1 : n) ↦
        have j := x_1;
        Pi.single (M := fun (i : m) ↦ R) x 1 ⬝ᵥ fun (i : m) ↦ M i j))
    (span R (Set.range fun (i : m) ↦ M i))
have simp_rw₂ : Eq (α := Submodule R (n → R)) (span R (Set.range fun (x : m) (x_1 : n) ↦ 1 * M x x_1))
  (span R (Set.range fun (i : m) ↦ M i))
Tactic: simp_rw [single_dotProduct, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
M : Matrix m n R
⊢ (Function.Injective (β := n → R) fun (v : m → R) ↦ v ᵥ* M) ↔ LinearIndependent R M.row
have rw : Function.Injective (α := m → R) (β := n → R) (⇑M.vecMulLinear : (a : m → R) → n → R) ↔
  Function.Injective (α := m → R) (β := n → R) (⇑(Fintype.linearCombination R M.row) : (a : m → R) → n → R)
Tactic: rw [← coe_vecMulLinear, linearIndependent_iff_injective_fintypeLinearCombination]