awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f g : α → β
hf : Function.Injective f
hg : Function.Injective g
have have₁ have₂ :
  ∀ (this : Finite.{u_2 + 1} (↑{x : β | x ∈ Set.range f} : Type u_2)),
    ∃ (σ : Perm β), ∀ (a : α), (σ : (a : β) → β) (f a) = g a
have₃ :
  ∀ (this : Finite.{u_2 + 1} (↑{x : β | x ∈ Set.range f} : Type u_2)) (a : α),
    (((ofInjective f hf).symm.trans (ofInjective g hg)).extendSubtype (p := Membership.mem (Set.range f)) (q :=
            Membership.mem (Set.range g)) :
          (a : β) → β)
        (f a) =
      g a
⊢ ∃ (σ : Perm β), ∀ (a : α), (σ : (a : β) → β) (f a) = g a

Tactic:
classical
  have : Finite {x | x ∈ Set.range f} := .of_surjective _ (Set.codRestrict_range_surjective f)
  refine ⟨((Equiv.ofInjective f hf).symm.trans (Equiv.ofInjective g hg)).extendSubtype, ?_⟩
  simp [Equiv.extendSubtype_apply_of_mem]

Premises used: Equiv.extendSubtype_apply_of_mem
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
β : Type u_2
s t : Finset β
h : s.card = t.card
obtain :
  ∀ (σ : Perm β)
    (hσ :
      ∀ (a : ↥s),
        Eq (α := β) ((σ : (a : β) → β) (↑a : β) : β) ((↑((Finset.equivOfCardEq h : (a : ↥s) → ↥t) a) : β) : β)),
    ∃ (σ : Perm β), Finset.map (Equiv.toEmbedding σ) s = t
⊢ ∃ (σ : Perm β), Finset.map (Equiv.toEmbedding σ) s = t

Tactic:
obtain ⟨σ, hσ⟩ := Perm.exists_extending_pair
    (fun x : s => (x : β)) (fun x : s => ((s.equivOfCardEq h) x : β))
    Subtype.val_injective (Subtype.val_injective.comp (s.equivOfCardEq h).injective)

Premises used: Subtype.val_injective, Finset.equivOfCardEq, Equiv.Perm.exists_extending_pair, Function.Injective.comp, Equiv.injective, Subtype.val, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
β : Type u_2
s t : Finset β
h : s.card = t.card
σ : Perm β
hσ : ∀ (a : ↥s), Eq (α := β) ((σ : (a : β) → β) (↑a : β) : β) ((↑((Finset.equivOfCardEq h : (a : ↥s) → ↥t) a) : β) : β)
⊢ t.card ≤ (Finset.map (Equiv.toEmbedding σ) s).card

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
β : Type u_2
s t : Finset β
h : s.card = t.card
σ : Perm β
hσ : ∀ (a : ↥s), Eq (α := β) ((σ : (a : β) → β) (↑a : β) : β) ((↑((Finset.equivOfCardEq h : (a : ↥s) → ↥t) a) : β) : β)
refine : ∀ (b : β) (hb : b ∈ Finset.map (Equiv.toEmbedding σ) s), b ∈ t
⊢ ∃ (σ : Perm β), Finset.map (Equiv.toEmbedding σ) s = t

Tactic:
refine ⟨σ, Finset.eq_of_subset_of_card_le (fun b hb => ?_) (by simp [h])⟩
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
β : Type u_2
s t : Finset β
h : s.card = t.card
σ : Perm β
hσ : ∀ (a : ↥s), Eq (α := β) ((σ : (a : β) → β) (↑a : β) : β) ((↑((Finset.equivOfCardEq h : (a : ↥s) → ↥t) a) : β) : β)
b : β
hb : b ∈ Finset.map (Equiv.toEmbedding σ) s
obtain :
  ∀ (a : β) (ha : a ∈ s)
    (hb : Membership.mem (α := β) (Finset.map (Equiv.toEmbedding σ) s) ((Equiv.toEmbedding σ : (a : β) → β) a : β)),
    Membership.mem (α := β) t ((Equiv.toEmbedding σ : (a : β) → β) a : β)
⊢ b ∈ t

