awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ a ∈ s, Injective (f a)
hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑s : Set α)) id
empty :
  ∀ (hf : ∀ (a : α), Membership.mem (γ := Finset α) ∅ a → Injective (f a))
    (hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑∅ : Set α)) id),
    #t ∣ #(image₂ f ∅ t)
insert insert₁ :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∀
        (ih :
          ∀ (hf : ∀ a ∈ s, Injective (f a))
            (hs : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑s : Set α)) id),
            #t ∣ #(image₂ f s t))
        (hf : ∀ a_2 ∈ Insert.insert a s, Injective (f a_2))
        (hs :
          PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(Insert.insert a s) : Set α))
            id),
        #t ∣ #(image₂ f (Insert.insert a s) t)
insert₂ :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∀ (hf : ∀ a_2 ∈ Insert.insert a s, Injective (f a_2))
        (hs :
          PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(Insert.insert a s) : Set α))
            id)
        (ih : #t ∣ #(image₂ f s t)), #t ∣ #(image₂ f (Insert.insert a s) t)
insert₃ :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∀ (hf : ∀ a_2 ∈ Insert.insert a s, Injective (f a_2))
        (hs :
          PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(Insert.insert a s) : Set α))
            id)
        (ih : #t ∣ #(image₂ f s t)), #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)
⊢ #t ∣ #(image₂ f s t)
have pos : ∀ (a : α) (s : Finset α),
  a ∉ s →
    ∀ (hf : ∀ a_2 ∈ Insert.insert a s, Injective (f a_2))
      (hs :
        PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (a : α) ↦ image (f a) t) '' (↑(Insert.insert a s) : Set α))
          id)
      (ih : #t ∣ #(image₂ f s t)) (h : Disjoint (image (f a) t) (image₂ f s t)),
      #t ∣ #(image (fun (b : β) ↦ f a b) t ∪ image₂ f s t)
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s _ ih => ?_
  specialize ih (forall_of_forall_insert hf)
    (hs.subset <| Set.image_mono <| coe_subset.2 <| subset_insert _ _)
  rw [image₂_insert_left]
  by_cases h : Disjoint (image (f a) t) (image₂ f s t)
  · rw [card_union_of_disjoint h]
    exact Nat.dvd_add (card_image_of_injective _ <| hf _ <| mem_insert_self _ _).symm.dvd ih
  simp_rw [← biUnion_image_left, disjoint_biUnion_right, not_forall] at h
  obtain ⟨b, hb, h⟩ := h
  rwa [union_eq_right.2]
  exact (hs.eq (Set.mem_image_of_mem _ <| mem_insert_self _ _)
      (Set.mem_image_of_mem _ <| mem_insert_of_mem hb) h).trans_subset
    (image_subset_image₂_right hb)
Cleared hypotheses: hf, hs
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ b ∈ t, Injective.{u_1 + 1, u_5 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_5, u_5} (α := Finset γ) ((fun (b : β) ↦ image (fun (a : α) ↦ f a b) s) '' (↑t : Set β)) id
⊢ #s ∣ #(image₂ f s t)
have rw : #s ∣ card.{u_5} (α := γ) (image₂ (fun (b : β) (a : α) ↦ f a b) t s)
Tactic: rw [← image₂_swap]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (hypothesis)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : (↑u : Set γ) ⊆ image2 f s t
⊢ ∃ (s' : Finset α) (t' : Finset β), (↑s' : Set α) ⊆ s ∧ (↑t' : Set β) ⊆ t ∧ u ⊆ image₂ f s' t'
have hu₁ : ∃ (s' : Finset (α × β)), (↑s' : Set (α × β)) ⊆ s ×ˢ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) s' = u
Tactic: rw [← Set.image_prod, subset_set_image_iff] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : ∃ (s' : Finset (α × β)), (↑s' : Set (α × β)) ⊆ s ×ˢ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) s' = u
⊢ ∃ (s' : Finset α) (t' : Finset β), (↑s' : Set α) ⊆ s ∧ (↑t' : Set β) ⊆ t ∧ u ⊆ image₂ f s' t'
have rcases : ∀ (u : Finset (α × β)) (hu : (↑u : Set (α × β)) ⊆ s ×ˢ t),
  ∃ (s' : Finset α) (t' : Finset β),
    (↑s' : Set α) ⊆ s ∧ (↑t' : Set β) ⊆ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f s' t'
