awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (hypothesis)
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
⊢ ψ x ≤ ψ y
have this : φ (ψ y) ≤ φ (ψ x)
Tactic: have := hφ (ψts ys) (ψts xs) ψyx
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (hypothesis)
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : φ (ψ y) ≤ φ (ψ x)
⊢ ψ x ≤ ψ y
have this₁ : y ≤ x
Tactic: rw [φψs.eq ys, φψs.eq xs] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
ψyx : ψ y ≤ ψ x
this : y ≤ x
⊢ ψ x ≤ ψ y
have inr : ∀ (ys : x ∈ s) (l : x ≤ x) (ψyx : ψ x ≤ ψ x) (this : x ≤ x), ψ x ≤ ψ x
Tactic: induction le_antisymm l this
Cleared hypotheses: ys, l, ψyx, this
-- Lean 4 proof step from Mathlib.Data.Set.MulAntidiagonal (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s t : Set α
a : α
x y : (↑(s.mulAntidiagonal t a) : Type u_1)
h : (↑x : α × α).1 = (↑y : α × α).1
⊢ a = (↑y : α × α).1 * (↑x : α × α).2
have rw : a = (↑x : α × α).1 * (↑x : α × α).2
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Set.MulAntidiagonal (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : IsCancelMul α
s t : Set α
a : α
x y : (↑(s.mulAntidiagonal t a) : Type u_1)
h : (↑x : α × α).2 = (↑y : α × α).2
⊢ a = (↑x : α × α).1 * (↑y : α × α).2
have rw : a = (↑x : α × α).1 * (↑x : α × α).2
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Set.MulAntidiagonal (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
⊢ (s.mulAntidiagonal t a).Finite
have by_contra! : ∀ (h : (s.mulAntidiagonal t a).Infinite), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Data.Set.MulAntidiagonal (hypothesis)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
⊢ False
have h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
Tactic: have h1 : (mulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o (· ≤ ·)) :=
    fun f ↦ hs fun n ↦ ⟨_, (mem_mulAntidiagonal.1 (f n).2).1⟩
-- Lean 4 proof step from Mathlib.Data.Set.MulAntidiagonal (hypothesis)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
⊢ False
have h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
Tactic: have h2 : (mulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o (· ≤ ·)) :=
    fun f ↦ ht fun n ↦ ⟨_, (mem_mulAntidiagonal.1 (f n).2).2.1⟩
-- Lean 4 proof step from Mathlib.Data.Set.MulAntidiagonal (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
⊢ False
have obtain : ∀ (g : ℕ ↪o ℕ)
  (hg :
    ∀ (m n : ℕ),
      m ≤ n →
        Order.Preimage (α := α × α) Prod.fst (fun (x1 x2 : α) ↦ x1 ≤ x2)
          (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
                ((g : (a : ℕ) → ℕ) m : ℕ)) :
            α × α)
          (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
                ((g : (a : ℕ) → ℕ) n : ℕ)) :
            α × α)),
  False
Tactic: obtain ⟨g, hg⟩ :=
    h1.exists_monotone_subseq fun n ↦ (h.natEmbedding _ n).2
-- Lean 4 proof step from Mathlib.Data.Set.MulAntidiagonal (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := α × α) Prod.fst (fun (x1 x2 : α) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          α × α)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          α × α)
⊢ False
have obtain : ∀ (m n : ℕ) (mn : m < n)
  (h2' :
    Subrel (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α × α) ↦ x ∈ s.mulAntidiagonal t a)
      ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
        ((g : (a : ℕ) → ℕ) m : ℕ))
      ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
        ((g : (a : ℕ) → ℕ) n : ℕ))),
  False
Tactic: obtain ⟨m, n, mn, h2'⟩ := h2 fun n ↦ h.natEmbedding _ _
-- Lean 4 proof step from Mathlib.Data.Set.MulAntidiagonal (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsCancelMul α
inst_3 : MulLeftMono α
inst_4 : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
h : (s.mulAntidiagonal t a).Infinite
h1 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
h2 : (s.mulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      Order.Preimage (α := α × α) Prod.fst (fun (x1 x2 : α) ↦ x1 ≤ x2)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) m : ℕ)) :
          α × α)
        (↑((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_2 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
              ((g : (a : ℕ) → ℕ) n : ℕ)) :
          α × α)
m n : ℕ
mn : m < n
h2' :
  Subrel (Prod.snd ⁻¹'o fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α × α) ↦ x ∈ s.mulAntidiagonal t a)
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
      ((g : (a : ℕ) → ℕ) m : ℕ))
    ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
      ((g : (a : ℕ) → ℕ) n : ℕ))
