awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
R : Type u_1
inst : Semiring R
inst_1 : InvariantBasisNumber R
⊢ InvariantBasisNumber.{u_1} Rᵐᵒᵖ

Tactic:
MulOpposite.invariantBasisNumber_iff.mpr ‹_›

Premises used: Iff.mpr, MulOpposite.invariantBasisNumber_iff
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
n : Type u_1
m : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
R : Type u_3
inst_4 : Semiring R
inst_5 : InvariantBasisNumber R
M : Matrix n m R
N : Matrix m n R
h : M * N = 1
h' : N * M = 1
⊢ Fintype.card n = Fintype.card m

Tactic:
card_eq_of_linearEquiv R (Matrix.toLinearEquivRight'OfInv h' h)

Premises used: card_eq_of_linearEquiv, Matrix.toLinearEquivRight'OfInv
-- Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
Goal:
n : Type u_1
m : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : DecidableEq m
R_1 : Type u_3
inst_4 : Semiring R_1
inst_5 : InvariantBasisNumber R_1
R : Type u_4
inst_6 : CommSemiring R
inst_7 : Nontrivial R
⊢ RankCondition R

Tactic:
inferInstance

Premises used: inferInstance
-- 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 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
by_contra : ∀ (h_row : ¬∃ (j : n), 0 < A i j), False
⊢ ∃ (j : n), 0 < A i j

Tactic:
by_contra h_row
-- 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 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
⊢ ∀ (j : n), IsEmpty (i ⟶ j)

Tactic:
have no_out : ∀ j : n, IsEmpty (i ⟶ j) :=
    fun j => ⟨fun e => h_row ⟨j, 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
inst_2 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
obtain : ∀ (j : n) (hij : ∃ (y : n), j ≠ y), False
⊢ False

Tactic:
obtain ⟨j, hij⟩ := exists_pair_ne n

Premises used: exists_pair_ne
-- 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 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
obtain : ∀ (p : Path i j) (hp_pos : 0 < p.length), False
⊢ False

Tactic:
obtain ⟨p, hp_pos⟩ := h_irr.connected 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 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
⊢ 1 ≤ p.length

Tactic:
have h_le : 1 ≤ p.length := Nat.succ_le_of_lt 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
inst_2 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
have : ∀ (v : n) (p₁ : Path i v) (p₂ : Path v j) (_hp_eq : p = p₁.comp p₂) (hp₁_len : p₁.length = 1), False
⊢ False

Tactic:
have ⟨v, p₁, p₂, _hp_eq, hp₁_len⟩ := p.exists_eq_comp_of_le_length (n := 1) h_le
-- 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 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₁ : Path i v
p₂ : Path v j
_hp_eq : p = p₁.comp p₂
hp₁_len : p₁.length = 1
⊢ p₁.length ≠ 0

