awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst : DecidableEq α
h : t.Nonempty
⊢ image2 (fun (x : α) (x_1 : β) ↦ x) (↑s : Set α) (↑t : Set β) = (↑s : Set α)

Tactic:
exact image2_left h

Premises used: Set.image2_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst : DecidableEq β
h : s.Nonempty
push_cast : image2 (fun (x : α) (y : β) ↦ y) (↑s : Set α) (↑t : Set β) = (↑t : Set β)
⊢ (↑(image₂ (fun (x : α) (y : β) ↦ y) s t) : Set β) = (↑t : Set β)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst : DecidableEq β
h : s.Nonempty
⊢ image2 (fun (x : α) (y : β) ↦ y) (↑s : Set α) (↑t : Set β) = (↑t : Set β)

Tactic:
image2_right h

Premises used: Set.image2_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst : DecidableEq β
h : s.Nonempty
⊢ image2 (fun (x : α) (y : β) ↦ y) (↑s : Set α) (↑t : Set β) = (↑t : Set β)

Tactic:
exact image2_right h

Premises used: Set.image2_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
δ : Type u_7
ε : Type u_9
ε' : Type u_10
inst : DecidableEq ε
inst_1 : DecidableEq ε'
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
push_cast :
  image2 f (image2 g (↑s : Set α) (↑t : Set β)) (↑u : Set γ) =
    image2 f' (↑s : Set α) (image2 g' (↑t : Set β) (↑u : Set γ))
⊢ (↑(image₂ f (image₂ g s t) u) : Set ε) = (↑(image₂ f' s (image₂ g' t u)) : Set ε)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
δ : Type u_7
ε : Type u_9
ε' : Type u_10
inst : DecidableEq ε
inst_1 : DecidableEq ε'
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ image2 f (image2 g (↑s : Set α) (↑t : Set β)) (↑u : Set γ) =
    image2 f' (↑s : Set α) (image2 g' (↑t : Set β) (↑u : Set γ))

Tactic:
image2_assoc h_assoc

Premises used: Set.image2_assoc
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
δ : Type u_7
ε : Type u_9
ε' : Type u_10
inst : DecidableEq ε
inst_1 : DecidableEq ε'
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ image2 f (image2 g (↑s : Set α) (↑t : Set β)) (↑u : Set γ) =
    image2 f' (↑s : Set α) (image2 g' (↑t : Set β) (↑u : Set γ))

Tactic:
exact image2_assoc h_assoc

Premises used: Set.image2_assoc
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
inst : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ image₂ (fun (a : β) (b : α) ↦ f b a) t s = image₂ g t s

Tactic:
simp_rw [h_comm]
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst : DecidableEq δ'
inst_1 : DecidableEq ε
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
push_cast :
  image2 f (↑s : Set α) (image2 g (↑t : Set β) (↑u : Set γ)) =
    image2 g' (↑t : Set β) (image2 f' (↑s : Set α) (↑u : Set γ))
⊢ (↑(image₂ f s (image₂ g t u)) : Set ε) = (↑(image₂ g' t (image₂ f' s u)) : Set ε)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst : DecidableEq δ'
inst_1 : DecidableEq ε
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 f (↑s : Set α) (image2 g (↑t : Set β) (↑u : Set γ)) =
    image2 g' (↑t : Set β) (image2 f' (↑s : Set α) (↑u : Set γ))

Tactic:
image2_left_comm h_left_comm

Premises used: Set.image2_left_comm
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst : DecidableEq δ'
inst_1 : DecidableEq ε
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 f (↑s : Set α) (image2 g (↑t : Set β) (↑u : Set γ)) =
    image2 g' (↑t : Set β) (image2 f' (↑s : Set α) (↑u : Set γ))

Tactic:
exact image2_left_comm h_left_comm

Premises used: Set.image2_left_comm
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst : DecidableEq δ'
inst_1 : DecidableEq ε
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
push_cast :
  image2 f (image2 g (↑s : Set α) (↑t : Set β)) (↑u : Set γ) =
    image2 g' (image2 f' (↑s : Set α) (↑u : Set γ)) (↑t : Set β)
