awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
h : ι → M i
h₁ :
  ∀ x_1 ∈ insert i (erase univ i),
    (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
        (((MonoidHom.mulSingle M x_1 : M x_1 →* (i : ι) → M i) : (a : M x_1) → (i : ι) → M i) (x x_1)) =
      Pi.mulSingle (M := M) x_1 (x x_1) i
⊢ noncommProd univ
      (fun (i_1 : ι) ↦
        (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
          (((MonoidHom.mulSingle M i_1 : M i_1 →* (i : ι) → M i) : (a : M i_1) → (i : ι) → M i) (x i_1)))
      ⋯ =
    x i
have h₂ : (insert i (erase univ i)).noncommProd (fun (j : ι) ↦ Pi.mulSingle (M := M) j (x j) i) sorry = x i
Tactic: convert! (noncommProd_congr (insert_erase (mem_univ i)).symm _ _).trans _
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (insert i (erase univ i)).noncommProd (fun (j : ι) ↦ Pi.mulSingle (M := M) j (x j) i) ⋯ = x i
have h : Pi.mulSingle (M := M) i (x i) i = x i
Tactic: rw [noncommProd_insert_of_notMem _ _ _ _ (notMem_erase _ _),
      noncommProd_eq_pow_card (univ.erase i), one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
h : Pi.mulSingle (M := M) i (x i) i = x i
⊢ (insert i (erase univ i)).noncommProd (fun (j : ι) ↦ Pi.mulSingle (M := M) j (x j) i) ⋯ = x i
have h₁ : ∀ x_1 ∈ erase univ i, Pi.mulSingle (M := M) x_1 (x x_1) i = 1
Tactic: rw [noncommProd_insert_of_notMem _ _ _ _ (notMem_erase _ _),
      noncommProd_eq_pow_card (univ.erase i), one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
ι : Type u_2
γ : Type u_5
inst : Monoid γ
M : ι → Type u_6
inst_1 : (i : ι) → Monoid (M i)
inst_2 : Finite ι
inst_3 : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
      ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
⊢ f = g
have intro : ∀ (val : Fintype ι), f = g
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
ι : Type u_2
γ : Type u_5
inst : Monoid γ
M : ι → Type u_6
inst_1 : (i : ι) → Monoid (M i)
inst_2 : Finite ι
inst_3 : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
      ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
val : Fintype ι
⊢ f = g
have intro : ∀ (x : (i : ι) → M i), Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) x : γ) ((g : (a : (i : ι) → M i) → γ) x : γ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
ι : Type u_2
γ : Type u_5
inst : Monoid γ
M : ι → Type u_6
inst_1 : (i : ι) → Monoid (M i)
inst_2 : Finite ι
inst_3 : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
      ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
val : Fintype ι
x : (i : ι) → M i
⊢ Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) x : γ) ((g : (a : (i : ι) → M i) → γ) x : γ)
have intro : Eq.{u_5 + 1} (α := γ) (noncommProd univ (fun (i : ι) ↦ (f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i))) sorry)
  (noncommProd univ (fun (i : ι) ↦ (g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i))) sorry)
Tactic: rw [← noncommProd_mulSingle x, univ.map_noncommProd, univ.map_noncommProd]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
ι : Type u_2
γ : Type u_5
inst : Monoid γ
M : ι → Type u_6
inst_1 : (i : ι) → Monoid (M i)
inst_2 : Finite ι
inst_3 : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
      ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
val : Fintype ι
x : (i : ι) → M i
⊢ Eq.{u_5 + 1} (α := γ)
    (noncommProd univ (fun (i : ι) ↦ (f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i))) ⋯)
    (noncommProd univ (fun (i : ι) ↦ (g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i))) ⋯)
have intro : ∀ (i : ι),
  Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i)) : γ)
    ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i)) : γ)