Tactic:
simp [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 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₁ : Path i v
p₂ : Path v j
_hp_eq : p = p₁.comp p₂
hp₁_len : p₁.length = 1
⊢ p₁.length ≠ 0

Tactic:
have hlen_ne : p₁.length ≠ 0 := by simp [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 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₁ : Path i v
p₂ : Path v j
_hp_eq : p = p₁.comp p₂
hp₁_len : p₁.length = 1
hlen_ne : p₁.length ≠ 0
⊢ p₁.length ≠ 0

Tactic:
lia
-- 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 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₁ : Path i v
p₂ : Path v j
_hp_eq : p = p₁.comp p₂
hp₁_len : p₁.length = 1
hlen_ne : p₁.length ≠ 0
obtain :
  ∀ (c : n) (p' : Path i c) (e : c ⟶ v) (_hp_eq : p = (p'.cons e).comp p₂) (hp₁_len : (p'.cons e).length = 1)
    (hlen_ne : (p'.cons e).length ≠ 0), False
⊢ False

Tactic:
obtain ⟨c, p', e, rfl⟩ := (Quiver.Path.length_ne_zero_iff_eq_cons (p := p₁)).1 (by lia)

Premises used: Quiver.Path.length_ne_zero_iff_eq_cons, 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 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₂ : Path v j
c : n
p' : Path i c
e : c ⟶ v
_hp_eq : p = (p'.cons e).comp p₂
hp₁_len : (p'.cons e).length = 1
hlen_ne : (p'.cons e).length ≠ 0
⊢ p'.length = 0

Tactic:
simp_all
-- 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 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₂ : Path v j
c : n
p' : Path i c
e : c ⟶ v
_hp_eq : p = (p'.cons e).comp p₂
hp₁_len : (p'.cons e).length = 1
hlen_ne : (p'.cons e).length ≠ 0
obtain :
  ∀ (p' : Path i i) (e : i ⟶ v) (_hp_eq : p = (p'.cons e).comp p₂) (hp₁_len : (p'.cons e).length = 1)
    (hlen_ne : (p'.cons e).length ≠ 0), False
⊢ False

Tactic:
obtain ⟨rfl⟩ : i = c := Quiver.Path.eq_of_length_zero p' (by simp_all)

Premises used: Quiver.Path.eq_of_length_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 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₂ : Path v j
p' : Path i i
e : i ⟶ v
_hp_eq : p = (p'.cons e).comp p₂
hp₁_len : (p'.cons e).length = 1
hlen_ne : (p'.cons e).length ≠ 0
⊢ False

Tactic:
(no_out _).false e

Premises used: IsEmpty.false
-- 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 : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ (j : n), 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ (y : n), j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₂ : Path v j
p' : Path i i
e : i ⟶ v
_hp_eq : p = (p'.cons e).comp p₂
hp₁_len : (p'.cons e).length = 1
hlen_ne : (p'.cons e).length ≠ 0
⊢ False

Tactic:
exact (no_out _).false e

Premises used: IsEmpty.false
-- 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 : n
⊢ 0 < HPow.hPow (β := ℕ) A 0 i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }

Tactic:
⟨fun h_pos ↦ ?_, fun ⟨p, hp⟩ ↦ ?_⟩

Premises used: _private.0.Matrix.pow_apply_pos_iff_nonempty_path.match_1, HPow.hPow, LT.lt, Iff.intro, OfNat.ofNat
-- 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 : n
zero : ∀ (h_pos : 0 < HPow.hPow (β := ℕ) A 0 i j), Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }
zero₁ :
  Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 } →
    ∀ (p : Path i j) (hp : p.length = 0), 0 < HPow.hPow (β := ℕ) A 0 i j
⊢ 0 < HPow.hPow (β := ℕ) A 0 i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }

Tactic:
refine ⟨fun h_pos ↦ ?_, fun ⟨p, hp⟩ ↦ ?_⟩
-- 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 : 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 }
zero₁ : ∀ (h_eq : i ≠ j), Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }

Tactic:
rcases eq_or_ne i j with rfl | h_eq

Premises used: eq_or_ne, 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
i : n
h_pos : 0 < HPow.hPow (β := ℕ) A 0 i i
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i i // p.length = 0 }

Tactic:
⟨⟨Quiver.Path.nil, rfl⟩⟩

Premises used: Quiver.Path.nil, Nonempty.intro, Subtype.mk, 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
i : n
h_pos : 0 < HPow.hPow (β := ℕ) A 0 i i
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i i // p.length = 0 }

Tactic:
exact ⟨⟨Quiver.Path.nil, 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
i j : n
h_pos : 0 < HPow.hPow (β := ℕ) A 0 i j
h_eq : i ≠ j
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }

Tactic:
simp_all
-- 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 : n
h : Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = 0 }
p : Path i j
hp : p.length = 0
⊢ 0 < HPow.hPow (β := ℕ) A 0 i j

Tactic:
simp [Quiver.Path.eq_of_length_zero p hp]

Premises used: Quiver.Path.eq_of_length_zero
-- 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
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 }
⊢ 0 < (A ^ (m + 1)) i j ↔ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }

Tactic:
rw [pow_succ, mul_apply]

Premises used: pow_succ, Matrix.mul_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
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 }
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)
⊢ 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
-- 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
h_pos : LT.lt.{u_2} (α := R) 0 (∑ j_1 : n, (A ^ m) i j_1 * A j_1 j)
⊢ ∃ (l : n), Membership.mem (γ := Finset n) Finset.univ l ∧ 0 < (A ^ m) i l * A l j

Tactic:
simpa [Finset.sum_pos_iff_of_nonneg
                 (fun x _ => mul_nonneg (pow_apply_nonneg hA m i x) (hA x j))]
          using h_pos

Premises used: mul_nonneg, Matrix.pow_apply_nonneg, Finset.sum_pos_iff_of_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
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)
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 }
⊢ 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

Premises used: Finset.univ
-- 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
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
⊢ 0 ≤ (A ^ m) i l

Tactic:
have hAm_nonneg : 0 ≤ (A ^ m) i l := pow_apply_nonneg hA m i l
-- 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
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
⊢ 0 ≤ A l j

Tactic:
have hA_nonneg' : 0 ≤ A l j := hA l 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
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
by_contra! : ∀ (h : (A ^ m) i l ≤ 0), False
⊢ 0 < (A ^ m) i l

Tactic:
by_contra! h
-- 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
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 : (A ^ m) i l ≤ 0
⊢ False

Tactic:
simp [le_antisymm h hAm_nonneg] at hl_pos

Premises used: le_antisymm
-- 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
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

Tactic:
have h_Am : 0 < (A ^ m) i l := by by_contra! h; simp [le_antisymm h hAm_nonneg] at hl_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
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
by_contra! : ∀ (h : A l j ≤ 0), False
⊢ 0 < A l j

Tactic:
by_contra! h
-- 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
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 l j ≤ 0
⊢ False

Tactic:
simp [le_antisymm h hA_nonneg'] at hl_pos

Premises used: le_antisymm
-- 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
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

Tactic:
have h_A : 0 < A l j := by by_contra! h; simp [le_antisymm h hA_nonneg'] at hl_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
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
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 }
⊢ Nonempty.{max 1 (u_1 + 1)} { p : Path i j // p.length = m + 1 }

Tactic:
obtain ⟨⟨p, rfl⟩⟩ := (ih i l).mp h_Am

Premises used: 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
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
⊢ (p.cons { down := h_A : PLift (0 < A l j) }).length = p.length + 1

Tactic:
simp