⊢ (↑(image₂ f (image₂ g s t) u) : Set ε) = (↑(image₂ g' (image₂ f' s u) t) : Set ε)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst : DecidableEq δ'
inst_1 : DecidableEq ε
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 g (↑s : Set α) (↑t : Set β)) (↑u : Set γ) =
    image2 g' (image2 f' (↑s : Set α) (↑u : Set γ)) (↑t : Set β)

Tactic:
image2_right_comm h_right_comm

Premises used: Set.image2_right_comm
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst : DecidableEq δ'
inst_1 : DecidableEq ε
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 g (↑s : Set α) (↑t : Set β)) (↑u : Set γ) =
    image2 g' (image2 f' (↑s : Set α) (↑u : Set γ)) (↑t : Set β)

Tactic:
exact image2_right_comm h_right_comm

Premises used: Set.image2_right_comm
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
inst : DecidableEq ε
inst_1 : DecidableEq ε'
s : Finset α
t : Finset β
γ : Type u_14
δ : Type u_15
u : Finset γ
v : Finset δ
inst_2 : DecidableEq ζ
inst_3 : DecidableEq ζ'
inst_4 : DecidableEq ν
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)
push_cast :
  image2 f (image2 g (↑s : Set α) (↑t : Set β)) (image2 h (↑u : Set γ) (↑v : Set δ)) =
    image2 f' (image2 g' (↑s : Set α) (↑u : Set γ)) (image2 h' (↑t : Set β) (↑v : Set δ))
⊢ (↑(image₂ f (image₂ g s t) (image₂ h u v)) : Set ν) = (↑(image₂ f' (image₂ g' s u) (image₂ h' t v)) : Set ν)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
inst : DecidableEq ε
inst_1 : DecidableEq ε'
s : Finset α
t : Finset β
γ : Type u_14
δ : Type u_15
u : Finset γ
v : Finset δ
inst_2 : DecidableEq ζ
inst_3 : DecidableEq ζ'
inst_4 : DecidableEq ν
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 : Set α) (↑t : Set β)) (image2 h (↑u : Set γ) (↑v : Set δ)) =
    image2 f' (image2 g' (↑s : Set α) (↑u : Set γ)) (image2 h' (↑t : Set β) (↑v : Set δ))

Tactic:
image2_image2_image2_comm h_comm

Premises used: Set.image2_image2_image2_comm
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
inst : DecidableEq ε
inst_1 : DecidableEq ε'
s : Finset α
t : Finset β
γ : Type u_14
δ : Type u_15
u : Finset γ
v : Finset δ
inst_2 : DecidableEq ζ
inst_3 : DecidableEq ζ'
inst_4 : DecidableEq ν
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 : Set α) (↑t : Set β)) (image2 h (↑u : Set γ) (↑v : Set δ)) =
    image2 f' (image2 g' (↑s : Set α) (↑u : Set γ)) (image2 h' (↑t : Set β) (↑v : Set δ))

Tactic:
exact image2_image2_image2_comm h_comm

Premises used: Set.image2_image2_image2_comm
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq β'
inst_2 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
push_cast : g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (g₁ '' (↑s : Set α)) (g₂ '' (↑t : Set β))
⊢ (↑(image g (image₂ f s t)) : Set δ) = (↑(image₂ f' (image g₁ s) (image g₂ t)) : Set δ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq β'
inst_2 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (g₁ '' (↑s : Set α)) (g₂ '' (↑t : Set β))

Tactic:
image_image2_distrib h_distrib

Premises used: Set.image_image2_distrib
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq β'
inst_2 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (g₁ '' (↑s : Set α)) (g₂ '' (↑t : Set β))

Tactic:
exact image_image2_distrib h_distrib

Premises used: Set.image_image2_distrib
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
push_cast : g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (g' '' (↑s : Set α)) (↑t : Set β)
⊢ (↑(image g (image₂ f s t)) : Set δ) = (↑(image₂ f' (image g' s) t) : Set δ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (g' '' (↑s : Set α)) (↑t : Set β)

Tactic:
image_image2_distrib_left h_distrib

Premises used: Set.image_image2_distrib_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (g' '' (↑s : Set α)) (↑t : Set β)

Tactic:
exact image_image2_distrib_left h_distrib

Premises used: Set.image_image2_distrib_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq β'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
push_cast : g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (↑s : Set α) (g' '' (↑t : Set β))
⊢ (↑(image g (image₂ f s t)) : Set δ) = (↑(image₂ f' s (image g' t)) : Set δ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq β'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (↑s : Set α) (g' '' (↑t : Set β))

Tactic:
image_image2_distrib_right h_distrib

Premises used: Set.image_image2_distrib_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq β'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (↑s : Set α) (g' '' (↑t : Set β))

Tactic:
exact image_image2_distrib_right h_distrib

Premises used: Set.image_image2_distrib_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
f : α' → β → γ
g : α → α'
f' : α → β → δ
g' : δ → γ
h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)
⊢ image₂ f (image g s) t = image g' (image₂ f' s t)

Tactic:
(image_image₂_distrib_left fun a b => (h_left_comm a b).symm).symm

Premises used: Eq.symm, Finset.image_image₂_distrib_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq β'
inst_1 : DecidableEq γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
⊢ image₂ f s (image g t) = image g' (image₂ f' s t)

Tactic:
(image_image₂_distrib_right fun a b => (h_right_comm a b).symm).symm

Premises used: Finset.image_image₂_distrib_right, Eq.symm
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ' : Type u_6
δ : Type u_7
ε : Type u_9
inst : DecidableEq β'
inst_1 : DecidableEq γ'
inst_2 : DecidableEq ε
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
push_cast :
  image2 f (↑s : Set α) (image2 g (↑t : Set β) (↑u : Set γ)) ⊆
    image2 g' (image2 f₁ (↑s : Set α) (↑t : Set β)) (image2 f₂ (↑s : Set α) (↑u : Set γ))
⊢ (↑(image₂ f s (image₂ g t u)) : Set ε) ⊆ (↑(image₂ g' (image₂ f₁ s t) (image₂ f₂ s u)) : Set ε)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ' : Type u_6
δ : Type u_7
ε : Type u_9
inst : DecidableEq β'
inst_1 : DecidableEq γ'
inst_2 : DecidableEq ε
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
γ : Type u_14
u : Finset γ
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 : Set α) (image2 g (↑t : Set β) (↑u : Set γ)) ⊆
    image2 g' (image2 f₁ (↑s : Set α) (↑t : Set β)) (image2 f₂ (↑s : Set α) (↑u : Set γ))

Tactic:
Set.image2_distrib_subset_left h_distrib

Premises used: Set.image2_distrib_subset_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ' : Type u_6
δ : Type u_7
ε : Type u_9
inst : DecidableEq β'
inst_1 : DecidableEq γ'
inst_2 : DecidableEq ε
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
γ : Type u_14
u : Finset γ
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 : Set α) (image2 g (↑t : Set β) (↑u : Set γ)) ⊆
    image2 g' (image2 f₁ (↑s : Set α) (↑t : Set β)) (image2 f₂ (↑s : Set α) (↑u : Set γ))

Tactic:
exact Set.image2_distrib_subset_left h_distrib

Premises used: Set.image2_distrib_subset_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
δ : Type u_7
ε : Type u_9
inst : DecidableEq α'
inst_1 : DecidableEq β'
inst_2 : DecidableEq ε
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
push_cast :
  image2 f (image2 g (↑s : Set α) (↑t : Set β)) (↑u : Set γ) ⊆
    image2 g' (image2 f₁ (↑s : Set α) (↑u : Set γ)) (image2 f₂ (↑t : Set β) (↑u : Set γ))
⊢ (↑(image₂ f (image₂ g s t) u) : Set ε) ⊆ (↑(image₂ g' (image₂ f₁ s u) (image₂ f₂ t u)) : Set ε)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
δ : Type u_7
ε : Type u_9
inst : DecidableEq α'
inst_1 : DecidableEq β'
inst_2 : DecidableEq ε
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
γ : Type u_14
u : Finset γ
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 : Set α) (↑t : Set β)) (↑u : Set γ) ⊆
    image2 g' (image2 f₁ (↑s : Set α) (↑u : Set γ)) (image2 f₂ (↑t : Set β) (↑u : Set γ))

Tactic:
Set.image2_distrib_subset_right h_distrib

Premises used: Set.image2_distrib_subset_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
δ : Type u_7
ε : Type u_9
inst : DecidableEq α'
inst_1 : DecidableEq β'
inst_2 : DecidableEq ε
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
γ : Type u_14
u : Finset γ
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 : Set α) (↑t : Set β)) (↑u : Set γ) ⊆
    image2 g' (image2 f₁ (↑s : Set α) (↑u : Set γ)) (image2 f₂ (↑t : Set β) (↑u : Set γ))

