Theorem: Finset.sup_univ_list_eq_sup_map (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
l : List σ
f : σ → α
⊢ (univ.sup fun i => f (l.get i)) = (List.map f l).sup
Tactic:
induction' l with s l ih <;> simp
State after:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
⊢ (univ.sup fun i => f ((s :: l).get i)) = f s ⊔ (List.map f l).sup

State before:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
⊢ (univ.sup fun i => f ((s :: l).get i)) = f s ⊔ (List.map f l).sup
Tactic:
{ have : (Finset.univ : Finset (Fin $ l.length + 1)) = insert 0 ((Finset.univ : Finset (Fin l.length)).image Fin.succ) := by ext; simp
  rw[this, Finset.sup_insert, Finset.sup_image]; simp[Function.comp, ih] }
State after:
no goals

State before:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
⊢ (univ.sup fun i => f ((s :: l).get i)) = f s ⊔ (List.map f l).sup
Tactic:
have : (Finset.univ : Finset (Fin $ l.length + 1)) = insert 0 ((Finset.univ : Finset (Fin l.length)).image Fin.succ) := by ext; simp
State after:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
this : univ = insert 0 (image Fin.succ univ)
⊢ (univ.sup fun i => f ((s :: l).get i)) = f s ⊔ (List.map f l).sup

State before:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
this : univ = insert 0 (image Fin.succ univ)
⊢ (univ.sup fun i => f ((s :: l).get i)) = f s ⊔ (List.map f l).sup
Tactic:
rw[this, Finset.sup_insert, Finset.sup_image]
State after:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
this : univ = insert 0 (image Fin.succ univ)
⊢ f ((s :: l).get 0) ⊔ univ.sup ((fun i => f ((s :: l).get i)) ∘ Fin.succ) = f s ⊔ (List.map f l).sup

State before:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
this : univ = insert 0 (image Fin.succ univ)
⊢ f ((s :: l).get 0) ⊔ univ.sup ((fun i => f ((s :: l).get i)) ∘ Fin.succ) = f s ⊔ (List.map f l).sup
Tactic:
simp[Function.comp, ih]
State after:
no goals

State before:
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
⊢ univ = insert 0 (image Fin.succ univ)
Tactic:
ext
State after:
case a
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
a✝ : Fin (l.length + 1)
⊢ a✝ ∈ univ ↔ a✝ ∈ insert 0 (image Fin.succ univ)

State before:
case a
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
a✝ : Fin (l.length + 1)
⊢ a✝ ∈ univ ↔ a✝ ∈ insert 0 (image Fin.succ univ)
Tactic:
simp
State after:
no goals