awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : ¬f a b ∈ image2 f s t'
⊢ f a b ∈ image2 f s (t \ t')

Tactic:
exact ⟨_, ha, _, ⟨hb, fun hb' ↦ h ⟨_, ha, _, hb', rfl⟩⟩, rfl⟩
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
t : Set β
a : α
x : γ
⊢ x ∈ image2 f {a} t ↔ x ∈ f a '' t

Tactic:
simp
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
b : β
x : γ
⊢ x ∈ image2 f s {b} ↔ Membership.mem (γ := Set γ) ((fun (a : α) ↦ f a b) '' s) x

Tactic:
simp
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
a : α
b : β
⊢ image2 f {a} {b} = {f a b}

Tactic:
simp
-- Module: Mathlib.Data.Set.NAry
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
rw₂ rw₃ : 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

Tactic:
rw [insert_eq, image2_union_left, image2_singleton_left]

Premises used: Set.insert_eq, Set.image2_singleton_left, Set.image2_union_left
-- Module: Mathlib.Data.Set.NAry
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
rw₂ rw₃ : (fun (a : α) ↦ f a b) '' s ∪ 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

Tactic:
rw [insert_eq, image2_union_right, image2_singleton_right]

Premises used: Set.insert_eq, Set.image2_singleton_right, Set.image2_union_right
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f f' : α → β → γ
s : Set α
t : Set β
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a b = f' a b
⊢ image2 f s t = image2 f' s t

Tactic:
grind
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f f' : α → β → γ
s : Set α
t : Set β
h : ∀ (a : α) (b : β), f a b = f' a b
⊢ image2 f s t = image2 f' s t

Tactic:
image2_congr fun a _ b _ => h a b

Premises used: Set.image2_congr
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → β → γ
g : γ → δ
⊢ g '' image2 f s t = image2 (fun (a : α) (b : β) ↦ g (f a b)) s t

Tactic:
simp only [← image_prod, image_image]

Premises used: Set.image_image, Set.image_prod
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : γ → β → δ
g : α → γ
h : ∀ (x : δ), x ∈ image2 f (g '' s) t ↔ Membership.mem (γ := Set δ) (image2 (fun (a : α) (b : β) ↦ f (g a) b) s t) x
⊢ image2 f (g '' s) t = image2 (fun (a : α) (b : β) ↦ f (g a) b) s t

Tactic:
ext
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : γ → β → δ
g : α → γ
x : δ
⊢ x ∈ image2 f (g '' s) t ↔ Membership.mem (γ := Set δ) (image2 (fun (a : α) (b : β) ↦ f (g a) b) s t) x

Tactic:
simp
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → γ → δ
g : β → γ
h : ∀ (x : δ), x ∈ image2 f s (g '' t) ↔ Membership.mem (γ := Set δ) (image2 (fun (a : α) (b : β) ↦ f a (g b)) s t) x
⊢ image2 f s (g '' t) = image2 (fun (a : α) (b : β) ↦ f a (g b)) s t

Tactic:
ext
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → γ → δ
g : β → γ
x : δ
⊢ x ∈ image2 f s (g '' t) ↔ Membership.mem (γ := Set δ) (image2 (fun (a : α) (b : β) ↦ f a (g b)) s t) x

Tactic:
simp
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
s : Set α
t : Set β
h : t.Nonempty
⊢ image2 (fun (x : α) (x_1 : β) ↦ x) s t = s

Tactic:
simp [nonempty_def.mp h, Set.ext_iff]

Premises used: Set.nonempty_def, Iff.mp, Set.ext_iff
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
s : Set α
t : Set β
h : s.Nonempty
⊢ image2 (fun (x : α) (y : β) ↦ y) s t = t

Tactic:
simp [nonempty_def.mp h, Set.ext_iff]

Premises used: Set.nonempty_def, Iff.mp, Set.ext_iff
-- Module: Mathlib.Data.Set.NAry
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)
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)
⊢ image2 f (range g) (range h) = range fun (x : α × β) ↦ f (g x.1) (h x.2)

Tactic:
simp_rw [← image_univ, image2_image_left, image2_image_right, ← image_prod, univ_prod_univ]

Premises used: Set.image2_image_right, Set.image_univ, Set.image_prod, Set.image2_image_left, Set.univ_prod_univ
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
x : Set ε
⊢ image2 f (image2 g s t) u ⊆ x ↔ image2 f' s (image2 g' t u) ⊆ x

