awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
x : α
h₁ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
h₂ : x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq → x ∉ sq
h₃ h₄ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
h₅ : x ∉ sq → ¬(x ∈ sp ∧ x ∉ sq) → x ∉ sp
h₆ : x ∉ sq → ¬(x ∈ sp ∧ x ∉ sq) → x ∉ sq
h₇ : x ∈ sp → x ∉ sq → x ∉ sq
h₈ : x ∉ sp → x ∉ sq → x ∉ sq
h₉ : x ∈ sp → x ∉ sq → x ∉ sq
h₁₀ : x ∉ sp → x ∉ sq → x ∉ sq
h₁₁ : x ∈ sp → x ∉ sq → x ∈ sq → False
h₁₂ : x ∉ sp → x ∉ sq → x ∈ sq → False
⊢ x ∉ sq ↔ x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
have h₁₃ : x ∉ sq → x ∈ sp → x ∉ sp → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
x : α
h₁ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
h₂ : x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq → x ∉ sq
h₃ h₄ : x ∉ sq → x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
h₅ : x ∉ sq → ¬(x ∈ sp ∧ x ∉ sq) → x ∉ sp
h₆ : x ∉ sq → ¬(x ∈ sp ∧ x ∉ sq) → x ∉ sq
h₇ : x ∈ sp → x ∉ sq → x ∉ sq
h₈ : x ∉ sp → x ∉ sq → x ∉ sq
h₉ : x ∈ sp → x ∉ sq → x ∉ sq
h₁₀ : x ∉ sp → x ∉ sq → x ∉ sq
h₁₁ : x ∈ sp → x ∉ sq → x ∈ sq → False
h₁₂ : x ∉ sp → x ∉ sq → x ∈ sq → False
h₁₃ : x ∉ sq → x ∈ sp → x ∉ sp → False
⊢ x ∉ sq ↔ x ∈ sp ∧ x ∉ sq ∨ x ∉ sp ∧ x ∉ sq
have h₁₄ : x ∉ sq → x ∈ sp → ¬x ∉ sq → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
hqc : sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
⊢ Disjoint (sq \ sp) (sp ∪ sq)ᶜ
have simp : ∀ ⦃a : α⦄, a ∈ sq → a ∉ sp → a ∈ sq
Tactic: simp [Set.disjoint_left]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
p q : α → Prop
inst : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : (↑{x : α | p x} : Type u_1) ≃ (↑{x : α | q x} : Type u_1)
sp : Set α := {x : α | p x}
sq : Set α := {x : α | q x}
this_1 : Fintype (↑sp : Type u_1) := Fintype.ofFinite (↑sp : Type u_1)
this : Fintype (↑sq : Type u_1) := Fintype.ofEquiv (↑sp : Type u_1) e
h : (↑({x : α | p x} \ {x : α | q x}) : Type u_1) ≃ (↑({x : α | q x} \ {x : α | p x}) : Type u_1)
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
hqc : sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
epc : (↑spᶜ : Type u_1) ≃ (↑(sq \ sp) : Type u_1) ⊕ (↑(sp ∪ sq)ᶜ : Type u_1) :=
  (setCongr (s := spᶜ) (t := sq \ sp ∪ (sp ∪ sq)ᶜ) hpc).trans (Set.union (s := sq \ sp) (t := (sp ∪ sq)ᶜ) ⋯)
⊢ Disjoint (sp \ sq) (sp ∪ sq)ᶜ
have simp : ∀ ⦃a : α⦄, a ∈ sp → a ∉ sq → a ∉ sp → a ∈ sq
Tactic: simp [Set.disjoint_left]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
inst_2 : Finite.{u_1 + 1} (↑{x : α | p x} : Type u_1)
e : { x : α // p x } ≃ { x : α // q x }
x : α
hx : ¬p x
⊢ Eq (α := α) ((e.extendSubtype (p := p) (q := q) : (a : α) → α) x : α)
    ((↑((e.toCompl (p := p) (q := q) : (a : (↑{x : α | ¬p x} : Type u_1)) → (↑{x : α | ¬q x} : Type u_1))
            (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {x : α | ¬p x} x) x hx)) :
        α) :
      α)