⊢ False
have refine : Eq (α := (↑(s.mulAntidiagonal t a) : Type u_1))
  ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
      ((g : (a : ℕ) → ℕ) m : ℕ) :
    (↑(s.mulAntidiagonal t a) : Type u_1))
  ((Infinite.natEmbedding (s.mulAntidiagonal t a) h : (a_1 : ℕ) → (↑(s.mulAntidiagonal t a) : Type u_1))
      ((g : (a : ℕ) → ℕ) n : ℕ) :
    (↑(s.mulAntidiagonal t a) : Type u_1))
Tactic: refine mn.ne (g.injective <| (h.natEmbedding _).injective ?_)
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hf : Injective2 f
a' : α
ha' : a' ∈ s
b' : β
hb' : b' ∈ t
h : f a' b' = f a b
⊢ a ∈ s ∧ b ∈ t
have rcases : ∀ (h : f a' b' = f a' b'), a' ∈ s ∧ b' ∈ t
Tactic: rcases hf h with ⟨rfl, rfl⟩
Cleared hypotheses: a, b, h
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ image2 f s t ⊆ u ↔ ∀ (a : α), a ∈ s → (fun (b : β) ↦ f a b) '' t ⊆ u
have simp_rw : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (a : α), a ∈ s → (fun (b : β) ↦ f a b) '' t ⊆ u
Tactic: simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
simp_rw : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (a : α), a ∈ s → (fun (b : β) ↦ f a b) '' t ⊆ u
⊢ image2 f s t ⊆ u ↔ ∀ (a : α), a ∈ s → (fun (b : β) ↦ f a b) '' t ⊆ u
have simp_rw₁ : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (a : α), a ∈ s → t ⊆ (fun (b : β) ↦ f a b) ⁻¹' u
Tactic: simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
simp_rw : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (a : α), a ∈ s → (fun (b : β) ↦ f a b) '' t ⊆ u
simp_rw₁ : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (a : α), a ∈ s → t ⊆ (fun (b : β) ↦ f a b) ⁻¹' u
⊢ image2 f s t ⊆ u ↔ ∀ (a : α), a ∈ s → (fun (b : β) ↦ f a b) '' t ⊆ u
have simp_rw₂ : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔
  ∀ (a : α), a ∈ s → ∀ (x : β), x ∈ t → Membership.mem (γ := Set β) ((fun (b : β) ↦ f a b) ⁻¹' u) x
Tactic: simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ image2 f s t ⊆ u ↔ ∀ (b : β), b ∈ t → (fun (a : α) ↦ f a b) '' s ⊆ u
have simp_rw : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → (fun (a : α) ↦ f a b) '' s ⊆ u
Tactic: simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage, @forall₂_comm α]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
simp_rw : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → (fun (a : α) ↦ f a b) '' s ⊆ u
⊢ image2 f s t ⊆ u ↔ ∀ (b : β), b ∈ t → (fun (a : α) ↦ f a b) '' s ⊆ u
have simp_rw₁ : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → s ⊆ (fun (a : α) ↦ f a b) ⁻¹' u
Tactic: simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage, @forall₂_comm α]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
simp_rw : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → (fun (a : α) ↦ f a b) '' s ⊆ u
simp_rw₁ : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → s ⊆ (fun (a : α) ↦ f a b) ⁻¹' u
⊢ image2 f s t ⊆ u ↔ ∀ (b : β), b ∈ t → (fun (a : α) ↦ f a b) '' s ⊆ u
have simp_rw₂ : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔
  ∀ (b : β), b ∈ t → ∀ (x : α), x ∈ s → Membership.mem (γ := Set α) ((fun (a : α) ↦ f a b) ⁻¹' u) x
Tactic: simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage, @forall₂_comm α]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
simp_rw : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → (fun (a : α) ↦ f a b) '' s ⊆ u
simp_rw₁ : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → s ⊆ (fun (a : α) ↦ f a b) ⁻¹' u
simp_rw₂ :
  (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔
    ∀ (b : β), b ∈ t → ∀ (x : α), x ∈ s → Membership.mem (γ := Set α) ((fun (a : α) ↦ f a b) ⁻¹' u) x
⊢ image2 f s t ⊆ u ↔ ∀ (b : β), b ∈ t → (fun (a : α) ↦ f a b) '' s ⊆ u
have simp_rw₃ : (∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → f x y ∈ u) ↔ ∀ (b : β), b ∈ t → ∀ (x : α), x ∈ s → f x b ∈ u
Tactic: simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage, @forall₂_comm α]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
⊢ image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t
have simp_rw : Eq.{u_5 + 1} (α := Set γ) ((fun (x : α × β) ↦ f x.1 x.2) '' (s ∪ s') ×ˢ t)
  ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t ∪ (fun (x : α × β) ↦ f x.1 x.2) '' s' ×ˢ t)
Tactic: simp_rw [← image_prod, union_prod, image_union]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
simp_rw :
  Eq.{u_5 + 1} (α := Set γ) ((fun (x : α × β) ↦ f x.1 x.2) '' (s ∪ s') ×ˢ t)
    ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t ∪ (fun (x : α × β) ↦ f x.1 x.2) '' s' ×ˢ t)
⊢ image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t
have simp_rw₁ : Eq.{u_5 + 1} (α := Set γ) ((fun (x : α × β) ↦ f x.1 x.2) '' (s ×ˢ t ∪ s' ×ˢ t))
  ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t ∪ (fun (x : α × β) ↦ f x.1 x.2) '' s' ×ˢ t)
Tactic: simp_rw [← image_prod, union_prod, image_union]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
⊢ image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t'
have rw : image2 (fun (b : β) (a : α) ↦ f a b) (t ∪ t') s = image2 f s t ∪ image2 f s t'
Tactic: rw [← image2_swap, image2_union_left, image2_swap f, image2_swap f]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
rw : image2 (fun (b : β) (a : α) ↦ f a b) (t ∪ t') s = image2 f s t ∪ image2 f s t'
⊢ image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t'
have rw₁ : image2 (fun (b : β) (a : α) ↦ f a b) t s ∪ image2 (fun (b : β) (a : α) ↦ f a b) t' s = image2 f s t ∪ image2 f s t'
Tactic: rw [← image2_swap, image2_union_left, image2_swap f, image2_swap f]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
rw : image2 (fun (b : β) (a : α) ↦ f a b) (t ∪ t') s = image2 f s t ∪ image2 f s t'
rw₁ :
  image2 (fun (b : β) (a : α) ↦ f a b) t s ∪ image2 (fun (b : β) (a : α) ↦ f a b) t' s = image2 f s t ∪ image2 f s t'
⊢ image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t'
have rw₂ : image2 (fun (b : β) (a : α) ↦ f a b) t s ∪ image2 (fun (b : β) (a : α) ↦ f a b) t' s =
  image2 (fun (a : β) (b : α) ↦ f b a) t s ∪ image2 f s t'
Tactic: rw [← image2_swap, image2_union_left, image2_swap f, image2_swap f]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
rw : image2 (fun (b : β) (a : α) ↦ f a b) (t ∪ t') s = image2 f s t ∪ image2 f s t'
rw₁ :
  image2 (fun (b : β) (a : α) ↦ f a b) t s ∪ image2 (fun (b : β) (a : α) ↦ f a b) t' s = image2 f s t ∪ image2 f s t'
rw₂ :
  image2 (fun (b : β) (a : α) ↦ f a b) t s ∪ image2 (fun (b : β) (a : α) ↦ f a b) t' s =
    image2 (fun (a : β) (b : α) ↦ f b a) t s ∪ image2 f s t'
⊢ image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t'
have rw₃ : Eq.{u_5 + 1} (α := Set γ) (image2 (fun (b : β) (a : α) ↦ f a b) t s ∪ image2 (fun (b : β) (a : α) ↦ f a b) t' s)
  (image2 (fun (a : β) (b : α) ↦ f b a) t s ∪ image2 (fun (a : β) (b : α) ↦ f b a) t' s)
Tactic: rw [← image2_swap, image2_union_left, image2_swap f, image2_swap f]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
hf : Injective2 f
⊢ image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t
have simp_rw : uncurry f '' (s ∩ s') ×ˢ t = uncurry f '' s ×ˢ t ∩ uncurry f '' s' ×ˢ t
Tactic: simp_rw [← image_uncurry_prod, inter_prod, image_inter hf.uncurry]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
hf : Injective2 f
simp_rw : uncurry f '' (s ∩ s') ×ˢ t = uncurry f '' s ×ˢ t ∩ uncurry f '' s' ×ˢ t
⊢ image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t
have simp_rw₁ : uncurry f '' (s ×ˢ t ∩ s' ×ˢ t) = uncurry f '' s ×ˢ t ∩ uncurry f '' s' ×ˢ t
Tactic: simp_rw [← image_uncurry_prod, inter_prod, image_inter hf.uncurry]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
hf : Injective2 f
⊢ image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t'
have simp_rw : uncurry f '' s ×ˢ (t ∩ t') = uncurry f '' s ×ˢ t ∩ uncurry f '' s ×ˢ t'
Tactic: simp_rw [← image_uncurry_prod, prod_inter, image_inter hf.uncurry]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
hf : Injective2 f
simp_rw : uncurry f '' s ×ˢ (t ∩ t') = uncurry f '' s ×ˢ t ∩ uncurry f '' s ×ˢ t'
⊢ image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t'
have simp_rw₁ : uncurry f '' (s ×ˢ t ∩ s ×ˢ t') = uncurry f '' s ×ˢ t ∩ uncurry f '' s ×ˢ t'
Tactic: simp_rw [← image_uncurry_prod, prod_inter, image_inter hf.uncurry]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅
have rw : ¬s.Nonempty ∨ ¬t.Nonempty ↔ s = ∅ ∨ t = ∅
Tactic: rw [← not_nonempty_iff_eq_empty, image2_nonempty_iff, not_and_or]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
s : Set α
t : Set β
hs : s.Subsingleton
ht : t.Subsingleton
f : α → β → γ
⊢ (Set.image2 f s t).Subsingleton
have rw : Set.Subsingleton.{u_5} (α := γ) ((fun (x : α × β) ↦ f x.1 x.2) '' s ×ˢ t)
Tactic: rw [← image_prod]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
⊢ image2 f (insert a s) t = (fun (b : β) ↦ f a b) '' t ∪ image2 f s t
have rw : image2 f ({a} ∪ s) t = (fun (b : β) ↦ f a b) '' t ∪ image2 f s t
Tactic: rw [insert_eq, image2_union_left, image2_singleton_left]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
rw : image2 f ({a} ∪ s) t = (fun (b : β) ↦ f a b) '' t ∪ image2 f s t
⊢ image2 f (insert a s) t = (fun (b : β) ↦ f a b) '' t ∪ image2 f s t
have rw₁ : image2 f {a} t ∪ image2 f s t = (fun (b : β) ↦ f a b) '' t ∪ image2 f s t
Tactic: rw [insert_eq, image2_union_left, image2_singleton_left]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
rw : image2 f ({a} ∪ s) t = (fun (b : β) ↦ f a b) '' t ∪ image2 f s t
rw₁ : image2 f {a} t ∪ image2 f s t = (fun (b : β) ↦ f a b) '' t ∪ image2 f s t
⊢ image2 f (insert a s) t = (fun (b : β) ↦ f a b) '' t ∪ image2 f s t
have rw₂ : f a '' t ∪ image2 f s t = (fun (b : β) ↦ f a b) '' t ∪ image2 f s t
Tactic: rw [insert_eq, image2_union_left, image2_singleton_left]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
b : β
⊢ image2 f s (insert b t) = (fun (a : α) ↦ f a b) '' s ∪ image2 f s t
have rw : image2 f s ({b} ∪ t) = (fun (a : α) ↦ f a b) '' s ∪ image2 f s t
Tactic: rw [insert_eq, image2_union_right, image2_singleton_right]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
b : β
rw : image2 f s ({b} ∪ t) = (fun (a : α) ↦ f a b) '' s ∪ image2 f s t
⊢ image2 f s (insert b t) = (fun (a : α) ↦ f a b) '' s ∪ image2 f s t
have rw₁ : image2 f s {b} ∪ image2 f s t = (fun (a : α) ↦ f a b) '' s ∪ image2 f s t
Tactic: rw [insert_eq, image2_union_right, image2_singleton_right]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
b : β
rw : image2 f s ({b} ∪ t) = (fun (a : α) ↦ f a b) '' s ∪ image2 f s t
rw₁ : image2 f s {b} ∪ image2 f s t = (fun (a : α) ↦ f a b) '' s ∪ image2 f s t
⊢ image2 f s (insert b t) = (fun (a : α) ↦ f a b) '' s ∪ image2 f s t
have rw₂ : (fun (a : α) ↦ f a b) '' s ∪ image2 f s t = (fun (a : α) ↦ f a b) '' s ∪ image2 f s t
Tactic: rw [insert_eq, image2_union_right, image2_singleton_right]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : γ → β → δ
g : α → γ
⊢ image2 f (g '' s) t = image2 (fun (a : α) (b : β) ↦ f (g a) b) s t
have h : ∀ (x : δ), x ∈ image2 f (g '' s) t ↔ Membership.mem (γ := Set δ) (image2 (fun (a : α) (b : β) ↦ f (g a) b) s t) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → γ → δ
g : β → γ
⊢ image2 f s (g '' t) = image2 (fun (a : α) (b : β) ↦ f a (g b)) s t
have h : ∀ (x : δ), x ∈ image2 f s (g '' t) ↔ Membership.mem (γ := Set δ) (image2 (fun (a : α) (b : β) ↦ f a (g b)) s t) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
f : α' → β' → γ
g : α → α'
h : β → β'
⊢ image2 f (range g) (range h) = range fun (x : α × β) ↦ f (g x.1) (h x.2)
have simp_rw : image2 f (g '' univ) (h '' univ) = (fun (x : α × β) ↦ f (g x.1) (h x.2)) '' univ
Tactic: simp_rw [← image_univ, image2_image_left, image2_image_right, ← image_prod, univ_prod_univ]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
f : α' → β' → γ
g : α → α'
h : β → β'
simp_rw : image2 f (g '' univ) (h '' univ) = (fun (x : α × β) ↦ f (g x.1) (h x.2)) '' univ
⊢ image2 f (range g) (range h) = range fun (x : α × β) ↦ f (g x.1) (h x.2)
have simp_rw₁ : Eq.{u_5 + 1} (α := Set γ) (image2 (fun (a : α) (b : β') ↦ f (g a) b) univ (h '' univ))
  ((fun (x : α × β) ↦ f (g x.1) (h x.2)) '' univ)
Tactic: simp_rw [← image_univ, image2_image_left, image2_image_right, ← image_prod, univ_prod_univ]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
f : α' → β' → γ
g : α → α'
h : β → β'
simp_rw : image2 f (g '' univ) (h '' univ) = (fun (x : α × β) ↦ f (g x.1) (h x.2)) '' univ
simp_rw₁ :
  Eq.{u_5 + 1} (α := Set γ) (image2 (fun (a : α) (b : β') ↦ f (g a) b) univ (h '' univ))
    ((fun (x : α × β) ↦ f (g x.1) (h x.2)) '' univ)
⊢ image2 f (range g) (range h) = range fun (x : α × β) ↦ f (g x.1) (h x.2)
have simp_rw₂ : Eq.{u_5 + 1} (α := Set γ) (image2 (fun (a : α) (b : β) ↦ f (g a) (h b)) univ univ)
  ((fun (x : α × β) ↦ f (g x.1) (h x.2)) '' univ)
Tactic: simp_rw [← image_univ, image2_image_left, image2_image_right, ← image_prod, univ_prod_univ]
-- Lean 4 proof step from Mathlib.Data.Set.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
f : α' → β' → γ
g : α → α'
h : β → β'
simp_rw : image2 f (g '' univ) (h '' univ) = (fun (x : α × β) ↦ f (g x.1) (h x.2)) '' univ
simp_rw₁ :
  Eq.{u_5 + 1} (α := Set γ) (image2 (fun (a : α) (b : β') ↦ f (g a) b) univ (h '' univ))
    ((fun (x : α × β) ↦ f (g x.1) (h x.2)) '' univ)
simp_rw₂ :
  Eq.{u_5 + 1} (α := Set γ) (image2 (fun (a : α) (b : β) ↦ f (g a) (h b)) univ univ)
    ((fun (x : α × β) ↦ f (g x.1) (h x.2)) '' univ)
⊢ image2 f (range g) (range h) = range fun (x : α × β) ↦ f (g x.1) (h x.2)
have simp_rw₃ : Eq.{u_5 + 1} (α := Set γ) ((fun (x : α × β) ↦ f (g x.1) (h x.2)) '' SProd.sprod (α := Set α) (β := Set β) univ univ)
  ((fun (x : α × β) ↦ f (g x.1) (h x.2)) '' univ)
Tactic: simp_rw [← image_univ, image2_image_left, image2_image_right, ← image_prod, univ_prod_univ]