Tactic:
simp only [image2_subset_iff, forall_mem_image2, h_assoc]

Premises used: Set.forall_mem_image2, Set.image2_subset_iff
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ image2 (fun (a : β) (b : α) ↦ f b a) t s = image2 g t s

Tactic:
simp_rw [h_comm]
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
rw : image2 (fun (a : δ) (b : α) ↦ f b a) (image2 g t u) s = image2 g' t (image2 (fun (a : γ) (b : α) ↦ f' b a) u s)
⊢ image2 f s (image2 g t u) = image2 g' t (image2 f' s u)

Tactic:
rw [image2_swap f', image2_swap f]

Premises used: Set.image2_swap
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 (fun (a : δ) (b : α) ↦ f b a) (image2 g t u) s = image2 g' t (image2 (fun (a : γ) (b : α) ↦ f' b a) u s)

Tactic:
image2_assoc fun _ _ _ => h_left_comm _ _ _

Premises used: Set.image2_assoc
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 (fun (a : δ) (b : α) ↦ f b a) (image2 g t u) s = image2 g' t (image2 (fun (a : γ) (b : α) ↦ f' b a) u s)

Tactic:
exact image2_assoc fun _ _ _ => h_left_comm _ _ _

Premises used: Set.image2_assoc
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
rw : image2 f (image2 (fun (a : β) (b : α) ↦ g b a) t s) u = image2 (fun (a : β) (b : δ') ↦ g' b a) t (image2 f' s u)
⊢ image2 f (image2 g s t) u = image2 g' (image2 f' s u) t

Tactic:
rw [image2_swap g, image2_swap g']

Premises used: Set.image2_swap
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 (fun (a : β) (b : α) ↦ g b a) t s) u = image2 (fun (a : β) (b : δ') ↦ g' b a) t (image2 f' s u)

Tactic:
image2_assoc fun _ _ _ => h_right_comm _ _ _

Premises used: Set.image2_assoc
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 (fun (a : β) (b : α) ↦ g b a) t s) u = image2 (fun (a : β) (b : δ') ↦ g' b a) t (image2 f' s u)

Tactic:
exact image2_assoc fun _ _ _ => h_right_comm _ _ _

Premises used: Set.image2_assoc
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
s : Set α
t : Set β
u : Set γ
v : Set δ
f : ε → ζ → ν
g : α → β → ε
h : γ → δ → ζ
f' : ε' → ζ' → ν
g' : α → γ → ε'
h' : β → δ → ζ'
h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)
⊢ image2 f (image2 g s t) (image2 h u v) = image2 f' (image2 g' s u) (image2 h' t v)

Tactic:
grind
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
simp_rw : image2 (fun (a : α) (b : β) ↦ g (f a b)) s t = image2 f' (g₁ '' s) (g₂ '' t)
simp_rw₁ :
  Eq.{u_7 + 1} (α := Set δ) (image2 (fun (a : α) (b : β) ↦ g (f a b)) s t)
    (image2 (fun (a : α) (b : β') ↦ f' (g₁ a) b) s (g₂ '' t))
simp_rw₂ :
  Eq.{u_7 + 1} (α := Set δ) (image2 (fun (a : α) (b : β) ↦ g (f a b)) s t)
    (image2 (fun (a : α) (b : β) ↦ f' (g₁ a) (g₂ b)) s t)
⊢ g '' image2 f s t = image2 f' (g₁ '' s) (g₂ '' t)

Tactic:
simp_rw [image_image2, image2_image_left, image2_image_right, h_distrib]

Premises used: Set.image2_image_right, Set.image2_image_left, Set.image_image2
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
rw rw₁ : image2 f' (g' '' s) t = image2 f' (g' '' s) t
⊢ image2 f' (g' '' s) ((fun (b : β) ↦ b) '' t) = image2 f' (g' '' s) t

Tactic:
rw [image_id']

Premises used: Set.image_id'
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
rw rw₁ : image2 f' s (g' '' t) = image2 f' s (g' '' t)
⊢ image2 f' ((fun (a : α) ↦ a) '' s) (g' '' t) = image2 f' s (g' '' t)

Tactic:
rw [image_id']

Premises used: Set.image_id'
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α' → β → γ
g : α → α'
f' : α → β → δ
g' : δ → γ
h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)
⊢ image2 f (g '' s) t = g' '' image2 f' s t

Tactic:
(image_image2_distrib_left fun a b => (h_left_comm a b).symm).symm

Premises used: Set.image_image2_distrib_left, Eq.symm
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
⊢ image2 f s (g '' t) = g' '' image2 f' s t