have simp : Eq.{u_1 + 1} (α := α)
  (↑((e.toCompl (p := p) (q := q) : (a : { x : α // ¬p x }) → { x : α // ¬q x })
        (Subtype.mk (p := fun (a : α) ↦ ¬p a) x hx)) :
    α)
  (↑((e.toCompl (p := p) (q := q) : (a : (↑{x : α | ¬p x} : Type u_1)) → (↑{x : α | ¬q x} : Type u_1))
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {x : α | ¬p x} x) x hx)) :
    α)
Tactic: simp only [extendSubtype, subtypeCongr, Equiv.trans_apply, Equiv.sumCongr_apply,
    sumCompl_symm_apply_of_neg hx, Sum.map_inr, sumCompl_apply_inr]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f g : α → β
hf : Function.Injective f
hg : Function.Injective g
⊢ ∃ (σ : Perm β), ∀ (a : α), (σ : (a : β) → β) (f a) = g a
have this : Finite.{u_2 + 1} (↑{x : β | x ∈ Set.range f} : Type u_2)
Tactic: have : Finite {x | x ∈ Set.range f} := .of_surjective _ (Set.codRestrict_range_surjective f)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f g : α → β
hf : Function.Injective f
hg : Function.Injective g
this : Finite.{u_2 + 1} (↑{x : β | x ∈ Set.range f} : Type u_2)
⊢ ∃ (σ : Perm β), ∀ (a : α), (σ : (a : β) → β) (f a) = g a
have refine : ∀ (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
Tactic: refine ⟨((Equiv.ofInjective f hf).symm.trans (Equiv.ofInjective g hg)).extendSubtype, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f g : α → β
hf : Function.Injective f
hg : Function.Injective g
⊢ ∃ (σ : Perm β), ∀ (a : α), (σ : (a : β) → β) (f a) = g a
have have : ∀ (this : Finite.{u_2 + 1} (↑{x : β | x ∈ Set.range f} : Type u_2)),
  ∃ (σ : 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]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
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
⊢ ∃ (σ : Perm β), ∀ (a : α), (σ : (a : β) → β) (f a) = g a
have 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
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]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
β : Type u_2
s t : Finset β
h : s.card = t.card
⊢ ∃ (σ : Perm β), Finset.map (Equiv.toEmbedding σ) s = t
have obtain : ∀ (σ : Perm β)
  (hσ :
    ∀ (a : ↥s), Eq (α := β) ((σ : (a : β) → β) (↑a : β) : β) ((↑((Finset.equivOfCardEq h : (a : ↥s) → ↥t) a) : β) : β)),
  ∃ (σ : 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)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
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) : β) : β)
⊢ ∃ (σ : Perm β), Finset.map (Equiv.toEmbedding σ) s = t
have refine : ∀ (b : β) (hb : b ∈ Finset.map (Equiv.toEmbedding σ) s), b ∈ t
Tactic: refine ⟨σ, Finset.eq_of_subset_of_card_le (fun b hb => ?_) (by simp [h])⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
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
⊢ b ∈ t
have obtain : ∀ (a : β) (ha : a ∈ s)
  (hb : Membership.mem (α := β) (Finset.map (Equiv.toEmbedding σ) s) ((Equiv.toEmbedding σ : (a : β) → β) a : β)),
  Membership.mem (α := β) t ((Equiv.toEmbedding σ : (a : β) → β) a : β)
