awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
a b : R
hab : IsCoprime a b
i : Fin 2
obtain :
  ∀ (u v : R) (h : u * a + v * b = 1),
    ∃ (g : SL(2, R)), (↑g : Matrix (Fin 2) (Fin 2) R) i 0 = a ∧ (↑g : Matrix (Fin 2) (Fin 2) R) i 1 = b
⊢ ∃ (g : SL(2, R)), (↑g : Matrix (Fin 2) (Fin 2) R) i 0 = a ∧ (↑g : Matrix (Fin 2) (Fin 2) R) i 1 = b

Tactic:
obtain ⟨u, v, h⟩ := hab
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ ∃ (g : SL(2, R)), (↑g : Matrix (Fin 2) (Fin 2) R) i 0 = a ∧ (↑g : Matrix (Fin 2) (Fin 2) R) i 1 = b

Tactic:
match i with
  | 0 => ⟨⟨!![a, b; -v, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, -u; a, b], ?_⟩, rfl, rfl⟩

Premises used: Matrix.of, Exists, Subtype.mk, And, _private.0.Matrix.SpecialLinearGroup.isCoprime_row.match_1, And.intro, Exists.intro, Matrix.vecEmpty, OfNat.ofNat, Subtype.val, Eq, DFunLike.coe, Matrix.vecCons, Neg.neg, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
refine_1 : Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![a, b; -v, u]) 1
refine_2 : Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![v, -u; a, b]) 1
⊢ ∃ (g : SL(2, R)), (↑g : Matrix (Fin 2) (Fin 2) R) i 0 = a ∧ (↑g : Matrix (Fin 2) (Fin 2) R) i 1 = b

Tactic:
refine match i with
  | 0 => ⟨⟨!![a, b; -v, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, -u; a, b], ?_⟩, rfl, rfl⟩
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
refine_1 : a * u - b * -v = u * a + v * b
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![a, b; -v, u]) 1

Tactic:
rw [Matrix.det_fin_two_of, ← h]

Premises used: Matrix.det_fin_two_of
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ a * u - b * -v = u * a + v * b

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
refine_2 : v * b - -u * a = u * a + v * b
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin 2) !![v, -u; a, b]) 1

Tactic:
rw [Matrix.det_fin_two_of, ← h]

Premises used: Matrix.det_fin_two_of
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ v * b - -u * a = u * a + v * b

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A : SL(2, R)
obtain :
  ∀ (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)
⊢ IsCoprime ((v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) R)) 0) ((v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) R)) 1)

Tactic:
obtain ⟨g, hg⟩ := hab.exists_SL2_row 0

Premises used: IsCoprime.exists_SL2_row, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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, ⋯⟩)
1 : v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ v t = (↑g : Matrix (Fin 2) (Fin 2) R) 0 t

Tactic:
fin_cases t
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
0 h h_1 h_2 h_3 h_4 h_5 h_6 :
  (↑g : Matrix (Fin 2) (Fin 2) R) 0 0 = v 0 →
    (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = v 1 →
      v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
tauto
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
1 h h_1 h_2 h_3 h_4 h_5 h_6 :
  (↑g : Matrix (Fin 2) (Fin 2) R) 0 0 = v 0 →
    (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = v 1 →
      v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
tauto
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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, ⋯⟩)
1 : v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
h : v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h_1 : v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
h_2 : v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h_3 : v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
h_4 : v ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
h_5 : v ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) = (↑g : Matrix (Fin 2) (Fin 2) R) 0 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ v t = (↑g : Matrix (Fin 2) (Fin 2) R) 0 t

Tactic:
{ fin_cases t <;> tauto }
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
⊢ v = (↑g : Matrix (Fin 2) (Fin 2) R) 0

Tactic:
have : v = g 0 := funext fun t ↦ by { fin_cases t <;> tauto }
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
this : v = (↑g : Matrix (Fin 2) (Fin 2) R) 0
⊢ IsCoprime ((v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) R)) 0) ((v ᵥ* (↑A : Matrix (Fin 2) (Fin 2) R)) 1)

Tactic:
simpa only [this] using isCoprime_row (g * A) 0

Premises used: HMul.hMul, Matrix.SpecialLinearGroup.isCoprime_row, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
R : Type u_1
inst : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A : SL(2, R)
⊢ IsCoprime (((↑A : Matrix (Fin 2) (Fin 2) R) *ᵥ v) 0) (((↑A : Matrix (Fin 2) (Fin 2) R) *ᵥ v) 1)

Tactic:
simpa only [← vecMul_transpose] using hab.vecMulSL A.transpose

