Theorem: gimme_another (Jordan/Mathlib/Extensions.lean)

State before:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ↑m < PartENat.card α
⊢ ∃ a, a ∉ Set.range f
Tactic:
rw [← Set.ne_univ_iff_exists_not_mem]
State after:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ↑m < PartENat.card α
⊢ Set.range f ≠ Set.univ

State before:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ↑m < PartENat.card α
⊢ Set.range f ≠ Set.univ
Tactic:
intro h
State after:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ↑m < PartENat.card α
h : Set.range f = Set.univ
⊢ False

State before:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ↑m < PartENat.card α
h : Set.range f = Set.univ
⊢ False
Tactic:
rw [← not_le] at hα
State after:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ False

State before:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ False
Tactic:
apply hα
State after:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ PartENat.card α ≤ ↑m

State before:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ PartENat.card α ≤ ↑m
Tactic:
rw [← PartENat.card_congr (Equiv.Set.univ α), ← h]
State after:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ PartENat.card ↑(Set.range f) ≤ ↑m

State before:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ PartENat.card ↑(Set.range f) ≤ ↑m
Tactic:
unfold PartENat.card
State after:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ Cardinal.toPartENat (Cardinal.mk ↑(Set.range f)) ≤ ↑m

State before:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ Cardinal.toPartENat (Cardinal.mk ↑(Set.range f)) ≤ ↑m
Tactic:
rw [Cardinal.toPartENat_le_natCast_iff]
State after:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ Cardinal.mk ↑(Set.range f) ≤ ↑m

State before:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ Cardinal.mk ↑(Set.range f) ≤ ↑m
Tactic:
convert Cardinal.mk_range_le
State after:
case h.e'_3.h.e'_1.h.e'_2
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ Set.range f = Set.range ?convert_3

case convert_3
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ ULift.{u_1, 0} (Fin m) → α

State before:
case h.e'_3.h.e'_1.h.e'_2
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ Set.range f = Set.range ?convert_3

case convert_3
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ ULift.{u_1, 0} (Fin m) → α
Tactic:
swap
State after:
case convert_3
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ ULift.{u_1, 0} (Fin m) → α

case h.e'_3.h.e'_1.h.e'_2
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ Set.range f = Set.range ?convert_3

State before:
case convert_3
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ ULift.{u_1, 0} (Fin m) → α

case h.e'_3.h.e'_1.h.e'_2
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ Set.range f = Set.range ?convert_3
Tactic:
exact fun n ↦ f (n.down)
State after:
case h.e'_3.h.e'_1.h.e'_2
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ Set.range f = Set.range fun n => f n.down

State before:
case h.e'_3.h.e'_1.h.e'_2
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ Set.range f = Set.range fun n => f n.down
Tactic:
ext a
State after:
case h.e'_3.h.e'_1.h.e'_2.h
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
a : α
⊢ a ∈ Set.range f ↔ a ∈ Set.range fun n => f n.down

State before:
case h.e'_3.h.e'_1.h.e'_2.h
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
a : α
⊢ a ∈ Set.range f ↔ a ∈ Set.range fun n => f n.down
Tactic:
simp only [Set.mem_range, ULift.exists]
State after:
no goals