-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem order_ofForallLtEqZero [Zero Γ] (f : Γ → R) (hf : f ≠ 0) (n : Γ)
    (hn : ∀(m : Γ), m < n → f m = 0) :
    n ≤ order (ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn))

Proof state:
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ n ≤ (ofSuppBddBelow f ⋯).order

Tactic:
dsimp only [order]

Result:
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ n ≤ if h : ofSuppBddBelow f ⋯ = 0 then 0 else ⋯.min ⋯

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ¬ofSuppBddBelow f ⋯ = 0
m : Γ
hm : m ∈ (ofSuppBddBelow f ⋯).support
⊢ n ≤ m

Tactic:
rw [HahnSeries.support, Function.mem_support, ne_eq] at hm

Result:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ¬ofSuppBddBelow f ⋯ = 0
m : Γ
hm : ¬(ofSuppBddBelow f ⋯).coeff m = 0
⊢ n ≤ m

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ¬ofSuppBddBelow f ⋯ = 0
⊢ ∀ b ∈ (ofSuppBddBelow f ⋯).support, n ≤ b

Tactic:
intro m hm

Result:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ¬ofSuppBddBelow f ⋯ = 0
m : Γ
hm : m ∈ (ofSuppBddBelow f ⋯).support
⊢ n ≤ m

Proof state:
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ n ≤ if h : ofSuppBddBelow f ⋯ = 0 then 0 else ⋯.min ⋯

Tactic:
by_cases h : ofSuppBddBelow f (forallLTEqZero_supp_BddBelow f n hn) = 0

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ofSuppBddBelow f ⋯ = 0
⊢ n ≤ if h : ofSuppBddBelow f ⋯ = 0 then 0 else ⋯.min ⋯

case neg
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ¬ofSuppBddBelow f ⋯ = 0
⊢ n ≤ if h : ofSuppBddBelow f ⋯ = 0 then 0 else ⋯.min ⋯

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ¬ofSuppBddBelow f ⋯ = 0
m : Γ
hm : ¬(ofSuppBddBelow f ⋯).coeff m = 0
⊢ n ≤ m

Tactic:
exact not_lt.mp (mt (hn m) hm)

Result:
no goals

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ¬ofSuppBddBelow f ⋯ = 0
⊢ n ≤ if h : ofSuppBddBelow f ⋯ = 0 then 0 else ⋯.min ⋯

Tactic:
simp_all only [dite_false]

Result:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ¬ofSuppBddBelow f ⋯ = 0
⊢ n ≤ ⋯.min ⋯

Proof state:
case pos.refl
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
n : Γ
hf : 0 ≠ 0
hn : ∀ m < n, 0 m = 0
⊢ n ≤ if h : ofSuppBddBelow 0 ⋯ = 0 then 0 else ⋯.min ⋯

Tactic:
exact (hf rfl).elim

Result:
no goals

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ofSuppBddBelow f ⋯ = 0
⊢ n ≤ if h : ofSuppBddBelow f ⋯ = 0 then 0 else ⋯.min ⋯

case neg
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ¬ofSuppBddBelow f ⋯ = 0
⊢ n ≤ if h : ofSuppBddBelow f ⋯ = 0 then 0 else ⋯.min ⋯

Tactic:
cases h

Result:
case pos.refl
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
n : Γ
hf : 0 ≠ 0
hn : ∀ m < n, 0 m = 0
⊢ n ≤ if h : ofSuppBddBelow 0 ⋯ = 0 then 0 else ⋯.min ⋯

case neg
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ¬ofSuppBddBelow f ⋯ = 0
⊢ n ≤ if h : ofSuppBddBelow f ⋯ = 0 then 0 else ⋯.min ⋯

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ¬ofSuppBddBelow f ⋯ = 0
⊢ n ≤ ⋯.min ⋯

Tactic:
rw [Set.IsWF.le_min_iff]

Result:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
h : ¬ofSuppBddBelow f ⋯ = 0
⊢ ∀ b ∈ (ofSuppBddBelow f ⋯).support, n ≤ b