awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst : g.NeBot
⊢ map₂ (fun (x : α) (x_1 : β) ↦ x) f g = f
have rw : map (fun (p : α × β) ↦ p.1) (f ×ˢ g) = f
Tactic: rw [← map_prod_eq_map₂, map_fst_prod]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst : g.NeBot
rw : map (fun (p : α × β) ↦ p.1) (f ×ˢ g) = f
⊢ map₂ (fun (x : α) (x_1 : β) ↦ x) f g = f
have rw₁ : f = f
Tactic: rw [← map_prod_eq_map₂, map_fst_prod]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst : f.NeBot
⊢ map₂ (fun (x : α) (y : β) ↦ y) f g = g
have rw : map₂ (fun (a : β) (b : α) ↦ a) g f = g
Tactic: rw [map₂_swap, map₂_left]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst : f.NeBot
rw : map₂ (fun (a : β) (b : α) ↦ a) g f = g
⊢ map₂ (fun (x : α) (y : β) ↦ y) f g = g
have rw₁ : g = g
Tactic: rw [map₂_swap, map₂_left]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β → γ
n : γ → δ
⊢ map n (map₂ m f g) = map₂ (fun (a : α) (b : β) ↦ n (m a b)) f g
have rw : map (n ∘ fun (p : α × β) ↦ m p.1 p.2) (f ×ˢ g) = map (fun (p : α × β) ↦ n (m p.1 p.2)) (f ×ˢ g)
Tactic: rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : γ → β → δ
n : α → γ
⊢ map₂ m (map n f) g = map₂ (fun (a : α) (b : β) ↦ m (n a) b) f g
have rw : Eq.{u_7 + 1} (α := Filter δ) (map ((fun (p : γ × β) ↦ m p.1 p.2) ∘ fun (p : α × β) ↦ (n p.1, id p.2)) (f ×ˢ g))
  (map (fun (p : α × β) ↦ m (n p.1) p.2) (f ×ˢ g))
Tactic: rw [← map_prod_eq_map₂, ← map_prod_eq_map₂, ← @map_id _ g, prod_map_map_eq, map_map, map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → γ → δ
n : β → γ
⊢ map₂ m f (map n g) = map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g
have rw : Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : γ) (b : α) ↦ m b a) (map n g) f)
  (map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g)
Tactic: rw [map₂_swap, map₂_map_left, map₂_swap]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → γ → δ
n : β → γ
rw :
  Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : γ) (b : α) ↦ m b a) (map n g) f)
    (map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g)
⊢ map₂ m f (map n g) = map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g
have rw₁ : Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : β) (b : α) ↦ m b (n a)) g f) (map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g)
Tactic: rw [map₂_swap, map₂_map_left, map₂_swap]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → γ → δ
n : β → γ
rw :
  Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : γ) (b : α) ↦ m b a) (map n g) f)
    (map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g)
rw₁ :
  Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : β) (b : α) ↦ m b (n a)) g f) (map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g)
⊢ map₂ m f (map n g) = map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g
have rw₂ : Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g) (map₂ (fun (a : α) (b : β) ↦ m a (n b)) f g)
Tactic: rw [map₂_swap, map₂_map_left, map₂_swap]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h)
have rw : Eq.{u_9 + 1} (α := Filter ε) (map (fun (p : (α × β) × γ) ↦ m (n p.1.1 p.1.2) p.2) ((f ×ˢ g) ×ˢ h))
  (map ((fun (p : α × β × γ) ↦ m' p.1 (n' p.2.1 p.2.2)) ∘ (⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ))
    ((f ×ˢ g) ×ˢ h))
