awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : (↑g : Matrix (Fin 2) (Fin 2) R) 0 0 = v 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = v 1
t : Fin 2
⊢ v t = (↑g : Matrix (Fin 2) (Fin 2) R) 0 t
have 0 : v ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: { fin_cases t <;> tauto }
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : (↑g : Matrix (Fin 2) (Fin 2) R) 0 0 = v 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = v 1
t : Fin 2
0 : v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ v t = (↑g : Matrix (Fin 2) (Fin 2) R) 0 t
have 1 : v ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: { fin_cases t <;> tauto }
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : (↑g : Matrix (Fin 2) (Fin 2) R) 0 0 = v 0 ∧ (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = v 1
⊢ IsCoprime ((v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) R)) 0) ((v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) R)) 1)
have this : v = (↑g : Matrix (Fin 2) (Fin 2) R) 0
Tactic: have : v = g 0 := funext fun t ↦ by { fin_cases t <;> tauto }
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
⊢ (↑(HPow.hPow (β := ℤ) T 0) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, 0; 0, 1]
have zero : Eq (α := Matrix (Fin 2) (Fin 2) ℤ) ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) : Matrix (Fin 2) (Fin 2) ℤ)
  (!![1, 0; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
Tactic: rw [zpow_zero, coe_one, Matrix.one_fin_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
zero :
  Eq (α := Matrix (Fin 2) (Fin 2) ℤ) ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) : Matrix (Fin 2) (Fin 2) ℤ)
    (!![1, 0; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
⊢ (↑(HPow.hPow (β := ℤ) T 0) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, 0; 0, 1]
have zero₁ : Eq (α := Matrix (Fin 2) (Fin 2) ℤ) (1 : Matrix (Fin 2) (Fin 2) ℤ) (!![1, 0; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
Tactic: rw [zpow_zero, coe_one, Matrix.one_fin_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
zero :
  Eq (α := Matrix (Fin 2) (Fin 2) ℤ) ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) : Matrix (Fin 2) (Fin 2) ℤ)
    (!![1, 0; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
zero₁ : Eq (α := Matrix (Fin 2) (Fin 2) ℤ) (1 : Matrix (Fin 2) (Fin 2) ℤ) (!![1, 0; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
⊢ (↑(HPow.hPow (β := ℤ) T 0) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, 0; 0, 1]
have zero₂ : Eq (α := Matrix (Fin 2) (Fin 2) ℤ) (!![1, 0; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
  (!![1, 0; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
Tactic: rw [zpow_zero, coe_one, Matrix.one_fin_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (↑n : ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, (↑n : ℤ); 0, 1]
⊢ (↑(T ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1; 0, 1]
have succ : Eq (α := Matrix (Fin 2) (Fin 2) ℤ)
  (!![HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 0, HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 1;
      HMul.hMul (α := ℤ) 0 1 + HMul.hMul (α := ℤ) 1 0, HMul.hMul (α := ℤ) 0 1 + HMul.hMul (α := ℤ) 1 1] :
    Matrix (Fin 2) (Fin 2) ℤ)
  (!![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
Tactic: simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (↑n : ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, (↑n : ℤ); 0, 1]
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℤ)
    (!![HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 0, HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 1;
        HMul.hMul (α := ℤ) 0 1 + HMul.hMul (α := ℤ) 1 0, HMul.hMul (α := ℤ) 0 1 + HMul.hMul (α := ℤ) 1 1] :
      Matrix (Fin 2) (Fin 2) ℤ)
    (!![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
have succ : HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
Tactic: congrm !![_, ?_; _, _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (↑n : ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, (↑n : ℤ); 0, 1]
⊢ HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
have succ : 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
Tactic: rw [mul_one, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (↑n : ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, (↑n : ℤ); 0, 1]
succ : 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
have succ₁ : HAdd.hAdd (α := ℤ) 1 (↑n : ℤ) = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
Tactic: rw [mul_one, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (↑n : ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, (↑n : ℤ); 0, 1]
succ : 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
succ₁ : HAdd.hAdd (α := ℤ) 1 (↑n : ℤ) = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
have succ₂ : HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
Tactic: rw [mul_one, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (-(↑n : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, -(↑n : ℤ); 0, 1]
⊢ (↑(T ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1; 0, 1]
have pred : Eq (α := Matrix (Fin 2) (Fin 2) ℤ)
  (!![HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (-(↑n : ℤ)) 0,
        HMul.hMul (α := ℤ) 1 (-1) + HMul.hMul (α := ℤ) (-(↑n : ℤ)) 1;
      HMul.hMul (α := ℤ) 0 1 + HMul.hMul (α := ℤ) 1 0, HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 1] :
    Matrix (Fin 2) (Fin 2) ℤ)
  (!![1, HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
Tactic: simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (-(↑n : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, -(↑n : ℤ); 0, 1]
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℤ)
    (!![HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (-(↑n : ℤ)) 0,
          HMul.hMul (α := ℤ) 1 (-1) + HMul.hMul (α := ℤ) (-(↑n : ℤ)) 1;
        HMul.hMul (α := ℤ) 0 1 + HMul.hMul (α := ℤ) 1 0, HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 1] :
      Matrix (Fin 2) (Fin 2) ℤ)
    (!![1, HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
have pred : HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (-(↑n : ℤ)) 0 = 1
Tactic: congrm !![?_, ?_; _, _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (-(↑n : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, -(↑n : ℤ); 0, 1]
pred : HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (-(↑n : ℤ)) 0 = 1
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℤ)
    (!![HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (-(↑n : ℤ)) 0,
          HMul.hMul (α := ℤ) 1 (-1) + HMul.hMul (α := ℤ) (-(↑n : ℤ)) 1;
        HMul.hMul (α := ℤ) 0 1 + HMul.hMul (α := ℤ) 1 0, HMul.hMul (α := ℤ) 0 (-1) + HMul.hMul (α := ℤ) 1 1] :
      Matrix (Fin 2) (Fin 2) ℤ)
    (!![1, HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1; 0, 1] : Matrix (Fin 2) (Fin 2) ℤ)
have pred₁ : HMul.hMul (α := ℤ) 1 (-1) + HMul.hMul (α := ℤ) (-(↑n : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
Tactic: congrm !![?_, ?_; _, _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : ℤ
⊢ (↑(T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, n; 0, 1]
have zero : (↑(HPow.hPow (β := ℤ) T 0) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, 0; 0, 1]
Tactic: induction n with
  | zero => rw [zpow_zero, coe_one, Matrix.one_fin_two]
  | succ n h =>
    simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
    congrm !![_, ?_; _, _]
    rw [mul_one, mul_one, add_comm]
  | pred n h =>
    simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
    congrm !![?_, ?_; _, _] <;> ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : ℤ
zero : (↑(HPow.hPow (β := ℤ) T 0) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, 0; 0, 1]
⊢ (↑(T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, n; 0, 1]
have succ : ∀ (n : ℕ) (h : (↑(HPow.hPow (β := ℤ) T (↑n : ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, (↑n : ℤ); 0, 1]),
  (↑(T ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1; 0, 1]
Tactic: induction n with
  | zero => rw [zpow_zero, coe_one, Matrix.one_fin_two]
  | succ n h =>
    simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
    congrm !![_, ?_; _, _]
    rw [mul_one, mul_one, add_comm]
  | pred n h =>
    simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
    congrm !![?_, ?_; _, _] <;> ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : ℤ
zero : (↑(HPow.hPow (β := ℤ) T 0) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, 0; 0, 1]
succ :
  ∀ (n : ℕ) (h : (↑(HPow.hPow (β := ℤ) T (↑n : ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, (↑n : ℤ); 0, 1]),
    (↑(T ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1; 0, 1]
⊢ (↑(T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, n; 0, 1]
have pred : ∀ (n : ℕ) (h : (↑(HPow.hPow (β := ℤ) T (-(↑n : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, -(↑n : ℤ); 0, 1]),
  (↑(T ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1; 0, 1]
Tactic: induction n with
  | zero => rw [zpow_zero, coe_one, Matrix.one_fin_two]
  | succ n h =>
    simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
    congrm !![_, ?_; _, _]
    rw [mul_one, mul_one, add_comm]
  | pred n h =>
    simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
    congrm !![?_, ?_; _, _] <;> ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
n : ℤ
g : SL(2, ℤ)
⊢ (↑(T ^ n * g) : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1
have h : ∀ (j : Fin 2), (↑(T ^ n * g) : Matrix (Fin 2) (Fin 2) ℤ) 1 j = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 j
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
⊢ (↑S : Matrix (Fin 2) (Fin 2) ℤ) * (↑S : Matrix (Fin 2) (Fin 2) ℤ) = -1
have simp : Eq (α := Matrix (Fin 2) (Fin 2) ℤ) (!![-1, 0; 0, -1] : Matrix (Fin 2) (Fin 2) ℤ) (-1 : Matrix (Fin 2) (Fin 2) ℤ)
Tactic: simp only [S, Int.reduceNeg, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd,
    vecMul_cons, head_cons, zero_smul, tail_cons, neg_smul, one_smul, neg_cons, neg_zero, neg_empty,
    empty_vecMul, add_zero, zero_add, empty_mul, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
⊢ S • S • S • T • S • T • S = T⁻¹
have a : ∀ (i j : Fin 2), (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
i j : Fin 2
⊢ (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) i j
have a : (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) j =
  (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
i j : Fin 2
a :
  (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
⊢ (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) i j
have a₁ : (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j =
  (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
j : Fin 2
⊢ (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have a : (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))
    ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
j : Fin 2
a :
  (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have a₁ : (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))
    ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
j : Fin 2
⊢ (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have a : (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))
    ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup (goal)
Goal:
j : Fin 2
a :
  (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have a₁ : (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))
    ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
x : n_1 → R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} N
⊢ Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} (M * N)
have refine : (M * N) *ᵥ 1 = 1
Tactic: refine ⟨fun i j => sum_nonneg fun i _ => mul_nonneg (hM.1 _ _) (hN.1 _ _), ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
x : n_1 → R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} N
⊢ (M * N) *ᵥ 1 = 1
have rw : M *ᵥ N *ᵥ 1 = 1
Tactic: rw [← mulVec_mulVec, hN.2, hM.2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
x : n_1 → R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} N
rw : M *ᵥ N *ᵥ 1 = 1
⊢ (M * N) *ᵥ 1 = 1
have rw₁ : M *ᵥ 1 = 1
Tactic: rw [← mulVec_mulVec, hN.2, hM.2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Stochastic (goal)
Goal:
R_1 : Type u_1
n_1 : Type u_2
inst : Fintype n_1
inst_1 : DecidableEq n_1
inst_2 : Semiring R_1
inst_3 : PartialOrder R_1
inst_4 : IsOrderedRing R_1
M_1 : Matrix n_1 n_1 R_1
x : n_1 → R_1
R : Type u_3
n : Type u_4
inst_5 : Fintype n
inst_6 : DecidableEq n
inst_7 : Semiring R
inst_8 : PartialOrder R
inst_9 : IsOrderedRing R
M N : Matrix n n R
hM : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} M
hN : Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} N
rw : M *ᵥ N *ᵥ 1 = 1
rw₁ : M *ᵥ 1 = 1
⊢ (M * N) *ᵥ 1 = 1
have rw₂ : Eq (α := n → R) 1 1
Tactic: rw [← mulVec_mulVec, hN.2, hM.2]
-- 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 : Matrix n n R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
i j : n
⊢ M i j ≤ 1
have rw : M i j ≤ ∑ j : n, M i j
Tactic: rw [← sum_row_of_mem_rowStochastic hM i]
-- 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 : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j : n
⊢ 0 ≤ (x ᵥ* M) j
have simp : LE.le.{u_1} (α := R) 0 (∑ x_1 : n, x x_1 * M x_1 j)
Tactic: simp only [Matrix.vecMul, dotProduct]
-- 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 : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j : n
⊢ LE.le.{u_1} (α := R) 0 (∑ x_1 : n, x x_1 * M x_1 j)
have h : ∀ (i : n), Membership.mem (γ := Finset n) univ i → 0 ≤ x i * M i j
Tactic: apply Finset.sum_nonneg
-- 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 : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j k : n
h : Membership.mem (γ := Finset n) univ k
⊢ 0 ≤ x k * M k j
have h : 0 ≤ M k j
Tactic: apply mul_nonneg (hx k)
-- 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 : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j : n
⊢ 0 ≤ (M *ᵥ x) j
have simp : LE.le.{u_1} (α := R) 0 (∑ x_1 : n, M j x_1 * x x_1)
Tactic: simp only [Matrix.mulVec, dotProduct]
-- 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 : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j : n
⊢ LE.le.{u_1} (α := R) 0 (∑ x_1 : n, M j x_1 * x x_1)
have h : ∀ (i : n), Membership.mem (γ := Finset n) univ i → 0 ≤ M j i * x i
Tactic: apply Finset.sum_nonneg
-- 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 : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : ∀ (i : n), 0 ≤ x i
j k : n
h : Membership.mem (γ := Finset n) univ k
⊢ 0 ≤ M j k * x k
have h : 0 ≤ M j k
Tactic: refine Left.mul_nonneg ?_ (hx k)
-- 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 : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : x ⬝ᵥ 1 = 1
⊢ x ᵥ* M ⬝ᵥ 1 = 1
have rw : x ⬝ᵥ M *ᵥ 1 = 1
Tactic: rw [← dotProduct_mulVec, hM.2, hx]
-- 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 : Matrix n n R
x : n → R
hM : Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) M
hx : x ⬝ᵥ 1 = 1
rw : x ⬝ᵥ M *ᵥ 1 = 1
rw₁ : x ⬝ᵥ 1 = 1
⊢ x ᵥ* M ⬝ᵥ 1 = 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [← dotProduct_mulVec, hM.2, hx]
-- 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
x : Matrix n n R
hx : x ∈ (↑(rowStochastic R n) : Set (Matrix n n R))
y : Matrix n n R
hy : y ∈ (↑(rowStochastic R n) : Set (Matrix n n R))
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
h : a + b = 1
⊢ a • x + b • y ∈ (↑(rowStochastic R n) : Set (Matrix n n R))
have simp : ∀ (hx : (∀ (i j : n), 0 ≤ x i j) ∧ ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, x i j) 1)
  (hy : (∀ (i j : n), 0 ≤ y i j) ∧ ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, y i j) 1),
  (∀ (i j : n), 0 ≤ (a • x + b • y) i j) ∧ ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, (a • x + b • y) i j) 1
Tactic: simp only [SetLike.mem_coe, mem_rowStochastic_iff_sum] at hx hy ⊢
Cleared hypotheses: hx, hy
-- 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
σ : Equiv.Perm n
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (rowStochastic R n) (Equiv.Perm.permMatrix R σ)
have rw : (∀ (i j : n), 0 ≤ Equiv.Perm.permMatrix R σ i j) ∧
  ∀ (i : n), Eq.{u_1 + 1} (α := R) (∑ j : n, Equiv.Perm.permMatrix R σ i j) 1
Tactic: rw [mem_rowStochastic_iff_sum]