Theorem: List.le_sup (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a : α
l : List α
⊢ a ∈ l → a ≤ l.sup
Tactic:
induction' l with a l ih <;> simp[*]
State after:
case cons
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
⊢ a✝ = a ∨ a✝ ∈ l → a✝ ≤ a ⊔ l.sup

State before:
case cons
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
⊢ a✝ = a ∨ a✝ ∈ l → a✝ ≤ a ⊔ l.sup
Tactic:
rintro (rfl | h)
State after:
case cons.inl
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a : α
l : List α
ih : a ∈ l → a ≤ l.sup
⊢ a ≤ a ⊔ l.sup

case cons.inr
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
h : a✝ ∈ l
⊢ a✝ ≤ a ⊔ l.sup

State before:
case cons.inl
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a : α
l : List α
ih : a ∈ l → a ≤ l.sup
⊢ a ≤ a ⊔ l.sup

case cons.inr
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
h : a✝ ∈ l
⊢ a✝ ≤ a ⊔ l.sup
Tactic:
{ simp }
State after:
case cons.inr
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
h : a✝ ∈ l
⊢ a✝ ≤ a ⊔ l.sup

State before:
case cons.inr
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
h : a✝ ∈ l
⊢ a✝ ≤ a ⊔ l.sup
Tactic:
{ exact le_sup_of_le_right $ ih h }
State after:
no goals

State before:
case cons.inl
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a : α
l : List α
ih : a ∈ l → a ≤ l.sup
⊢ a ≤ a ⊔ l.sup
Tactic:
simp
State after:
no goals

State before:
case cons.inr
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
h : a✝ ∈ l
⊢ a✝ ≤ a ⊔ l.sup
Tactic:
exact le_sup_of_le_right $ ih h
State after:
no goals