awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
x : α
hx : x ∈ l
hx' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l)) f
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hl₁ : Nodup (α := α) ((Equiv.symm g : (a : α) → α) x :: l : List α)
hmeml₁ :
  ∀ {f : Equiv.Perm α},
    f ∈ permsOfList l →
      Eq (α := α) ((f : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((Equiv.symm g : (a : α) → α) x : α)
hf₃ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap
      (fun (b : α) ↦
        List.map
          (fun (f : Equiv.Perm α) ↦
            HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) b : Equiv.Perm α) f)
          (permsOfList l))
      l)
    f
hx'₁ :
  Membership.mem (γ := List (Equiv.Perm α))
    (List.map
      (fun (f : Equiv.Perm α) ↦
        HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) f)
      (permsOfList l))
    f
⊢ False
have hg₁ : g ∈ permsOfList l ∧ HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) g = f
Tactic: obtain rfl : g.symm x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
Cleared hypotheses: a, hl, hmeml, hf₂, hx', hg
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl' : l.Nodup
hln' : (permsOfList l).Nodup
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
x : α
hx : x ∈ l
g : Equiv.Perm α
hl : Nodup (α := α) ((Equiv.symm g : (a : α) → α) x :: l : List α)
hmeml :
  ∀ {f : Equiv.Perm α},
    f ∈ permsOfList l →
      Eq (α := α) ((f : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((Equiv.symm g : (a : α) → α) x : α)
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap
      (fun (b : α) ↦
        List.map
          (fun (f : Equiv.Perm α) ↦
            HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) b : Equiv.Perm α) f)
          (permsOfList l))
      l)
    f
hx' :
  Membership.mem (γ := List (Equiv.Perm α))
    (List.map
      (fun (f : Equiv.Perm α) ↦
        HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) f)
      (permsOfList l))
    f
hg :
  g ∈ permsOfList l ∧ HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) g = f