Tactic:
exact Set.image2_distrib_subset_right h_distrib

Premises used: Set.image2_distrib_subset_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq β'
inst_2 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
rw : image g (image₂ (fun (a : β) (b : α) ↦ f b a) t s) = image₂ f' (image g₁ t) (image g₂ s)
⊢ image g (image₂ f s t) = image₂ f' (image g₁ t) (image g₂ s)

Tactic:
rw [image₂_swap f]

Premises used: Finset.image₂_swap
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq β'
inst_2 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ image g (image₂ (fun (a : β) (b : α) ↦ f b a) t s) = image₂ f' (image g₁ t) (image g₂ s)

Tactic:
image_image₂_distrib fun _ _ => h_antidistrib _ _

Premises used: Finset.image_image₂_distrib
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq β'
inst_2 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_3 : DecidableEq δ
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ image g (image₂ (fun (a : β) (b : α) ↦ f b a) t s) = image₂ f' (image g₁ t) (image g₂ s)

Tactic:
exact image_image₂_distrib fun _ _ => h_antidistrib _ _

Premises used: Finset.image_image₂_distrib
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq β'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
push_cast : g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (g' '' (↑t : Set β)) (↑s : Set α)
⊢ (↑(image g (image₂ f s t)) : Set δ) = (↑(image₂ f' (image g' t) s) : Set δ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq β'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (g' '' (↑t : Set β)) (↑s : Set α)

