awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : (s.sort fun (a b : α) ↦ a ≤ b).length - 1 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
this : s.max' H ∈ l
i : Fin l.length
hi : l.get i = s.max' H
⊢ s.max' H ≤
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.sort fun (a b : α) ↦ a ≤ b)
      ((s.sort fun (a b : α) ↦ a ≤ b).length - 1) h
have a : l.get i ≤
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (s.sort fun (a b : α) ↦ a ≤ b)
    ((s.sort fun (a b : α) ↦ a ≤ b).length - 1) h
Tactic: rw [← hi]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
s : Finset α
h : (s.sort fun (a b : α) ↦ a ≤ b).length - 1 < (s.sort fun (a b : α) ↦ a ≤ b).length
⊢ s.Nonempty
have h₁ : #s - 1 < #s
Tactic: rw [length_sort] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ (↑i : ℕ) < (s.sort fun (a b : α) ↦ a ≤ b).length
have rw : (↑i : ℕ) < k
Tactic: rw [length_sort, h]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ image (α := Fin k) (⇑(s.orderEmbOfFin h) : (a : Fin k) → α) univ = s
have a : (↑(image (α := Fin k) (⇑(s.orderEmbOfFin h) : (a : Fin k) → α) univ) : Set α) = (↑s : Set α)
Tactic: apply Finset.coe_injective
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ List.map (⇑(s.orderEmbOfFin h) : (a : Fin k) → α) (List.finRange k) = s.sort fun (a b : α) ↦ a ≤ b
have obtain : ∀ (h : #s = (s.sort fun (a b : α) ↦ a ≤ b).length),
  List.map (α := Fin (s.sort fun (a b : α) ↦ a ≤ b).length)
      (⇑(s.orderEmbOfFin h) : (a : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) → α)
      (List.finRange (s.sort fun (a b : α) ↦ a ≤ b).length) =
    s.sort fun (a b : α) ↦ a ≤ b
Tactic: obtain rfl : k = s.sort.length := by simp [h]
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a : α
i : Fin 1
⊢ (orderEmbOfFin {a} ⋯ : (a : Fin 1) → α) i = a
have rw : (orderEmbOfFin {a} sorry : (a : Fin 1) → α) (⟨0, Nat.zero_lt_one⟩ : Fin 1) = a
Tactic: rw [Subsingleton.elim i ⟨0, Nat.zero_lt_one⟩, orderEmbOfFin_zero _ Nat.zero_lt_one,
    min'_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a : α
i : Fin 1
rw : (orderEmbOfFin {a} ⋯ : (a : Fin 1) → α) (⟨0, Nat.zero_lt_one⟩ : Fin 1) = a
⊢ (orderEmbOfFin {a} ⋯ : (a : Fin 1) → α) i = a
have rw₁ : min' {a} sorry = a
Tactic: rw [Subsingleton.elim i ⟨0, Nat.zero_lt_one⟩, orderEmbOfFin_zero _ Nat.zero_lt_one,
    min'_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a : α
i : Fin 1
rw : (orderEmbOfFin {a} ⋯ : (a : Fin 1) → α) (⟨0, Nat.zero_lt_one⟩ : Fin 1) = a
rw₁ : min' {a} ⋯ = a
⊢ (orderEmbOfFin {a} ⋯ : (a : Fin 1) → α) i = a
have rw₂ : a = a
Tactic: rw [Subsingleton.elim i ⟨0, Nat.zero_lt_one⟩, orderEmbOfFin_zero _ Nat.zero_lt_one,
    min'_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ f = (⇑(s.orderEmbOfFin h) : (a : Fin k) → α)
have rw : image f univ = s
Tactic: rw [← hmono.range_inj (s.orderEmbOfFin h).strictMono, range_orderEmbOfFin, ← Set.image_univ,
    ← coe_univ, ← coe_image, coe_inj]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ image f univ = s
have refine_1 : ∀ (x : α) (hx : x ∈ image f univ), x ∈ s
Tactic: refine eq_of_subset_of_card_le (fun x hx => ?_) ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
refine_1 : ∀ (x : α) (hx : x ∈ image f univ), x ∈ s
⊢ image f univ = s
have refine_2 : #s ≤ #(image f univ)
Tactic: refine eq_of_subset_of_card_le (fun x hx => ?_) ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
x : α
hx : x ∈ image f univ
⊢ x ∈ s
have refine_1 : ∀ (x : Fin k), Membership.mem (γ := Finset (Fin k)) univ x → ∀ (hx : f x ∈ image f univ), f x ∈ s
Tactic: rcases mem_image.1 hx with ⟨x, _, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ #s ≤ #(image f univ)
have refine_2 : k ≤ #(image f univ)
Tactic: rw [h, card_image_of_injective _ hmono.injective, card_univ, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
refine_2 : k ≤ #(image f univ)
⊢ #s ≤ #(image f univ)
have refine_2₁ : k ≤ card (α := Fin k) univ
Tactic: rw [h, card_image_of_injective _ hmono.injective, card_univ, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
refine_2 : k ≤ #(image f univ)
refine_2₁ : k ≤ card (α := Fin k) univ
⊢ #s ≤ #(image f univ)
have refine_2₂ : k ≤ Fintype.card (Fin k)
Tactic: rw [h, card_image_of_injective _ hmono.injective, card_univ, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
refine_2 : k ≤ #(image f univ)
refine_2₁ : k ≤ card (α := Fin k) univ
refine_2₂ : k ≤ Fintype.card (Fin k)
⊢ #s ≤ #(image f univ)
have refine_2₃ : k ≤ k
Tactic: rw [h, card_image_of_injective _ hmono.injective, card_univ, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
k l : ℕ
s : Finset α
i : Fin k
j : Fin l
h : #s = k
h' : #s = l
⊢ Eq (α := α) ((s.orderEmbOfFin h : (a : Fin k) → α) i : α) ((s.orderEmbOfFin h' : (a : Fin l) → α) j : α) ↔
    (↑i : ℕ) = (↑j : ℕ)
have substs : ∀ {i j : Fin #s},
  Eq (α := α) ((s.orderEmbOfFin sorry : (a : Fin #s) → α) i : α) ((s.orderEmbOfFin sorry : (a : Fin #s) → α) j : α) ↔
    (↑i : ℕ) = (↑j : ℕ)
Tactic: substs k l
Cleared hypotheses: k, l, i, j, h, h'
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
⊢ orderEmbOfFin {i}ᶜ h =
    RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
      fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb
have a : Eq (α := (a : Fin k) → Fin (n + 1))
  ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
    (orderEmbOfFin {i}ᶜ h))
  ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
    (RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
      fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso sorry).toOrderEmbedding i.succAboveOrderEmb))
Tactic: apply DFunLike.coe_injective
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
⊢ Eq (α := (a : Fin k) → Fin (n + 1))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (orderEmbOfFin {i}ᶜ h))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
        fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb))
have a : Eq (α := (a : Fin k) → Fin (n + 1))
  ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
    (RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
      fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso sorry).toOrderEmbedding i.succAboveOrderEmb))
  ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
    (orderEmbOfFin {i}ᶜ h))
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
⊢ Eq (α := (a : Fin k) → Fin (n + 1))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
        fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (orderEmbOfFin {i}ᶜ h))
have a : ∀ (x : Fin k), Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ ((i.succAbove ∘ Fin.cast sorry) x)
Tactic: convert!
    orderEmbOfFin_unique _ (fun x ↦ ?_) ((Fin.strictMono_succAbove _).comp (Fin.cast_strictMono _))
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
a : ∀ (x : Fin k), Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ ((i.succAbove ∘ Fin.cast ⋯) x)
⊢ Eq (α := (a : Fin k) → Fin (n + 1))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
        fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb))
    ((fun (f : Fin k ↪o Fin (n + 1)) ↦ ((⇑f : (a : Fin k) → Fin (n + 1)) : (a : Fin k) → Fin (n + 1)))
      (orderEmbOfFin {i}ᶜ h))
have a₁ : k = n
Tactic: convert!
    orderEmbOfFin_unique _ (fun x ↦ ?_) ((Fin.strictMono_succAbove _).comp (Fin.cast_strictMono _))
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : card (α := Fin (n + 1)) {i}ᶜ = k
j : Fin k
⊢ (orderEmbOfFin {i}ᶜ h : (a : Fin k) → Fin (n + 1)) j = i.succAbove (Fin.cast ⋯ j)
have rw : (RelEmbedding.trans (r := fun (x1 x2 : Fin k) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (t :=
        fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (Fin.castOrderIso sorry).toOrderEmbedding i.succAboveOrderEmb :
      (a : Fin k) → Fin (n + 1))
    j =
  i.succAbove (Fin.cast sorry j)
Tactic: rw [orderEmbOfFin_compl_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
hα : Finite α
β : Type u_2
inst_1 : LinearOrder β
hβ : Infinite β
⊢ Nonempty (α ↪o β)
have haveI : ∀ (this : Fintype α), Nonempty (α ↪o β)
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
hα : Finite α
β : Type u_2
inst_1 : LinearOrder β
hβ : Infinite β
this : Fintype α
⊢ Nonempty (α ↪o β)
have obtain : ∀ (s : Finset β) (hs : s.card = Fintype.card α), Nonempty (α ↪o β)
Tactic: obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq β (Fintype.card α)
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α ↪o β
⊢ Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β)) ↔
    f = g
have refine : ∀
  (h :
    Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))),
  f = g
Tactic: refine ⟨fun h ↦ ?_, by rintro rfl; rfl⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α ↪o β
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
ef : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑f : (a : α) → β) Set.univ ⋯
eg : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑g : (a : α) → β) Set.univ ⋯
i : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) ≃o
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  let __spread.0 :=
    Equiv.setCongr (s := Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) (t :=
      Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) ⋯;
  RelIso.mk (r := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2)
    (s := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2) __spread.0
    ⋯