Tactic:
(image_image2_distrib_right fun a b => (h_right_comm a b).symm).symm

Premises used: Eq.symm, Set.image_image2_distrib_right
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
⊢ image2 f s (image2 g t u) ⊆ image2 g' (image2 f₁ s t) (image2 f₂ s u)

Tactic:
grind
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
⊢ image2 f (image2 g s t) u ⊆ image2 g' (image2 f₁ s u) (image2 f₂ t u)

Tactic:
grind
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
rw : g '' image2 (fun (a : β) (b : α) ↦ f b a) t s = image2 f' (g₁ '' t) (g₂ '' s)
⊢ g '' image2 f s t = image2 f' (g₁ '' t) (g₂ '' s)

Tactic:
rw [image2_swap f]

Premises used: Set.image2_swap
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ g '' image2 (fun (a : β) (b : α) ↦ f b a) t s = image2 f' (g₁ '' t) (g₂ '' s)

Tactic:
image_image2_distrib fun _ _ => h_antidistrib _ _

Premises used: Set.image_image2_distrib
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ g '' image2 (fun (a : β) (b : α) ↦ f b a) t s = image2 f' (g₁ '' t) (g₂ '' s)

Tactic:
exact image_image2_distrib fun _ _ => h_antidistrib _ _

Premises used: Set.image_image2_distrib
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
rw rw₁ : image2 f' (g' '' t) s = image2 f' (g' '' t) s
⊢ image2 f' (g' '' t) ((fun (a : α) ↦ a) '' s) = image2 f' (g' '' t) s

Tactic:
rw [image_id']

Premises used: Set.image_id'
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
rw rw₁ : image2 f' t (g' '' s) = image2 f' t (g' '' s)
⊢ image2 f' ((fun (b : β) ↦ b) '' t) (g' '' s) = image2 f' t (g' '' s)

Tactic:
rw [image_id']

Premises used: Set.image_id'
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
⊢ image2 f (g '' s) t = g' '' image2 f' t s

Tactic:
(image_image2_antidistrib_left fun a b => (h_left_anticomm b a).symm).symm

Premises used: Set.image_image2_antidistrib_left, Eq.symm
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
⊢ image2 f s (g '' t) = g' '' image2 f' t s

Tactic:
(image_image2_antidistrib_right fun a b => (h_right_anticomm b a).symm).symm

Premises used: Set.image_image2_antidistrib_right, Eq.symm
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
t : Set β
rw : f a '' t = t
rw₁ : id '' t = t
rw₂ rw₃ : t = t
⊢ image2 f {a} t = t

Tactic:
rw [image2_singleton_left, show f a = id from funext h, image_id]

Premises used: Set.image2_singleton_left, funext, Set.image_id
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
s : Set α
rw : (fun (a : α) ↦ f a b) '' s = s
rw₁ : (fun (x : α) ↦ x) '' s = s
rw₂ rw₃ : s = s
⊢ image2 f s {b} = s

Tactic:
rw [image2_singleton_right, funext h, image_id']

Premises used: Set.image_id', funext, Set.image2_singleton_right
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
rw : image2 f (s ∩ s') t ∪ image2 f (s ∩ s') t' ⊆ image2 f s t ∪ image2 f s' t'
⊢ image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
rw [image2_union_right]

Premises used: Set.image2_union_right
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∩ s') t ∪ image2 f (s ∩ s') t' ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
union_subset_union (image2_subset_right inter_subset_left)
      (image2_subset_right inter_subset_right)

Premises used: Set.union_subset_union, Set.inter_subset_left, Set.image2_subset_right, Set.inter_subset_right
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∩ s') t ∪ image2 f (s ∩ s') t' ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
exact
    union_subset_union (image2_subset_right inter_subset_left)
      (image2_subset_right inter_subset_right)

