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

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
f : Fin n → α
⊢ (ofFn f).sup = Finset.univ.sup f
Tactic:
induction' n with n ih <;> simp
State after:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
⊢ f 0 ⊔ (ofFn fun i => f i.succ).sup = Finset.univ.sup f

State before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
⊢ f 0 ⊔ (ofFn fun i => f i.succ).sup = Finset.univ.sup f
Tactic:
{ simp[ih]
  have : (Finset.univ : Finset (Fin (n + 1))) = insert 0 ((Finset.univ : Finset (Fin n)).image Fin.succ) := by
    ext i; simp
  rw[this, Finset.sup_insert]; simp
  have : Finset.sup Finset.univ (fun i => f (Fin.succ i)) = Finset.sup {0}ᶜ f := by
    simpa[Function.comp] using Eq.symm <| Finset.sup_image (Finset.univ : Finset (Fin n)) Fin.succ f
  rw[this] }
State after:
no goals

State before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
⊢ f 0 ⊔ (ofFn fun i => f i.succ).sup = Finset.univ.sup f
Tactic:
simp[ih]
State after:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = Finset.univ.sup f

State before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = Finset.univ.sup f
Tactic:
have : (Finset.univ : Finset (Fin (n + 1))) = insert 0 ((Finset.univ : Finset (Fin n)).image Fin.succ) := by
  ext i; simp
State after:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = Finset.univ.sup f

State before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = Finset.univ.sup f
Tactic:
rw[this, Finset.sup_insert]
State after:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ (Finset.image Fin.succ Finset.univ).sup f

State before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ (Finset.image Fin.succ Finset.univ).sup f
Tactic:
simp
State after:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ {0}ᶜ.sup f

State before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ {0}ᶜ.sup f
Tactic:
have : Finset.sup Finset.univ (fun i => f (Fin.succ i)) = Finset.sup {0}ᶜ f := by
  simpa[Function.comp] using Eq.symm <| Finset.sup_image (Finset.univ : Finset (Fin n)) Fin.succ f
State after:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this✝ : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
this : (Finset.univ.sup fun i => f i.succ) = {0}ᶜ.sup f
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ {0}ᶜ.sup f

State before:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this✝ : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
this : (Finset.univ.sup fun i => f i.succ) = {0}ᶜ.sup f
⊢ (f 0 ⊔ Finset.univ.sup fun i => f i.succ) = f 0 ⊔ {0}ᶜ.sup f
Tactic:
rw[this]
State after:
no goals

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
⊢ Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
Tactic:
ext i
State after:
case a
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
i : Fin (n + 1)
⊢ i ∈ Finset.univ ↔ i ∈ insert 0 (Finset.image Fin.succ Finset.univ)

State before:
case a
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
i : Fin (n + 1)
⊢ i ∈ Finset.univ ↔ i ∈ insert 0 (Finset.image Fin.succ Finset.univ)
Tactic:
simp
State after:
no goals

State before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
this : Finset.univ = insert 0 (Finset.image Fin.succ Finset.univ)
⊢ (Finset.univ.sup fun i => f i.succ) = {0}ᶜ.sup f
Tactic:
simpa[Function.comp] using Eq.symm <| Finset.sup_image (Finset.univ : Finset (Fin n)) Fin.succ f
State after:
no goals