Premises used: IsCoprime.vecMulSL, Matrix.SpecialLinearGroup.transpose, Matrix.vecMul_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
F : Type u_1
inst : CommRing F
ι : Type u_2
inst_1 : DecidableEq ι
inst_2 : Fintype ι
m : SpecialLinearGroup ι F
v : ι → F
⊢ m • v = (↑m : Matrix ι ι F) • v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
⊢ Eq (α := ℤ) (det (n := Fin 2) !![0, -1; 1, 0]) 1

Tactic:
simp [Matrix.det_fin_two_of]

Premises used: Matrix.det_fin_two_of
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
⊢ Eq (α := ℤ) (det (n := Fin 2) !![1, 1; 0, 1]) 1

Tactic:
simp [Matrix.det_fin_two_of]

Premises used: Matrix.det_fin_two_of
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
⊢ (↑S : Matrix (Fin 2) (Fin 2) ℤ) = !![0, -1; 1, 0]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
⊢ S⁻¹ = -S

Tactic:
decide
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
⊢ (↑T : Matrix (Fin 2) (Fin 2) ℤ) = !![1, 1; 0, 1]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
⊢ (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) = !![1, -1; 0, 1]

Tactic:
simp [coe_inv, coe_T, adjugate_fin_two]

Premises used: Matrix.adjugate_fin_two, Matrix.SpecialLinearGroup.coe_inv, ModularGroup.coe_T
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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) ℤ)
zero₂ 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) ℤ)
⊢ (↑(HPow.hPow (β := ℤ) T 0) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, 0; 0, 1]

Tactic:
rw [zpow_zero, coe_one, Matrix.one_fin_two]

Premises used: Matrix.SpecialLinearGroup.coe_one, zpow_zero, Matrix.one_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (↑n : ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, (↑n : ℤ); 0, 1]
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) ℤ)
⊢ (↑(T ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1; 0, 1]

Tactic:
simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]

Premises used: zpow_add, zpow_one, Matrix.mul_fin_two, ModularGroup.coe_T, Matrix.SpecialLinearGroup.coe_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (↑n : ℤ)) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, (↑n : ℤ); 0, 1]
succ : HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 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) ℤ)

Tactic:
congrm !![_, ?_; _, _]
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
succ₂ succ₃ : HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
⊢ HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (↑n : ℤ) 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1

Tactic:
rw [mul_one, mul_one, add_comm]

Premises used: add_comm, mul_one
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (-(↑n : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, -(↑n : ℤ); 0, 1]
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) ℤ)
⊢ (↑(T ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1; 0, 1]

Tactic:
simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]

Premises used: ModularGroup.coe_T_inv, zpow_one, Matrix.mul_fin_two, Matrix.SpecialLinearGroup.coe_mul, zpow_sub
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
pred₁ : HMul.hMul (α := ℤ) 1 (-1) + HMul.hMul (α := ℤ) (-(↑n : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑n : ℤ)) 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) ℤ)