Tactic:
obtain ⟨a, ha, rfl⟩ := Finset.mem_map.mp hb

Premises used: Iff.mp, Finset.mem_map, rfl
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
β : Type u_2
s t : Finset β
h : s.card = t.card
σ : Perm β
hσ : ∀ (a : ↥s), Eq (α := β) ((σ : (a : β) → β) (↑a : β) : β) ((↑((Finset.equivOfCardEq h : (a : ↥s) → ↥t) a) : β) : β)
a : β
ha : a ∈ s
hb : Membership.mem (α := β) (Finset.map (Equiv.toEmbedding σ) s) ((Equiv.toEmbedding σ : (a : β) → β) a : β)
⊢ Membership.mem (α := β) t ((Equiv.toEmbedding σ : (a : β) → β) a : β)

Tactic:
(hσ ⟨a, ha⟩) ▸ ((s.equivOfCardEq h) ⟨a, ha⟩).2

Premises used: Set.Mem, setOf, Eq.rec, Finset.equivOfCardEq, Subtype.mk, Eq.symm, DFunLike.coe, Subtype.property
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
β : Type u_2
s t : Finset β
h : s.card = t.card
σ : Perm β
hσ : ∀ (a : ↥s), Eq (α := β) ((σ : (a : β) → β) (↑a : β) : β) ((↑((Finset.equivOfCardEq h : (a : ↥s) → ↥t) a) : β) : β)
a : β
ha : a ∈ s
hb : Membership.mem (α := β) (Finset.map (Equiv.toEmbedding σ) s) ((Equiv.toEmbedding σ : (a : β) → β) a : β)
⊢ Membership.mem (α := β) t ((Equiv.toEmbedding σ : (a : β) → β) a : β)

Tactic:
exact (hσ ⟨a, ha⟩) ▸ ((s.equivOfCardEq h) ⟨a, ha⟩).2
-- Module: Mathlib.Logic.Equiv.Fintype
Goal:
β : Type u_2
s t : Finset β
h : s.card = t.card
obtain :
  ∀ (σ : Perm β)
    (hσ :
      ∀ (a : ↥s),
        Eq (α := β) ((σ : (a : β) → β) (↑a : β) : β) ((↑((Finset.equivOfCardEq h : (a : ↥s) → ↥t) a) : β) : β)),
    ∃ (σ : Perm β), Finset.map (Equiv.toEmbedding σ) s = t
obtain₁ :
  ∀ (σ : Perm β)
    (hσ :
      ∀ (a : ↥s),
        Eq (α := β) ((σ : (a : β) → β) (↑a : β) : β) ((↑((Finset.equivOfCardEq h : (a : ↥s) → ↥t) a) : β) : β))
    (b : β) (hb : b ∈ Finset.map (Equiv.toEmbedding σ) s), b ∈ t
obtain₂ :
  ∀ (σ : Perm β)
    (hσ :
      ∀ (a : ↥s),
        Eq (α := β) ((σ : (a : β) → β) (↑a : β) : β) ((↑((Finset.equivOfCardEq h : (a : ↥s) → ↥t) a) : β) : β))
    (a : β) (ha : a ∈ s)
    (hb : Membership.mem (α := β) (Finset.map (Equiv.toEmbedding σ) s) ((Equiv.toEmbedding σ : (a : β) → β) a : β)),
    Membership.mem (α := β) t ((Equiv.toEmbedding σ : (a : β) → β) a : β)
⊢ ∃ (σ : Perm β), Finset.map (Equiv.toEmbedding σ) s = t

Tactic:
classical
  obtain ⟨σ, hσ⟩ := Perm.exists_extending_pair
    (fun x : s => (x : β)) (fun x : s => ((s.equivOfCardEq h) x : β))
    Subtype.val_injective (Subtype.val_injective.comp (s.equivOfCardEq h).injective)
  refine ⟨σ, Finset.eq_of_subset_of_card_le (fun b hb => ?_) (by simp [h])⟩
  obtain ⟨a, ha, rfl⟩ := Finset.mem_map.mp hb
  exact (hσ ⟨a, ha⟩) ▸ ((s.equivOfCardEq h) ⟨a, ha⟩).2