Tactic: congr 1 with i
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
a : α
o : Option α
⊢ a ∈ o.toFinset ↔ a ∈ o
have none : Membership.mem (γ := Finset α) (toFinset none) a ↔ Membership.mem (γ := Option α) none a
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
a : α
o : Option α
none : Membership.mem (γ := Finset α) (toFinset Option.none) a ↔ Membership.mem (γ := Option α) Option.none a
⊢ a ∈ o.toFinset ↔ a ∈ o
have some : ∀ (val : α), a ∈ (some val).toFinset ↔ a ∈ some val
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
o : Option α
⊢ o.toFinset.card = o.elim 0 1
have none : Finset.card.{u_1} (α := α) (toFinset none) = Option.elim.{u_1, 1} (α := α) none 0 1
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
o : Option α
none : Finset.card.{u_1} (α := α) (toFinset Option.none) = Option.elim.{u_1, 1} (α := α) Option.none 0 1
⊢ o.toFinset.card = o.elim 0 1
have some : ∀ (val : α), (some val).toFinset.card = (some val).elim 0 1
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
⊢ cons none (map Embedding.some s) ⋯ ≤ cons none (map Embedding.some t) ⋯ ↔ s ≤ t
have rw : cons none (map Embedding.some s) sorry ⊆ cons none (map Embedding.some t) sorry ↔ s ≤ t
Tactic: rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
rw : cons none (map Embedding.some s) ⋯ ⊆ cons none (map Embedding.some t) ⋯ ↔ s ≤ t
⊢ cons none (map Embedding.some s) ⋯ ≤ cons none (map Embedding.some t) ⋯ ↔ s ≤ t
have rw₁ : map Embedding.some s ⊆ map Embedding.some t ↔ s ≤ t
Tactic: rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
rw : cons none (map Embedding.some s) ⋯ ⊆ cons none (map Embedding.some t) ⋯ ↔ s ≤ t
rw₁ : map Embedding.some s ⊆ map Embedding.some t ↔ s ≤ t
⊢ cons none (map Embedding.some s) ⋯ ≤ cons none (map Embedding.some t) ⋯ ↔ s ≤ t
have rw₂ : s ⊆ t ↔ s ≤ t
Tactic: rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
rw : cons none (map Embedding.some s) ⋯ ⊆ cons none (map Embedding.some t) ⋯ ↔ s ≤ t
rw₁ : map Embedding.some s ⊆ map Embedding.some t ↔ s ≤ t
rw₂ : s ⊆ t ↔ s ≤ t
⊢ cons none (map Embedding.some s) ⋯ ≤ cons none (map Embedding.some t) ⋯ ↔ s ≤ t
have rw₃ : s ⊆ t ↔ s ⊆ t
Tactic: rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset (Option α)
⊢ (eraseNone : (a : Finset (Option α)) → Finset α) s = s.biUnion Option.toFinset
have h : ∀ (a : α),
  Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) a ↔
    a ∈ s.biUnion Option.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
s : Finset α
⊢ (eraseNone : (a : Finset (Option α)) → Finset α) (map Embedding.some s) = s
have h : ∀ (a : α),
  Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (map Embedding.some s) : Finset α)
      a ↔
    a ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq (Option α)
inst_1 : DecidableEq α
s t : Finset (Option α)
⊢ Eq (α := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (s ∪ t) : Finset α)
    ((eraseNone : (a : Finset (Option α)) → Finset α) s ∪ (eraseNone : (a : Finset (Option α)) → Finset α) t : Finset α)
have h : ∀ (a : α),
  Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (s ∪ t) : Finset α) a ↔
    Membership.mem (γ := Finset α)
      ((eraseNone : (a : Finset (Option α)) → Finset α) s ∪ (eraseNone : (a : Finset (Option α)) → Finset α) t :
        Finset α)
      a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq (Option α)
inst_1 : DecidableEq α
s t : Finset (Option α)
⊢ Eq (α := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (s ∩ t) : Finset α)
    ((eraseNone : (a : Finset (Option α)) → Finset α) s ∩ (eraseNone : (a : Finset (Option α)) → Finset α) t : Finset α)
have h : ∀ (a : α),
  Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (s ∩ t) : Finset α) a ↔
    Membership.mem (γ := Finset α)
      ((eraseNone : (a : Finset (Option α)) → Finset α) s ∩ (eraseNone : (a : Finset (Option α)) → Finset α) t :
        Finset α)
      a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) ∅ : Finset α) (∅ : Finset α)