Tactic: obtain ⟨a, ha, rfl⟩ := Finset.mem_map.mp hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
Goal:
β : Type u_2
s t : Finset β
h : s.card = t.card
⊢ ∃ (σ : Perm β), Finset.map (Equiv.toEmbedding σ) s = t
have obtain : ∀ (σ : Perm β)
  (hσ :
    ∀ (a : ↥s), Eq (α := β) ((σ : (a : β) → β) (↑a : β) : β) ((↑((Finset.equivOfCardEq h : (a : ↥s) → ↥t) 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
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
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
have 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
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
-- Lean 4 proof step from Mathlib.Logic.Equiv.Fintype (goal)
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
⊢ ∃ (σ : Perm β), Finset.map (Equiv.toEmbedding σ) s = t
have 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 : β)
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
-- Lean 4 proof step from Mathlib.Logic.Equiv.Functor (goal)
Goal:
α : Type u
f : Type u → Type v
inst : Functor f
inst_1 : LawfulFunctor f
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
have H : ∀ (x : f α),
  Eq (α := f α) ((mapEquiv f (Equiv.refl α) : (a : f α) → f α) x : f α) ((Equiv.refl (f α) : (a : f α) → f α) x : f α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Functor (goal)
Goal:
α : Type u
f : Type u → Type v
inst : Functor f
inst_1 : LawfulFunctor f
x : f α
⊢ Eq (α := f α) ((mapEquiv f (Equiv.refl α) : (a : f α) → f α) x : f α) ((Equiv.refl (f α) : (a : f α) → f α) x : f α)
have H : (⇑(Equiv.refl α) : (a : α) → α) <$> x = x
Tactic: simp only [mapEquiv_apply, refl_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Functor (goal)
Goal:
α : Type u
α' : Type v
F : Type u → Type v → Type w
inst : Bifunctor F
inst_1 : LawfulBifunctor F
⊢ mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α')
have H : ∀ (x : F α α'),
  Eq (α := F α α') ((mapEquiv F (Equiv.refl α) (Equiv.refl α') : (a : F α α') → F α α') x : F α α')
    ((Equiv.refl (F α α') : (a : F α α') → F α α') x : F α α')
Tactic: ext x
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
l : List α
⊢ map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) l) = l
have rw : map (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)) l = l
Tactic: rw [List.map_map, e.symm_comp_self, List.map_id]
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
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
⊢ map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) l) = l
have rw₁ : map id l = l
Tactic: rw [List.map_map, e.symm_comp_self, List.map_id]
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
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
⊢ map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) l) = l
have rw₂ : l = l
Tactic: rw [List.map_map, e.symm_comp_self, List.map_id]
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
l : List β
⊢ map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) l) = l
have rw : map (Function.comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) l = l
Tactic: rw [List.map_map, e.self_comp_symm, List.map_id]
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
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
⊢ map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) l) = l
have rw₁ : map id l = l
Tactic: rw [List.map_map, e.self_comp_symm, List.map_id]
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
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
⊢ map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) l) = l
have rw₂ : l = l
Tactic: rw [List.map_map, e.self_comp_symm, List.map_id]
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
inst : Encodable α
l : List α
⊢ decodeList (encodeList l) = some l
have nil : Eq.{u_1 + 1} (α := Option (List α)) (decodeList (encodeList.{u_1} (α := α) [])) (some [])
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
inst : Encodable α
l : List α
nil : Eq.{u_1 + 1} (α := Option (List α)) (decodeList (encodeList.{u_1} (α := α) [])) (some [])
⊢ decodeList (encodeList l) = some l
have cons : ∀ (head : α) (tail : List α),
  decodeList (encodeList tail) = some tail → decodeList (encodeList (head :: tail)) = some (head :: tail)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α_1 : Type u_1
inst : Encodable α_1
α : Type u_2
inst_1 : Countable α
⊢ Countable.{u_2 + 1} (List α)
have haveI : ∀ (this : Encodable α), Countable.{u_2 + 1} (List α)
Tactic: haveI := Encodable.ofCountable α
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
inst : Encodable α
⊢ Eq.{u_1 + 1} (α := Option (List α)) (decodeList 0) (some [])
have rw : Eq.{u_1 + 1} (α := Option (List α)) (some []) (some [])
Tactic: rw [decodeList]
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
inst : Encodable α
v : ℕ
⊢ Eq.{u_1 + 1} (α := Option (List α)) (decodeList v.succ)
    ((fun (x1 : α) (x2 : List α) ↦ x1 :: x2) <$> decode (unpair v).1 <*> decode (unpair v).2)
have 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)
Tactic: rcases e : unpair v with ⟨v₁, v₂⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
inst : Encodable α
v 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)
have 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₂)
Tactic: simp [decodeList, e]
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
inst : Denumerable α
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList 0) a ∧ encodeList a = 0
have rw : ∃ (a : List α), Membership.mem (γ := Option (List α)) (some []) a ∧ encodeList a = 0
Tactic: rw [decodeList]
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
inst : Denumerable α
v : ℕ
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList v.succ) a ∧ encodeList a = v.succ
have rcases : ∀ (v₁ v₂ : ℕ) (e : unpair v = (v₁, v₂)),
  ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList v.succ) a ∧ encodeList a = v.succ