Premises used: Subtype.val_injective, Finset.equivOfCardEq, Equiv.Perm.exists_extending_pair, Function.Injective.comp, Equiv.injective, Subtype.val, DFunLike.coe, rfl
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α β : Type u
f : Type u → Type v
inst : Functor f
inst_1 : LawfulFunctor f
h : α ≃ β
x : f α
⊢ map (α := β) (⇑h.symm : (a : β) → α) ((⇑h : (a : α) → β) <$> x) = x

Tactic:
simp [map_map]

Premises used: Functor.map_map
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α β : Type u
f : Type u → Type v
inst : Functor f
inst_1 : LawfulFunctor f
h : α ≃ β
x : f β
⊢ map (α := α) (⇑h : (a : α) → β) ((⇑h.symm : (a : β) → α) <$> x) = x

Tactic:
simp [map_map]

Premises used: Functor.map_map
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α β : Type u
f : Type u → Type v
inst : Functor f
inst_1 : LawfulFunctor f
h : α ≃ β
x : f α
⊢ Eq (α := f β) ((mapEquiv f h : (a : f α) → f β) x : f β) ((⇑h : (a : α) → β) <$> x : f β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α β : Type u
f : Type u → Type v
inst : Functor f
inst_1 : LawfulFunctor f
h : α ≃ β
y : f β
⊢ Eq (α := f α) (((mapEquiv f h).symm : (a : f β) → f α) y : f α) ((⇑h.symm : (a : β) → α) <$> y : f α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α : Type u
f : Type u → Type v
inst : Functor f
inst_1 : LawfulFunctor f
H :
  ∀ (x : f α),
    Eq (α := f α) ((mapEquiv f (Equiv.refl α) : (a : f α) → f α) x : f α) ((Equiv.refl (f α) : (a : f α) → f α) x : f α)
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)

Tactic:
ext x
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α : Type u
f : Type u → Type v
inst : Functor f
inst_1 : LawfulFunctor f
x : f α
H : (⇑(Equiv.refl α) : (a : α) → α) <$> x = x
⊢ Eq (α := f α) ((mapEquiv f (Equiv.refl α) : (a : f α) → f α) x : f α) ((Equiv.refl (f α) : (a : f α) → f α) x : f α)

Tactic:
simp only [mapEquiv_apply, refl_apply]

Premises used: Equiv.refl_apply, Functor.mapEquiv_apply
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α : Type u
f : Type u → Type v
inst : Functor f
inst_1 : LawfulFunctor f
x : f α
⊢ (⇑(Equiv.refl α) : (a : α) → α) <$> x = x

Tactic:
LawfulFunctor.id_map x

Premises used: LawfulFunctor.id_map
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α : Type u
f : Type u → Type v
inst : Functor f
inst_1 : LawfulFunctor f
x : f α
⊢ (⇑(Equiv.refl α) : (a : α) → α) <$> x = x

Tactic:
exact LawfulFunctor.id_map x

Premises used: LawfulFunctor.id_map
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst : Bifunctor F
inst_1 : LawfulBifunctor F
h : α ≃ β
h' : α' ≃ β'
x : F α α'
⊢ bimap (F := F) (α := β) (β := β') (⇑h.symm : (a : β) → α) (⇑h'.symm : (a : β') → α')
      (bimap (F := F) (⇑h : (a : α) → β) (⇑h' : (a : α') → β') x) =
    x

Tactic:
simp [bimap_bimap, id_bimap]

Premises used: LawfulBifunctor.id_bimap, LawfulBifunctor.bimap_bimap
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst : Bifunctor F
inst_1 : LawfulBifunctor F
h : α ≃ β
h' : α' ≃ β'
x : F β β'
⊢ bimap (F := F) (α := α) (β := α') (⇑h : (a : α) → β) (⇑h' : (a : α') → β')
      (bimap (F := F) (⇑h.symm : (a : β) → α) (⇑h'.symm : (a : β') → α') x) =
    x

Tactic:
simp [bimap_bimap, id_bimap]

Premises used: LawfulBifunctor.id_bimap, LawfulBifunctor.bimap_bimap
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst : Bifunctor F
inst_1 : LawfulBifunctor F
h : α ≃ β
h' : α' ≃ β'
x : F α α'
⊢ Eq (α := F β β') ((mapEquiv F h h' : (a : F α α') → F β β') x : F β β')
    (bimap (F := F) (⇑h : (a : α) → β) (⇑h' : (a : α') → β') x : F β β')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst : Bifunctor F
inst_1 : LawfulBifunctor F
h : α ≃ β
h' : α' ≃ β'
y : F β β'
⊢ Eq (α := F α α') (((mapEquiv F h h').symm : (a : F β β') → F α α') y : F α α')
    (bimap (F := F) (⇑h.symm : (a : β) → α) (⇑h'.symm : (a : β') → α') y : F α α')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α : Type u
α' : Type v
F : Type u → Type v → Type w
inst : Bifunctor F
inst_1 : LawfulBifunctor F
H :
  ∀ (x : F α α'),
    Eq (α := F α α') ((mapEquiv F (Equiv.refl α) (Equiv.refl α') : (a : F α α') → F α α') x : F α α')
      ((Equiv.refl (F α α') : (a : F α α') → F α α') x : F α α')
⊢ mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α')

Tactic:
ext x
-- Module: Mathlib.Logic.Equiv.Functor
Goal:
α : Type u
α' : Type v
F : Type u → Type v → Type w
inst : Bifunctor F
inst_1 : LawfulBifunctor F
x : F α α'
⊢ Eq (α := F α α') ((mapEquiv F (Equiv.refl α) (Equiv.refl α') : (a : F α α') → F α α') x : F α α')
    ((Equiv.refl (F α α') : (a : F α α') → F α α') x : F α α')

Tactic:
simp [id_bimap]

Premises used: LawfulBifunctor.id_bimap
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
l : List α
rw : map (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)) l = l
rw₁ : map id l = l
rw₂ rw₃ : l = l
⊢ map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) l) = l

Tactic:
rw [List.map_map, e.symm_comp_self, List.map_id]

Premises used: Equiv.symm_comp_self, List.map_id, List.map_map
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
l : List β
rw : map (Function.comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) l = l
rw₁ : map id l = l
rw₂ rw₃ : l = l
⊢ map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) l) = l

Tactic:
rw [List.map_map, e.self_comp_symm, List.map_id]

Premises used: List.map_id, List.map_map, Equiv.self_comp_symm
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Encodable α
l : List α
nil : Eq.{u_1 + 1} (α := Option (List α)) (decodeList (encodeList.{u_1} (α := α) [])) (some [])
cons :
  ∀ (head : α) (tail : List α),
    decodeList (encodeList tail) = some tail → decodeList (encodeList (head :: tail)) = some (head :: tail)
⊢ decodeList (encodeList l) = some l

Tactic:
induction l
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Encodable α
⊢ Eq.{u_1 + 1} (α := Option (List α)) (decodeList (encodeList.{u_1} (α := α) [])) (some [])

Tactic:
simp [encodeList, decodeList, unpair_pair, encodek, *]

Premises used: Encodable.decodeList, Encodable.encodeList, Encodable.encodek, Nat.unpair_pair
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Encodable α
head : α
tail : List α
tail_ih : decodeList (encodeList tail) = some tail
⊢ decodeList (encodeList (head :: tail)) = some (head :: tail)

Tactic:
simp [encodeList, decodeList, unpair_pair, encodek, *]

Premises used: Encodable.decodeList, Encodable.encodeList, Encodable.encodek, Nat.unpair_pair
-- Module: Mathlib.Logic.Equiv.List
Goal:
α_1 : Type u_1
inst : Encodable α_1
α : Type u_2
inst_1 : Countable α
haveI : ∀ (this : Encodable α), Countable.{u_2 + 1} (List α)
⊢ Countable.{u_2 + 1} (List α)

Tactic:
haveI := Encodable.ofCountable α
-- Module: Mathlib.Logic.Equiv.List
Goal:
α_1 : Type u_1
inst : Encodable α_1
α : Type u_2
inst_1 : Countable α
this : Encodable α
⊢ Countable.{u_2 + 1} (List α)

Tactic:
infer_instance
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Encodable α
⊢ encode.{u_1} (α := List α) [] = 0

Tactic:
rfl

Premises used: Encodable.encodeList, rfl
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Encodable α
a : α
l : List α
⊢ encode (a :: l) = (pair (encode a) (encode l)).succ

Tactic:
rfl

Premises used: Encodable.encodeList, rfl
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Encodable α
rw rw₁ : Eq.{u_1 + 1} (α := Option (List α)) (some []) (some [])
⊢ Eq.{u_1 + 1} (α := Option (List α)) (decodeList 0) (some [])

Tactic:
rw [decodeList]

Premises used: Encodable.decodeList
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Encodable α
v : ℕ
rcases :
  ∀ (v₁ v₂ : ℕ) (e : unpair v = (v₁, v₂)),
    Eq.{u_1 + 1} (α := Option (List α)) (decodeList v.succ)
      ((fun (x1 : α) (x2 : List α) ↦ x1 :: x2) <$> decode (v₁, v₂).1 <*> decode (v₁, v₂).2)
⊢ Eq.{u_1 + 1} (α := Option (List α)) (decodeList v.succ)
    ((fun (x1 : α) (x2 : List α) ↦ x1 :: x2) <$> decode (unpair v).1 <*> decode (unpair v).2)

Tactic:
rcases e : unpair v with ⟨v₁, v₂⟩

Premises used: Nat.unpair
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
simp :
  Eq.{u_1 + 1} (α := Option (List α)) (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) (decode v₁) <*> decodeList v₂)
    (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) (decode v₁) <*> decode v₂)
⊢ Eq.{u_1 + 1} (α := Option (List α)) (decodeList v.succ)
    ((fun (x1 : α) (x2 : List α) ↦ x1 :: x2) <$> decode (v₁, v₂).1 <*> decode (v₁, v₂).2)

Tactic:
simp [decodeList, e]

Premises used: Encodable.decodeList
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ Eq.{u_1 + 1} (α := Option (List α)) (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) (decode v₁) <*> decodeList v₂)
    (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) (decode v₁) <*> decode v₂)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Countable α
