awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.NAry
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

Tactic:
⟨_, image2_mem_map₂ hu hv, w₁ ∩ w₂, inter_mem hw₁ hw₂, ?_⟩

Premises used: Filter.image2_mem_map₂, Set.Mem, Filter.inter_mem, setOf, Inter.inter, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.NAry
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 : image2 m (image2 n u v) (w₁ ∩ w₂) ⊆ s
⊢ s ∈ map₂ m (map₂ n f g) h

Tactic:
refine ⟨_, image2_mem_map₂ hu hv, w₁ ∩ w₂, inter_mem hw₁ hw₂, ?_⟩
-- Module: Mathlib.Order.Filter.NAry
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

Tactic:
(image2_distrib_subset_right h_distrib).trans ((image2_subset ?_ ?_).trans hs)

Premises used: Set.image2_subset, Set.image2_distrib_subset_right, HasSubset.Subset.trans
-- Module: Mathlib.Order.Filter.NAry
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₁
refine_2 : image2 m₂ v (w₁ ∩ w₂) ⊆ t₂
⊢ image2 m (image2 n u v) (w₁ ∩ w₂) ⊆ s

Tactic:
refine (image2_distrib_subset_right h_distrib).trans ((image2_subset ?_ ?_).trans hs)

Premises used: Set.image2_subset, Set.image2_distrib_subset_right, HasSubset.Subset.trans
-- Module: Mathlib.Order.Filter.NAry
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₁ u (w₁ ∩ w₂) ⊆ t₁

Tactic:
(image2_subset_left inter_subset_left).trans ht₁

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.image2_subset_left
-- Module: Mathlib.Order.Filter.NAry
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₁ u (w₁ ∩ w₂) ⊆ t₁

Tactic:
exact (image2_subset_left inter_subset_left).trans ht₁

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.image2_subset_left
-- Module: Mathlib.Order.Filter.NAry
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₂ v (w₁ ∩ w₂) ⊆ t₂

Tactic:
(image2_subset_left inter_subset_right).trans ht₂

Premises used: HasSubset.Subset.trans, Set.image2_subset_left, Set.inter_subset_right
-- Module: Mathlib.Order.Filter.NAry
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₂ v (w₁ ∩ w₂) ⊆ t₂

Tactic:
exact (image2_subset_left inter_subset_right).trans ht₂

Premises used: HasSubset.Subset.trans, Set.image2_subset_left, Set.inter_subset_right
-- Module: Mathlib.Order.Filter.NAry
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)
rw : map n (map₂ (fun (a : β) (b : α) ↦ m b a) g f) = map₂ m' (map n₁ g) (map n₂ f)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ g) (map n₂ f)

Tactic:
rw [map₂_swap m]

Premises used: Filter.map₂_swap
-- Module: Mathlib.Order.Filter.NAry
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₂ (fun (a : β) (b : α) ↦ m b a) g f) = map₂ m' (map n₁ g) (map n₂ f)

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

Premises used: Filter.map_map₂_distrib
-- Module: Mathlib.Order.Filter.NAry
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₂ (fun (a : β) (b : α) ↦ m b a) g f) = map₂ m' (map n₁ g) (map n₂ f)

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

Premises used: Filter.map_map₂_distrib
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : β' → α → δ
n' : β → β'
h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n' b) a
⊢ map n (map₂ m f g) = map₂ m' (map n' g) f

Tactic:
map_map₂_antidistrib h_antidistrib

Premises used: Set.Mem, Filter.map, setOf, Set.preimage, Filter.map_map₂_antidistrib
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : β → α' → δ
n' : α → α'
h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' b (n' a)
⊢ map n (map₂ m f g) = map₂ m' g (map n' f)

Tactic:
map_map₂_antidistrib h_antidistrib

Premises used: Set.Mem, Filter.map, setOf, Set.preimage, Filter.map_map₂_antidistrib
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α' → β → γ
n : α → α'
m' : β → α → δ
n' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), m (n a) b = n' (m' b a)
⊢ map₂ m (map n f) g = map n' (map₂ m' g f)

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