⊢ False
have hxa : x ≠ (Equiv.symm g : (a : α) → α) x
Tactic: have hxa : x ≠ g.symm x := fun h => (List.nodup_cons.1 hl).1 (h ▸ hx)
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : DecidableEq α_1
inst_1 : DecidableEq β_1
α : Type u_4
β : Type u_5
inst_2 : Mul α
inst_3 : Mul β
inst_4 : DecidableEq α
inst_5 : DecidableEq β
inst_6 : Fintype α
inst_7 : Fintype β
me : α ≃* β
⊢ (if h :
        ∀ (a b : α),
          (me.toEquiv : (a : α) → β) (a * b) =
            HMul.hMul (α := β) (β := β) ((me.toEquiv : (a : α) → β) a : β) ((me.toEquiv : (a : α) → β) b : β) then
      some { toEquiv := me.toEquiv, map_mul' := h }
    else none) =
    some me
have simp : { toEquiv := (↑me : α ≃ β), map_mul' := sorry } = me
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : DecidableEq α_1
inst_1 : DecidableEq β_1
α : Type u_4
β : Type u_5
inst_2 : Mul α
inst_3 : Mul β
inst_4 : DecidableEq α
inst_5 : DecidableEq β
inst_6 : Fintype α
inst_7 : Fintype β
me : α ≃* β
⊢ (if h :
        ∀ (a b : α),
          (me.toEquiv : (a : α) → β) (a * b) =
            HMul.hMul (α := β) (β := β) ((me.toEquiv : (a : α) → β) a : β) ((me.toEquiv : (a : α) → β) b : β) then
      some { toEquiv := me.toEquiv, map_mul' := h }
    else none) =
    some me
have this : { toEquiv := (↑me : α ≃ β), map_mul' := sorry } = me
Tactic: {simp; rfl}
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset (δ := δ) t ↔ ∀ (a : α), f a ∈ t a
have mp : f ∈ piFinset (δ := δ) t → ∀ (a : α), f a ∈ t a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
mp : f ∈ piFinset (δ := δ) t → ∀ (a : α), f a ∈ t a
⊢ f ∈ piFinset (δ := δ) t ↔ ∀ (a : α), f a ∈ t a
have mpr : (∀ (a : α), f a ∈ t a) → f ∈ piFinset (δ := δ) t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset (δ := δ) t → ∀ (a : α), f a ∈ t a
have mp : ∀ (x : (a : α) → Membership.mem (γ := Finset α) univ a → δ a),
  (∀ (a : α), x a sorry ∈ t a) →
    ({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a sorry, inj' := sorry } :
            (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
          x =
        f →
      ∀ (a : α), f a ∈ t a
Tactic: simp only [piFinset, mem_map, and_imp, forall_prop_of_true, mem_univ, exists_imp,
      mem_pi]
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → Membership.mem (γ := Finset α) univ a → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf :
  ({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a ⋯, inj' := ⋯ } :
        (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
      g =
    f
a : α
⊢ f a ∈ t a
have mp : Membership.mem (α := δ a) (t a)
  (({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a sorry, inj' := sorry } :
        (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
      g a :
    δ a)
Tactic: rw [← hgf]
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset (δ := δ) t
have mpr : (∀ (a : α), f a ∈ t a) →
  ∃ (a : (a : α) → Membership.mem (γ := Finset α) univ a → δ a),
    (∀ (a_1 : α), a a_1 sorry ∈ t a_1) ∧
      ({ toFun := fun (f : (a : α) → Membership.mem (γ := Finset α) univ a → δ a) (a : α) ↦ f a sorry, inj' := sorry } :
            (a : (a : α) → a ∈ univ → δ a) → (a : α) → δ a)
          a =
        f
Tactic: simp only [piFinset, mem_map, forall_prop_of_true, mem_univ, mem_pi]
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ (↑(piFinset (δ := δ) t) : Set ((a : α) → δ a)) ↔
    Membership.mem (γ := Set ((a : α) → δ a)) (Set.pi (α := δ) Set.univ fun (a : α) ↦ (↑(t a) : Set (δ a))) x
have rw : x ∈ (↑(piFinset (δ := δ) t) : Set ((a : α) → δ a)) ↔ ∀ (i : α), x i ∈ (↑(t i) : Set (δ i))
Tactic: rw [Set.mem_univ_pi]
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
γ : α → Type u_3
δ : α → Type u_4
inst_2 : (a : α) → DecidableEq (δ a)
f : (a : α) → γ a → δ a
s : (a : α) → Finset (γ a)
⊢ Eq (α := Finset ((a : α) → δ a)) (piFinset (δ := δ) fun (a : α) ↦ image (f a) (s a))
    (image (fun (b : (a : α) → γ a) (a : α) ↦ f a (b a)) (piFinset (δ := γ) s))
have h : ∀ (a : (a : α) → δ a),
  Membership.mem (γ := Finset ((a : α) → δ a)) (piFinset (δ := δ) fun (a : α) ↦ image (f a) (s a)) a ↔
    Membership.mem (γ := Finset ((a : α) → δ a))
      (image (fun (b : (a : α) → γ a) (a : α) ↦ f a (b a)) (piFinset (δ := γ) s)) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst_2 : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
⊢ image (fun (f : (a : α) → δ a) ↦ f a) (piFinset (δ := δ) t) = t a
have refine : ∀ (x : δ a) (h : x ∈ t a), ∃ a_1 ∈ piFinset (δ := δ) t, a_1 a = x
Tactic: refine (eval_image_piFinset_subset _ _).antisymm fun x h ↦ mem_image.2 ?_
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst_2 : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
x : δ a
h : x ∈ t a
⊢ ∃ a_1 ∈ piFinset (δ := δ) t, a_1 a = x
have choose : ∀ (f : (b : α) → a ≠ b → δ b) (hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b), ∃ a_1 ∈ piFinset (δ := δ) t, a_1 a = x
Tactic: choose f hf using ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_5
inst_2 : DecidableEq β
t : Finset β
a : α
⊢ image (fun (f : (a : α) → β) ↦ f a) (piFinset (δ := fun (_i : α) ↦ β) fun (_i : α) ↦ t) = t
have inl : Eq.{u_5 + 1} (α := Finset β) (image (fun (f : (a : α) → β) ↦ f a) (piFinset (δ := fun (_i : α) ↦ β) fun (_i : α) ↦ ∅)) ∅
Tactic: obtain rfl | ht := t.eq_empty_or_nonempty
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_5
inst_2 : DecidableEq β
t : Finset β
a : α
inl :
  Eq.{u_5 + 1} (α := Finset β) (image (fun (f : (a : α) → β) ↦ f a) (piFinset (δ := fun (_i : α) ↦ β) fun (_i : α) ↦ ∅))
    ∅
⊢ image (fun (f : (a : α) → β) ↦ f a) (piFinset (δ := fun (_i : α) ↦ β) fun (_i : α) ↦ t) = t
have inr : ∀ (ht : t.Nonempty), image (fun (f : (a : α) → β) ↦ f a) (piFinset (δ := fun (_i : α) ↦ β) fun (_i : α) ↦ t) = t
Tactic: obtain rfl | ht := t.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_5
inst_2 : DecidableEq β
a : α
⊢ Eq.{u_5 + 1} (α := Finset β) (image (fun (f : (a : α) → β) ↦ f a) (piFinset (δ := fun (_i : α) ↦ β) fun (_i : α) ↦ ∅))
    ∅
have this : Nonempty α
Tactic: haveI : Nonempty α := ⟨a⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_3
β : α → Type u_4
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : (a : α) → Fintype (β a)
⊢ Eq (α := Finset ((a : α) → Membership.mem (γ := Finset α) univ a → β a)) (pi (β := β) univ fun (a : α) ↦ univ) univ
have h : ∀ (a : (a : α) → Membership.mem (γ := Finset α) univ a → β a),
  Membership.mem (γ := Finset ((a : α) → Membership.mem (γ := Finset α) univ a → β a))
      (pi (β := β) univ fun (a : α) ↦ univ) a ↔
    Membership.mem (γ := Finset ((a : α) → Membership.mem (γ := Finset α) univ a → β a)) univ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
ι : Type u_3
inst : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ (Set.pi (α := κ) univ t).Finite
have intro : ∀ (val : Fintype ι), (Set.pi (α := κ) univ t).Finite
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
ι : Type u_3
inst : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
val : Fintype ι
⊢ (Set.pi (α := κ) univ t).Finite
have intro : ∀ (t : (i : ι) → Finset (κ i)),
  Set.Finite (α := (i : ι) → κ i) (Set.pi (α := κ) univ fun (i : ι) ↦ (↑(t i) : Set (κ i)))
Tactic: lift t to ∀ d, Finset (κ d) using ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
ι : Type u_3
inst : Finite ι
κ : ι → Type u_4
val : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ Set.Finite (α := (i : ι) → κ i) (pi (α := κ) univ fun (i : ι) ↦ (↑(t i) : Set (κ i)))
have intro : (↑(Fintype.piFinset (δ := κ) t) : Set ((a : ι) → κ a)).Finite
Tactic: rw [← Fintype.coe_piFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
ι : Type u_3
inst : Finite ι
κ : ι → Type u_4
val : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ Set.Finite (α := (i : ι) → κ i) (Set.pi (α := κ) univ fun (i : ι) ↦ (↑(t i) : Set (κ i)))
have intro : (↑(Fintype.piFinset (δ := κ) t) : Set ((a : ι) → κ a)).Finite
Tactic: classical
    rw [← Fintype.coe_piFinset]
    apply Finset.finite_toSet
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
⊢ iUnion (ι := Fin (n + 1)) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) s f) = s ∪ ⋃ (i : Fin n), f i
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (iUnion (ι := Fin (n + 1)) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) s f)) x ↔
    x ∈ s ∪ ⋃ (i : Fin n), f i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
⊢ iUnion (ι := Fin (n + 1)) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) f s) = (⋃ (i : Fin n), f i) ∪ s
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (iUnion (ι := Fin (n + 1)) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) f s)) x ↔
    x ∈ (⋃ (i : Fin n), f i) ∪ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin (n + 1) → Set α
⊢ ⋃ (i : Fin (n + 1)), f i = f 0 ∪ iUnion (f ∘ Fin.succ)
have cons : ∀ (x₀ : Set α) (x : (i : Fin n) → Set α),
  Eq.{u_1 + 1} (α := Set α) (⋃ (i : Fin (n + 1)), Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) x₀ x i)
    (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) x₀ x 0 ∪
      iUnion (ι := Fin n) (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Set α) x₀ x ∘ Fin.succ))
Tactic: cases f using Fin.consCases
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Fintype.Pi (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin (n + 1) → Set α
⊢ ⋃ (i : Fin (n + 1)), f i = iUnion (f ∘ Fin.castSucc) ∪ f (Fin.last n)
have snoc : ∀ (xs : (i : Fin n) → Set α) (x : Set α),
  Eq.{u_1 + 1} (α := Set α) (⋃ (i : Fin (n + 1)), Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) xs x i)
    (iUnion (ι := Fin n) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) xs x ∘ Fin.castSucc) ∪
      Fin.snoc (α := fun (a : Fin (n + 1)) ↦ Set α) xs x (Fin.last n))
Tactic: cases f using Fin.snocCases
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Fintype.Pigeonhole (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Infinite α
inst_1 : Finite β
f : α → β
⊢ ∃ (y : β), Infinite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)
have by_contra! : ∀ (hf : ∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)), False
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.Data.Fintype.Pigeonhole (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Infinite α
inst_1 : Finite β
f : α → β
hf : ∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)
⊢ False
have intro : ∀ (val : Fintype β), False
Tactic: cases nonempty_fintype β
-- Lean 4 proof step from Mathlib.Data.Fintype.Pigeonhole (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Infinite α
inst_1 : Finite β
f : α → β
⊢ ∃ (y : β), Infinite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)
have by_contra! : (¬∃ (y : β), Infinite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)) → False
Tactic: classical
    by_contra! hf
    cases nonempty_fintype β
    let key : Fintype α :=
      { elems := univ.biUnion fun y : β => (f ⁻¹' {y}).toFinset
        complete := by simp }
    exact key.false
-- Lean 4 proof step from Mathlib.Data.Fintype.Pigeonhole (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Infinite α
inst_1 : Finite β
f : α → β
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : (¬∃ (y : β), Infinite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)) → False
⊢ ∃ (y : β), Infinite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)
have by_contra!₄ : (∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)) → False
Tactic: classical
    by_contra! hf
    cases nonempty_fintype β
    let key : Fintype α :=
      { elems := univ.biUnion fun y : β => (f ⁻¹' {y}).toFinset
        complete := by simp }
    exact key.false
-- Lean 4 proof step from Mathlib.Data.Fintype.Pigeonhole (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Infinite α
inst_1 : Finite β
f : α → β
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : (¬∃ (y : β), Infinite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)) → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ :
  ∀ (hf : ∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)), False