⊢ Countable.{u_1 + 1} (Multiset α)

Tactic:
Quotient.countable

Premises used: Multiset, Quotient.countable, Quotient
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Countable α
⊢ Countable.{u_1 + 1} (Finset α)

Tactic:
Finset.val_injective.countable

Premises used: Function.Injective.countable, Finset.val_injective
-- Module: Mathlib.Logic.Equiv.List
Goal:
α_1 : Type u_1
α : Type u_2
inst : Fintype α
⊢ Encodable α

Tactic:
exact (Fintype.truncEncodable α).out

Premises used: Fintype.truncEncodable, Trunc.out
-- Module: Mathlib.Logic.Equiv.List
Goal:
α_1 : Type u_1
α : Type u_2
inst : Fintype α
⊢ Encodable α

Tactic:
classical exact (Fintype.truncEncodable α).out
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
rw : ∃ (a : List α), Membership.mem (γ := Option (List α)) (some []) a ∧ encodeList a = 0
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList 0) a ∧ encodeList a = 0

Tactic:
rw [decodeList]

Premises used: Encodable.decodeList
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (some []) a ∧ encodeList a = 0

Tactic:
⟨_, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (some []) a ∧ encodeList a = 0

Tactic:
exact ⟨_, rfl, rfl⟩
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
v : ℕ
rcases :
  ∀ (v₁ v₂ : ℕ) (e : unpair v = (v₁, v₂)),
    ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList v.succ) a ∧ encodeList a = v.succ
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList v.succ) a ∧ encodeList a = v.succ