Tactic: rcases hu with ⟨u, hu, rfl⟩
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : (↑u : Set (α × β)) ⊆ s ×ˢ t
⊢ ∃ (s' : Finset α) (t' : Finset β),
    (↑s' : Set α) ⊆ s ∧ (↑t' : Set β) ⊆ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f s' t'
have h : (↑(image Prod.fst u) : Set α) ⊆ s ∧
  (↑(image Prod.snd u) : Set β) ⊆ t ∧
    image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f (image Prod.fst u) (image Prod.snd u)
Tactic: use u.image Prod.fst, u.image Prod.snd
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : (↑u : Set (α × β)) ⊆ s ×ˢ t
⊢ (↑(image Prod.fst u) : Set α) ⊆ s ∧
    (↑(image Prod.snd u) : Set β) ⊆ t ∧
      image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f (image Prod.fst u) (image Prod.snd u)
have h : (↑u : Set (α × β)) ⊆ Prod.fst ⁻¹' s ∧
  (↑u : Set (α × β)) ⊆ Prod.snd ⁻¹' t ∧
    ∀ x ∈ u, Membership.mem (γ := Finset γ) (image₂ (fun (a b : α × β) ↦ f a.1 b.2) u u) (f x.1 x.2)
Tactic: simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
    image_subset_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : (↑u : Set (α × β)) ⊆ s ×ˢ t
⊢ ∃ (s' : Finset α) (t' : Finset β),
    (↑s' : Set α) ⊆ s ∧ (↑t' : Set β) ⊆ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f s' t'
have w : Finset α
Tactic: classical
  use u.image Prod.fst, u.image Prod.snd
  simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
    image_subset_iff]
  exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : (↑u : Set (α × β)) ⊆ s ×ˢ t
w : Finset α
⊢ ∃ (s' : Finset α) (t' : Finset β),
    (↑s' : Set α) ⊆ s ∧ (↑t' : Set β) ⊆ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f s' t'
have w₁ : Finset β
Tactic: classical
  use u.image Prod.fst, u.image Prod.snd
  simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
    image_subset_iff]
  exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : (↑u : Set (α × β)) ⊆ s ×ˢ t
w : Finset α
w₁ : Finset β
⊢ ∃ (s' : Finset α) (t' : Finset β),
    (↑s' : Set α) ⊆ s ∧ (↑t' : Set β) ⊆ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f s' t'
have h : (↑(image Prod.fst u) : Set α) ⊆ s ∧
  (↑(image Prod.snd u) : Set β) ⊆ t ∧
    image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f (image Prod.fst u) (image Prod.snd u)
Tactic: classical
  use u.image Prod.fst, u.image Prod.snd
  simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
    image_subset_iff]
  exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : (↑u : Set (α × β)) ⊆ s ×ˢ t
w : Finset α
w₁ : Finset β
h h₁ :
  (↑(image Prod.fst u) : Set α) ⊆ s ∧
    (↑(image Prod.snd u) : Set β) ⊆ t ∧
      image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f (image Prod.fst u) (image Prod.snd u)
⊢ ∃ (s' : Finset α) (t' : Finset β),
    (↑s' : Set α) ⊆ s ∧ (↑t' : Set β) ⊆ t ∧ image (fun (x : α × β) ↦ f x.1 x.2) u ⊆ image₂ f s' t'
have h₂ : (↑u : Set (α × β)) ⊆ Prod.fst ⁻¹' s ∧
  (↑u : Set (α × β)) ⊆ Prod.snd ⁻¹' t ∧
    ∀ x ∈ u, Membership.mem (γ := Finset γ) (image₂ (fun (a b : α × β) ↦ f a.1 b.2) u u) (f x.1 x.2)
Tactic: classical
  use u.image Prod.fst, u.image Prod.snd
  simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
    image_subset_iff]
  exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
⊢ (↑(image₂ f (s ∩ s') (t ∪ t')) : Set γ) ⊆ (↑(image₂ f s t ∪ image₂ f s' t') : Set γ)
have push_cast : image2 f ((↑s : Set α) ∩ (↑s' : Set α)) ((↑t : Set β) ∪ (↑t' : Set β)) ⊆
  image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s' : Set α) (↑t' : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