⊢ f = g
have this : (ef.trans i).trans eg.symm = OrderIso.refl (↑Set.univ : Type u_1)
Tactic: have : (ef.trans i).trans eg.symm = .refl _ := by
    exact Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α ↪o β
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
ef : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑f : (a : α) → β) Set.univ ⋯
eg : OrderIso.{u_1, u_2} (↑Set.univ : Type u_1)
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  StrictMonoOn.orderIso (⇑g : (a : α) → β) Set.univ ⋯
i : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2) ≃o
  (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2) :=
  let __spread.0 :=
    Equiv.setCongr (s := Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) (t :=
      Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) ⋯;
  RelIso.mk (r := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2)
    (s := fun (x1 x2 : (↑(Set.image.{u_1, u_2} (α := α) (⇑g : (a : α) → β) Set.univ) : Type u_2)) ↦ x1 ≤ x2) __spread.0
    ⋯
this : (ef.trans i).trans eg.symm = OrderIso.refl (↑Set.univ : Type u_1)
⊢ f = g
have h₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α →o β
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hg : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑g : (a : α) → β)
⊢ Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β)) ↔
    f = g
have refine : ∀
  (h :
    Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
      (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))),
  f = g
Tactic: refine ⟨fun h ↦ ?_, by rintro rfl; rfl⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
inst_2 : Finite α
f g : α →o β
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hg : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑g : (a : α) → β)
h :
  Eq.{u_2 + 1} (α := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
    (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β))