Tactic:
rcases e : unpair v with ⟨v₁, v₂⟩

Premises used: Nat.unpair
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ (unpair v).2 ≤ v

Tactic:
have h := unpair_right_le v
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (unpair v).2 ≤ v
⊢ (v₁, v₂).2 ≤ v

Tactic:
rw [e] at h
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
rcases :
  ∀ (a : List α) (h₁ : Membership.mem (γ := Option (List α)) (decodeList v₂) a) (h₂ : encodeList a = v₂),
    ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList v.succ) a ∧ encodeList a = v.succ
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList v.succ) a ∧ encodeList a = v.succ

Tactic:
rcases have : v₂ < succ v := lt_succ_of_le h
      denumerable_list_aux v₂ with
      ⟨a, h₁, h₂⟩

Premises used: Nat.lt_succ_of_le
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : Membership.mem (γ := Option (List α)) (decodeList v₂) a
h₂ : encodeList a = v₂
⊢ decodeList v₂ = some a

Tactic:
rw [Option.mem_def] at h₁

Premises used: Option.mem_def
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : Membership.mem (γ := Option (List α)) (decodeList v₂) a
h₂ : encodeList a = v₂
h₃ : decodeList v₂ = some a
⊢ encodeList a = v₂

Tactic:
rw [Option.mem_def] at h₁

