awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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 : n
h_pos : 0 < HPow.hPow (β := ℕ) A 0 i j
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }
have zero : ∀ (h_pos : 0 < HPow.hPow (β := ℕ) A 0 i i), Nonempty.{max 1 (u_1 + 1)} { p : Path i i // p.length = 0 }
Tactic: rcases eq_or_ne i j with rfl | h_eq
Cleared hypotheses: j, h_pos
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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 : n
h_pos : 0 < HPow.hPow (β := ℕ) A 0 i j
zero : ∀ (h_pos : 0 < HPow.hPow (β := ℕ) A 0 i i), Nonempty.{max 1 (u_1 + 1)} { p : Path i i // p.length = 0 }
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }
have zero₁ : ∀ (h_eq : i ≠ j), Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }
Tactic: rcases eq_or_ne i j with rfl | h_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
⊢ 0 < (A ^ (m + 1)) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
have succ : LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j) ↔
  Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
Tactic: rw [pow_succ, mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
⊢ LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j) ↔
    Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
have succ : LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j) →
  Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
succ :
  LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j) →
    Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
⊢ LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j) ↔
    Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
have succ₁ : Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 } →
  LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
h_pos : LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
have succ : ∀ (l : n) (hl_mem : Membership.mem (γ := Finset n) Finset.univ l) (hl_pos : 0 < (A ^ m) i l * A l j),
  Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
Tactic: 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
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
h_pos : LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
l : n
hl_mem : Membership.mem (γ := Finset n) Finset.univ l
hl_pos : 0 < (A ^ m) i l * A l j
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
have hAm_nonneg : 0 ≤ (A ^ m) i l
Tactic: have hAm_nonneg : 0 ≤ (A ^ m) i l := pow_apply_nonneg hA m i l
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
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
h_pos : LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
l : n
hl_mem : Membership.mem (γ := Finset n) Finset.univ l
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
have hA_nonneg' : 0 ≤ A l j
Tactic: have hA_nonneg' : 0 ≤ A l j := hA l j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
h_pos : LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
l : n
hl_mem : Membership.mem (γ := Finset n) Finset.univ l
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
⊢ 0 < (A ^ m) i l
have by_contra! : ∀ (h : (A ^ m) i l ≤ 0), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
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
h_pos : LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
l : n
hl_mem : Membership.mem (γ := Finset n) Finset.univ l
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
have h_Am : 0 < (A ^ m) i l
Tactic: have h_Am : 0 < (A ^ m) i l := by by_contra! h; simp [le_antisymm h hAm_nonneg] at hl_pos
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
h_pos : LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
l : n
hl_mem : Membership.mem (γ := Finset n) Finset.univ l
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
h_Am : 0 < (A ^ m) i l
⊢ 0 < A l j
have by_contra! : ∀ (h : A l j ≤ 0), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
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
h_pos : LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
l : n
hl_mem : Membership.mem (γ := Finset n) Finset.univ l
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
h_Am : 0 < (A ^ m) i l
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
have h_A : 0 < A l j
Tactic: have h_A : 0 < A l j := by by_contra! h; simp [le_antisymm h hA_nonneg'] at hl_pos
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
h_pos : LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
l : n
hl_mem : Membership.mem (γ := Finset n) Finset.univ l
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
h_Am : 0 < (A ^ m) i l
h_A : 0 < A l j
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }
have succ : ∀ (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: obtain ⟨⟨p, rfl⟩⟩ := (ih i l).mp h_Am
Cleared hypotheses: m, ih, h_pos, hl_pos, hAm_nonneg, h_Am
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
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
⊢ LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
have hp_len₁ : q.length = m
Tactic: simp only [Quiver.Path.length_cons, Nat.succ.injEq] at hp_len
Cleared hypotheses: hp_len
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
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
⊢ LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
have h_Am_pos : 0 < (A ^ m) i b
Tactic: have h_Am_pos : 0 < (A ^ m) i b := (ih i b).mpr ⟨q, hp_len⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
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
⊢ LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
have h_prod : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
⊢ LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
have 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)
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⟩
Cleared hypotheses: j, p, hp_len
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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)
⊢ LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
have 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)
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⟩
Cleared hypotheses: p, hp_len
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
⊢ 0 < (A ^ k) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = k }
have zero : ∀ (i j : n), 0 < HPow.hPow (β := ℕ) A 0 i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }
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⟩
Cleared hypotheses: k, i, j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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 }
⊢ 0 < (A ^ k) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = k }
have 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 }
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⟩
Cleared hypotheses: k, i, j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
⊢ A.IsIrreducible ↔ ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
have mp : A.IsIrreducible → ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
⊢ A.IsIrreducible ↔ ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
have mpr : (∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j) → A.IsIrreducible
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
⊢ ∃ k > 0, 0 < (A ^ k) i j
have mp : ∀ (p : Path i j) (hp_len : 0 < p.length), ∃ k > 0, 0 < (A ^ k) i j
Tactic: obtain ⟨p, hp_len⟩ := h_irr.2 i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
have mp : 0 < (A ^ p.length) i j
Tactic: refine ⟨p.length, hp_len, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
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
⊢ 0 < (A ^ p.length) i j
have this₁ : 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⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
⊢ A.IsIrreducible
have mpr₁ : IsSStronglyConnected n
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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), 0 < p.length
have mpr : ∀ (k : ℕ) (hk_pos : k > 0) (hk_entry : 0 < (A ^ k) i j), ∃ (p : Path i j), 0 < p.length
Tactic: obtain ⟨k, hk_pos, hk_entry⟩ := h_exists i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
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
⊢ ∃ (p : Path i j), 0 < p.length
have 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
Tactic: obtain ⟨⟨p, rfl⟩⟩ :=
        (pow_apply_pos_iff_nonempty_path (A := A) hA k i j).mp hk_entry
Cleared hypotheses: k, hk_pos, hk_entry