internlm/Lean-Github huggingface dataset:
Theorem: jordan_three_cycle
Proof state before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ Nat.factorial (Fintype.card α) ≤ 2 * Fintype.card ↥G
Tactic:
apply le_trans (Nat.factorial_le hα4)
Proof state after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ Nat.factorial 3 ≤ 2 * Fintype.card ↥G
Theorem: jordan_three_cycle
Proof state before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ Nat.factorial 3 ≤ 2 * Fintype.card ↥G
Tactic:
change 2 * 3 ≤ _
Proof state after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 2 * 3 ≤ 2 * Fintype.card ↥G
Theorem: jordan_three_cycle
Proof state before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 2 * 3 ≤ 2 * Fintype.card ↥G
Tactic:
simp only [mul_le_mul_left, Nat.succ_pos']
Proof state after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 3 ≤ Fintype.card ↥G
Theorem: jordan_three_cycle
Proof state before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 3 ≤ Fintype.card ↥G
Tactic:
apply Nat.le_of_dvd Fintype.card_pos
Proof state after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 3 ∣ Fintype.card ↥G
Theorem: jordan_three_cycle
Proof state before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 3 ∣ Fintype.card ↥G
Tactic:
suffices 3 = orderOf (⟨g, hg⟩ : G) by
  rw [this]
  exact orderOf_dvd_card
Proof state after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 3 = orderOf { val := g, property := hg }
Theorem: jordan_three_cycle
Proof state before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 3 = orderOf { val := g, property := hg }
Tactic:
rw [← Equiv.Perm.IsThreeCycle.orderOf h3g]
Proof state after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ orderOf g = orderOf { val := g, property := hg }
Theorem: jordan_three_cycle
Proof state before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ orderOf g = orderOf { val := g, property := hg }
Tactic:
convert orderOf_submonoid _
Proof state after:
case h.e'_2.h.e'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ g = ↑{ val := g, property := hg }
Theorem: jordan_three_cycle
Proof state before:
case h.e'_2.h.e'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ g = ↑{ val := g, property := hg }
Tactic:
rfl
Proof state after:
no goals
Theorem: jordan_three_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
this : 3 = orderOf { val := g, property := hg }
⊢ 3 ∣ Fintype.card ↥G
Tactic:
rw [this]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
this : 3 = orderOf { val := g, property := hg }
⊢ orderOf { val := g, property := hg } ∣ Fintype.card ↥G
Theorem: jordan_three_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
this : 3 = orderOf { val := g, property := hg }
⊢ orderOf { val := g, property := hg } ∣ Fintype.card ↥G
Tactic:
exact orderOf_dvd_card
Proof state after:
no goals
Theorem: jordan_three_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
⊢ Fintype.card α - 2 = 1 + Nat.succ n
Tactic:
simp [hn, add_comm 1]
Proof state after:
no goals
Theorem: jordan_three_cycle
Proof state before:
case inr.intro.hmt.h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
Tactic:
apply Nat.add_left_cancel
Proof state after:
case inr.intro.hmt.h.refine'_2.a
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ ?inr.intro.hmt.h.refine'_2.n + Set.ncard (↑(Equiv.Perm.support g))ᶜ = ?inr.intro.hmt.h.refine'_2.n + Nat.succ n

case inr.intro.hmt.h.refine'_2.n
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ ℕ
Theorem: jordan_three_cycle
Proof state before:
case inr.intro.hmt.h.refine'_2.a
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ ?inr.intro.hmt.h.refine'_2.n + Set.ncard (↑(Equiv.Perm.support g))ᶜ = ?inr.intro.hmt.h.refine'_2.n + Nat.succ n

case inr.intro.hmt.h.refine'_2.n
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ ℕ
Tactic:
rw [Set.ncard_add_ncard_compl, Set.ncard_coe_Finset,
  Equiv.Perm.IsThreeCycle.card_support h3g,
  add_comm, Nat.card_eq_fintype_card, hn]
Proof state after:
no goals
Theorem: jordan_three_cycle
Proof state before:
case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ 1 + Nat.succ n < Fintype.card α
Tactic:
rw [hn, Nat.succ_eq_add_one, add_comm, add_assoc]
Proof state after:
case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ n + (1 + 1) < n + 4
Theorem: jordan_three_cycle
Proof state before:
case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ n + (1 + 1) < n + 4
Tactic:
simp only [add_lt_add_iff_left]
Proof state after:
case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ 1 + 1 < 4
Theorem: jordan_three_cycle
Proof state before:
case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ 1 + 1 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: jordan_three_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ IsPretransitive ?m.354282 ?m.354283
Tactic:
apply isPretransitive_of_cycle hg
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ Equiv.Perm.IsCycle g
Theorem: jordan_three_cycle
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ Equiv.Perm.IsCycle g
Tactic:
exact Equiv.Perm.IsThreeCycle.isCycle h3g
Proof state after:
no goals
Theorem: gimme_some
Proof state before:
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
⊢ Nonempty (Fin m ↪ α)
Tactic:
suffices Nonempty (ULift (Fin m) ↪ α) by
  obtain ⟨x'⟩ := this;
  use Equiv.ulift.symm.toEmbedding.trans x'
  apply Function.Embedding.injective
Proof state after:
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
⊢ Nonempty (ULift.{?u.347, 0} (Fin m) ↪ α)
Theorem: gimme_some
Proof state before:
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
⊢ Nonempty (ULift.{?u.347, 0} (Fin m) ↪ α)
Tactic:
rw [← Cardinal.le_def, Cardinal.mk_fintype, Fintype.card_ulift, Fintype.card_fin]
Proof state after:
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
⊢ ↑m ≤ Cardinal.mk α
Theorem: gimme_some
Proof state before:
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
⊢ ↑m ≤ Cardinal.mk α
Tactic:
exact Iff.mp Cardinal.natCast_le_toPartENat_iff hα
Proof state after:
no goals
Theorem: gimme_some
Proof state before:
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
this : Nonempty (ULift.{?u.347, 0} (Fin m) ↪ α)
⊢ Nonempty (Fin m ↪ α)
Tactic:
obtain ⟨x'⟩ := this
Proof state after:
case intro
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
x' : ULift.{?u.347, 0} (Fin m) ↪ α
⊢ Nonempty (Fin m ↪ α)
Theorem: gimme_some
Proof state before:
case intro
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
x' : ULift.{?u.347, 0} (Fin m) ↪ α
⊢ Nonempty (Fin m ↪ α)
Tactic:
use Equiv.ulift.symm.toEmbedding.trans x'
Proof state after:
case inj'
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
x' : ULift.{?u.347, 0} (Fin m) ↪ α
⊢ Function.Injective ⇑(Function.Embedding.trans (Equiv.toEmbedding Equiv.ulift.symm) x')
Theorem: gimme_some
Proof state before:
case inj'
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
x' : ULift.{?u.347, 0} (Fin m) ↪ α
⊢ Function.Injective ⇑(Function.Embedding.trans (Equiv.toEmbedding Equiv.ulift.symm) x')
Tactic:
apply Function.Embedding.injective
Proof state after:
no goals
Theorem: gimme_some_equiv
Proof state before:
α : Type u_1
m : ℕ
inst✝ : Fintype α
hα : m = Fintype.card α
⊢ Nonempty (Fin m ≃ α)
Tactic:
exact ⟨(Fintype.equivFinOfCardEq hα.symm).symm⟩
Proof state after:
no goals
Theorem: equiv_fin_of_partENat_card_eq
Proof state before:
α : Type u_1
m : ℕ
hα : PartENat.card α = ↑m
⊢ Nonempty (Fin m ≃ α)
Tactic:
cases' fintypeOrInfinite α with h h
Proof state after:
case inl
α : Type u_1
m : ℕ
hα : PartENat.card α = ↑m
h : Fintype α
⊢ Nonempty (Fin m ≃ α)

case inr
α : Type u_1
m : ℕ
hα : PartENat.card α = ↑m
h : Infinite α
⊢ Nonempty (Fin m ≃ α)
Theorem: equiv_fin_of_partENat_card_eq
Proof state before:
case inl
α : Type u_1
m : ℕ
hα : PartENat.card α = ↑m
h : Fintype α
⊢ Nonempty (Fin m ≃ α)
Tactic:
simp only [PartENat.card_eq_coe_fintype_card, PartENat.natCast_inj] at hα
Proof state after:
case inl
α : Type u_1
m : ℕ
h : Fintype α
hα : Fintype.card α = m
⊢ Nonempty (Fin m ≃ α)
Theorem: equiv_fin_of_partENat_card_eq
Proof state before:
case inl
α : Type u_1
m : ℕ
h : Fintype α
hα : Fintype.card α = m
⊢ Nonempty (Fin m ≃ α)
Tactic:
exact ⟨(Fintype.equivFinOfCardEq hα).symm⟩
Proof state after:
no goals
Theorem: equiv_fin_of_partENat_card_eq
Proof state before:
case inr
α : Type u_1
m : ℕ
hα : PartENat.card α = ↑m
h : Infinite α
⊢ Nonempty (Fin m ≃ α)
Tactic:
rw [PartENat.card_eq_top_of_infinite] at hα
Proof state after:
case inr
α : Type u_1
m : ℕ
hα : ⊤ = ↑m
h : Infinite α
⊢ Nonempty (Fin m ≃ α)
Theorem: equiv_fin_of_partENat_card_eq
Proof state before:
case inr
α : Type u_1
m : ℕ
hα : ⊤ = ↑m
h : Infinite α
⊢ Nonempty (Fin m ≃ α)
Tactic:
exfalso
Proof state after:
case inr
α : Type u_1
m : ℕ
hα : ⊤ = ↑m
h : Infinite α
⊢ False
Theorem: equiv_fin_of_partENat_card_eq
Proof state before:
case inr
α : Type u_1
m : ℕ
hα : ⊤ = ↑m
h : Infinite α
⊢ False
Tactic:
apply PartENat.natCast_ne_top m
Proof state after:
case inr
α : Type u_1
m : ℕ
hα : ⊤ = ↑m
h : Infinite α
⊢ ↑m = ⊤
Theorem: equiv_fin_of_partENat_card_eq
Proof state before:
case inr
α : Type u_1
m : ℕ
hα : ⊤ = ↑m
h : Infinite α
⊢ ↑m = ⊤
Tactic:
rw [hα]
Proof state after:
no goals
Theorem: gimme_another
Proof 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]
Proof state after:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ↑m < PartENat.card α
⊢ Set.range f ≠ Set.univ
Theorem: gimme_another
Proof state before:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ↑m < PartENat.card α
⊢ Set.range f ≠ Set.univ
Tactic:
intro h
Proof state after:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ↑m < PartENat.card α
h : Set.range f = Set.univ
⊢ False
Theorem: gimme_another
Proof 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α
Proof state after:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ False
Theorem: gimme_another
Proof state before:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ False
Tactic:
apply hα
Proof state after:
α : Type u_1
m : ℕ
f : Fin m → α
hα : ¬PartENat.card α ≤ ↑m
h : Set.range f = Set.univ
⊢ PartENat.card α ≤ ↑m
Theorem: gimme_another
Proof 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]
Proof 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
Theorem: gimme_another
Proof 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
Proof 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
Theorem: gimme_another
Proof 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]
Proof 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
Theorem: gimme_another
Proof 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
Proof 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) → α
Theorem: gimme_another
Proof 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
Proof 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
Theorem: gimme_another
Proof 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)
Proof 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
Theorem: gimme_another
Proof 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
Proof 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
Theorem: gimme_another
Proof 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]
Proof state after:
no goals
Theorem: may_extend_with
Proof state before:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = x ∧ x' { val := n, isLt := ⋯ } = a
Tactic:
let p := fun i : Fin n.succ => i.val < n
Proof state after:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = x ∧ x' { val := n, isLt := ⋯ } = a
Theorem: may_extend_with
Proof state before:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = x ∧ x' { val := n, isLt := ⋯ } = a
Tactic:
let f : {i : Fin n.succ | i.val < n} → α := fun i => x.toFun (Fin.castLT i.val i.prop)
Proof state after:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = x ∧ x' { val := n, isLt := ⋯ } = a
Theorem: may_extend_with
Proof state before:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = x ∧ x' { val := n, isLt := ⋯ } = a
Tactic:
let f' : {i : Fin n.succ | ¬p i} ↪ α := {
  toFun := fun ⟨_, _⟩ => a
  inj' := by
    rintro ⟨i, hi⟩ ⟨j, hj⟩ _
    simp only [Subtype.mk_eq_mk, Fin.ext_iff]
    rw [Nat.eq_of_lt_succ_of_not_lt i.prop hi, Nat.eq_of_lt_succ_of_not_lt j.prop hj] }
