awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
i j l : n
hl_mem : Membership.mem (γ := Finset n) Finset.univ l
hA_nonneg' : 0 ≤ A l j
h_A : 0 < A l j
p : Path i l
ih : ∀ (i_1 j : n), 0 < (A ^ p.length) i_1 j ↔ Nonempty.{max 1 (u_1 + 1)} { p_1 : Path i_1 j // p_1.length = p.length }
h_pos : LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ p.length) i j_1 * A j_1 j)
hl_pos : 0 < (A ^ p.length) i l * A l j
hAm_nonneg : 0 ≤ (A ^ p.length) i l
h_Am : 0 < (A ^ p.length) i l
⊢ Nonempty.{max 1 (u_1 + 1)} { p_1 : Path i j // p_1.length = p.length + 1 }

Tactic:
exact ⟨p.cons (PLift.up h_A), by simp⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m }
i : n
hp_len : length.{u_1, 0} (V := n) (a := i) nil = m + 1
⊢ LT.lt.{u_2} (α := R) 0 (∑ j : n, (A ^ m) i j * A j i)

Tactic:
simp [Quiver.Path.length] at hp_len

Premises used: Quiver.Path.length
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m }
i j b : n
q : Path i b
e : b ⟶ j
hp_len : (q.cons e).length = m + 1
⊢ q.length = m

Tactic:
simp only [Quiver.Path.length_cons, Nat.succ.injEq] at hp_len

Premises used: Nat.succ.injEq, Quiver.Path.length_cons
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m }
i j b : n
q : Path i b
e : b ⟶ j
hp_len : q.length = m
⊢ 0 < (A ^ m) i b

Tactic:
have h_Am_pos : 0 < (A ^ m) i b := (ih i b).mpr ⟨q, hp_len⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m }
i j b : n
q : Path i b
e : b ⟶ j
hp_len : q.length = m
h_Am_pos : 0 < (A ^ m) i b
h_A_pos : b ⟶ j := e
⊢ 0 < (A ^ m) i b * A b j

Tactic:
have h_prod : 0 < (A ^ m) i b * A b j := mul_pos h_Am_pos h_A_pos.down
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m }
i j b : n
q : Path i b
e : b ⟶ j
hp_len : q.length = m
h_Am_pos : 0 < (A ^ m) i b
h_A_pos : b ⟶ j := e
h_prod : 0 < (A ^ m) i b * A b j
⊢ LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)

Tactic:
(Finset.sum_pos_iff_of_nonneg
            (fun x _ => mul_nonneg (pow_apply_nonneg hA m i x) (hA x j))).2
            ⟨b, Finset.mem_univ b, h_prod⟩

Premises used: Iff.mpr, Finset.mem_univ, mul_nonneg, Matrix.pow_apply_nonneg, Finset.sum_pos_iff_of_nonneg, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m }
i j b : n
q : Path i b
e : b ⟶ j
hp_len : q.length = m
h_Am_pos : 0 < (A ^ m) i b
h_A_pos : b ⟶ j := e
h_prod : 0 < (A ^ m) i b * A b j
⊢ LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)

Tactic:
exact
          (Finset.sum_pos_iff_of_nonneg
            (fun x _ => mul_nonneg (pow_apply_nonneg hA m i x) (hA x j))).2
            ⟨b, Finset.mem_univ b, h_prod⟩

Premises used: Iff.mpr, Finset.mem_univ, mul_nonneg, Matrix.pow_apply_nonneg, Finset.sum_pos_iff_of_nonneg, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m }
i j : n
p : Path i j
hp_len : p.length = m + 1
succ : ∀ (hp_len : length.{u_1, 0} (V := n) (a := i) nil = m + 1), LT.lt.{u_2} (α := R) 0 (∑ j : n, (A ^ m) i j * A j i)
succ₁ :
  ∀ {b : n} (q : Path i b) (e : b ⟶ j) (hp_len : (q.cons e).length = m + 1),
    LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
⊢ LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)

Tactic:
cases p with
      | nil => simp [Quiver.Path.length] at hp_len
      | @cons b _ q e =>
        simp only [Quiver.Path.length_cons, Nat.succ.injEq] at hp_len
        have h_Am_pos : 0 < (A ^ m) i b := (ih i b).mpr ⟨q, hp_len⟩
        let h_A_pos := e
        have h_prod : 0 < (A ^ m) i b * A b j := mul_pos h_Am_pos h_A_pos.down
        exact
          (Finset.sum_pos_iff_of_nonneg
            (fun x _ => mul_nonneg (pow_apply_nonneg hA m i x) (hA x j))).2
            ⟨b, Finset.mem_univ b, h_prod⟩