have h : ∀ (a : α),
  Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) ∅ : Finset α) a ↔
    Membership.mem (γ := Finset α) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
⊢ Eq (α := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) {none} : Finset α) (∅ : Finset α)
have h : ∀ (a : α),
  Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) {none} : Finset α) a ↔
    Membership.mem (γ := Finset α) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
⊢ image some ((eraseNone : (a : Finset (Option α)) → Finset α) s) = s.erase none
have h : Membership.mem (γ := Finset (Option α)) (image some ((eraseNone : (a : Finset (Option α)) → Finset α) s)) none ↔
  none ∈ s.erase none
Tactic: ext (_ | x)
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
h :
  Membership.mem (γ := Finset (Option α)) (image some ((eraseNone : (a : Finset (Option α)) → Finset α) s)) none ↔
    none ∈ s.erase none
⊢ image some ((eraseNone : (a : Finset (Option α)) → Finset α) s) = s.erase none
have h₁ : ∀ (x : α),
  Membership.mem (γ := Finset (Option α)) (image some ((eraseNone : (a : Finset (Option α)) → Finset α) s)) (some x) ↔
    some x ∈ s.erase none
Tactic: ext (_ | x)
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
⊢ map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s) = s.erase none
have rw : image (α := α) (⇑Embedding.some : (a : α) → Option α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) =
  s.erase none
Tactic: rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
rw :
  image (α := α) (⇑Embedding.some : (a : α) → Option α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) =
    s.erase none
⊢ map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s) = s.erase none
have rw₁ : image some ((eraseNone : (a : Finset (Option α)) → Finset α) s) = s.erase none
Tactic: rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
rw :
  image (α := α) (⇑Embedding.some : (a : α) → Option α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) =
    s.erase none
rw₁ : image some ((eraseNone : (a : Finset (Option α)) → Finset α) s) = s.erase none
⊢ map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s) = s.erase none
have rw₂ : s.erase none = s.erase none
Tactic: rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
⊢ (insertNone : (a : Finset α) → Finset (Option α)) ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) =
    insert none s
have h : Membership.mem (γ := Finset (Option α))
    ((insertNone : (a : Finset α) → Finset (Option α)) ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) :
      Finset (Option α))
    none ↔
  none ∈ insert none s
Tactic: ext (_ | x)
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
h :
  Membership.mem (γ := Finset (Option α))
      ((insertNone : (a : Finset α) → Finset (Option α))
          ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) :
        Finset (Option α))
      none ↔
    none ∈ insert none s
⊢ (insertNone : (a : Finset α) → Finset (Option α)) ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) =
    insert none s
have h₁ : ∀ (x : α),
  Membership.mem (γ := Finset (Option α))
      ((insertNone : (a : Finset α) → Finset (Option α))
          ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) :
        Finset (Option α))
      (some x) ↔
    some x ∈ insert none s
Tactic: ext (_ | x)
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
s : Finset α
⊢ (eraseNone : (a : Finset (Option α)) → Finset α)
      ((insertNone : (a : Finset α) → Finset (Option α)) s : Finset (Option α)) =
    s
have h : ∀ (a : α),
  Membership.mem (γ := Finset α)
      ((eraseNone : (a : Finset (Option α)) → Finset α)
          ((insertNone : (a : Finset α) → Finset (Option α)) s : Finset (Option α)) :
        Finset α)
      a ↔
    a ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #(s.erase none)