Tactic: rcases e : unpair v with ⟨v₁, v₂⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (hypothesis)
Goal:
α : Type u_1
inst : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList v.succ) a ∧ encodeList a = v.succ
have h : (unpair v).2 ≤ v
Tactic: have h := unpair_right_le v
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (hypothesis)
Goal:
α : Type u_1
inst : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (unpair v).2 ≤ v
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList v.succ) a ∧ encodeList a = v.succ
have h₁ : (v₁, v₂).2 ≤ v
Tactic: rw [e] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
inst : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList v.succ) a ∧ encodeList a = v.succ
have 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
Tactic: rcases have : v₂ < succ v := lt_succ_of_le h
      denumerable_list_aux v₂ with
      ⟨a, h₁, h₂⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (hypothesis)
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₂
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList v.succ) a ∧ encodeList a = v.succ
have h₃ : decodeList v₂ = some a
Tactic: rw [Option.mem_def] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
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₂
⊢ ∃ (a : List α), Membership.mem (γ := Option (List α)) (decodeList v.succ) a ∧ encodeList a = v.succ
have h₃ : Membership.mem (γ := Option (List α)) (decodeList v.succ) (ofNat α v₁ :: a) ∧ encodeList (ofNat α v₁ :: a) = v.succ
Tactic: use ofNat α v₁ :: a
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
inst : Denumerable α
⊢ Eq.{u_1 + 1} (α := List α) (ofNat (List α) 0) []
have rw : Eq.{u_1 + 1} (α := List α) (ofNat (List α) (encode.{u_1} (α := List α) [])) []
Tactic: rw [← @encode_list_nil α, ofNat_encode]
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
inst : Denumerable α
rw : Eq.{u_1 + 1} (α := List α) (ofNat (List α) (encode.{u_1} (α := List α) [])) []
⊢ Eq.{u_1 + 1} (α := List α) (ofNat (List α) 0) []
have rw₁ : Eq.{u_1 + 1} (α := List α) [] []
Tactic: rw [← @encode_list_nil α, ofNat_encode]
-- Lean 4 proof step from Mathlib.Logic.Equiv.List (goal)
Goal:
α : Type u_1
inst : Denumerable α
v : ℕ
⊢ decodeList v.succ = some (ofNat α (unpair v).1 :: ofNat (List α) (unpair v).2)
have rcases : ∀ (v₁ v₂ : ℕ) (e : unpair v = (v₁, v₂)), decodeList v.succ = some (ofNat α (v₁, v₂).1 :: ofNat (List α) (v₁, v₂).2)
Tactic: rcases e : unpair v with ⟨v₁, v₂⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.Multiset (goal)
Goal:
m : ℕ
l : List ℕ
n : ℕ
⊢ lower (raise (m :: l) n) n = m :: l
have rw : lower ((m + n) :: raise l (m + n)) n = m :: l
Tactic: rw [raise, lower, Nat.add_sub_cancel_right, lower_raise l]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Multiset (goal)
Goal:
m : ℕ
l : List ℕ
n : ℕ
rw : lower ((m + n) :: raise l (m + n)) n = m :: l
⊢ lower (raise (m :: l) n) n = m :: l
have rw₁ : (m + n - n) :: lower (raise l (m + n)) (m + n) = m :: l
Tactic: rw [raise, lower, Nat.add_sub_cancel_right, lower_raise l]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Multiset (goal)
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
⊢ lower (raise (m :: l) n) n = m :: l
have rw₂ : m :: lower (raise l (m + n)) (m + n) = m :: l
Tactic: rw [raise, lower, Nat.add_sub_cancel_right, lower_raise l]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Multiset (goal)
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
⊢ lower (raise (m :: l) n) n = m :: l
have rw₃ : m :: l = m :: l
Tactic: rw [raise, lower, Nat.add_sub_cancel_right, lower_raise l]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Multiset (hypothesis)
Goal:
m : ℕ
l : List ℕ
n : ℕ
h : (n :: m :: l).SortedLE
⊢ raise (lower (m :: l) n) n = m :: l
have this : n ≤ m
Tactic: have : n ≤ m := List.rel_of_pairwise_cons h.pairwise List.mem_cons_self
-- Lean 4 proof step from Mathlib.Logic.Equiv.Multiset (hypothesis)
Goal:
α : Type u_1
inst : Denumerable α
s : Multiset α
⊢ (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
have this : 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
-- Lean 4 proof step from Mathlib.Logic.Equiv.Nat (goal)
Goal:
⊢ Eq (α := (a : ℕ ⊕ ℕ) → ℕ) (⇑natSumNatEquivNat : (a : ℕ ⊕ ℕ) → ℕ)
    (Sum.elim (fun (x : ℕ) ↦ 2 * x) fun (x : ℕ) ↦ 2 * x + 1)
have h : ∀ (x : ℕ),
  Eq (α := ℕ) ((natSumNatEquivNat : (a : ℕ ⊕ ℕ) → ℕ) (Sum.inl x) : ℕ)
    (Sum.elim (fun (x : ℕ) ↦ 2 * x) (fun (x : ℕ) ↦ 2 * x + 1) (Sum.inl x) : ℕ)
Tactic: ext (x | x)