⊢ ∃ (y : β), Infinite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)
have intro : ∀ (hf : ∀ (y : β), Finite.{u_1 + 1} (↑(f ⁻¹' {y}) : Type u_1)) (val : Fintype β), False
Tactic: classical
    by_contra! hf
    cases nonempty_fintype β
    let key : Fintype α :=
      { elems := univ.biUnion fun y : β => (f ⁻¹' {y}).toFinset
        complete := by simp }
    exact key.false
-- Lean 4 proof step from Mathlib.Data.Fintype.Powerset (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Finset α
⊢ {t : Finset α | t ⊆ s} = s.powerset
have h : ∀ (a : Finset α), Membership.mem (γ := Finset (Finset α)) {t : Finset α | t ⊆ s} a ↔ a ∈ s.powerset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Powerset (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
⊢ s.powerset = univ ↔ s = univ
have rw : s.powerset = powerset univ ↔ s = univ
Tactic: rw [← Finset.powerset_univ, powerset_inj]
-- Lean 4 proof step from Mathlib.Data.Fintype.Powerset (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
rw : s.powerset = powerset univ ↔ s = univ
⊢ s.powerset = univ ↔ s = univ
have rw₁ : s = univ ↔ s = univ
Tactic: rw [← Finset.powerset_univ, powerset_inj]
-- Lean 4 proof step from Mathlib.Data.Fintype.Powerset (goal)
Goal:
α : Type u_1
inst : Fintype α
k : ℕ
⊢ Eq.{u_1 + 1} (α := Finset (Finset α)) {s : Finset α | #s = k} (powersetCard k univ)
have h : ∀ (a : Finset α),
  Membership.mem (γ := Finset (Finset α)) {s : Finset α | #s = k} a ↔
    Membership.mem (γ := Finset (Finset α)) (powersetCard k univ) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Powerset (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
⊢ Membership.mem (γ := Finset (Set α))
    (map (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2) coeEmb)
      Finset.univ)
    s
have refine : {x : α | Membership.mem (γ := Finset α) Finset.univ x ∧ x ∈ s} = s
Tactic: refine mem_map.2 ⟨({a | a ∈ s} : Finset _), Finset.mem_univ _, (coe_filter _ _).trans ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Powerset (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
⊢ Membership.mem (γ := Finset (Set α))
    (map (RelEmbedding.toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s := fun (x1 x2 : Set α) ↦ x1 ≤ x2) coeEmb)
      Finset.univ)
    s
have refine : {x : α | Membership.mem (γ := Finset α) Finset.univ x ∧ x ∈ s} = s
Tactic: classical
    refine mem_map.2 ⟨({a | a ∈ s} : Finset _), Finset.mem_univ _, (coe_filter _ _).trans ?_⟩
    simp
-- Lean 4 proof step from Mathlib.Data.Fintype.Powerset (goal)
Goal:
α : Type u_1
inst : Finite α
⊢ Finite.{u_1 + 1} (Set α)
have intro : ∀ (val : Fintype α), Finite.{u_1 + 1} (Set α)
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Fintype (↑s : Type u_1)
inst_1 : Fintype (↑t : Type u_2)
inst_2 : Fintype (↑(s ×ˢ t) : Type (max u_1 u_2))
⊢ (s ×ˢ t).toFinset = s.toFinset ×ˢ t.toFinset
have h : ∀ (a : α × β), a ∈ (s ×ˢ t).toFinset ↔ a ∈ s.toFinset ×ˢ t.toFinset
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
⊢ Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
have H : ∀ (H : Infinite (α × β)), Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
Tactic: refine
    ⟨fun H => ?_, fun H =>
      H.elim (and_imp.2 <| @Prod.infinite_of_left α β) (and_imp.2 <| @Prod.infinite_of_right α β)⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
have rw : Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
Tactic: rw [and_comm]
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
have rcases : ∀ (a : α) (b : β), Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
Tactic: rcases Infinite.nonempty (α × β) with ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
a : α
b : β
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
have contrapose! : ∀ (H : (∀ (_ : Nonempty β), Finite α) ∧ ∀ (_ : Nonempty α), Finite β), Finite (α × β)
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
H : (∀ (_ : Nonempty β), Finite α) ∧ ∀ (_ : Nonempty α), Finite β
⊢ Finite (α × β)
have this : Finite α
Tactic: haveI := H.1 ⟨b⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
H : (∀ (_ : Nonempty β), Finite α) ∧ ∀ (_ : Nonempty α), Finite β
this : Finite α
⊢ Finite (α × β)
have this₁ : Finite β
Tactic: haveI := H.2 ⟨a⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst : ∀ (i : ι), Nontrivial.{u_5} (π i)
inst_1 : Infinite ι
⊢ Infinite ((i : ι) → π i)
have choose : ∀ (m n : (i : ι) → π i) (hm : ∀ (i : ι), m i ≠ n i), Infinite ((i : ι) → π i)
Tactic: choose m n hm using fun i => exists_pair_ne (π i)
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst : ∀ (i : ι), Nontrivial.{u_5} (π i)
inst_1 : Infinite ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
⊢ Infinite ((i : ι) → π i)
have refine : ∀ (x y : ι)
  (h :
    Eq (α := (i : ι) → π i) ((fun (i : ι) ↦ update (β := π) m i (n i)) x) ((fun (i : ι) ↦ update (β := π) m i (n i)) y))
  (hne : ¬x = y), False
Tactic: refine Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => ?_
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst : ∀ (i : ι), Nontrivial.{u_5} (π i)
inst_1 : Infinite ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
x y : ι
h : Eq (α := (i : ι) → π i) ((fun (i : ι) ↦ update (β := π) m i (n i)) x) ((fun (i : ι) ↦ update (β := π) m i (n i)) y)
hne : ¬x = y
⊢ False
have h₁ : n x = m x ∧ ∀ (x_1 : ι), x_1 ≠ x → m x_1 = update (β := π) m y (n y) x_1
Tactic: simp_rw [update_eq_iff, update_of_ne hne] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst : ∀ (i : ι), Nontrivial.{u_5} (π i)
inst_1 : Infinite ι
⊢ Infinite ((i : ι) → π i)
have choose : ∀ (m n : (i : ι) → π i) (hm : ∀ (i : ι), m i ≠ n i), Infinite ((i : ι) → π i)
Tactic: classical
  choose m n hm using fun i => exists_pair_ne (π i)
  refine Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => ?_
  simp_rw [update_eq_iff, update_of_ne hne] at h
  exact (hm x h.1.symm).elim
-- Lean 4 proof step from Mathlib.Data.Fintype.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst : ∀ (i : ι), Nontrivial.{u_5} (π i)
inst_1 : Infinite ι
choose : ∀ (m n : (i : ι) → π i) (hm : ∀ (i : ι), m i ≠ n i), Infinite ((i : ι) → π i)
⊢ Infinite ((i : ι) → π i)
have choose₁ : ∀ (m n : (i : ι) → π i) (hm : ∀ (i : ι), m i ≠ n i) (x y : ι)
  (h :
    Eq (α := (i : ι) → π i) ((fun (i : ι) ↦ update (β := π) m i (n i)) x) ((fun (i : ι) ↦ update (β := π) m i (n i)) y))
  (hne : ¬x = y), False
Tactic: classical
  choose m n hm using fun i => exists_pair_ne (π i)
  refine Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => ?_
  simp_rw [update_eq_iff, update_of_ne hne] at h
  exact (hm x h.1.symm).elim