awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
pos :
  ∀ (h : a.fst (β := α) = b.fst (β := β)),
    map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β))) ≠
        ∅ ↔
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
        f
            (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
              (a.snd (β := fun (i : ι) ↦ α i)) ⋯)
            (b.snd (β := fun (i : ι) ↦ β i)) ≠
          ∅
⊢ Ne (α := Finset (Sigma γ))
      (if h : a.fst (β := α) = b.fst (β := β) then
        map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))
      else ∅)
      ∅ ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) ⋯)
          (b.snd (β := fun (i : ι) ↦ β i)) ≠
        ∅
have neg : ∀ (h : ¬a.fst (β := α) = b.fst (β := β)),
  Ne (α := Finset (Sigma γ)) ∅ ∅ ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) sorry)
          (b.snd (β := fun (i : ι) ↦ β i)) ≠
        ∅
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ Eq (α := Finset (Sigma γ))
      (if h : a.fst (β := α) = b.fst (β := β) then
        map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))
      else ∅)
      ∅ ↔
    ∀ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i)) =
        ∅
have pos : ∀ (h : a.fst (β := α) = b.fst (β := β)),
  map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
        (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β))) =
      ∅ ↔
    ∀ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i)) =
        ∅
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
pos :
  ∀ (h : a.fst (β := α) = b.fst (β := β)),
    map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β))) =
        ∅ ↔
      ∀ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
        f
            (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
              (a.snd (β := fun (i : ι) ↦ α i)) h)
            (b.snd (β := fun (i : ι) ↦ β i)) =
          ∅
⊢ Eq (α := Finset (Sigma γ))
      (if h : a.fst (β := α) = b.fst (β := β) then
        map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))
      else ∅)
      ∅ ↔
    ∀ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i)) =
        ∅
