awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
h :
  (c.ofMatrix : (a : R) → R → Prop) x y →
    Relation.Map (⇑c : (a : Matrix n n R) → Matrix n n R → Prop) (fun (x : Matrix n n R) ↦ x i j)
      (fun (x : Matrix n n R) ↦ x i j) x y
⊢ (c.ofMatrix : (a : R) → R → Prop) x y ↔
    Relation.Map (⇑c : (a : Matrix n n R) → Matrix n n R → Prop) (fun (x : Matrix n n R) ↦ x i j)
      (fun (x : Matrix n n R) ↦ x i j) x y
have h₁ : Relation.Map (⇑c : (a : Matrix n n R) → Matrix n n R → Prop) (fun (x : Matrix n n R) ↦ x i j)
    (fun (x : Matrix n n R) ↦ x i j) x y →
  (c.ofMatrix : (a : R) → R → Prop) x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
h : (c.ofMatrix : (a : R) → R → Prop) x y
⊢ Relation.Map (⇑c : (a : Matrix n n R) → Matrix n n R → Prop) (fun (x : Matrix n n R) ↦ x i j)
    (fun (x : Matrix n n R) ↦ x i j) x y
have h₁ : (fun (x : Matrix n n R) ↦ x i j) (single i j x) = x ∧ (fun (x : Matrix n n R) ↦ x i j) (single i j y) = y
Tactic: refine ⟨_,_, h i j, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
⊢ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R) =
    {x : R | ∃ N ∈ I, N i j = x}
have h : ∀ (r : R),
  r ∈ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R) ↔
    Membership.mem (γ := Set R) {x : R | ∃ N ∈ I, N i j = x} r
Tactic: ext r
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
⊢ r ∈ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R) ↔
    Membership.mem (γ := Set R) {x : R | ∃ N ∈ I, N i j = x} r
have h : r ∈ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R) →
  Membership.mem (γ := Set R) {x : R | ∃ N ∈ I, N i j = x} r
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
h :
  r ∈ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R) →
    Membership.mem (γ := Set R) {x : R | ∃ N ∈ I, N i j = x} r
⊢ r ∈ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R) ↔
    Membership.mem (γ := Set R) {x : R | ∃ N ∈ I, N i j = x} r
have h₁ : Membership.mem (γ := Set R) {x : R | ∃ N ∈ I, N i j = x} r →
  r ∈ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
n_1 : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n_1
inst_2 : Nonempty n_1
inst_3 : DecidableEq n_1
I : TwoSidedIdeal (Matrix n_1 n_1 R)
i j : n_1
n : Matrix n_1 n_1 R
hn : n ∈ I
⊢ n i j ∈
    (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n_1 n_1 R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R)
have h : Relation.Map (δ := R) (⇑I.ringCon : (a : Matrix n_1 n_1 R) → Matrix n_1 n_1 R → Prop)
  (fun (x : Matrix n_1 n_1 R) ↦ x i j) (fun (x : Matrix n_1 n_1 R) ↦ x i j) (n i j) 0
Tactic: rw [SetLike.mem_coe, mem_iff, equivMatrix_symm_apply_ringCon,
      RingCon.coe_ofMatrix_eq_relationMap i j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I J : TwoSidedIdeal R
⊢ LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I) (matrix n J) ↔ I ≤ J
have mp : LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I) (matrix n J) → I ≤ J
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I J : TwoSidedIdeal R
mp : LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I) (matrix n J) → I ≤ J
⊢ LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I) (matrix n J) ↔ I ≤ J
have mpr : I ≤ J → LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I) (matrix n J)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (hypothesis)
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I J : TwoSidedIdeal R
le : LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I) (matrix n J)
x : R
xI : x ∈ I
⊢ x ∈ J
have le₁ : Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n J)
  ((of : (a : n → n → R) → Matrix n n R) fun (x_1 x_2 : n) ↦ x)