Tactic:
image_image2_antidistrib_left h_antidistrib

Premises used: Set.image_image2_antidistrib_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq β'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (g' '' (↑t : Set β)) (↑s : Set α)

Tactic:
exact image_image2_antidistrib_left h_antidistrib

Premises used: Set.image_image2_antidistrib_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
push_cast : g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (↑t : Set β) (g' '' (↑s : Set α))
⊢ (↑(image g (image₂ f s t)) : Set δ) = (↑(image₂ f' t (image g' s)) : Set δ)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (↑t : Set β) (g' '' (↑s : Set α))

Tactic:
image_image2_antidistrib_right h_antidistrib

Premises used: Set.image_image2_antidistrib_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ g '' image2 f (↑s : Set α) (↑t : Set β) = image2 f' (↑t : Set β) (g' '' (↑s : Set α))

Tactic:
exact image_image2_antidistrib_right h_antidistrib

Premises used: Set.image_image2_antidistrib_right
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst : DecidableEq α'
inst_1 : DecidableEq γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
⊢ image₂ f (image g s) t = image g' (image₂ f' t s)

Tactic:
(image_image₂_antidistrib_left fun a b => (h_left_anticomm b a).symm).symm

Premises used: Eq.symm, Finset.image_image₂_antidistrib_left
-- Module: Mathlib.Data.Finset.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst : DecidableEq β'
inst_1 : DecidableEq γ
s : Finset α
t : Finset β
inst_2 : DecidableEq δ
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
⊢ image₂ f s (image g t) = image g' (image₂ f' t s)

Tactic:
(image_image₂_antidistrib_right fun a b => (h_right_anticomm b a).symm).symm

Premises used: Finset.image_image₂_antidistrib_right, Eq.symm