⊢ f = g
have h₁ : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ Disjoint (map Embedding.inl s) (map Embedding.inr t)
have simp_rw : ∀ ⦃a : α ⊕ β⦄,
  (∃ a_1 ∈ s, (Embedding.inl : (a : α) → α ⊕ β) a_1 = a) → ¬∃ a_2 ∈ t, (Embedding.inr : (a : β) → α ⊕ β) a_2 = a
Tactic: simp_rw [disjoint_left, mem_map]
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ u.toLeft.disjSum u.toRight = u
have h : ∀ (x : α), inl x ∈ u.toLeft.disjSum u.toRight ↔ inl x ∈ u
Tactic: ext (x | x)
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
h : ∀ (x : α), inl x ∈ u.toLeft.disjSum u.toRight ↔ inl x ∈ u
⊢ u.toLeft.disjSum u.toRight = u
have h₁ : ∀ (x : β), inr x ∈ u.toLeft.disjSum u.toRight ↔ inr x ∈ u
Tactic: ext (x | x)
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ #u.toLeft + #u.toRight = #u
have rw : #(u.toLeft.disjSum u.toRight) = #u
Tactic: rw [← card_disjSum, toLeft_disjSum_toRight]
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
rw : #(u.toLeft.disjSum u.toRight) = #u
⊢ #u.toLeft + #u.toRight = #u
have rw₁ : #u = #u
Tactic: rw [← card_disjSum, toLeft_disjSum_toRight]
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s.disjSum t).toLeft = s
have h : ∀ (x : α), x ∈ (s.disjSum t).toLeft ↔ x ∈ s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s.disjSum t).toRight = t
have h : ∀ (x : β), x ∈ (s.disjSum t).toRight ↔ x ∈ t
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ (map (Equiv.sumComm α β).toEmbedding u).toLeft = u.toRight
have h : ∀ (x : β), x ∈ (map (Equiv.sumComm α β).toEmbedding u).toLeft ↔ x ∈ u.toRight
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ (map (Equiv.sumComm α β).toEmbedding u).toRight = u.toLeft
have h : ∀ (x : α), x ∈ (map (Equiv.sumComm α β).toEmbedding u).toRight ↔ x ∈ u.toLeft
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
⊢ (cons (inl a) u ha).toLeft = cons a u.toLeft ⋯
have h : ∀ (y : α), y ∈ (cons (inl a) u ha).toLeft ↔ y ∈ cons a u.toLeft sorry
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
⊢ (cons (inr b) u hb).toLeft = u.toLeft
have h : ∀ (y : α), y ∈ (cons (inr b) u hb).toLeft ↔ y ∈ u.toLeft
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
⊢ (cons (inl a) u ha).toRight = u.toRight
have h : ∀ (y : β), y ∈ (cons (inl a) u ha).toRight ↔ y ∈ u.toRight
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
⊢ (cons (inr b) u hb).toRight = cons b u.toRight ⋯
have h : ∀ (y : β), y ∈ (cons (inr b) u hb).toRight ↔ y ∈ cons b u.toRight sorry
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (image Sum.swap u).toLeft = u.toRight
have h : ∀ (x : β), x ∈ (image Sum.swap u).toLeft ↔ x ∈ u.toRight
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (image Sum.swap u).toRight = u.toLeft
have h : ∀ (x : α), x ∈ (image Sum.swap u).toRight ↔ x ∈ u.toLeft
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (insert (inl a) u).toLeft = insert a u.toLeft
have h : ∀ (y : α), y ∈ (insert (inl a) u).toLeft ↔ y ∈ insert a u.toLeft
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (insert (inr b) u).toLeft = u.toLeft
have h : ∀ (y : α), y ∈ (insert (inr b) u).toLeft ↔ y ∈ u.toLeft
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (insert (inl a) u).toRight = u.toRight
have h : ∀ (y : β), y ∈ (insert (inl a) u).toRight ↔ y ∈ u.toRight
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (insert (inr b) u).toRight = insert b u.toRight
have h : ∀ (y : β), y ∈ (insert (inr b) u).toRight ↔ y ∈ insert b u.toRight
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (u ∩ v).toLeft = u.toLeft ∩ v.toLeft
have h : ∀ (x : α), x ∈ (u ∩ v).toLeft ↔ x ∈ u.toLeft ∩ v.toLeft
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (u ∩ v).toRight = u.toRight ∩ v.toRight
have h : ∀ (x : β), x ∈ (u ∩ v).toRight ↔ x ∈ u.toRight ∩ v.toRight
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (u ∪ v).toLeft = u.toLeft ∪ v.toLeft
have h : ∀ (x : α), x ∈ (u ∪ v).toLeft ↔ x ∈ u.toLeft ∪ v.toLeft
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (u ∪ v).toRight = u.toRight ∪ v.toRight
have h : ∀ (x : β), x ∈ (u ∪ v).toRight ↔ x ∈ u.toRight ∪ v.toRight
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (u \ v).toLeft = u.toLeft \ v.toLeft
have h : ∀ (x : α), x ∈ (u \ v).toLeft ↔ x ∈ u.toLeft \ v.toLeft
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst : DecidableEq α
inst_1 : DecidableEq β
⊢ (u \ v).toRight = u.toRight \ v.toRight
have h : ∀ (x : β), x ∈ (u \ v).toRight ↔ x ∈ u.toRight \ v.toRight
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst : Std.Commutative op
inst_1 : Std.Associative op
⊢ fold op (op b₁ b₂) f (s.disjSum t) =
    op (fold op b₁ (fun (x : α) ↦ f (inl x)) s) (fold op b₂ (fun (x : β) ↦ f (inr x)) t)
have simp_rw : Multiset.fold op (op b₁ b₂) (Multiset.map f (s.disjSum t).val) =
  op (Multiset.fold op b₁ (Multiset.map (fun (x : α) ↦ f (inl x)) s.val))
    (Multiset.fold op b₂ (Multiset.map (fun (x : β) ↦ f (inr x)) t.val))
Tactic: simp_rw [fold, disjSum, Multiset.map_disjSum, fold_add]