Premises used: Nat.succ.injEq, Quiver.Path.length_cons, Quiver.Path.nil, Quiver.Path.cons, Quiver.Path.length
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
k : ℕ
i j : n
this : Quiver n := A.toQuiver
zero : ∀ (i j : n), 0 < HPow.hPow (β := ℕ) A 0 i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }
succ :
  ∀ (m : ℕ) (ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m }) (i j : n),
    0 < (A ^ (m + 1)) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
⊢ 0 < (A ^ k) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = k }

Tactic:
induction k generalizing i j with
  | zero =>
    refine ⟨fun h_pos ↦ ?_, fun ⟨p, hp⟩ ↦ ?_⟩
    · rcases eq_or_ne i j with rfl | h_eq
      · exact ⟨⟨Quiver.Path.nil, rfl⟩⟩
      · simp_all
    · simp [Quiver.Path.eq_of_length_zero p hp]
  | succ m ih =>
    rw [pow_succ, mul_apply]
    constructor
    · intro h_pos
      obtain ⟨l, hl_mem, hl_pos⟩ :
          ∃ l ∈ (Finset.univ : Finset n), 0 < (A ^ m) i l * A l j := by
        simpa [Finset.sum_pos_iff_of_nonneg
                 (fun x _ => mul_nonneg (pow_apply_nonneg hA m i x) (hA x j))]
          using h_pos
      have hAm_nonneg : 0 ≤ (A ^ m) i l := pow_apply_nonneg hA m i l
      have hA_nonneg' : 0 ≤ A l j := hA l j
      have h_Am : 0 < (A ^ m) i l := by by_contra! h; simp [le_antisymm h hAm_nonneg] at hl_pos
      have h_A : 0 < A l j := by by_contra! h; simp [le_antisymm h hA_nonneg'] at hl_pos
      obtain ⟨⟨p, rfl⟩⟩ := (ih i l).mp h_Am
      exact ⟨p.cons (PLift.up h_A), by simp⟩
    · rintro ⟨p, hp_len⟩
      cases p with
      | nil => simp [Quiver.Path.length] at hp_len
      | @cons b _ q e =>
        simp only [Quiver.Path.length_cons, Nat.succ.injEq] at hp_len
        have h_Am_pos : 0 < (A ^ m) i b := (ih i b).mpr ⟨q, hp_len⟩
        let h_A_pos := e
        have h_prod : 0 < (A ^ m) i b * A b j := mul_pos h_Am_pos h_A_pos.down
        exact
          (Finset.sum_pos_iff_of_nonneg
            (fun x _ => mul_nonneg (pow_apply_nonneg hA m i x) (hA x j))).2
            ⟨b, Finset.mem_univ b, h_prod⟩

Premises used: Nat.succ.injEq, Finset.univ, Quiver.Path.length_cons, Quiver.Path.nil, pow_succ, Matrix.mul_apply, Quiver.Path.cons, Quiver.Path.length, eq_or_ne, Matrix.zero, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
mp : A.IsIrreducible → ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
mpr : (∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j) → A.IsIrreducible
⊢ A.IsIrreducible ↔ ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
h_irr : A.IsIrreducible
i j : n
mp : ∀ (p : Path i j) (hp_len : 0 < p.length), ∃ k > 0, 0 < (A ^ k) i j
⊢ ∃ k > 0, 0 < (A ^ k) i j

Tactic:
obtain ⟨p, hp_len⟩ := h_irr.2 i j

Premises used: Matrix.IsIrreducible.connected
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
h_irr : A.IsIrreducible
i j : n
p : Path i j
hp_len : 0 < p.length
⊢ ∃ k > 0, 0 < (A ^ k) i j

Tactic:
⟨p.length, hp_len, ?_⟩

Premises used: Quiver.Path.length, And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
h_irr : A.IsIrreducible
i j : n
p : Path i j
hp_len : 0 < p.length
mp : 0 < (A ^ p.length) i j
⊢ ∃ k > 0, 0 < (A ^ k) i j

Tactic:
refine ⟨p.length, hp_len, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
h_irr : A.IsIrreducible
i j : n
p : Path i j
hp_len : 0 < p.length
⊢ Nonempty.{max 1 (u_1 + 1)} { q : Path i j // q.length = p.length }

Tactic:
have : Nonempty {q : Path i j // q.length = p.length} := ⟨⟨p, rfl⟩⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this_1 : Quiver n := A.toQuiver
h_irr : A.IsIrreducible
i j : n
p : Path i j
hp_len : 0 < p.length
this : Nonempty.{max 1 (u_1 + 1)} { q : Path i j // q.length = p.length }
⊢ 0 < (A ^ p.length) i j

Tactic:
have hpos :=
      (pow_apply_pos_iff_nonempty_path (A := A) hA p.length i j).2 this
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this_1 : Quiver n := A.toQuiver
h_irr : A.IsIrreducible
i j : n
p : Path i j
hp_len : 0 < p.length
this : Nonempty.{max 1 (u_1 + 1)} { q : Path i j // q.length = p.length }
hpos : 0 < (A ^ p.length) i j
⊢ 0 < (A ^ p.length) i j

Tactic:
simpa using hpos
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
mpr : ∀ (i j : n), 0 ≤ A i j
mpr₁ : IsSStronglyConnected n
⊢ A.IsIrreducible

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
⊢ ∀ (i j : n), 0 ≤ A i j

Tactic:
hA
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
⊢ ∀ (i j : n), 0 ≤ A i j

Tactic:
exact hA
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
i j : n
mpr : ∀ (k : ℕ) (hk_pos : k > 0) (hk_entry : 0 < (A ^ k) i j), ∃ (p : Path i j), 0 < p.length
⊢ ∃ (p : Path i j), 0 < p.length

Tactic:
obtain ⟨k, hk_pos, hk_entry⟩ := h_exists i j
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
i j : n
k : ℕ
hk_pos : k > 0
hk_entry : 0 < (A ^ k) i j
mpr : ∀ (p : Path i j) (hk_pos : p.length > 0) (hk_entry : 0 < (A ^ p.length) i j), ∃ (p : Path i j), 0 < p.length
⊢ ∃ (p : Path i j), 0 < p.length

Tactic:
obtain ⟨⟨p, rfl⟩⟩ :=
        (pow_apply_pos_iff_nonempty_path (A := A) hA k i j).mp hk_entry

Premises used: Matrix.pow_apply_pos_iff_nonempty_path, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
i j : n
p : Path i j
hk_pos : p.length > 0
hk_entry : 0 < (A ^ p.length) i j
⊢ ∃ (p : Path i j), 0 < p.length

Tactic:
⟨p, hk_pos⟩

Premises used: Exists.intro
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
i j : n
p : Path i j
hk_pos : p.length > 0
hk_entry : 0 < (A ^ p.length) i j
⊢ ∃ (p : Path i j), 0 < p.length

Tactic:
exact ⟨p, hk_pos⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
h_prim : A.IsPrimitive
obtain :
  ∀ (h_nonneg : ∀ (i j : n), 0 ≤ A i j) (k : ℕ) (hk_pos : k > 0) (hk_all : ∀ (i j : n), 0 < (A ^ k) i j),
    A.IsIrreducible
⊢ A.IsIrreducible

Tactic:
obtain ⟨h_nonneg, k, hk_pos, hk_all⟩ := h_prim
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
h_nonneg : ∀ (i j : n), 0 ≤ A i j
k : ℕ
hk_pos : k > 0
hk_all : ∀ (i j : n), 0 < (A ^ k) i j
rw : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
⊢ A.IsIrreducible

Tactic:
rw [isIrreducible_iff_exists_pow_pos h_nonneg]

Premises used: Matrix.isIrreducible_iff_exists_pow_pos
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
h_nonneg : ∀ (i j : n), 0 ≤ A i j
k : ℕ
hk_pos : k > 0
hk_all : ∀ (i j : n), 0 < (A ^ k) i j
⊢ ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
i j : n
this : Quiver n := A.toQuiver
⊢ Path i i

Tactic:
exact (@Quiver.Path.nil _ (toQuiver Aᵀ) _)

Premises used: Quiver.Path.nil
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
i j : n
this : Quiver n := A.toQuiver
b c : n
q : Path i b
e : b ⟶ c
ih : Path b i
⊢ 0 < Aᵀ c b

Tactic:
simpa [Matrix.transpose_apply] using e.down

Premises used: PLift.down, Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
i j : n
this : Quiver n := A.toQuiver
b c : n
q : Path i b
e : b ⟶ c
ih : Path b i
⊢ 0 < Aᵀ c b

Tactic:
have eT : 0 < (Aᵀ) c b := by
      simpa [Matrix.transpose_apply] using e.down
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
i j : n
this : Quiver n := A.toQuiver
b c : n
q : Path i b
e : b ⟶ c
ih : Path b i
eT : 0 < Aᵀ c b
⊢ Path c i

Tactic:
exact (@Quiver.Path.comp n (toQuiver Aᵀ) c b i (@Quiver.Hom.toPath n (toQuiver Aᵀ) c b
      (PLift.up eT)) ih)

Premises used: PLift.up, Quiver.Hom.toPath, Quiver.Path.comp
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
i j : n
p : Path i j
this : Quiver n := A.toQuiver
nil : Path i i
cons : {b c : n} → (q : Path i b) → (e : b ⟶ c) → (ih : Path b i) → Path c i
⊢ Path j i

Tactic:
induction p with
  | nil =>
    exact (@Quiver.Path.nil _ (toQuiver Aᵀ) _)
  | @cons b c q e ih =>
    have eT : 0 < (Aᵀ) c b := by
      simpa [Matrix.transpose_apply] using e.down
    exact (@Quiver.Path.comp n (toQuiver Aᵀ) c b i (@Quiver.Hom.toPath n (toQuiver Aᵀ) c b
      (PLift.up eT)) ih)

Premises used: Quiver.Path.nil, Quiver.Path.cons
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
i j : n
⊢ 0 ≤ Aᵀ i j

Tactic:
simpa [Matrix.transpose_apply] using hA.nonneg j i

Premises used: Matrix.IsIrreducible.nonneg, Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
⊢ ∀ (i j : n), 0 ≤ Aᵀ i j

Tactic:
have hA_T_nonneg : ∀ i j, 0 ≤ Aᵀ i j := fun i j => by
    simpa [Matrix.transpose_apply] using hA.nonneg j i
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
⊢ Aᵀ.IsIrreducible

Tactic:
⟨hA_T_nonneg, ?_⟩

Premises used: Matrix.IsIrreducible.mk
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
refine : IsSStronglyConnected n
⊢ Aᵀ.IsIrreducible

Tactic:
refine ⟨hA_T_nonneg, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this : Quiver n := A.toQuiver
obtain : ∀ (p : Path j i) (hp_pos : 0 < p.length), ∃ (p : Path i j), 0 < p.length
⊢ ∃ (p : Path i j), 0 < p.length

Tactic:
obtain ⟨p, hp_pos⟩ := hA.connected j i

Premises used: Matrix.IsIrreducible.connected
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i : n
this : Quiver n := A.toQuiver
hp_pos : 0 < length.{u_1, 0} (V := n) (a := i) nil
⊢ ∃ (p : Path i i), 0 < p.length

Tactic:
simp at hp_pos
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this_1 : Quiver n := A.toQuiver
b : n
q : Path j b
e : b ⟶ i
hp_pos : 0 < (q.cons e).length
qT : Path i j := transposePath (q.cons e)
this : Quiver n := Aᵀ.toQuiver
h : 0 < qT.length
⊢ ∃ (p : Path i j), 0 < p.length

Tactic:
use qT
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this_1 : Quiver n := A.toQuiver
b : n
q : Path j b
e : b ⟶ i
hp_pos : 0 < (q.cons e).length
qT : Path i j := transposePath (q.cons e)
this : Quiver n := Aᵀ.toQuiver
⊢ 0 < qT.length

Tactic:
simp [qT, transposePath, Quiver.Path.length_comp, Quiver.Path.length_toPath]

Premises used: Quiver.Path.length_comp, Matrix.transposePath, Quiver.Path.length_toPath
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this : Quiver n := A.toQuiver
p : Path j i
hp_pos : 0 < p.length
nil : ∀ (hp_pos : 0 < length.{u_1, 0} (V := n) (a := i) Path.nil), ∃ (p : Path i i), 0 < p.length
cons : ∀ {b : n} (q : Path j b) (e : b ⟶ i) (hp_pos : 0 < (q.cons e).length), ∃ (p : Path i j), 0 < p.length
⊢ ∃ (p : Path i j), 0 < p.length

Tactic:
cases p with
  | nil =>
    simp at hp_pos
  | @cons b _ q e =>
    let qT := transposePath (A := A) (q.cons e)
    letI : Quiver n := toQuiver Aᵀ
    use qT
    simp [qT, transposePath, Quiver.Path.length_comp, Quiver.Path.length_toPath]

Premises used: Quiver.Path.nil, Quiver.Path.cons, Quiver.Path.length_comp, Matrix.transposePath, Quiver.Path.length_toPath
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
pos : ∀ (hA_nonneg : ∀ (i j : n), 0 ≤ A i j), Aᵀ.IsIrreducible ↔ A.IsIrreducible
neg : ∀ (hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j), Aᵀ.IsIrreducible ↔ A.IsIrreducible
⊢ Aᵀ.IsIrreducible ↔ A.IsIrreducible

Tactic:
by_cases hA_nonneg : ∀ i j, 0 ≤ A i j
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA_nonneg : ∀ (i j : n), 0 ≤ A i j
h : Aᵀ.IsIrreducible
i j : n
⊢ 0 ≤ Aᵀ i j

Tactic:
simpa [Matrix.transpose_apply] using hA_nonneg j i

Premises used: Matrix.transpose_apply