Tactic: rw [← map_prod_eq_map₂ n, ← map_prod_eq_map₂ n', map₂_map_left, map₂_map_right,
    ← map_prod_eq_map₂, ← map_prod_eq_map₂, ← prod_assoc, map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m' : α → γ → δ'
n' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)
⊢ map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h)
have rw : map₂ (fun (a : δ) (b : α) ↦ m b a) (map₂ n g h) f = map₂ n' g (map₂ (fun (a : γ) (b : α) ↦ m' b a) h f)
Tactic: rw [map₂_swap m', map₂_swap m]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g
have rw : map₂ m (map₂ (fun (a : β) (b : α) ↦ n b a) g f) h = map₂ (fun (a : β) (b : δ') ↦ n' b a) g (map₂ m' f h)
Tactic: rw [map₂_swap n, map₂_swap n']
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ f) (map n₂ g)
have simp_rw : map₂ (fun (a : α) (b : β) ↦ n (m a b)) f g = map₂ m' (map n₁ f) (map n₂ g)
Tactic: simp_rw [map_map₂, map₂_map_left, map₂_map_right, h_distrib]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
simp_rw : map₂ (fun (a : α) (b : β) ↦ n (m a b)) f g = map₂ m' (map n₁ f) (map n₂ g)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ f) (map n₂ g)
have simp_rw₁ : Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : α) (b : β) ↦ n (m a b)) f g)
  (map₂ (fun (a : α) (b : β') ↦ m' (n₁ a) b) f (map n₂ g))
Tactic: simp_rw [map_map₂, map₂_map_left, map₂_map_right, h_distrib]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
simp_rw : map₂ (fun (a : α) (b : β) ↦ n (m a b)) f g = map₂ m' (map n₁ f) (map n₂ g)
simp_rw₁ :
  Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : α) (b : β) ↦ n (m a b)) f g)
    (map₂ (fun (a : α) (b : β') ↦ m' (n₁ a) b) f (map n₂ g))
⊢ map n (map₂ m f g) = map₂ m' (map n₁ f) (map n₂ g)
have simp_rw₂ : Eq.{u_7 + 1} (α := Filter δ) (map₂ (fun (a : α) (b : β) ↦ n (m a b)) f g)
  (map₂ (fun (a : α) (b : β) ↦ m' (n₁ a) (n₂ b)) f g)
Tactic: simp_rw [map_map₂, map₂_map_left, map₂_map_right, h_distrib]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ s ∈ map₂ m f (map₂ n g h)
have refine : image2 m (u₁ ∩ u₂) (image2 n v w) ⊆ s
Tactic: refine ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂, _, image2_mem_map₂ hv hw, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m (u₁ ∩ u₂) (image2 n v w) ⊆ s
have refine_1 : image2 m₁ (u₁ ∩ u₂) v ⊆ t₁
Tactic: refine (image2_distrib_subset_left h_distrib).trans ((image2_subset ?_ ?_).trans hs)
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
γ' : Type u_6
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
u₁ : Set α
hu₁ : u₁ ∈ f
v : Set β
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
t₂ : Set γ'
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
hu₂ : u₂ ∈ f
w : Set γ
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
refine_1 : image2 m₁ (u₁ ∩ u₂) v ⊆ t₁
⊢ image2 m (u₁ ∩ u₂) (image2 n v w) ⊆ s
have refine_2 : image2 m₂ (u₁ ∩ u₂) w ⊆ t₂
Tactic: refine (image2_distrib_subset_left h_distrib).trans ((image2_subset ?_ ?_).trans hs)
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ s ∈ map₂ m (map₂ n f g) h
have refine : image2 m (image2 n u v) (w₁ ∩ w₂) ⊆ s
Tactic: refine ⟨_, image2_mem_map₂ hu hv, w₁ ∩ w₂, inter_mem hw₁ hw₂, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ image2 m (image2 n u v) (w₁ ∩ w₂) ⊆ s
have refine_1 : image2 m₁ u (w₁ ∩ w₂) ⊆ t₁
Tactic: refine (image2_distrib_subset_right h_distrib).trans ((image2_subset ?_ ?_).trans hs)
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
refine_1 : image2 m₁ u (w₁ ∩ w₂) ⊆ t₁
⊢ image2 m (image2 n u v) (w₁ ∩ w₂) ⊆ s
have refine_2 : image2 m₂ v (w₁ ∩ w₂) ⊆ t₂
Tactic: refine (image2_distrib_subset_right h_distrib).trans ((image2_subset ?_ ?_).trans hs)
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : β' → α' → δ
n₁ : β → β'
n₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ g) (map n₂ f)
have rw : map n (map₂ (fun (a : β) (b : α) ↦ m b a) g f) = map₂ m' (map n₁ g) (map n₂ f)
Tactic: rw [map₂_swap m]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
l : Filter β
⊢ map₂ f (pure a) l = l
have rw : map (f a) l = l
Tactic: rw [map₂_pure_left, show f a = id from funext h, map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
l : Filter β
rw : map (f a) l = l
⊢ map₂ f (pure a) l = l
have rw₁ : map id l = l
Tactic: rw [map₂_pure_left, show f a = id from funext h, map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
l : Filter β
rw : map (f a) l = l
rw₁ : map id l = l
⊢ map₂ f (pure a) l = l
have rw₂ : l = l
Tactic: rw [map₂_pure_left, show f a = id from funext h, map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
l : Filter α
⊢ map₂ f l (pure b) = l
have rw : map (fun (x : α) ↦ f x b) l = l
Tactic: rw [map₂_pure_right, funext h, map_id']
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
l : Filter α
rw : map (fun (x : α) ↦ f x b) l = l
⊢ map₂ f l (pure b) = l
have rw₁ : map (fun (x : α) ↦ x) l = l
Tactic: rw [map₂_pure_right, funext h, map_id']
-- Lean 4 proof step from Mathlib.Order.Filter.NAry (goal)
Goal:
α : Type u_1
β : Type u_3
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
l : Filter α
rw : map (fun (x : α) ↦ f x b) l = l
rw₁ : map (fun (x : α) ↦ x) l = l
⊢ map₂ f l (pure b) = l
have rw₂ : l = l
Tactic: rw [map₂_pure_right, funext h, map_id']
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
x y : Set β
hs : Membership.mem (γ := Set (Set β)) {s : Set β | r.core s ∈ l} x
ht : Membership.mem (γ := Set (Set β)) {s : Set β | r.core s ∈ l} y
⊢ Membership.mem (γ := Set (Set β)) {s : Set β | r.core s ∈ l} (x ∩ y)
have simp : r.core (x ∩ y) ∈ l
Tactic: simp only [Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
x y : Set β
hs : Membership.mem (γ := Set (Set β)) {s : Set β | r.core s ∈ l} x
ht : Membership.mem (γ := Set (Set β)) {s : Set β | r.core s ∈ l} y
⊢ r.core (x ∩ y) ∈ l
have h : r.core (x ∩ y) = r.core x ∩ r.core y
Tactic: convert! inter_mem hs ht
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
x y : Set β
hs : Membership.mem (γ := Set (Set β)) {s : Set β | r.core s ∈ l} x
ht : Membership.mem (γ := Set (Set β)) {s : Set β | r.core s ∈ l} y
⊢ r.core (x ∩ y) = r.core x ∩ r.core y
have h : r.core (x ∩ y) = r.core (x ∩ y)
Tactic: rw [← SetRel.core_inter]
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
⊢ (rcomap r (rcomap s l)).sets = (rcomap (r.comp s) l).sets
have h : ∀ (t : Set α), t ∈ (rcomap r (rcomap s l)).sets ↔ t ∈ (rcomap (r.comp s) l).sets
Tactic: ext t
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ t ∈ (rcomap r (rcomap s l)).sets ↔ t ∈ (rcomap (r.comp s) l).sets
have h : (∃ (a : Set β), (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.core a ⊆ t) ↔ ∃ a ∈ l, r.core (s.core a) ⊆ t
Tactic: simp only [rcomap_sets, SetRel.image, Filter.mem_sets, Set.mem_setOf_eq, SetRel.core_comp]
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ (∃ (a : Set β), (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.core a ⊆ t) ↔ ∃ a ∈ l, r.core (s.core a) ⊆ t
have h : (∃ (a : Set β), (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.core a ⊆ t) → ∃ a ∈ l, r.core (s.core a) ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
h : (∃ (a : Set β), (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.core a ⊆ t) → ∃ a ∈ l, r.core (s.core a) ⊆ t
⊢ (∃ (a : Set β), (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.core a ⊆ t) ↔ ∃ a ∈ l, r.core (s.core a) ⊆ t
have h₁ : (∃ a ∈ l, r.core (s.core a) ⊆ t) → ∃ (a : Set β), (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.core a ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto r l₁ l₂ ↔ l₁ ≤ rcomap r l₂
have rw : (∀ s ∈ l₂, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂
Tactic: rw [rtendsto_def]
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂.sets, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂
have mp : (∀ s ∈ l₂.sets, r.core s ∈ l₁) → l₁ ≤ rcomap r l₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
mp : (∀ s ∈ l₂.sets, r.core s ∈ l₁) → l₁ ≤ rcomap r l₂
⊢ (∀ s ∈ l₂.sets, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂
have mpr : l₁ ≤ rcomap r l₂ → ∀ s ∈ l₂.sets, r.core s ∈ l₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ t ∈ rcomap' r (rcomap' s l) ↔ t ∈ rcomap' (r.comp s) l
have simp : (∃ (t_1 : Set β), (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) ↔ ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t
Tactic: simp only [mem_rcomap', SetRel.preimage_comp]
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
⊢ (∃ (t_1 : Set β), (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) ↔ ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t
have mp : (∃ (t_1 : Set β), (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) → ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
mp : (∃ (t_1 : Set β), (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) → ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t
⊢ (∃ (t_1 : Set β), (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t) ↔ ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t
have mpr : (∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t) → ∃ (t_1 : Set β), (∃ t ∈ l, s.preimage t ⊆ t_1) ∧ r.preimage t_1 ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤
      {
        sets :=
          SetRel.image
            {x : Prod.{v, u} (Set β) (Set α) |
              match (motive := Prod.{v, u} (Set β) (Set α) → Prop) x with
              | (s, t) => r.preimage s ⊆ t}
            l₂.sets,
        univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ↔
    ∀ s ∈ l₂, r.preimage s ∈ l₁
have mp : l₁ ≤
    {
      sets :=
        SetRel.image
          {x : Prod.{v, u} (Set β) (Set α) |
            match (motive := Prod.{v, u} (Set β) (Set α) → Prop) x with
            | (s, t) => r.preimage s ⊆ t}
          l₂.sets,
      univ_sets := sorry, sets_of_superset := sorry, inter_sets := sorry } →
  ∀ s ∈ l₂, r.preimage s ∈ l₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
mp :
  l₁ ≤
      {
        sets :=
          SetRel.image
            {x : Prod.{v, u} (Set β) (Set α) |
              match (motive := Prod.{v, u} (Set β) (Set α) → Prop) x with
              | (s, t) => r.preimage s ⊆ t}
            l₂.sets,
        univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } →
    ∀ s ∈ l₂, r.preimage s ∈ l₁
⊢ l₁ ≤
      {
        sets :=
          SetRel.image
            {x : Prod.{v, u} (Set β) (Set α) |
              match (motive := Prod.{v, u} (Set β) (Set α) → Prop) x with
              | (s, t) => r.preimage s ⊆ t}
            l₂.sets,
        univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ↔
    ∀ s ∈ l₂, r.preimage s ∈ l₁
have mpr : (∀ s ∈ l₂, r.preimage s ∈ l₁) →
  l₁ ≤
    {
      sets :=
        SetRel.image
          {x : Prod.{v, u} (Set β) (Set α) |
            match (motive := Prod.{v, u} (Set β) (Set α) → Prop) x with
            | (s, t) => r.preimage s ⊆ t}
          l₂.sets,
      univ_sets := sorry, sets_of_superset := sorry, inter_sets := sorry }
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
⊢ pmap (PFun.res f s) l = map f (l ⊓ 𝓟 s)
have h : ∀ (t : Set β), t ∈ pmap (PFun.res f s) l ↔ t ∈ map f (l ⊓ 𝓟 s)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
t : Set β
⊢ t ∈ pmap (PFun.res f s) l ↔ t ∈ map f (l ⊓ 𝓟 s)
have h : sᶜ ∪ f ⁻¹' t ∈ l ↔ {x : α | x ∉ s ∨ x ∈ f ⁻¹' t} ∈ l
Tactic: simp only [PFun.core_res, mem_pmap, mem_map, mem_inf_principal, imp_iff_not_or]
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ PTendsto (PFun.res f Set.univ) l₁ l₂
have rw : Tendsto f l₁ l₂ ↔ Tendsto f (l₁ ⊓ 𝓟 Set.univ) l₂
Tactic: rw [← tendsto_iff_ptendsto]
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ PTendsto' f l₁ l₂ → PTendsto f l₁ l₂
have rw : (∀ s ∈ l₂, f.preimage s ∈ l₁) → ∀ s ∈ l₂, f.core s ∈ l₁
Tactic: rw [ptendsto_def, ptendsto'_def]
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
⊢ PTendsto f l₁ l₂ → PTendsto' f l₁ l₂
have rw : (∀ s ∈ l₂, f.core s ∈ l₁) → ∀ s ∈ l₂, f.preimage s ∈ l₁
Tactic: rw [ptendsto_def, ptendsto'_def]
-- Lean 4 proof step from Mathlib.Order.Filter.Partial (goal)
Goal:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
h' : ∀ s ∈ l₂, f.core s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ f.preimage s ∈ l₁
have rw : f.core s ∩ f.Dom ∈ l₁
Tactic: rw [PFun.preimage_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : Type u_3
m : β → (i : ι) → α i
l : Filter β
⊢ Tendsto m l (pi (α := α) f) ↔ ∀ (i : ι), Tendsto (fun (x : β) ↦ m x i) l (f i)
have simp : (∀ (i : ι), Tendsto (eval (β := α) i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun (x : β) ↦ m x i) l (f i)
Tactic: simp only [pi, tendsto_iInf, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
⊢ I.pi (α := α) s ∈ pi (α := α) f
have rw : ⋂ (x : (↑I : Type u_1)), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) ∈ pi (α := α) f
Tactic: rw [pi_def, biInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
I : Set ι
hI : I.Finite
h : ∀ i ∈ I, s i ∈ f i
⊢ ⋂ (x : (↑I : Type u_1)), eval (β := α) (↑x : ι) ⁻¹' s (↑x : ι) ∈ pi (α := α) f
have refine : ∀ (i : (↑I : Type u_1)), eval (β := α) (↑i : ι) ⁻¹' s (↑i : ι) ∈ comap (eval (β := α) (↑i : ι)) (f (↑i : ι))
Tactic: refine mem_iInf_of_iInter hI (fun i => ?_) Subset.rfl
-- Lean 4 proof step from Mathlib.Order.Filter.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi (α := α) f ↔
    ∃ (I : Set ι), I.Finite ∧ ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ I.pi (α := α) t ⊆ s
have mp : s ∈ pi (α := α) f → ∃ (I : Set ι), I.Finite ∧ ∃ (t : (i : ι) → Set (α i)), (∀ (i : ι), t i ∈ f i) ∧ I.pi (α := α) t ⊆ s
Tactic: constructor