awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
p : Finset α → Sort u_4
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
s : Finset α
⊢ strongInduction (p := p) H s = H s fun (t : Finset α) (x : t ⊂ s) ↦ strongInduction (p := p) H t
have rw : (H s fun (t : Finset α) (h : t ⊂ s) ↦
    have this := sorry;
    strongInduction (p := p) H t) =
  H s fun (t : Finset α) (x : t ⊂ s) ↦ strongInduction (p := p) H t
Tactic: rw [strongInduction]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
p : Finset α → Sort u_4
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ s.strongInductionOn (p := fun (x : Finset α) ↦ p x) H =
    H s fun (t : Finset α) (x : t ⊂ s) ↦ t.strongInductionOn (p := fun (x : Finset α) ↦ p x) H
have dsimp : strongInduction (p := fun (x : Finset α) ↦ p x) H s =
  H s fun (t : Finset α) (x : t ⊂ s) ↦ strongInduction (p := fun (x : Finset α) ↦ p x) H t
Tactic: dsimp only [strongInductionOn]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
p : Finset α → Sort u_4
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ strongInduction (p := fun (x : Finset α) ↦ p x) H s =
    H s fun (t : Finset α) (x : t ⊂ s) ↦ strongInduction (p := fun (x : Finset α) ↦ p x) H t
have rw : (H s fun (t : Finset α) (h : t ⊂ s) ↦
    have this := sorry;
    strongInduction (p := fun (x : Finset α) ↦ p x) H t) =
  H s fun (t : Finset α) (x : t ⊂ s) ↦ strongInduction (p := fun (x : Finset α) ↦ p x) H t