inst_1 : DecidableEq α
inst_2 : DecidableEq β
⊢ (↑(image₂ f (s ∪ s') (t ∩ t')) : Set γ) ⊆ (↑(image₂ f s t ∪ image₂ f s' t') : Set γ)
have push_cast : image2 f ((↑s : Set α) ∪ (↑s' : Set α)) ((↑t : Set β) ∩ (↑t' : Set β)) ⊆
  image2 f (↑s : Set α) (↑t : Set β) ∪ image2 f (↑s' : Set α) (↑t' : Set β)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ (↑(image₂ f (s ∩ t) (s ∪ t)) : Set β) ⊆ (↑(image₂ f s t) : Set β)
have push_cast : image2 f ((↑s : Set α) ∩ (↑t : Set α)) ((↑s : Set α) ∪ (↑t : Set α)) ⊆ image2 f (↑s : Set α) (↑t : Set α)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ (↑(image₂ f (s ∪ t) (s ∩ t)) : Set β) ⊆ (↑(image₂ f s t) : Set β)
have push_cast : image2 f ((↑s : Set α) ∪ (↑t : Set α)) ((↑s : Set α) ∩ (↑t : Set α)) ⊆ image2 f (↑s : Set α) (↑t : Set α)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
g : γ → δ
a : δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).sup' h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
have rw : (∀ b ∈ image₂ f s t, g b ≤ a) ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
Tactic: rw [sup'_le_iff, forall_mem_image₂]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
g : γ → δ
a : δ
h : (image₂ f s t).Nonempty
rw : (∀ b ∈ image₂ f s t, g b ≤ a) ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
⊢ (image₂ f s t).sup' h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
have rw₁ : (∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a) ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
Tactic: rw [sup'_le_iff, forall_mem_image₂]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).sup' h g = s.sup' ⋯ fun (x : α) ↦ t.sup' ⋯ fun (x_1 : β) ↦ g (f x x_1)
have simp : Eq.{u_7 + 1} (α := δ) (s.sup' sorry fun (i : α) ↦ t.sup' sorry fun (i' : β) ↦ (g ∘ uncurry f) (i, i'))
  (s.sup' sorry fun (x : α) ↦ t.sup' sorry fun (x_1 : β) ↦ g (f x x_1))
Tactic: simp only [image₂, sup'_image, sup'_product_left]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).sup' h g = t.sup' ⋯ fun (y : β) ↦ s.sup' ⋯ fun (x : α) ↦ g (f x y)
have simp : Eq.{u_7 + 1} (α := δ) (t.sup' sorry fun (i' : β) ↦ s.sup' sorry fun (i : α) ↦ (g ∘ uncurry f) (i, i'))
  (t.sup' sorry fun (y : β) ↦ s.sup' sorry fun (x : α) ↦ g (f x y))
Tactic: simp only [image₂, sup'_image, sup'_product_right]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
inst_2 : OrderBot δ
g : γ → δ
a : δ
⊢ (image₂ f s t).sup g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
have rw : (∀ b ∈ image₂ f s t, g b ≤ a) ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
Tactic: rw [Finset.sup_le_iff, forall_mem_image₂]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
inst_2 : OrderBot δ
g : γ → δ
a : δ
rw : (∀ b ∈ image₂ f s t, g b ≤ a) ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
⊢ (image₂ f s t).sup g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
have rw₁ : (∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a) ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
Tactic: rw [Finset.sup_le_iff, forall_mem_image₂]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
inst_2 : OrderBot δ
g : γ → δ
⊢ (image₂ f s t).sup g = s.sup fun (x : α) ↦ t.sup fun (x_1 : β) ↦ g (f x x_1)
have simp : Eq.{u_7 + 1} (α := δ) (s.sup fun (i : α) ↦ t.sup fun (i' : β) ↦ (g ∘ uncurry f) (i, i'))
  (s.sup fun (x : α) ↦ t.sup fun (x_1 : β) ↦ g (f x x_1))