Tactic: specialize @le (of fun _ _ => x) (by simp [xI])
Cleared hypotheses: le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Ring R
inst_1 : Fintype n
inst_2 : DecidableEq n
I : TwoSidedIdeal R
⊢ Eq (α := Ideal (Matrix n n R))
    ((asIdeal : (a : TwoSidedIdeal (Matrix n n R)) → Ideal (Matrix n n R)) (matrix n I) : Ideal (Matrix n n R))
    (Ideal.matrix n ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I) : Ideal (Matrix n n R))
have h : ∀ (x : Matrix n n R),
  Membership.mem (γ := Ideal (Matrix n n R))
      ((asIdeal : (a : TwoSidedIdeal (Matrix n n R)) → Ideal (Matrix n n R)) (matrix n I) : Ideal (Matrix n n R)) x ↔
    Membership.mem (γ := Ideal (Matrix n n R)) (Ideal.matrix n ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
Mmem : Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) M
p q : n
⊢ (I.jacobson.ringCon : (a : R) → R → Prop) (M p q) (0 p q)
have simp : M p q ∈ I.jacobson
Tactic: simp only [zero_apply, ← mem_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
Mmem : Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) M
p q : n
⊢ M p q ∈ I.jacobson
have rw : ∀ (y : R), ∃ (z : R), z * y * M p q + z - 1 ∈ I
Tactic: rw [mem_jacobson_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
Mmem : Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) M
p q : n
⊢ ∀ (y : R), ∃ (z : R), z * y * M p q + z - 1 ∈ I
have Mmem₁ : Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) (M * single q p 1)
Tactic: replace Mmem := mul_mem_right _ _ (single q p 1) Mmem
Cleared hypotheses: Mmem
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
Mmem : Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) (M * single q p 1)
⊢ ∀ (y : R), ∃ (z : R), z * y * M p q + z - 1 ∈ I
have Mmem₁ : ∀ (y : Matrix n n R),
  ∃ (z : Matrix n n R),
    Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I) (z * y * (M * single q p 1) + z - 1)
Tactic: rw [mem_jacobson_iff] at Mmem
Cleared hypotheses: Mmem
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
Mmem :
  ∀ (y : Matrix n n R),
    ∃ (z : Matrix n n R),
      Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I) (z * y * (M * single q p 1) + z - 1)
y : R
⊢ ∃ (z : R), z * y * M p q + z - 1 ∈ I
have Mmem₁ : ∃ (z : Matrix n n R),
  Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
    (z * HSMul.hSMul (β := Matrix n n R) y (single p p 1) * (M * single q p 1) + z - 1)
Tactic: specialize Mmem (y • single p p 1)
Cleared hypotheses: Mmem
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
y : R
Mmem :
  ∃ (z : Matrix n n R),
    Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
      (z * HSMul.hSMul (β := Matrix n n R) y (single p p 1) * (M * single q p 1) + z - 1)
⊢ ∃ (z : R), z * y * M p q + z - 1 ∈ I
have have : ∀ (N : Matrix n n R)
  (NxMI :
    Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
      (N * HSMul.hSMul (β := Matrix n n R) y (single p p 1) * (M * single q p 1) + N - 1)),
  ∃ (z : R), z * y * M p q + z - 1 ∈ I
Tactic: have ⟨N, NxMI⟩ := Mmem
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
y : R
Mmem :
  ∃ (z : Matrix n n R),
    Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
      (z * HSMul.hSMul (β := Matrix n n R) y (single p p 1) * (M * single q p 1) + z - 1)
N : Matrix n n R
NxMI :
  Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
    (N * HSMul.hSMul (β := Matrix n n R) y (single p p 1) * (M * single q p 1) + N - 1)