Premises used: Set.union_subset_union, Set.inter_subset_left, Set.image2_subset_right, Set.inter_subset_right
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
rw : image2 f s (t ∩ t') ∪ image2 f s' (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'
⊢ image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
rw [image2_union_left]

Premises used: Set.image2_union_left
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f s (t ∩ t') ∪ image2 f s' (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
union_subset_union (image2_subset_left inter_subset_left)
      (image2_subset_left inter_subset_right)

Premises used: Set.union_subset_union, Set.inter_subset_left, Set.image2_subset_left, Set.inter_subset_right
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f s (t ∩ t') ∪ image2 f s' (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
exact
    union_subset_union (image2_subset_left inter_subset_left)
      (image2_subset_left inter_subset_right)

Premises used: Set.union_subset_union, Set.inter_subset_left, Set.image2_subset_left, Set.inter_subset_right
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
rw : image2 f (t ∩ s) (s ∪ t) ⊆ image2 f s t
⊢ image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (t ∩ s) (s ∪ t) ⊆ image2 f s t

Tactic:
image2_inter_union_subset_union.trans (union_subset (image2_comm hf).subset Subset.rfl)

Premises used: Set.image2_inter_union_subset_union, HasSubset.Subset.trans, Set.union_subset, Eq.subset, Set.Subset.rfl, Set.image2_comm
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (t ∩ s) (s ∪ t) ⊆ image2 f s t

Tactic:
exact image2_inter_union_subset_union.trans (union_subset (image2_comm hf).subset Subset.rfl)

Premises used: Set.image2_inter_union_subset_union, HasSubset.Subset.trans, Set.union_subset, Eq.subset, Set.Subset.rfl, Set.image2_comm
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
rw : image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t
⊢ image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t

Tactic:
rw [image2_comm hf]

Premises used: Set.image2_comm
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t

Tactic:
image2_inter_union_subset hf

Premises used: Set.image2_inter_union_subset
-- Module: Mathlib.Data.Set.NAry
Goal:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t

Tactic:
exact image2_inter_union_subset hf

Premises used: Set.image2_inter_union_subset
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
x : α
p : α → Prop
⊢ Membership.mem (γ := Set α) {y : α | p y} x = p x

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
p : α → Prop
⊢ p = fun (x : α) ↦ Membership.mem (γ := Set α) {a : α | p a} x

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
a : α
p : α → Prop
⊢ Membership.mem (γ := Set α) {x : α | p x} a ↔ p a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
a : α
p : α → Prop
⊢ ¬Membership.mem (γ := Set α) {x : α | p x} a ↔ ¬p a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
s : Set α
⊢ {x : α | x ∈ s} = s

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
x : α
⊢ Membership.mem (γ := Set α) univ x

Tactic:
trivial

Premises used: trivial, Set.Mem, Set.univ, setOf
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
s : Set α
x : α
⊢ x ∈ sᶜ ↔ ¬x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Not
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
s t : Set α
⊢ s \ t = s ∩ tᶜ

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Not, rfl
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
s t : Set α
x : α
⊢ x ∈ s \ t ↔ x ∈ s ∧ ¬x ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Set.diff, Iff.rfl, setOf
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
s t : Set α
x : α
h1 : x ∈ s
h2 : ¬x ∈ t
⊢ x ∈ s \ t

Tactic:
⟨h1, h2⟩

Premises used: Set.Mem, Set.diff, setOf, And.intro
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
f : α → β
s : Set β
a : α
⊢ a ∈ f ⁻¹' s ↔ f a ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
y : β
⊢ y ∈ f '' s ↔ ∃ (x : α), x ∈ s ∧ f x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
f : α → β
x : α
a : Set α
h : x ∈ a
⊢ f x ∈ f '' a

Tactic:
⟨_, h, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
β : Type v
s : Set β
t : Set α
f : α → β
⊢ s ⊆ kernImage f t ↔ f ⁻¹' s ⊆ t

Tactic:
⟨fun h _ hx ↦ h hx rfl,
    fun h _ hx y hy ↦ h (show f y ∈ s from hy.symm ▸ hx)⟩

Premises used: Eq.rec, Iff.intro, Eq.symm, rfl
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
ι : Sort u_1
f : ι → α
x : α
⊢ x ∈ range f ↔ ∃ (y : ι), f y = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
ι : Sort u_1
f : ι → α
i : ι
⊢ f i ∈ range f

Tactic:
⟨i, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
ι : Sort u_1
f : ι → α
⊢ Function.Injective (rangeFactorization f) ↔ Function.Injective f

Tactic:
simp [Function.Injective, rangeFactorization]

Premises used: Function.Injective, Set.rangeFactorization
-- Module: Mathlib.Data.Set.Operations
Goal:
α : Type u
ι : Sort u_1
f : ι → α
⊢ Function.Surjective (rangeFactorization f)

Tactic:
fun ⟨_, i, rfl⟩ ↦ ⟨i, rfl⟩

Premises used: Exists, _private.0.Set.rangeFactorization_surjective.match_1, Exists.intro, Set.rangeFactorization, Eq, Function.Surjective, rfl