Tactic: simp only [image₂, sup_image, sup_product_left]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeSup δ
inst_2 : OrderBot δ
g : γ → δ
⊢ (image₂ f s t).sup g = t.sup fun (y : β) ↦ s.sup fun (x : α) ↦ g (f x y)
have simp : Eq.{u_7 + 1} (α := δ) (t.sup fun (i' : β) ↦ s.sup fun (i : α) ↦ (g ∘ uncurry f) (i, i'))
  (t.sup fun (y : β) ↦ s.sup fun (x : α) ↦ g (f x y))
Tactic: simp only [image₂, sup_image, sup_product_right]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeInf δ
g : γ → δ
a : δ
h : (image₂ f s t).Nonempty
⊢ a ≤ (image₂ f s t).inf' h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
have rw : (∀ b ∈ image₂ f s t, a ≤ g b) ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
Tactic: rw [le_inf'_iff, forall_mem_image₂]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_1 : SemilatticeInf δ
g : γ → δ
a : δ
h : (image₂ f s t).Nonempty
rw : (∀ b ∈ image₂ f s t, a ≤ g b) ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
⊢ a ≤ (image₂ f s t).inf' h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
have rw₁ : (∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)) ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
Tactic: rw [le_inf'_iff, forall_mem_image₂]
-- Lean 4 proof step from Mathlib.Data.Finset.NAry (goal)
Goal:
ι : Type u_14
α : ι → Type u_15
β : ι → Type u_16
γ : ι → Type u_17
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (γ i)
f : (i : ι) → α i → β i → γ i
s : (i : ι) → Finset (α i)
t : (i : ι) → Finset (β i)
⊢ Eq (α := Finset ((a : ι) → γ a)) (piFinset (δ := γ) fun (i : ι) ↦ image₂ (f i) (s i) (t i))
    (image₂ (fun (a : (a : ι) → α a) (b : (a : ι) → β a) (i : ι) ↦ f i (a i) (b i)) (piFinset (δ := α) s)
      (piFinset (δ := β) t))
have h : ∀ (a : (a : ι) → γ a),
  Membership.mem (γ := Finset ((a : ι) → γ a)) (piFinset (δ := γ) fun (i : ι) ↦ image₂ (f i) (s i) (t i)) a ↔
    Membership.mem (γ := Finset ((a : ι) → γ a))
      (image₂ (fun (a : (a : ι) → α a) (b : (a : ι) → β a) (i : ι) ↦ f i (a i) (b i)) (piFinset (δ := α) s)
        (piFinset (δ := β) t))
      a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.NatDivisors (goal)
Goal:
m n : ℕ
⊢ (m * n).divisors = m.divisors * n.divisors
have h : ∀ (k : ℕ), k ∈ (m * n).divisors ↔ k ∈ m.divisors * n.divisors
Tactic: ext k
-- Lean 4 proof step from Mathlib.Data.Finset.NatDivisors (goal)
Goal:
m n k : ℕ
⊢ k ∈ (m * n).divisors ↔ k ∈ m.divisors * n.divisors
have h : (∃ (x : ℕ) (x_1 : ℕ), (x ∣ m ∧ x_1 ∣ n ∧ x * x_1 = k) ∧ m ≠ 0 ∧ n ≠ 0) ↔
  ∃ (y : ℕ) (x : ℕ), (y ∣ m ∧ m ≠ 0) ∧ (x ∣ n ∧ n ≠ 0) ∧ y * x = k
Tactic: simp_rw [mem_mul, mem_divisors, Nat.dvd_mul, mul_ne_zero_iff, ← exists_and_left,
    ← exists_and_right]
-- Lean 4 proof step from Mathlib.Data.Finset.NatDivisors (hypothesis)
Goal:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ : ℕ
h₁ : (dm₁, dn₁) ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ))
dm₂ dn₂ : ℕ
h₂ : (dm₂, dn₂) ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ))
hd : Eq (α := ℕ) ((fun (p : ℕ × ℕ) ↦ p.1 * p.2) (dm₁, dn₁)) ((fun (p : ℕ × ℕ) ↦ p.1 * p.2) (dm₂, dn₂))
⊢ (dm₁, dn₁) = (dm₂, dn₂)
have h₃ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
Tactic: simp only [Finset.mem_coe, Finset.mem_product, mem_divisors] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Finset.NatDivisors (hypothesis)
Goal:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ : ℕ
h₁ : (dm₁, dn₁) ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ))
dm₂ dn₂ : ℕ
h₂ : (dm₂, dn₂) ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ))
hd : Eq (α := ℕ) ((fun (p : ℕ × ℕ) ↦ p.1 * p.2) (dm₁, dn₁)) ((fun (p : ℕ × ℕ) ↦ p.1 * p.2) (dm₂, dn₂))
h₃ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
⊢ (dm₁, dn₁) = (dm₂, dn₂)
have h₄ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
Tactic: simp only [Finset.mem_coe, Finset.mem_product, mem_divisors] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Finset.NatDivisors (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ dm₂ dn₂ : ℕ
hd : dm₁ * dn₁ = dm₂ * dn₂
h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
this : dm₁ = dm₂
⊢ (dm₁, dn₁).2 = (dm₂, dn₂).2
have rwa : ∀ (hd : dm₂ * dn₁ = dm₂ * dn₂) (h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0) (h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0)
  (this : dm₁ = dm₂), (dm₁, dn₁).2 = (dm₂, dn₂).2
Tactic: rwa [this, Nat.mul_right_inj (by simp [·] at h₂)] at hd
Cleared hypotheses: hd, h₁, h₂, this
-- Lean 4 proof step from Mathlib.Data.Finset.NatDivisors (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ dm₂ dn₂ : ℕ
hd : dm₁ * dn₁ = dm₂ * dn₂
h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
this : dm₁ = dm₂
rwa :
  ∀ (hd : dm₂ * dn₁ = dm₂ * dn₂) (h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0) (h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0)
    (this : dm₁ = dm₂), (dm₁, dn₁).2 = (dm₂, dn₂).2
⊢ (dm₁, dn₁).2 = (dm₂, dn₂).2
have rwa₁ : ∀ (hd : dn₁ = dn₂) (h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0) (h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0)
  (this : dm₁ = dm₂), (dm₁, dn₁).2 = (dm₂, dn₂).2
Tactic: rwa [this, Nat.mul_right_inj (by simp [·] at h₂)] at hd
Cleared hypotheses: hd, h₁, h₂, this
-- Lean 4 proof step from Mathlib.Data.Finset.NatDivisors (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ dm₂ dn₂ : ℕ
hd : dm₁ * dn₁ = dm₂ * dn₂
h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
⊢ (dm₁, dn₁) = (dm₂, dn₂)
have suffices : dm₁ = dm₂
Tactic: suffices dm₁ = dm₂ from Prod.ext this <| by
    rwa [this, Nat.mul_right_inj (by simp [·] at h₂)] at hd
-- Lean 4 proof step from Mathlib.Data.Finset.NatDivisors (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
⊢ (m * n).divisors =
    image (fun (p : ℕ × ℕ) ↦ p.1 * p.2)
      (image (Subtype.val (p := fun (x : ℕ × ℕ) ↦ x ∈ m.divisors ×ˢ n.divisors)) (m.divisors ×ˢ n.divisors).attach)
have rw : (m * n).divisors = image (fun (p : ℕ × ℕ) ↦ p.1 * p.2) (m.divisors ×ˢ n.divisors)
Tactic: rw [Finset.attach_image_val, ← Finset.mul_def, Nat.divisors_mul]
-- Lean 4 proof step from Mathlib.Data.Finset.NatDivisors (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
rw : (m * n).divisors = image (fun (p : ℕ × ℕ) ↦ p.1 * p.2) (m.divisors ×ˢ n.divisors)
⊢ (m * n).divisors =
    image (fun (p : ℕ × ℕ) ↦ p.1 * p.2)
      (image (Subtype.val (p := fun (x : ℕ × ℕ) ↦ x ∈ m.divisors ×ˢ n.divisors)) (m.divisors ×ˢ n.divisors).attach)
have rw₁ : (m * n).divisors = m.divisors * n.divisors
Tactic: rw [Finset.attach_image_val, ← Finset.mul_def, Nat.divisors_mul]
-- Lean 4 proof step from Mathlib.Data.Finset.NatDivisors (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
rw : (m * n).divisors = image (fun (p : ℕ × ℕ) ↦ p.1 * p.2) (m.divisors ×ˢ n.divisors)
rw₁ : (m * n).divisors = m.divisors * n.divisors
⊢ (m * n).divisors =
    image (fun (p : ℕ × ℕ) ↦ p.1 * p.2)
      (image (Subtype.val (p := fun (x : ℕ × ℕ) ↦ x ∈ m.divisors ×ˢ n.divisors)) (m.divisors ×ˢ n.divisors).attach)
have rw₂ : m.divisors * n.divisors = m.divisors * n.divisors
Tactic: rw [Finset.attach_image_val, ← Finset.mul_def, Nat.divisors_mul]
-- Lean 4 proof step from Mathlib.Data.Finset.NatDivisors (goal)
Goal:
m n : ℕ
hmn : m.Coprime n
⊢ Eq (α := Finset ℕ)
    (image (fun (p : ℕ × ℕ) ↦ p.1 * p.2)
      (image (Subtype.val (p := fun (x : ℕ × ℕ) ↦ x ∈ m.divisors ×ˢ n.divisors)) (m.divisors ×ˢ n.divisors).attach))
    (map
      {
        toFun := fun (p : { x : ℕ × ℕ // x ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ)) }) ↦
          (↑p : ℕ × ℕ).1 * (↑p : ℕ × ℕ).2,
        inj' := ⋯ }
      (m.divisors ×ˢ n.divisors).attach)
have rw : Eq (α := Finset ℕ)
  (image ((fun (p : ℕ × ℕ) ↦ p.1 * p.2) ∘ Subtype.val (p := fun (x : ℕ × ℕ) ↦ x ∈ m.divisors ×ˢ n.divisors))
    (m.divisors ×ˢ n.divisors).attach)
  (image
    (⇑{
          toFun := fun (p : { x : ℕ × ℕ // x ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ)) }) ↦
            (↑p : ℕ × ℕ).1 * (↑p : ℕ × ℕ).2,
          inj' := sorry } :
      (a : { x : ℕ × ℕ // x ∈ (↑(m.divisors ×ˢ n.divisors) : Set (ℕ × ℕ)) }) → ℕ)
    (m.divisors ×ˢ n.divisors).attach)
Tactic: rw [Finset.map_eq_image, Finset.image_image]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : Set.Pairwise {x : α | x ∈ (↑l : Multiset α)} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f (↑l : Multiset α) comm b = List.foldr f b l
have simp : List.foldr (fun (x : { x : α // x ∈ (↑l : Multiset α) }) ↦ f (↑x : α)) b
    (List.pmap (P := fun (x : α) ↦ x ∈ l) (Subtype.mk (p := fun (x : α) ↦ x ∈ l)) l sorry) =
  List.foldr f b l
Tactic: simp only [noncommFoldr, coe_foldr, coe_attach, List.attach, List.attachWith, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : Set.Pairwise {x : α | x ∈ (↑l : Multiset α)} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr (fun (x : { x : α // x ∈ (↑l : Multiset α) }) ↦ f (↑x : α)) b
      (List.pmap (P := fun (x : α) ↦ x ∈ l) (Subtype.mk (p := fun (x : α) ↦ x ∈ l)) l ⋯) =
    List.foldr f b l
have rw : List.foldr f b
    (List.map (Subtype.val (p := fun (x : α) ↦ x ∈ (↑l : Multiset α)))
      (List.pmap (P := fun (x : α) ↦ x ∈ l) (Subtype.mk (p := fun (x : α) ↦ x ∈ l)) l sorry)) =
  List.foldr f b l
Tactic: rw [← List.foldr_map]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
f : α → β → β
s : Multiset α
a : α
h : Set.Pairwise {x : α | x ∈ a ::ₘ s} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)
h' : Set.Pairwise {x : α | x ∈ s} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f (a ::ₘ s) h b = f a (noncommFoldr f s h' b)
have h₁ : ∀ (a_1 : List α) (h : Set.Pairwise {x : α | x ∈ a ::ₘ ⟦a_1⟧} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b))
  (h' : Set.Pairwise {x : α | x ∈ ⟦a_1⟧} fun (x y : α) ↦ ∀ (b : β), f x (f y b) = f y (f x b)),
  noncommFoldr f (a ::ₘ ⟦a_1⟧) h b = f a (noncommFoldr f ⟦a_1⟧ h' b)
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: s, h, h'