Proof state after:
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ ∃ x', Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding x' = x ∧ x' { val := n, isLt := ⋯ } = a
Theorem: may_extend_with
Proof state before:
case h
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding
        { toFun := fun i => if hi : p i then f { val := i, property := hi } else f' { val := i, property := hi },
          inj' := ⋯ } =
      x ∧
    { toFun := fun i => if hi : p i then f { val := i, property := hi } else f' { val := i, property := hi },
          inj' := ⋯ }
        { val := n, isLt := ⋯ } =
      a
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ Function.Embedding.trans (Fin.castLEEmb ⋯).toEmbedding
      { toFun := fun i => if hi : p i then f { val := i, property := hi } else f' { val := i, property := hi },
        inj' := ⋯ } =
    x

case h.right
α : Type u_1
n : ℕ
x : Fin n ↪ α
a : α
ha : a ∉ Set.range x.toFun
p : Fin (succ n) → Prop := fun i => ↑i < n
f : ↑{i | ↑i < n} → α := fun i => x.toFun (Fin.castLT ↑i ⋯)
f' : ↑{i | ¬p i} ↪ α :=
  {
    toFun := fun x =>
      match x with
      | { val := val, property := property } => a,
    inj' := ⋯ }
⊢ { toFun := fun i => if hi : p i then f { val := i, property := hi } else f' { val := i, property := hi }, inj' := ⋯ }
      { val := n, isLt := ⋯ } =
    a