Tactic: rw [strongInduction]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs : s.Nonempty
⊢ p s hs
have inl : ∀ (a : α) (hs : Finset.Nonempty (α := α) {a}), p {a} hs
Tactic: obtain ⟨a, rfl⟩ | hs := hs.exists_eq_singleton_or_nontrivial
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs : s.Nonempty
inl : ∀ (a : α) (hs : Finset.Nonempty (α := α) {a}), p {a} hs
⊢ p s hs
have inr : ∀ (hs_1 : s.Nontrivial), p s hs
Tactic: obtain ⟨a, rfl⟩ | hs := hs.exists_eq_singleton_or_nontrivial
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs_1 : s.Nonempty
hs : s.Nontrivial
⊢ p s hs_1
have inr : ∀ (t : Finset α) (ht : t.Nonempty) (hts : t ⊂ s), p t ht
Tactic: refine h₁ hs fun t ht hts ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs_1 : s.Nonempty
hs : s.Nontrivial
t : Finset α
ht : t.Nonempty
hts : t ⊂ s
⊢ p t ht
have inr : ∀ (this : #t < #s), p t ht
Tactic: have := card_lt_card hts
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
n : ℕ
p : Finset α → Sort u_4
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
s : Finset α
⊢ strongDownwardInduction (p := p) H s =
    H s fun {t : Finset α} (ht : #t ≤ n) (x : s ⊂ t) ↦ strongDownwardInduction (p := p) H t ht
have rw : (H s fun {t : Finset α} (ht : #t ≤ n) (h : s ⊂ t) ↦
    have this := sorry;
    have this := sorry;
    strongDownwardInduction (p := p) H t ht) =
  H s fun {t : Finset α} (ht : #t ≤ n) (x : s ⊂ t) ↦ strongDownwardInduction (p := p) H t ht
Tactic: rw [strongDownwardInduction]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
n : ℕ
p : Finset α → Sort u_4
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
⊢ (fun (a : #s ≤ n) ↦ s.strongDownwardInductionOn (p := fun (x : Finset α) ↦ p x) H a) =
    H s fun {t : Finset α} (ht : #t ≤ n) (x : s ⊂ t) ↦ t.strongDownwardInductionOn (p := fun (x : Finset α) ↦ p x) H ht
have dsimp : (fun (a : #s ≤ n) ↦ strongDownwardInduction (p := fun (x : Finset α) ↦ p x) H s a) =
  H s fun {t : Finset α} (ht : #t ≤ n) (x : s ⊂ t) ↦ strongDownwardInduction (p := fun (x : Finset α) ↦ p x) H t ht
Tactic: dsimp only [strongDownwardInductionOn]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
n : ℕ
p : Finset α → Sort u_4
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
⊢ (fun (a : #s ≤ n) ↦ strongDownwardInduction (p := fun (x : Finset α) ↦ p x) H s a) =
    H s fun {t : Finset α} (ht : #t ≤ n) (x : s ⊂ t) ↦ strongDownwardInduction (p := fun (x : Finset α) ↦ p x) H t ht
have rw : (fun (a : #s ≤ n) ↦
    H s
      (fun {t : Finset α} (ht : #t ≤ n) (h : s ⊂ t) ↦
        have this := sorry;
        have this := sorry;
        strongDownwardInduction (p := fun (x : Finset α) ↦ p x) H t ht)
      a) =
  H s fun {t : Finset α} (ht : #t ≤ n) (x : s ⊂ t) ↦ strongDownwardInduction (p := fun (x : Finset α) ↦ p x) H t ht
Tactic: rw [strongDownwardInduction]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s : Finset α
a : α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
hs : a ∈ s
⊢ (↑(#(s.erase a)) : R) = HSub.hSub (α := R) (↑(#s) : R) 1
have rw : (↑(#(s.erase a)) : R) = HSub.hSub (α := R) (↑(#(s.erase a) + 1) : R) 1
Tactic: rw [← card_erase_add_one hs, cast_add, cast_one, eq_sub_iff_add_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s : Finset α
a : α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
hs : a ∈ s
rw : (↑(#(s.erase a)) : R) = HSub.hSub (α := R) (↑(#(s.erase a) + 1) : R) 1
⊢ (↑(#(s.erase a)) : R) = HSub.hSub (α := R) (↑(#s) : R) 1
have rw₁ : (↑(#(s.erase a)) : R) = HAdd.hAdd (α := R) (↑(#(s.erase a)) : R) (↑1 : R) - 1
Tactic: rw [← card_erase_add_one hs, cast_add, cast_one, eq_sub_iff_add_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s : Finset α
a : α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
hs : a ∈ s
rw : (↑(#(s.erase a)) : R) = HSub.hSub (α := R) (↑(#(s.erase a) + 1) : R) 1
rw₁ : (↑(#(s.erase a)) : R) = HAdd.hAdd (α := R) (↑(#(s.erase a)) : R) (↑1 : R) - 1
⊢ (↑(#(s.erase a)) : R) = HSub.hSub (α := R) (↑(#s) : R) 1
have rw₂ : (↑(#(s.erase a)) : R) = HAdd.hAdd (α := R) (↑(#(s.erase a)) : R) 1 - 1
Tactic: rw [← card_erase_add_one hs, cast_add, cast_one, eq_sub_iff_add_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s : Finset α
a : α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
hs : a ∈ s
rw : (↑(#(s.erase a)) : R) = HSub.hSub (α := R) (↑(#(s.erase a) + 1) : R) 1
rw₁ : (↑(#(s.erase a)) : R) = HAdd.hAdd (α := R) (↑(#(s.erase a)) : R) (↑1 : R) - 1
rw₂ : (↑(#(s.erase a)) : R) = HAdd.hAdd (α := R) (↑(#(s.erase a)) : R) 1 - 1
⊢ (↑(#(s.erase a)) : R) = HSub.hSub (α := R) (↑(#s) : R) 1
have rw₃ : HAdd.hAdd (α := R) (↑(#(s.erase a)) : R) 1 = HAdd.hAdd (α := R) (↑(#(s.erase a)) : R) 1
Tactic: rw [← card_erase_add_one hs, cast_add, cast_one, eq_sub_iff_add_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
⊢ (↑(#(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) - (↑(#(s ∪ t)) : R)
have rw : HAdd.hAdd (α := R) (↑(#(s ∩ t)) : R) (↑(#(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
Tactic: rw [eq_sub_iff_add_eq, ← cast_add, card_inter_add_card_union, cast_add]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
rw : HAdd.hAdd (α := R) (↑(#(s ∩ t)) : R) (↑(#(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
⊢ (↑(#(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) - (↑(#(s ∪ t)) : R)
have rw₁ : (↑(#(s ∩ t) + #(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
Tactic: rw [eq_sub_iff_add_eq, ← cast_add, card_inter_add_card_union, cast_add]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
rw : HAdd.hAdd (α := R) (↑(#(s ∩ t)) : R) (↑(#(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
rw₁ : (↑(#(s ∩ t) + #(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
⊢ (↑(#(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) - (↑(#(s ∪ t)) : R)
have rw₂ : (↑(#s + #t) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
Tactic: rw [eq_sub_iff_add_eq, ← cast_add, card_inter_add_card_union, cast_add]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
rw : HAdd.hAdd (α := R) (↑(#(s ∩ t)) : R) (↑(#(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
rw₁ : (↑(#(s ∩ t) + #(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
rw₂ : (↑(#s + #t) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
⊢ (↑(#(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) - (↑(#(s ∪ t)) : R)
have rw₃ : HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
Tactic: rw [eq_sub_iff_add_eq, ← cast_add, card_inter_add_card_union, cast_add]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
⊢ (↑(#(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) - (↑(#(s ∩ t)) : R)
have rw : HAdd.hAdd (α := R) (↑(#(s ∪ t)) : R) (↑(#(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
Tactic: rw [eq_sub_iff_add_eq, ← cast_add, card_union_add_card_inter, cast_add]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
rw : HAdd.hAdd (α := R) (↑(#(s ∪ t)) : R) (↑(#(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
⊢ (↑(#(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) - (↑(#(s ∩ t)) : R)
have rw₁ : (↑(#(s ∪ t) + #(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
Tactic: rw [eq_sub_iff_add_eq, ← cast_add, card_union_add_card_inter, cast_add]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
rw : HAdd.hAdd (α := R) (↑(#(s ∪ t)) : R) (↑(#(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
rw₁ : (↑(#(s ∪ t) + #(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
⊢ (↑(#(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) - (↑(#(s ∩ t)) : R)
have rw₂ : (↑(#s + #t) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
Tactic: rw [eq_sub_iff_add_eq, ← cast_add, card_union_add_card_inter, cast_add]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
rw : HAdd.hAdd (α := R) (↑(#(s ∪ t)) : R) (↑(#(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
rw₁ : (↑(#(s ∪ t) + #(s ∩ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
rw₂ : (↑(#s + #t) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
⊢ (↑(#(s ∪ t)) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) - (↑(#(s ∩ t)) : R)
have rw₃ : HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R) = HAdd.hAdd (α := R) (↑(#s) : R) (↑(#t) : R)
Tactic: rw [eq_sub_iff_add_eq, ← cast_add, card_union_add_card_inter, cast_add]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
h : s ⊆ t
⊢ (↑(#(t \ s)) : R) = HSub.hSub (α := R) (↑(#t) : R) (↑(#s) : R)
have rw : (↑(#t - #s) : R) = HSub.hSub (α := R) (↑(#t) : R) (↑(#s) : R)
Tactic: rw [card_sdiff_of_subset h, Nat.cast_sub (card_mono h)]
-- Lean 4 proof step from Mathlib.Data.Finset.CastCard (goal)
Goal:
α : Type u_1
R : Type u_2
s t : Finset α
inst : DecidableEq α
inst_1 : AddGroupWithOne R
h : s ⊆ t
rw : (↑(#t - #s) : R) = HSub.hSub (α := R) (↑(#t) : R) (↑(#s) : R)
⊢ (↑(#(t \ s)) : R) = HSub.hSub (α := R) (↑(#t) : R) (↑(#s) : R)
have rw₁ : HSub.hSub (α := R) (↑(#t) : R) (↑(#s) : R) = HSub.hSub (α := R) (↑(#t) : R) (↑(#s) : R)
Tactic: rw [card_sdiff_of_subset h, Nat.cast_sub (card_mono h)]
-- Lean 4 proof step from Mathlib.Data.Finset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ s.toFinset ⊂ t.toFinset ↔ s ⊂ t
have simp_rw : s ⊆ t ∧ ¬t ⊆ s ↔ s ⊂ t
Tactic: simp_rw [Finset.ssubset_def, toFinset_subset]
-- Lean 4 proof step from Mathlib.Data.Finset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ s.val.toFinset = s
have h : ∀ (a : α), a ∈ s.val.toFinset ↔ a ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ a ∈ s.val.toFinset ↔ a ∈ s
have h : a ∈ s.val ↔ a ∈ s
Tactic: rw [Multiset.mem_toFinset, ← mem_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
h : a ∈ s.val ↔ a ∈ s
⊢ a ∈ s.val.toFinset ↔ a ∈ s
have h₁ : a ∈ s ↔ a ∈ s
Tactic: rw [Multiset.mem_toFinset, ← mem_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ l ~ l'
have rw : (↑l : Multiset α) = (↑l' : Multiset α)
Tactic: rw [← Multiset.coe_eq_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Dedup (goal)
Goal:
α : Type u_1
s : Finset α
⊢ s.toList.Nodup
have rw : s.val.Nodup
Tactic: rw [toList, ← Multiset.coe_nodup, Multiset.coe_toList]
-- Lean 4 proof step from Mathlib.Data.Finset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ s.toList.toFinset = s
have h : ∀ (a : α), a ∈ s.toList.toFinset ↔ a ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : List α
hs : s.Nodup
⊢ s.toFinset.toList.Perm s
have apply : s.toFinset.toList.toFinset = s.toFinset
Tactic: apply List.perm_of_nodup_nodup_toFinset_eq (nodup_toList _) hs
-- Lean 4 proof step from Mathlib.Data.Finset.Dedup (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : List α
hs : s.Nodup
⊢ s.toFinset.toList.toFinset = s.toFinset
have rw : s.toFinset = s.toFinset
Tactic: rw [toList_toFinset]
-- Lean 4 proof step from Mathlib.Data.Finset.Defs (goal)
Goal:
α : Type u_1
s : Multiset α
nodup : s.Nodup
t : Multiset α
nodup_1 : t.Nodup
h : { val := s, nodup := nodup : Finset α }.val = { val := t, nodup := nodup_1 }.val
⊢ { val := s, nodup := nodup : Finset α } = { val := t, nodup := nodup_1 }
have refl : ∀ (nodup_2 : s.Nodup), { val := s, nodup := nodup : Finset α } = { val := s, nodup := nodup_2 }
Tactic: cases h
Cleared hypotheses: t, nodup_1, h
-- Lean 4 proof step from Mathlib.Data.Finset.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
have h : ∀ (x : α), (∀ x_1 ∈ s, x_1 < x) ↔ s.max' hs < x
Tactic: convert! _root_.exists_between (a₁ := s.max' hs) (a₂ := t.min' ht) (by simp_all)
-- Lean 4 proof step from Mathlib.Data.Finset.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
h : ∀ (x : α), (∀ x_1 ∈ s, x_1 < x) ↔ s.max' hs < x
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
have h₁ : ∀ (x : α), (∀ y ∈ t, x < y) ↔ x < t.min' ht
Tactic: convert! _root_.exists_between (a₁ := s.max' hs) (a₂ := t.min' ht) (by simp_all)
-- Lean 4 proof step from Mathlib.Data.Finset.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
have pos : ∀ (hs : s.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
Tactic: by_cases hs : s.Nonempty
-- Lean 4 proof step from Mathlib.Data.Finset.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
pos : ∀ (hs : s.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
have neg : ∀ (hs : ¬s.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
Tactic: by_cases hs : s.Nonempty
-- Lean 4 proof step from Mathlib.Data.Finset.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
have pos : ∀ (ht : t.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
Tactic: by_cases ht : t.Nonempty
-- Lean 4 proof step from Mathlib.Data.Finset.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
pos : ∀ (ht : t.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
have neg : ∀ (ht : ¬t.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
Tactic: by_cases ht : t.Nonempty
-- Lean 4 proof step from Mathlib.Data.Finset.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
have pos : ∀ (ht : t.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
Tactic: by_cases ht : t.Nonempty
-- Lean 4 proof step from Mathlib.Data.Finset.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Finset α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
pos : ∀ (ht : t.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
have neg : ∀ (ht : ¬t.Nonempty), ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
Tactic: by_cases ht : t.Nonempty
-- Lean 4 proof step from Mathlib.Data.Finset.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
have h : Eq.{u_1 + 1} (α := α → Prop) (fun (b : α) ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) fun (b : α) ↦
  (∀ x ∈ hsf.toFinset (s := s), x < b) ∧ ∀ y ∈ htf.toFinset (s := t), b < y
Tactic: convert!
    Finset.exists_between (s := hsf.toFinset) (t := htf.toFinset) (by simpa) (by simpa)
      (by simpa) using
    1
-- Lean 4 proof step from Mathlib.Data.Finset.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : DenselyOrdered α
inst_2 : NoMaxOrder α
inst_3 : NoMinOrder α
inst_4 : Nonempty α
s t : Set α
hs : s.Finite
ht : t.Finite
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
have h : Eq.{u_1 + 1} (α := α → Prop) (fun (b : α) ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) fun (b : α) ↦
  (∀ x ∈ hs.toFinset (s := s), x < b) ∧ ∀ y ∈ ht.toFinset (s := t), b < y
Tactic: convert! hs.toFinset.exists_between' ht.toFinset (by simpa) using 1
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
h : Disjoint s t
⊢ (s.disjUnion t h).dens = s.dens + t.dens
have simp_rw : HDiv.hDiv (α := ℚ≥0) (↑(#(s.disjUnion t h)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
  HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
    HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
Tactic: simp_rw [dens, card_disjUnion, Nat.cast_add, add_div]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
h : Disjoint s t
simp_rw :
  HDiv.hDiv (α := ℚ≥0) (↑(#(s.disjUnion t h)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
⊢ (s.disjUnion t h).dens = s.dens + t.dens
have simp_rw₁ : HDiv.hDiv (α := ℚ≥0) (↑(#s + #t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
  HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
    HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
Tactic: simp_rw [dens, card_disjUnion, Nat.cast_add, add_div]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s t : Finset α
h : Disjoint s t
simp_rw :
  HDiv.hDiv (α := ℚ≥0) (↑(#(s.disjUnion t h)) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
simp_rw₁ :
  HDiv.hDiv (α := ℚ≥0) (↑(#s + #t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) =
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
⊢ (s.disjUnion t h).dens = s.dens + t.dens
have simp_rw₂ : HAdd.hAdd (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(#t) : ℚ≥0) / (↑(Fintype.card α) : ℚ≥0) =
  HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0) +
    HDiv.hDiv (α := ℚ≥0) (↑(#t) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
Tactic: simp_rw [dens, card_disjUnion, Nat.cast_add, add_div]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
⊢ (map f s).dens ≤ s.dens
have inl : IsEmpty α → (map f s).dens ≤ s.dens
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
inl : IsEmpty α → (map f s).dens ≤ s.dens
⊢ (map f s).dens ≤ s.dens
have inr : Nonempty α → (map f s).dens ≤ s.dens
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
h : Nonempty α
⊢ (map f s).dens ≤ s.dens
have inr : HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card β) : ℚ≥0) ≤
  HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
Tactic: simp_rw [dens, card_map]
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
h : Nonempty α
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card β) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
have inr : LT.lt (α := ℚ≥0) 0 (↑(Fintype.card α) : ℚ≥0)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Fintype α
s : Finset α
inst_1 : Fintype β
f : α ↪ β
h : Nonempty α
inr : LT.lt (α := ℚ≥0) 0 (↑(Fintype.card α) : ℚ≥0)
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card β) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#s) : ℚ≥0) (↑(Fintype.card α) : ℚ≥0)
have inr₁ : Fintype.card α ≤ Fintype.card β
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
⊢ (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)
have inl : IsEmpty α → (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Finset.Density (goal)
Goal:
α : Type u_2
inst : Fintype α
s : Finset α
inl : IsEmpty α → (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)
⊢ (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)
have inr : Nonempty α → (↑(Fintype.card α) : ℚ≥0) * s.dens = (↑(#s) : ℚ≥0)
Tactic: cases isEmpty_or_nonempty α