Premises used: Filter.map_map₂_antidistrib_left, Eq.symm
-- Module: Mathlib.Order.Filter.NAry
Goal:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : Filter α
g : Filter β
m : α → β' → γ
n : β → β'
m' : β → α → δ
n' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), m a (n b) = n' (m' b a)
⊢ map₂ m f (map n g) = map n' (map₂ m' g f)

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

Premises used: Filter.map_map₂_antidistrib_right, Eq.symm
-- Module: Mathlib.Order.Filter.NAry
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
rw₂ rw₃ : l = l
⊢ map₂ f (pure a) l = l

Tactic:
rw [map₂_pure_left, show f a = id from funext h, map_id]

Premises used: Filter.map₂_pure_left, funext, Filter.map_id
-- Module: Mathlib.Order.Filter.NAry
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
rw₂ rw₃ : l = l
⊢ map₂ f l (pure b) = l

Tactic:
rw [map₂_pure_right, funext h, map_id']

Premises used: funext, Filter.map_id', Filter.map₂_pure_right
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
l : Filter α
⊢ Membership.mem (γ := Set (Set β)) {s : Set β | r.core s ∈ l} Set.univ

Tactic:
simp
-- Module: Mathlib.Order.Filter.Partial
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
simp : r.core (x ∩ y) ∈ l
⊢ Membership.mem (γ := Set (Set β)) {s : Set β | r.core s ∈ l} (x ∩ y)

Tactic:
simp only [Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Order.Filter.Partial
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 ∩ r.core y ∈ l

Tactic:
inter_mem hs ht

Premises used: Filter.inter_mem
-- Module: Mathlib.Order.Filter.Partial
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
h : r.core (x ∩ y) = r.core x ∩ r.core y
⊢ r.core (x ∩ y) ∈ l

Tactic:
convert! inter_mem hs ht

Premises used: Filter.inter_mem
-- Module: Mathlib.Order.Filter.Partial
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
h h₁ : r.core (x ∩ y) = r.core (x ∩ y)
⊢ r.core (x ∩ y) = r.core x ∩ r.core y

Tactic:
rw [← SetRel.core_inter]

Premises used: SetRel.core_inter
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
r : SetRel α β
l : Filter α
⊢ (rmap r l).sets = r.core ⁻¹' l.sets

Tactic:
rfl

Premises used: setOf, Set.preimage, rfl
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
r : SetRel α β
l : Filter α
s : Set β
⊢ s ∈ rmap r l ↔ r.core s ∈ l

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter α
⊢ (rmap s (rmap r l)).sets = (rmap (r.comp s) l).sets

Tactic:
simp [rmap_sets, Set.preimage, SetRel.core_comp]

Premises used: SetRel.core_comp, Set.preimage, Filter.rmap_sets
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
⊢ rmap s ∘ rmap r = rmap (r.comp s)

Tactic:
funext <| rmap_rmap _ _

Premises used: funext, Filter.rmap_rmap
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto r l₁ l₂ ↔ ∀ s ∈ l₂, r.core s ∈ l₁

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Filter.RTendsto
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
r : SetRel α β
f : Filter β
⊢ (rcomap r f).sets =
    SetRel.image
      {x : Prod.{v, u} (Set β) (Set α) |
        match (motive := Prod.{v, u} (Set β) (Set α) → Prop) x with
        | (s, t) => r.core s ⊆ t}
      f.sets

Tactic:
rfl

Premises used: setOf, SetRel.image, rfl
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
h : ∀ (t : Set α), t ∈ (rcomap r (rcomap s l)).sets ↔ t ∈ (rcomap (r.comp s) l).sets
⊢ (rcomap r (rcomap s l)).sets = (rcomap (r.comp s) l).sets

Tactic:
ext t
-- Module: Mathlib.Order.Filter.Partial
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
⊢ t ∈ (rcomap r (rcomap s l)).sets ↔ t ∈ (rcomap (r.comp s) l).sets

Tactic:
simp only [rcomap_sets, SetRel.image, Filter.mem_sets, Set.mem_setOf_eq, SetRel.core_comp]

Premises used: Filter.mem_sets, Filter.rcomap_sets, SetRel.core_comp, Set.mem_setOf_eq, SetRel.image
-- Module: Mathlib.Order.Filter.Partial
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
h₁ : (∃ a ∈ l, r.core (s.core a) ⊆ t) → ∃ (a : Set β), (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.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

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
u : Set β
h : r.core u ⊆ t
v : Set γ
vsets : v ∈ l
hv : s.core v ⊆ u
⊢ ∃ a ∈ l, r.core (s.core a) ⊆ t

Tactic:
⟨v, vsets, Set.Subset.trans (SetRel.core_mono hv) h⟩

Premises used: SetRel.core_mono, Set.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
u : Set β
h : r.core u ⊆ t
v : Set γ
vsets : v ∈ l
hv : s.core v ⊆ u
⊢ ∃ a ∈ l, r.core (s.core a) ⊆ t

Tactic:
exact ⟨v, vsets, Set.Subset.trans (SetRel.core_mono hv) h⟩
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t_1 : Set α
t : Set γ
tsets : t ∈ l
ht : r.core (s.core t) ⊆ t_1
⊢ ∃ (a : Set β), (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.core a ⊆ t_1

Tactic:
⟨SetRel.core s t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩

Premises used: SetRel.core, Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t_1 : Set α
t : Set γ
tsets : t ∈ l
ht : r.core (s.core t) ⊆ t_1
⊢ ∃ (a : Set β), (∃ a_1 ∈ l, s.core a_1 ⊆ a) ∧ r.core a ⊆ t_1

Tactic:
exact ⟨SetRel.core s t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
⊢ rcomap r ∘ rcomap s = rcomap (r.comp s)

Tactic:
funext <| rcomap_rcomap _ _

Premises used: funext, Filter.rcomap_rcomap
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
rw : (∀ s ∈ l₂, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂
⊢ RTendsto r l₁ l₂ ↔ l₁ ≤ rcomap r l₂

Tactic:
rw [rtendsto_def]

Premises used: Filter.rtendsto_def
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
mp : (∀ s ∈ l₂.sets, r.core s ∈ l₁) → l₁ ≤ rcomap r l₂
mpr : l₁ ≤ rcomap r l₂ → ∀ s ∈ l₂.sets, r.core s ∈ l₁
⊢ (∀ s ∈ l₂.sets, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂.sets, r.core s ∈ l₁) → l₁ ≤ rcomap r l₂

Tactic:
simpa [Filter.le_def, rcomap, SetRel.mem_image]
      using fun h s t tl₂ => mem_of_superset (h t tl₂)

Premises used: SetRel.mem_image, Filter.rcomap, Filter.le_def, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤ rcomap r l₂ → ∀ s ∈ l₂.sets, r.core s ∈ l₁

Tactic:
simpa [Filter.le_def, rcomap, SetRel.mem_image]
      using fun h t tl₂ => h _ t tl₂ Set.Subset.rfl

Premises used: SetRel.mem_image, Filter.rcomap, Filter.le_def
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
r : SetRel α β
l : Filter β
s : Set α
⊢ s ∈ rcomap' r l ↔ ∃ t ∈ l, r.preimage t ⊆ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SetRel.image
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
r : SetRel α β
f : Filter β
⊢ (rcomap' r f).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}
      f.sets

Tactic:
rfl

Premises used: setOf, SetRel.image, rfl
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
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
⊢ t ∈ rcomap' r (rcomap' s l) ↔ t ∈ rcomap' (r.comp s) l

Tactic:
simp only [mem_rcomap', SetRel.preimage_comp]

Premises used: SetRel.preimage_comp, Filter.mem_rcomap'
-- Module: Mathlib.Order.Filter.Partial
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
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
⊢ (∃ (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
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
u : Set β
h : r.preimage u ⊆ t
v : Set γ
vsets : v ∈ l
hv : s.preimage v ⊆ u
⊢ ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t

Tactic:
⟨v, vsets, (SetRel.preimage_mono hv).trans h⟩

Premises used: SetRel.preimage_mono, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
u : Set β
h : r.preimage u ⊆ t
v : Set γ
vsets : v ∈ l
hv : s.preimage v ⊆ u
⊢ ∃ t_1 ∈ l, r.preimage (s.preimage t_1) ⊆ t

Tactic:
exact ⟨v, vsets, (SetRel.preimage_mono hv).trans h⟩
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t_1 : Set α
t : Set γ
tsets : t ∈ l
ht : r.preimage (s.preimage t) ⊆ t_1
⊢ ∃ (t : Set β), (∃ t_2 ∈ l, s.preimage t_2 ⊆ t) ∧ r.preimage t ⊆ t_1

Tactic:
⟨s.preimage t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro, SetRel.preimage
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t_1 : Set α
t : Set γ
tsets : t ∈ l
ht : r.preimage (s.preimage t) ⊆ t_1
⊢ ∃ (t : Set β), (∃ t_2 ∈ l, s.preimage t_2 ⊆ t) ∧ r.preimage t ⊆ t_1

Tactic:
exact ⟨s.preimage t, ⟨t, tsets, Set.Subset.rfl⟩, ht⟩
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
⊢ rcomap' r ∘ rcomap' s = rcomap' (r.comp s)

Tactic:
funext <| rcomap'_rcomap' _ _

Premises used: Filter.rcomap'_rcomap', funext
-- Module: Mathlib.Order.Filter.Partial
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₁
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 := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
⊢ 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₁

Tactic:
constructor
-- Module: Mathlib.Order.Filter.Partial
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₁

Tactic:
simpa [le_def, SetRel.mem_image] using fun h s hs => h _ _ hs Set.Subset.rfl

Premises used: SetRel.mem_image, Filter.le_def
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
r : SetRel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ 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 := ⋯ }

Tactic:
simpa [le_def, SetRel.mem_image] using fun h s t ht => mem_of_superset (h t ht)

Premises used: SetRel.mem_image, Filter.le_def, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ RTendsto (Function.graph f) l₁ l₂

Tactic:
simp [tendsto_def, Function.graph, rtendsto_def, SetRel.core, Set.preimage]

Premises used: Filter.rtendsto_def, Filter.tendsto_def, Function.graph, SetRel.core, Set.preimage
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ RTendsto' (Function.graph f) l₁ l₂

Tactic:
simp [tendsto_def, Function.graph, rtendsto'_def, SetRel.preimage, Set.preimage]

Premises used: Filter.tendsto_def, Filter.rtendsto'_def, Function.graph, Set.preimage, SetRel.preimage
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
f : α →. β
l : Filter α
s : Set β
⊢ s ∈ pmap f l ↔ f.core s ∈ l

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, PFun.core
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ PTendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f.core s ∈ l₁

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, PFun.core, Filter.PTendsto
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α →. β
⊢ PTendsto f l₁ l₂ ↔ RTendsto f.graph' l₁ l₂

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Filter.RTendsto, Filter.PTendsto
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
h : ∀ (t : Set β), t ∈ pmap (PFun.res f s) l ↔ t ∈ map f (l ⊓ 𝓟 s)
⊢ pmap (PFun.res f s) l = map f (l ⊓ 𝓟 s)

Tactic:
ext t
-- Module: Mathlib.Order.Filter.Partial
Goal:
α : Type u
β : Type v
l : Filter α
s : Set α
f : α → β
t : Set β
h : sᶜ ∪ f ⁻¹' t ∈ l ↔ {x : α | x ∉ s ∨ x ∈ f ⁻¹' t} ∈ l
⊢ t ∈ pmap (PFun.res f s) l ↔ t ∈ map f (l ⊓ 𝓟 s)

Tactic:
simp only [PFun.core_res, mem_pmap, mem_map, mem_inf_principal, imp_iff_not_or]

Premises used: imp_iff_not_or, Filter.mem_pmap, Filter.mem_inf_principal, PFun.core_res, Filter.mem_map