Tactic:
congrm !![?_, ?_; _, _]
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (-(↑n : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, -(↑n : ℤ); 0, 1]
⊢ HMul.hMul (α := ℤ) 1 1 + HMul.hMul (α := ℤ) (-(↑n : ℤ)) 0 = 1

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : ℕ
h : (↑(HPow.hPow (β := ℤ) T (-(↑n : ℤ))) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, -(↑n : ℤ); 0, 1]
⊢ HMul.hMul (α := ℤ) 1 (-1) + HMul.hMul (α := ℤ) (-(↑n : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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]
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]
⊢ (↑(T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) = !![1, n; 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

Premises used: zpow_add, Matrix.SpecialLinearGroup.coe_one, zpow_zero, ModularGroup.coe_T_inv, zpow_one, add_comm, Matrix.mul_fin_two, ModularGroup.coe_T, mul_one, Matrix.zero, Matrix.SpecialLinearGroup.coe_mul, zpow_sub, Matrix.one_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : ℤ
g : SL(2, ℤ)
h : ∀ (j : Fin 2), (↑(T ^ n * g) : Matrix (Fin 2) (Fin 2) ℤ) 1 j = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 j
⊢ (↑(T ^ n * g) : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
n : ℤ
g : SL(2, ℤ)
j : Fin 2
⊢ (↑(T ^ n * g) : Matrix (Fin 2) (Fin 2) ℤ) 1 j = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 j

Tactic:
simp [coe_T_zpow, Matrix.vecMul, dotProduct, Fin.sum_univ_succ]

Premises used: dotProduct, Matrix.vecMul, ModularGroup.coe_T_zpow, Fin.sum_univ_succ
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
g : SL(2, ℤ)
⊢ (↑(T * g) : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1

Tactic:
simpa using T_pow_mul_apply_one 1 g

Premises used: ModularGroup.T_pow_mul_apply_one, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
g : SL(2, ℤ)
⊢ (↑(T⁻¹ * g) : Matrix (Fin 2) (Fin 2) ℤ) 1 = (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1

Tactic:
simpa using T_pow_mul_apply_one (-1) g

Premises used: ModularGroup.T_pow_mul_apply_one, OfNat.ofNat, Neg.neg
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
simp : Eq (α := Matrix (Fin 2) (Fin 2) ℤ) (!![-1, 0; 0, -1] : Matrix (Fin 2) (Fin 2) ℤ) (-1 : Matrix (Fin 2) (Fin 2) ℤ)
⊢ (↑S : Matrix (Fin 2) (Fin 2) ℤ) * (↑S : Matrix (Fin 2) (Fin 2) ℤ) = -1

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]

Premises used: Matrix.empty_vecMul, neg_smul, Matrix.neg_cons, Nat.succ_eq_add_one, Equiv.symm_apply_apply, Matrix.head_cons, Int.reduceNeg, Matrix.tail_cons, Nat.reduceAdd, Matrix.cons_mul, zero_add, one_smul, ModularGroup.S, zero_smul, Matrix.empty_mul, add_zero, Matrix.neg_empty, neg_zero, Matrix.vecMul_cons
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℤ) (!![-1, 0; 0, -1] : Matrix (Fin 2) (Fin 2) ℤ) (-1 : Matrix (Fin 2) (Fin 2) ℤ)

Tactic:
Eq.symm (eta_fin_two (-1))

Premises used: Matrix.eta_fin_two, OfNat.ofNat, Eq.symm, Neg.neg
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℤ) (!![-1, 0; 0, -1] : Matrix (Fin 2) (Fin 2) ℤ) (-1 : Matrix (Fin 2) (Fin 2) ℤ)

Tactic:
exact Eq.symm (eta_fin_two (-1))

Premises used: Matrix.eta_fin_two, OfNat.ofNat, Eq.symm, Neg.neg
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
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
⊢ S • S • S • T • S • T • S = T⁻¹

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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
a₁ :
  (↑(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
⊢ (↑(S • S • S • T • S • T • S) : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) i j

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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, ⋯⟩)
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) (⟨1, ⋯⟩ : Fin 2)) =
    (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑(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

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
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, ⋯⟩)
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) (⟨1, ⋯⟩ : Fin 2)) =
    (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (↑(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

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
⊢ (↑(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, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
⊢ (↑(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) (⟨1, ⋯⟩ : Fin 2)) =
    (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
⊢ (↑(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, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Goal:
⊢ (↑(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) (⟨1, ⋯⟩ : Fin 2)) =
    (↑T⁻¹ : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.StdBasis
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
m : Type u_4
n : Type u_5
inst : Fintype m
inst_1 : Fintype n
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
i : m
j : n
k : ι
inst_5 : DecidableEq m
inst_6 : DecidableEq n
⊢ Eq (α := Matrix m n M) ((Basis.matrix m n b : (a : m × n × ι) → Matrix m n M) (i, j, k) : Matrix m n M)
    (Matrix.single i j ((b : (a : ι) → M) k) : Matrix m n M)

Tactic:
simp [Basis.matrix, Matrix.single_eq_of_single_single]

Premises used: Module.Basis.matrix, Matrix.single_eq_of_single_single
-- Module: Mathlib.LinearAlgebra.Matrix.StdBasis
Goal:
R : Type u_1
m : Type u_2
n : Type u_3
inst : Fintype m
inst_1 : Finite n
inst_2 : Semiring R
i : m
j : n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
⊢ Eq (α := Matrix m n R) ((stdBasis R m n : (a : m × n) → Matrix m n R) (i, j) : Matrix m n R)
    (single i j 1 : Matrix m n R)

Tactic:
simp [stdBasis, single_eq_of_single_single]

Premises used: Matrix.stdBasis, Matrix.single_eq_of_single_single
-- Module: Mathlib.LinearAlgebra.Matrix.StdBasis
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
m : Type u_3
n : Type u_4
inst_4 : Finite m
inst_5 : Finite n
⊢ Free R (Matrix m n M)

Tactic:
Module.Free.pi R _

Premises used: Matrix, Module.Free.pi
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
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)

Tactic:
⟨fun i j => sum_nonneg fun i _ => mul_nonneg (hM.1 _ _) (hN.1 _ _), ?_⟩

Premises used: mul_nonneg, Set.Mem, setOf, Finset.sum_nonneg, And.left, And.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Stochastic
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
refine : (M * N) *ᵥ 1 = 1
⊢ Membership.mem (γ := Set (Matrix n n R)) {M : Matrix n n R | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1} (M * N)

Tactic:
refine ⟨fun i j => sum_nonneg fun i _ => mul_nonneg (hM.1 _ _) (hN.1 _ _), ?_⟩