Premises used: Option.mem_def
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
h₃ : Membership.mem (γ := Option (List α)) (decodeList v.succ) (ofNat α v₁ :: a) ∧ encodeList (ofNat α v₁ :: a) = v.succ
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList v.succ) a ∧ encodeList a = v.succ

Tactic:
use ofNat α v₁ :: a

Premises used: Denumerable.ofNat
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ Membership.mem (γ := Option (List α)) (decodeList v.succ) (ofNat α v₁ :: a) ∧ encodeList (ofNat α v₁ :: a) = v.succ

Tactic:
simp [decodeList, e, h₂, h₁, encodeList, pair_eq_of_unpair_eq e]

Premises used: Encodable.decodeList, Encodable.encodeList, Nat.pair_eq_of_unpair_eq
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
rw : Eq.{u_1 + 1} (α := List α) (ofNat (List α) (encode.{u_1} (α := List α) [])) []
rw₁ rw₂ : Eq.{u_1 + 1} (α := List α) [] []
⊢ Eq.{u_1 + 1} (α := List α) (ofNat (List α) 0) []

Tactic:
rw [← @encode_list_nil α, ofNat_encode]

Premises used: Encodable.encode_list_nil, Denumerable.ofNat_encode
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
v : ℕ
rcases :
  ∀ (v₁ v₂ : ℕ) (e : unpair v = (v₁, v₂)), decodeList v.succ = some (ofNat α (v₁, v₂).1 :: ofNat (List α) (v₁, v₂).2)
⊢ decodeList v.succ = some (ofNat α (unpair v).1 :: ofNat (List α) (unpair v).2)

Tactic:
rcases e : unpair v with ⟨v₁, v₂⟩

Premises used: Nat.unpair
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ decodeList v.succ = some (ofNat α (v₁, v₂).1 :: ofNat (List α) (v₁, v₂).2)

Tactic:
simp [decodeList, e, show decodeList v₂ = decode (α := List α) v₂ from rfl]

Premises used: Encodable.decodeList, rfl
-- Module: Mathlib.Logic.Equiv.List
Goal:
α : Type u_1
inst : Unique α
u : List α
⊢ length.{u_1} (α := α) ((fun (n : ℕ) ↦ (replicate n default : List α)) u.length) = u.length

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Multiset
Goal:
α : Type u_1
inst : Encodable α
⊢ IsLinearOrder α enle

Tactic:
(RelEmbedding.preimage ⟨encode, encode_injective⟩ (· ≤ ·)).isLinearOrder

Premises used: _private.0.enle, Function.Embedding.mk, Encodable.encode_injective, LE.le, RelEmbedding.preimage, Encodable.encode, RelEmbedding.isLinearOrder, Order.Preimage
-- Module: Mathlib.Logic.Equiv.Multiset
Goal:
α : Type u_1
inst : Encodable α
s : Multiset α
⊢ decodeMultiset (encodeMultiset s) = some s

Tactic:
simp [encodeMultiset, decodeMultiset, encodek]

Premises used: encodeMultiset, decodeMultiset, Encodable.encodek
-- Module: Mathlib.Logic.Equiv.Multiset
Goal:
m : ℕ
l : List ℕ
n : ℕ
rw : lower ((m + n) :: raise l (m + n)) n = m :: l
rw₁ : (m + n - n) :: lower (raise l (m + n)) (m + n) = m :: l
rw₂ : m :: lower (raise l (m + n)) (m + n) = m :: l
rw₃ rw₄ : m :: l = m :: l
⊢ lower (raise (m :: l) n) n = m :: l