⊢ ∃ (z : R), z * y * M p q + z - 1 ∈ I
have h : N p p * y * M p q + N p p - 1 ∈ I
Tactic: use N p p
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : TwoSidedIdeal R
⊢ Eq (α := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) (matrix n I.jacobson)
have a : LE.le (α := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) (matrix n I.jacobson)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : TwoSidedIdeal R
a : LE.le (α := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) (matrix n I.jacobson)
⊢ Eq (α := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) (matrix n I.jacobson)
have a₁ : LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I.jacobson) (jacobson (matrix n I))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have obtain : ∀ (k : ℕ) (hk : A.den = (A i j).den * k), HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
Tactic: obtain ⟨k, hk⟩ := den_dvd_iff.mp (dvd_refl A.den) i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw₁ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A i j).num : ℚ) (↑A.den : ℚ) = A i j
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
rw₁ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A i j).num : ℚ) (↑A.den : ℚ) = A i j
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw₂ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) (A i j)).num : ℚ) (↑A.den : ℚ) = A i j
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
rw₁ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₂ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) (A i j)).num : ℚ) (↑A.den : ℚ) = A i j
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw₃ : HDiv.hDiv (α := ℚ) (↑((↑A.den : ℚ) * A i j).num : ℚ) (↑A.den : ℚ) = A i j
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
rw₁ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₂ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) (A i j)).num : ℚ) (↑A.den : ℚ) = A i j
rw₃ : HDiv.hDiv (α := ℚ) (↑((↑A.den : ℚ) * A i j).num : ℚ) (↑A.den : ℚ) = A i j
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw₄ : HDiv.hDiv (α := ℚ) (↑(A i j * (↑A.den : ℚ)).num : ℚ) (↑A.den : ℚ) = A i j
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
rw₁ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₂ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) (A i j)).num : ℚ) (↑A.den : ℚ) = A i j
rw₃ : HDiv.hDiv (α := ℚ) (↑((↑A.den : ℚ) * A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₄ : HDiv.hDiv (α := ℚ) (↑(A i j * (↑A.den : ℚ)).num : ℚ) (↑A.den : ℚ) = A i j
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw₅ : (↑(A i j * (↑A.den : ℚ)).num : ℚ) = A i j * (↑A.den : ℚ)
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
rw₁ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₂ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) (A i j)).num : ℚ) (↑A.den : ℚ) = A i j
rw₃ : HDiv.hDiv (α := ℚ) (↑((↑A.den : ℚ) * A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₄ : HDiv.hDiv (α := ℚ) (↑(A i j * (↑A.den : ℚ)).num : ℚ) (↑A.den : ℚ) = A i j
rw₅ : (↑(A i j * (↑A.den : ℚ)).num : ℚ) = A i j * (↑A.den : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw₆ : (↑(A i j * (↑((A i j).den * k) : ℚ)).num : ℚ) = A i j * (↑((A i j).den * k) : ℚ)
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
rw₁ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₂ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) (A i j)).num : ℚ) (↑A.den : ℚ) = A i j
rw₃ : HDiv.hDiv (α := ℚ) (↑((↑A.den : ℚ) * A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₄ : HDiv.hDiv (α := ℚ) (↑(A i j * (↑A.den : ℚ)).num : ℚ) (↑A.den : ℚ) = A i j
rw₅ : (↑(A i j * (↑A.den : ℚ)).num : ℚ) = A i j * (↑A.den : ℚ)
rw₆ : (↑(A i j * (↑((A i j).den * k) : ℚ)).num : ℚ) = A i j * (↑((A i j).den * k) : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw₇ : (↑(A i j * HMul.hMul (α := ℚ) (↑(A i j).den : ℚ) (↑k : ℚ)).num : ℚ) =
  A i j * HMul.hMul (α := ℚ) (↑(A i j).den : ℚ) (↑k : ℚ)
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
rw₁ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₂ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) (A i j)).num : ℚ) (↑A.den : ℚ) = A i j
rw₃ : HDiv.hDiv (α := ℚ) (↑((↑A.den : ℚ) * A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₄ : HDiv.hDiv (α := ℚ) (↑(A i j * (↑A.den : ℚ)).num : ℚ) (↑A.den : ℚ) = A i j
rw₅ : (↑(A i j * (↑A.den : ℚ)).num : ℚ) = A i j * (↑A.den : ℚ)
rw₆ : (↑(A i j * (↑((A i j).den * k) : ℚ)).num : ℚ) = A i j * (↑((A i j).den * k) : ℚ)
rw₇ :
  (↑(A i j * HMul.hMul (α := ℚ) (↑(A i j).den : ℚ) (↑k : ℚ)).num : ℚ) =
    A i j * HMul.hMul (α := ℚ) (↑(A i j).den : ℚ) (↑k : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw₈ : (↑(A i j * (↑(A i j).den : ℚ) * (↑k : ℚ)).num : ℚ) = A i j * (↑(A i j).den : ℚ) * (↑k : ℚ)
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
rw₁ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₂ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) (A i j)).num : ℚ) (↑A.den : ℚ) = A i j
rw₃ : HDiv.hDiv (α := ℚ) (↑((↑A.den : ℚ) * A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₄ : HDiv.hDiv (α := ℚ) (↑(A i j * (↑A.den : ℚ)).num : ℚ) (↑A.den : ℚ) = A i j
rw₅ : (↑(A i j * (↑A.den : ℚ)).num : ℚ) = A i j * (↑A.den : ℚ)
rw₆ : (↑(A i j * (↑((A i j).den * k) : ℚ)).num : ℚ) = A i j * (↑((A i j).den * k) : ℚ)
rw₇ :
  (↑(A i j * HMul.hMul (α := ℚ) (↑(A i j).den : ℚ) (↑k : ℚ)).num : ℚ) =
    A i j * HMul.hMul (α := ℚ) (↑(A i j).den : ℚ) (↑k : ℚ)
rw₈ : (↑(A i j * (↑(A i j).den : ℚ) * (↑k : ℚ)).num : ℚ) = A i j * (↑(A i j).den : ℚ) * (↑k : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw₉ : (↑(HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑k : ℚ)).num : ℚ) = HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑k : ℚ)
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Integer (goal)
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
k : ℕ
hk : A.den = (A i j).den * k
rw : HDiv.hDiv (α := ℚ) (↑((HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A).map Rat.num i j) : ℚ) (↑A.den : ℚ) = A i j
rw₁ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₂ : HDiv.hDiv (α := ℚ) (↑(HSMul.hSMul (α := ℚ) (↑A.den : ℚ) (A i j)).num : ℚ) (↑A.den : ℚ) = A i j
rw₃ : HDiv.hDiv (α := ℚ) (↑((↑A.den : ℚ) * A i j).num : ℚ) (↑A.den : ℚ) = A i j
rw₄ : HDiv.hDiv (α := ℚ) (↑(A i j * (↑A.den : ℚ)).num : ℚ) (↑A.den : ℚ) = A i j
rw₅ : (↑(A i j * (↑A.den : ℚ)).num : ℚ) = A i j * (↑A.den : ℚ)
rw₆ : (↑(A i j * (↑((A i j).den * k) : ℚ)).num : ℚ) = A i j * (↑((A i j).den * k) : ℚ)
rw₇ :
  (↑(A i j * HMul.hMul (α := ℚ) (↑(A i j).den : ℚ) (↑k : ℚ)).num : ℚ) =
    A i j * HMul.hMul (α := ℚ) (↑(A i j).den : ℚ) (↑k : ℚ)
rw₈ : (↑(A i j * (↑(A i j).den : ℚ) * (↑k : ℚ)).num : ℚ) = A i j * (↑(A i j).den : ℚ) * (↑k : ℚ)
rw₉ : (↑(HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑k : ℚ)).num : ℚ) = HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑k : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
have rw₁₀ : (↑(HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑(↑k : ℤ) : ℚ)).num : ℚ) =
  HMul.hMul (α := ℚ) (↑(A i j).num : ℚ) (↑(↑k : ℤ) : ℚ)
Tactic: rw [Matrix.num, map_apply, smul_apply, smul_eq_mul, mul_comm,
    div_eq_iff <| Nat.cast_ne_zero.mpr A.den_ne_zero, hk, Nat.cast_mul, ← mul_assoc,
    Rat.mul_den_eq_num, ← Int.cast_natCast k, ← Int.cast_mul, Rat.num_intCast]