have rw : card.{u_1} (α := Option α) (map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s)) = #(s.erase none)
Tactic: rw [← card_map Function.Embedding.some, map_some_eraseNone]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset (Option α)
rw :
  card.{u_1} (α := Option α) (map Embedding.some ((eraseNone : (a : Finset (Option α)) → Finset α) s)) = #(s.erase none)
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #(s.erase none)
have rw₁ : #(s.erase none) = #(s.erase none)
Tactic: rw [← card_map Function.Embedding.some, map_some_eraseNone]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
s : Finset (Option α)
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) ≤ #s
have rw : #(s.erase none) ≤ #s
Tactic: rw [card_eraseNone_eq_card_erase]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
s : Finset (Option α)
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) ≤ #s
have rw : #(s.erase none) ≤ #s
Tactic: classical
  rw [card_eraseNone_eq_card_erase]
  apply card_erase_le
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
s : Finset (Option α)
h : none ∈ s
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #s - 1
have rw : #(s.erase none) = #s - 1
Tactic: rw [card_eraseNone_eq_card_erase, card_erase_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
s : Finset (Option α)
h : none ∈ s
rw : #(s.erase none) = #s - 1
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #s - 1
have rw₁ : #s - 1 = #s - 1
Tactic: rw [card_eraseNone_eq_card_erase, card_erase_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
s : Finset (Option α)
h : none ∈ s
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #s - 1
have classical : #(s.erase none) = #s - 1
Tactic: classical rw [card_eraseNone_eq_card_erase, card_erase_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
s : Finset (Option α)
h : none ∈ s
classical : #(s.erase none) = #s - 1
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #s - 1
have classical₁ : #s - 1 = #s - 1
Tactic: classical rw [card_eraseNone_eq_card_erase, card_erase_of_mem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
s : Finset (Option α)
h : none ∉ s
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #s
have rw : #(s.erase none) = #s
Tactic: rw [card_eraseNone_eq_card_erase, erase_eq_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
s : Finset (Option α)
h : none ∉ s
rw : #(s.erase none) = #s
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #s
have rw₁ : #s = #s
Tactic: rw [card_eraseNone_eq_card_erase, erase_eq_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
s : Finset (Option α)
h : none ∉ s
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #s
have classical : #(s.erase none) = #s
Tactic: classical rw [card_eraseNone_eq_card_erase, erase_eq_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Finset.Option (goal)
Goal:
α : Type u_1
s : Finset (Option α)
h : none ∉ s
classical : #(s.erase none) = #s
⊢ card.{u_1} (α := α) ((eraseNone : (a : Finset (Option α)) → Finset α) s) = #s
have classical₁ : #s = #s
Tactic: classical rw [card_eraseNone_eq_card_erase, erase_eq_of_notMem h]
-- Lean 4 proof step from Mathlib.Data.Finset.PImage (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → β
inst_1 : (x : α) → Decidable (Part.some (f x)).Dom
⊢ pimage (fun (x : α) ↦ Part.some (f x)) s = image f s
have h : ∀ (a : β), Membership.mem (γ := Finset β) (pimage (fun (x : α) ↦ Part.some (f x)) s) a ↔ a ∈ image f s
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.PImage (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α →. β
inst_1 : (x : α) → Decidable (f x).Dom
⊢ pimage f ∅ = ∅
have h : ∀ (a : β), a ∈ pimage f ∅ ↔ Membership.mem (γ := Finset β) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Pairwise (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : DecidableEq ι
s : Finset ι
f : ι → α
hs : (↑s : Set ι).PairwiseDisjoint f
g : ι → ι
hf : ∀ (a : ι), f (g a) ≤ f a
⊢ (↑(Finset.image g s) : Set ι).PairwiseDisjoint f
have rw : (g '' (↑s : Set ι)).PairwiseDisjoint f
Tactic: rw [coe_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Pairwise (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a : ι
ha : Membership.mem (γ := Set ι) (⋃ i ∈ s, (↑(g i) : Set ι)) a
b : ι
hb : Membership.mem (γ := Set ι) (⋃ i ∈ s, (↑(g i) : Set ι)) b
hab : a ≠ b
⊢ Function.onFun Disjoint f a b
have ha₁ : ∃ (i : ι') (_ : i ∈ s), a ∈ (↑(g i) : Set ι)
Tactic: simp_rw [Set.mem_iUnion] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Data.Finset.Pairwise (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a : ι
ha : Membership.mem (γ := Set ι) (⋃ i ∈ s, (↑(g i) : Set ι)) a
b : ι
hb : Membership.mem (γ := Set ι) (⋃ i ∈ s, (↑(g i) : Set ι)) b
hab : a ≠ b
ha₁ : ∃ (i : ι') (_ : i ∈ s), a ∈ (↑(g i) : Set ι)
⊢ Function.onFun Disjoint f a b
have hb₁ : ∃ (i : ι') (_ : i ∈ s), b ∈ (↑(g i) : Set ι)
Tactic: simp_rw [Set.mem_iUnion] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Data.Finset.Pairwise (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a b : ι
hab : a ≠ b
ha : ∃ (i : ι') (_ : i ∈ s), a ∈ (↑(g i) : Set ι)
hb : ∃ (i : ι') (_ : i ∈ s), b ∈ (↑(g i) : Set ι)
⊢ Function.onFun Disjoint f a b
have obtain : ∀ (c : ι') (hc : c ∈ s) (ha : a ∈ (↑(g c) : Set ι)), Function.onFun Disjoint f a b
Tactic: obtain ⟨c, hc, ha⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Finset.Pairwise (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a b : ι
hab : a ≠ b
hb : ∃ (i : ι') (_ : i ∈ s), b ∈ (↑(g i) : Set ι)
c : ι'
hc : c ∈ s
ha : a ∈ (↑(g c) : Set ι)
⊢ Function.onFun Disjoint f a b
have obtain : ∀ (d : ι') (hd : d ∈ s) (hb : b ∈ (↑(g d) : Set ι)), Function.onFun Disjoint f a b
Tactic: obtain ⟨d, hd, hb⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.Finset.Pairwise (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ (↑(g c) : Set ι)
d : ι'
hd : d ∈ s
hb : b ∈ (↑(g d) : Set ι)
⊢ Function.onFun Disjoint f a b
have inl : ∀ (hcd : g c = g d), Function.onFun Disjoint f a b
Tactic: obtain hcd | hcd := eq_or_ne (g c) (g d)
-- Lean 4 proof step from Mathlib.Data.Finset.Pairwise (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ (↑(g c) : Set ι)
d : ι'
hd : d ∈ s
hb : b ∈ (↑(g d) : Set ι)
inl : ∀ (hcd : g c = g d), Function.onFun Disjoint f a b
⊢ Function.onFun Disjoint f a b
have inr : ∀ (hcd : g c ≠ g d), Function.onFun Disjoint f a b
Tactic: obtain hcd | hcd := eq_or_ne (g c) (g d)
-- Lean 4 proof step from Mathlib.Data.Finset.Pairwise (goal)
Goal:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst : Lattice α
inst_1 : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : PairwiseDisjoint.{u_1, u_3} (α := α) s fun (i' : ι') ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i) : Set ι).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ (↑(g c) : Set ι)
d : ι'
hd : d ∈ s
hb : b ∈ (↑(g d) : Set ι)
hcd : g c = g d
⊢ a ∈ (↑(g d) : Set ι)
have rwa : ∀ (ha : a ∈ (↑(g d) : Set ι)) (hd : d ∈ s) (hb : b ∈ (↑(g d) : Set ι)) (hcd : g c = g d), a ∈ (↑(g d) : Set ι)
Tactic: rwa [hcd] at ha
Cleared hypotheses: ha, hd, hb, hcd
-- Lean 4 proof step from Mathlib.Data.Finset.Pairwise (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
l : List α
hl : (↑l.toFinset : Set α).Pairwise r
hn : l.Nodup
⊢ Pairwise r l
have hl₁ : Set.Pairwise {a : α | a ∈ l} r
Tactic: rw [coe_toFinset] at hl
Cleared hypotheses: hl, hn
-- Lean 4 proof step from Mathlib.Data.Finset.Pairwise (goal)
Goal:
α : Type u_1
inst : DecidableEq α
r : α → α → Prop
l : List α
hn : l.Nodup
hs : Symmetric r
this : Std.Symm r := ⋯
⊢ (↑l.toFinset : Set α).Pairwise r ↔ Pairwise r l
have rw : Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l
Tactic: rw [coe_toFinset, hn.pairwise_coe]