Tactic:
rw [raise, lower, Nat.add_sub_cancel_right, lower_raise l]

Premises used: Denumerable.lower, Nat.add_sub_cancel_right, Denumerable.raise
-- Module: Mathlib.Logic.Equiv.Multiset
Goal:
m : ℕ
l : List ℕ
n : ℕ
h : (n :: m :: l).SortedLE
⊢ n ≤ m

Tactic:
have : n ≤ m := List.rel_of_pairwise_cons h.pairwise List.mem_cons_self
-- Module: Mathlib.Logic.Equiv.Multiset
Goal:
m : ℕ
l : List ℕ
n : ℕ
h : (n :: m :: l).SortedLE
this : n ≤ m
⊢ raise (lower (m :: l) n) n = m :: l

Tactic:
simp [raise, lower, Nat.sub_add_cancel this, raise_lower h.pairwise.of_cons.sortedLE]

Premises used: Denumerable.lower, List.SortedLE.pairwise, Nat.sub_add_cancel, Denumerable.raise, List.Pairwise.sortedLE, List.Pairwise.of_cons
-- Module: Mathlib.Logic.Equiv.Multiset
Goal:
l : List ℕ
n : ℕ
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (n :: raise l n)

Tactic:
isChain_raise (n :: l) 0

Premises used: List.cons, Denumerable.isChain_raise, Denumerable.raise, OfNat.ofNat
-- Module: Mathlib.Logic.Equiv.Multiset
Goal:
l : List ℕ
n : ℕ
⊢ (raise l n).SortedLE

Tactic:
(isChain_raise _ _).sortedLE

Premises used: List.IsChain.sortedLE, Denumerable.isChain_raise
-- Module: Mathlib.Logic.Equiv.Multiset
Goal:
α : Type u_1
inst : Denumerable α
s : Multiset α
⊢ raise (lower ((Multiset.map encode s).sort LE.le) 0) 0 = (Multiset.map encode s).sort LE.le

Tactic:
have :=
        raise_lower (List.pairwise_cons.2 ⟨fun n _ => Nat.zero_le n,
        (s.map encode).pairwise_sort _⟩).sortedLE
-- Module: Mathlib.Logic.Equiv.Multiset
Goal:
α : Type u_1
inst : Denumerable α
s : Multiset α
this : raise (lower ((Multiset.map encode s).sort LE.le) 0) 0 = (Multiset.map encode s).sort LE.le
⊢ (fun (n : ℕ) ↦ Multiset.map (ofNat α) (↑(raise (ofNat (List ℕ) n) 0) : Multiset ℕ))
      ((fun (s : Multiset α) ↦ encode (lower ((Multiset.map encode s).sort fun (a b : ℕ) ↦ a ≤ b) 0)) s) =
    s

Tactic:
simp [-Multiset.map_coe, this]

Premises used: Multiset.map_coe
-- Module: Mathlib.Logic.Equiv.Multiset
Goal:
α : Type u_1
inst : Denumerable α
n : ℕ
⊢ (fun (s : Multiset α) ↦ encode (lower ((Multiset.map encode s).sort fun (a b : ℕ) ↦ a ≤ b) 0))
      ((fun (n : ℕ) ↦ Multiset.map (ofNat α) (↑(raise (ofNat (List ℕ) n) 0) : Multiset ℕ)) n) =
    n

Tactic:
simp [-Multiset.map_coe, List.mergeSort_eq_self _ (raise_sorted _ _).pairwise, lower_raise]

Premises used: List.mergeSort_eq_self, List.SortedLE.pairwise, Denumerable.lower_raise, Multiset.map_coe, Denumerable.raise_sorted
-- Module: Mathlib.Logic.Equiv.Nat
Goal:
α : Type u_1
x : Bool × ℕ
b : Bool
n : ℕ
⊢ (fun (n : ℕ) ↦ (n.bodd, n.div2)) (uncurry bit (b, n)) = (b, n)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Nat
Goal:
α : Type u_1
n : ℕ
⊢ uncurry bit ((fun (n : ℕ) ↦ (n.bodd, n.div2)) n) = n

Tactic:
simp