have neg : ∀ (h : ¬a.fst (β := α) = b.fst (β := β)),
  Eq (α := Finset (Sigma γ)) ∅ ∅ ↔
    ∀ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i)) =
        ∅
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx : x ∈ sigmaLift (α := α) (β := β) (γ := γ) f a b
⊢ x ∈ sigmaLift (α := α) (β := β) (γ := γ) g a b
have rw : ∀
  (hx :
    ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
        (x.snd (β := γ))),
  ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
    Membership.mem (γ := Finset (γ (x.fst (β := γ))))
      (g (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
        (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
      (x.snd (β := γ))
Tactic: rw [mem_sigmaLift] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx :
  ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
    Membership.mem (γ := Finset (γ (x.fst (β := γ))))
      (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
        (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
      (x.snd (β := γ))
⊢ ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
    Membership.mem (γ := Finset (γ (x.fst (β := γ))))
      (g (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
        (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
      (x.snd (β := γ))
have ha : a.fst (β := α) = x.fst (β := γ)
Tactic: obtain ⟨ha, hb, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx :
  ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
    Membership.mem (γ := Finset (γ (x.fst (β := γ))))
      (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
        (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
      (x.snd (β := γ))
ha : a.fst (β := α) = x.fst (β := γ)
⊢ ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
    Membership.mem (γ := Finset (γ (x.fst (β := γ))))
      (g (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
        (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
      (x.snd (β := γ))
have hb : b.fst (β := β) = x.fst (β := γ)
Tactic: obtain ⟨ha, hb, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx :
  ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
    Membership.mem (γ := Finset (γ (x.fst (β := γ))))
      (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
        (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
      (x.snd (β := γ))
ha : a.fst (β := α) = x.fst (β := γ)
hb : b.fst (β := β) = x.fst (β := γ)
⊢ ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
    Membership.mem (γ := Finset (γ (x.fst (β := γ))))
      (g (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
        (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
      (x.snd (β := γ))
have hx₁ : Membership.mem (γ := Finset (γ (x.fst (β := γ))))
  (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
    (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
  (x.snd (β := γ))
Tactic: obtain ⟨ha, hb, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ card (α := Sigma γ)
      (if h : a.fst (β := α) = b.fst (β := β) then
        map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))
      else ∅) =
    if h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i) then
      #(f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i)))
    else 0
have pos : ∀ (h : a.fst (β := α) = b.fst (β := β)),
  #(map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
        (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))) =
    #(f
        (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h)
        (b.snd (β := fun (i : ι) ↦ β i)))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
pos :
  ∀ (h : a.fst (β := α) = b.fst (β := β)),
    #(map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))) =
      #(f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i)))
⊢ card (α := Sigma γ)
      (if h : a.fst (β := α) = b.fst (β := β) then
        map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))
      else ∅) =
    if h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i) then
      #(f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i)))
    else 0
have neg : ∀ (h : ¬a.fst (β := α) = b.fst (β := β)), card (α := Sigma γ) ∅ = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finset.Slice (goal)
Goal:
α : Type u_1
ι : Sort u_2
r : ℕ
f : ι → Set (Finset α)
⊢ Sized.{u_1} (α := α) r (⋃ (i : ι), f i) ↔ ∀ (i : ι), Sized r (f i)
have simp_rw : (∀ ⦃x : Finset α⦄ (x_1 : ι) (h : x ∈ f x_1), #x = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → #x = r
Tactic: simp_rw [Set.Sized, Set.mem_iUnion, forall_exists_index]
-- Lean 4 proof step from Mathlib.Data.Finset.Slice (goal)
Goal:
α : Type u_1
inst : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
A : Finset α
⊢ A ∈ 𝒜 → Membership.mem (γ := Finset (Finset α)) (powersetCard r univ) A ↔ A ∈ (↑𝒜 : Set (Finset α)) → #A = r
have rw : A ∈ 𝒜 → #A = r ↔ A ∈ (↑𝒜 : Set (Finset α)) → #A = r
Tactic: rw [mem_powersetCard_univ, mem_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Slice (goal)
Goal:
α : Type u_1
inst : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
A : Finset α
rw : A ∈ 𝒜 → #A = r ↔ A ∈ (↑𝒜 : Set (Finset α)) → #A = r
⊢ A ∈ 𝒜 → Membership.mem (γ := Finset (Finset α)) (powersetCard r univ) A ↔ A ∈ (↑𝒜 : Set (Finset α)) → #A = r
have rw₁ : A ∈ 𝒜 → #A = r ↔ A ∈ 𝒜 → #A = r
Tactic: rw [mem_powersetCard_univ, mem_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Slice (goal)
Goal:
α : Type u_1
inst : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r (↑𝒜 : Set (Finset α))
⊢ #𝒜 ≤ (Fintype.card α).choose r
have rw : #𝒜 ≤ card.{u_1} (α := Finset α) (powersetCard r univ)
Tactic: rw [Fintype.card, ← card_powersetCard]
-- Lean 4 proof step from Mathlib.Data.Finset.Slice (goal)
Goal:
α : Type u_1
𝒜 : Finset (Finset α)
inst : Fintype α
this : DecidableEq α := Classical.decEq α
⊢ ∑ r ∈ Iic (Fintype.card α), #(𝒜 # r) = #𝒜
have rw : (↑(Iic (Fintype.card α)) : Set ℕ).PairwiseDisjoint 𝒜.slice
Tactic: rw [← card_biUnion, biUnion_slice]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ (↑(s.sort r) : Multiset α).Nodup
have rw : s.val.Nodup
Tactic: rw [sort_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
⊢ s.sort r ~ s.toList
have rw : (↑(s.sort r) : Multiset α) = (↑s.toList : Multiset α)
Tactic: rw [← Multiset.coe_eq_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
inst_4 : DecidableEq α
l : List α
hl : l.Nodup
⊢ l.toFinset.sort r = l ↔ List.Pairwise r l
have refine : l.toFinset.sort r = l → List.Pairwise r l
Tactic: refine ⟨?_, ((sort_perm_toList _ r).trans (List.toFinset_toList hl)).eq_of_pairwise'
    (pairwise_sort _ _)⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
inst_4 : DecidableEq α
l : List α
hl : l.Nodup
h : l.toFinset.sort r = l
⊢ List.Pairwise r l
have rw : List.Pairwise r (l.toFinset.sort r)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ (cons a s h₂).sort r = a :: s.sort r
have rw : (cons a s h₂).val.sort r = a :: s.sort r
Tactic: rw [sort, cons_val, Multiset.sort_cons a _ r h₁, sort_val]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
rw : (cons a s h₂).val.sort r = a :: s.sort r
⊢ (cons a s h₂).sort r = a :: s.sort r
have rw₁ : (a ::ₘ s.val).sort r = a :: s.sort r
Tactic: rw [sort, cons_val, Multiset.sort_cons a _ r h₁, sort_val]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
rw : (cons a s h₂).val.sort r = a :: s.sort r
rw₁ : (a ::ₘ s.val).sort r = a :: s.sort r
⊢ (cons a s h₂).sort r = a :: s.sort r
have rw₂ : a :: s.val.sort r = a :: s.sort r
Tactic: rw [sort, cons_val, Multiset.sort_cons a _ r h₁, sort_val]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
rw : (cons a s h₂).val.sort r = a :: s.sort r
rw₁ : (a ::ₘ s.val).sort r = a :: s.sort r
rw₂ : a :: s.val.sort r = a :: s.sort r
⊢ (cons a s h₂).sort r = a :: s.sort r
have rw₃ : a :: s.sort r = a :: s.sort r
Tactic: rw [sort, cons_val, Multiset.sort_cons a _ r h₁, sort_val]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
inst_4 : DecidableEq α
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ (insert a s).sort r = a :: s.sort r
have rw : (cons a s h₂).sort r = a :: s.sort r
Tactic: rw [← cons_eq_insert _ _ h₂, sort_cons r h₁]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
s : Finset α
r : α → α → Prop
inst : DecidableRel r
inst_1 : IsTrans α r
inst_2 : Std.Antisymm r
inst_3 : Std.Total r
inst_4 : DecidableEq α
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
rw : (cons a s h₂).sort r = a :: s.sort r
⊢ (insert a s).sort r = a :: s.sort r
have rw₁ : a :: s.sort r = a :: s.sort r
Tactic: rw [← cons_eq_insert _ _ h₂, sort_cons r h₁]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
⊢ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) = s.min' H
have a : (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ s.min' H
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
a : (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ s.min' H
⊢ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) = s.min' H
have a₁ : s.min' H ≤ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
⊢ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ s.min' H
have this : s.min' H ∈ l
Tactic: have : s.min' H ∈ l := (s.mem_sort (· ≤ ·)).mpr (s.min'_mem H)
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
this : s.min' H ∈ l
⊢ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ s.min' H
have a : ∀ (i : Fin l.length) (hi : l.get i = s.min' H),
  (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ s.min' H
Tactic: obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
this : s.min' H ∈ l
i : Fin l.length
hi : l.get i = s.min' H
⊢ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ s.min' H
have a : (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length) ≤ l.get i
Tactic: rw [← hi]
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun (a b : α) ↦ a ≤ b
⊢ s.min' H ≤ (s.sort fun (a b : α) ↦ a ≤ b).get (⟨0, h⟩ : Fin (s.sort fun (a b : α) ↦ a ≤ b).length)
have this : l.get (⟨0, h⟩ : Fin l.length) ∈ s
Tactic: have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l _)
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
s : Finset α
h : 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
⊢ 0 < #s
have rwa : ∀ (h : 0 < #s), 0 < #s
Tactic: rwa [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 α
h : s.Nonempty
⊢ 0 < (s.sort fun (a b : α) ↦ a ≤ b).length
have rw : 0 < #s
Tactic: rw [length_sort]
-- 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
⊢ 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 =
    s.max' H
have a : 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 ≤
  s.max' H
Tactic: apply le_antisymm
-- 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
a :
  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 ≤
    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 =
    s.max' H
have a₁ : 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
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (hypothesis)
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
⊢ 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 ≤
    s.max' H
have this : l.get (⟨(s.sort fun (a b : α) ↦ a ≤ b).length - 1, h⟩ : Fin l.length) ∈ s
Tactic: have : l.get ⟨s.sort.length - 1, h⟩ ∈ s :=
      (s.mem_sort (· ≤ ·)).1 (List.get_mem l _)
-- Lean 4 proof step from Mathlib.Data.Finset.Sort (hypothesis)
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
⊢ 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 this : s.max' H ∈ l
Tactic: have : s.max' H ∈ l := (s.mem_sort (· ≤ ·)).mpr (s.max'_mem H)
-- 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
⊢ 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 : ∀ (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
Tactic: obtain ⟨i, hi⟩ : ∃ i, l.get i = s.max' H := List.mem_iff_get.1 this