awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
f : Filter α
simp_rw : f.smallSets = ⨅ s ∈ powerset '' f.sets, 𝓟 s
⊢ f.smallSets = generate (powerset '' f.sets)
have simp_rw₁ : f.lift' powerset = ⨅ s ∈ powerset '' f.sets, 𝓟 s
Tactic: simp_rw [generate_eq_biInf, smallSets, iInf_image, Filter.lift', Filter.lift, Function.comp_apply,
    Filter.mem_sets]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
f : Filter α
simp_rw : f.smallSets = ⨅ s ∈ powerset '' f.sets, 𝓟 s
simp_rw₁ : f.lift' powerset = ⨅ s ∈ powerset '' f.sets, 𝓟 s
⊢ f.smallSets = generate (powerset '' f.sets)
have simp_rw₂ : f.lift' powerset = ⨅ b ∈ f.sets, 𝓟 (𝒫 b)
Tactic: simp_rw [generate_eq_biInf, smallSets, iInf_image, Filter.lift', Filter.lift, Function.comp_apply,
    Filter.mem_sets]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
f : Filter α
simp_rw : f.smallSets = ⨅ s ∈ powerset '' f.sets, 𝓟 s
simp_rw₁ : f.lift' powerset = ⨅ s ∈ powerset '' f.sets, 𝓟 s
simp_rw₂ : f.lift' powerset = ⨅ b ∈ f.sets, 𝓟 (𝒫 b)
⊢ f.smallSets = generate (powerset '' f.sets)
have simp_rw₃ : f.lift (𝓟 ∘ powerset) = ⨅ b ∈ f.sets, 𝓟 (𝒫 b)
Tactic: simp_rw [generate_eq_biInf, smallSets, iInf_image, Filter.lift', Filter.lift, Function.comp_apply,
    Filter.mem_sets]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
f : Filter α
simp_rw : f.smallSets = ⨅ s ∈ powerset '' f.sets, 𝓟 s
simp_rw₁ : f.lift' powerset = ⨅ s ∈ powerset '' f.sets, 𝓟 s
simp_rw₂ : f.lift' powerset = ⨅ b ∈ f.sets, 𝓟 (𝒫 b)
simp_rw₃ : f.lift (𝓟 ∘ powerset) = ⨅ b ∈ f.sets, 𝓟 (𝒫 b)
⊢ f.smallSets = generate (powerset '' f.sets)
have simp_rw₄ : Eq.{u_1 + 1} (α := Filter (Set α)) (⨅ s ∈ f, (𝓟 ∘ powerset) s) (⨅ b ∈ f.sets, 𝓟 (𝒫 b))
Tactic: simp_rw [generate_eq_biInf, smallSets, iInf_image, Filter.lift', Filter.lift, Function.comp_apply,
    Filter.mem_sets]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
f : Filter α
simp_rw : f.smallSets = ⨅ s ∈ powerset '' f.sets, 𝓟 s
simp_rw₁ : f.lift' powerset = ⨅ s ∈ powerset '' f.sets, 𝓟 s
simp_rw₂ : f.lift' powerset = ⨅ b ∈ f.sets, 𝓟 (𝒫 b)
simp_rw₃ : f.lift (𝓟 ∘ powerset) = ⨅ b ∈ f.sets, 𝓟 (𝒫 b)
simp_rw₄ : Eq.{u_1 + 1} (α := Filter (Set α)) (⨅ s ∈ f, (𝓟 ∘ powerset) s) (⨅ b ∈ f.sets, 𝓟 (𝒫 b))
⊢ f.smallSets = generate (powerset '' f.sets)
have simp_rw₅ : Eq.{u_1 + 1} (α := Filter (Set α)) (⨅ s ∈ f, 𝓟 (𝒫 s)) (⨅ b ∈ f.sets, 𝓟 (𝒫 b))
Tactic: simp_rw [generate_eq_biInf, smallSets, iInf_image, Filter.lift', Filter.lift, Function.comp_apply,
    Filter.mem_sets]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
L : Filter (Set α)
l : Filter α
⊢ (fun (L : Filter (Set α)) ↦ L.bind 𝓟) L ≤ l ↔ L ≤ l.smallSets
have simp_rw : L.bind 𝓟 ≤ l ↔ l.sets ⊆ powerset ⁻¹' L.sets
Tactic: simp_rw [smallSets_eq_generate, le_generate_iff, image_subset_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q t → q s
⊢ (∀ᶠ (s : Set α) in l.smallSets, q s) ↔ ∃ (i : ι), p i ∧ q (s i)
have rw : (∃ s ∈ l, q s) ↔ ∃ (i : ι), p i ∧ q (s i)
Tactic: rw [l.eventually_smallSets' hq, hl.exists_iff hq]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q t → q s
rw : (∃ s ∈ l, q s) ↔ ∃ (i : ι), p i ∧ q (s i)
⊢ (∀ᶠ (s : Set α) in l.smallSets, q s) ↔ ∃ (i : ι), p i ∧ q (s i)
have rw₁ : (∃ (i : ι), p i ∧ q (s i)) ↔ ∃ (i : ι), p i ∧ q (s i)
Tactic: rw [l.eventually_smallSets' hq, hl.exists_iff hq]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_4
l : Filter α
p : Set α → Prop
hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t
⊢ (∃ᶠ (s : Set α) in l.smallSets, p s) ↔ ∀ t ∈ l, p t
have h : (∀ t ∈ l, p t) ↔ ¬∃ s ∈ l, (fun (x : Set α) ↦ ¬p x) s
Tactic: convert! not_iff_not.mpr <| l.eventually_smallSets' (p := (¬p ·)) (by tauto)
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q s → q t
⊢ (∃ᶠ (s : Set α) in l.smallSets, q s) ↔ ∀ (i : ι), p i → q (s i)
have rw : (∀ t ∈ l, q t) ↔ ∀ (i : ι), p i → q (s i)
Tactic: rw [Filter.frequently_smallSets' hq, hl.forall_iff hq]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_4
ι : Sort u_5
p : ι → Prop
l : Filter α
s : ι → Set α
q : Set α → Prop
hl : l.HasBasis p s
hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q s → q t
rw : (∀ t ∈ l, q t) ↔ ∀ (i : ι), p i → q (s i)
⊢ (∃ᶠ (s : Set α) in l.smallSets, q s) ↔ ∀ (i : ι), p i → q (s i)
have rw₁ : (∀ (i : ι), p i → q (s i)) ↔ ∀ (i : ι), p i → q (s i)
Tactic: rw [Filter.frequently_smallSets' hq, hl.forall_iff hq]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ Tendsto (fun (x : Set α) ↦ f '' x) la.smallSets lb.smallSets ↔ Tendsto f la lb
have rw : (∀ t ∈ lb, ∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ t) ↔ Tendsto f la lb
Tactic: rw [tendsto_smallSets_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ (∀ t ∈ lb, ∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ t) ↔ Tendsto f la lb
have refine : ∀ (u : Set β) (hu : u ∈ lb), (∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ u) ↔ u ∈ map f la
Tactic: refine forall₂_congr fun u hu ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
⊢ (∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ u) ↔ u ∈ map f la
have rw : (∃ s ∈ la, f '' s ⊆ u) ↔ u ∈ map f la
Tactic: rw [eventually_smallSets' fun s t hst ht ↦ (image_mono hst).trans ht]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Filter (Set α)) (smallSets ⊥) (pure ∅)
have rw : Monotone.{u_1, u_1} (α := Set α) powerset
Tactic: rw [smallSets, lift'_bot, powerset_empty, principal_singleton]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Filter (Set α)) (smallSets ⊤) ⊤
have rw : Eq.{u_1 + 1} (α := Filter (Set α)) (Filter.lift' ⊤ powerset) ⊤
Tactic: rw [smallSets, lift'_top, powerset_univ, principal_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
rw : Eq.{u_1 + 1} (α := Filter (Set α)) (Filter.lift' ⊤ powerset) ⊤
⊢ Eq.{u_1 + 1} (α := Filter (Set α)) (smallSets ⊤) ⊤
have rw₁ : Eq.{u_1 + 1} (α := Filter (Set α)) (𝓟 (𝒫 univ)) ⊤
Tactic: rw [smallSets, lift'_top, powerset_univ, principal_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
rw : Eq.{u_1 + 1} (α := Filter (Set α)) (Filter.lift' ⊤ powerset) ⊤
rw₁ : Eq.{u_1 + 1} (α := Filter (Set α)) (𝓟 (𝒫 univ)) ⊤
⊢ Eq.{u_1 + 1} (α := Filter (Set α)) (smallSets ⊤) ⊤
have rw₂ : Eq.{u_1 + 1} (α := Filter (Set α)) (𝓟 univ) ⊤
Tactic: rw [smallSets, lift'_top, powerset_univ, principal_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
rw : Eq.{u_1 + 1} (α := Filter (Set α)) (Filter.lift' ⊤ powerset) ⊤
rw₁ : Eq.{u_1 + 1} (α := Filter (Set α)) (𝓟 (𝒫 univ)) ⊤
rw₂ : Eq.{u_1 + 1} (α := Filter (Set α)) (𝓟 univ) ⊤
⊢ Eq.{u_1 + 1} (α := Filter (Set α)) (smallSets ⊤) ⊤
have rw₃ : Eq.{u_1 + 1} (α := Filter (Set α)) ⊤ ⊤
Tactic: rw [smallSets, lift'_top, powerset_univ, principal_univ]
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter β
f : α → β
⊢ (comap f l).smallSets = comap (image f) l.smallSets
have refine : ∀ (x : Filter (Set α)), map f (x.bind 𝓟) = (map (image f) x).bind 𝓟
Tactic: refine (gc_map_comap _).u_comm_of_l_comm (gc_map_comap _) bind_smallSets_gc bind_smallSets_gc ?_
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
l_1 l' la : Filter α
lb : Filter β
l : Filter α
⊢ l.smallSets.NeBot
have refine : Monotone.{u_1, u_1} (α := Set α) powerset
Tactic: refine (lift'_neBot_iff ?_).2 fun _ _ => powerset_nonempty
-- Lean 4 proof step from Mathlib.Order.Filter.SmallSets (goal)
Goal:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : Tendsto t la lb.smallSets
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ Tendsto s la lb.smallSets
have rw : ∀ (ht : ∀ t_1 ∈ lb, ∀ᶠ (x : α) in la, t x ⊆ t_1) (hst : ∀ᶠ (x : α) in la, s x ⊆ t x),
  ∀ t ∈ lb, ∀ᶠ (x : α) in la, s x ⊆ t
Tactic: rw [tendsto_smallSets_iff] at ht ⊢
Cleared hypotheses: ht, hst
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
la : Filter α
lb : Filter β
h : la.NeBot → Tendsto f la lb
⊢ Tendsto f la lb
have inl : ∀ (h : NeBot.{u_1} (α := α) ⊥ → Tendsto f ⊥ lb), Tendsto f ⊥ lb
Tactic: rcases eq_or_neBot la with rfl | hla
Cleared hypotheses: la, h
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ g ≤ map mab f
have rw : map mab (map mba g) ≤ map mab f
Tactic: rw [← @map_id _ g, ← map_congr h₁, ← map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
⊢ Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂
have rw : map f₁ l₁ ≤ l₂ ↔ Tendsto f₂ l₁ l₂
Tactic: rw [Tendsto, Tendsto, map_congr hl]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
rw : map f₁ l₁ ≤ l₂ ↔ Tendsto f₂ l₁ l₂
⊢ Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂
have rw₁ : map f₁ l₁ ≤ l₂ ↔ map f₂ l₁ ≤ l₂
Tactic: rw [Tendsto, Tendsto, map_congr hl]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
rw : map f₁ l₁ ≤ l₂ ↔ Tendsto f₂ l₁ l₂
rw₁ : map f₁ l₁ ≤ l₂ ↔ map f₂ l₁ ≤ l₂
⊢ Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂
have rw₂ : map f₂ l₁ ≤ l₂ ↔ map f₂ l₁ ≤ l₂
Tactic: rw [Tendsto, Tendsto, map_congr hl]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : Filter α
y : Filter γ
⊢ Tendsto f (map g x) y ↔ Tendsto (f ∘ g) x y
have rw : map f (map g x) ≤ y ↔ Tendsto (f ∘ g) x y
Tactic: rw [Tendsto, Tendsto, map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : Filter α
y : Filter γ
rw : map f (map g x) ≤ y ↔ Tendsto (f ∘ g) x y
⊢ Tendsto f (map g x) y ↔ Tendsto (f ∘ g) x y
have rw₁ : map f (map g x) ≤ y ↔ map (f ∘ g) x ≤ y
Tactic: rw [Tendsto, Tendsto, map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
x : Filter α
y : Filter γ
rw : map f (map g x) ≤ y ↔ Tendsto (f ∘ g) x y
rw₁ : map f (map g x) ≤ y ↔ map (f ∘ g) x ≤ y
⊢ Tendsto f (map g x) y ↔ Tendsto (f ∘ g) x y
have rw₂ : map (f ∘ g) x ≤ y ↔ map (f ∘ g) x ≤ y
Tactic: rw [Tendsto, Tendsto, map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
c : Filter γ
h : Tendsto (g ∘ f) a c
⊢ map g (map f a) ≤ c
have rwa : map (g ∘ f) a ≤ c
Tactic: rwa [map_map]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α → β
f : Filter α
g : Filter β
i : γ → α
h : range i ∈ f
⊢ Tendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g
have rw : (map m ∘ map i) (comap i f) ≤ g ↔ Tendsto m f g
Tactic: rw [Tendsto, ← map_compose]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : Tendsto (g ∘ f) a c
hg : comap g c ≤ b
⊢ Tendsto f a b
have rw : ∀ (hfg : a ≤ comap (g ∘ f) c) (hg : comap g c ≤ b), a ≤ comap f b
Tactic: rw [tendsto_iff_comap] at hfg ⊢
Cleared hypotheses: hfg, hg
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
⊢ a ≤ comap f b
have a₁ : comap (g ∘ f) c ≤ comap f b
Tactic: calc
    a ≤ comap (g ∘ f) c := hfg
    _ ≤ comap f b := by simpa [comap_comap] using comap_mono hg
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap φ g = f
have refine : comap φ (comap ψ f) ≤ f
Tactic: refine ((comap_mono <| map_le_iff_le_comap.1 hψ).trans ?_).antisymm (map_le_iff_le_comap.1 hφ)
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap φ (comap ψ f) ≤ f
have rw : comap (ψ ∘ φ) f ≤ f
Tactic: rw [comap_comap, eq, comap_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
rw : comap (ψ ∘ φ) f ≤ f
⊢ comap φ (comap ψ f) ≤ f
have rw₁ : comap id f ≤ f
Tactic: rw [comap_comap, eq, comap_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
rw : comap (ψ ∘ φ) f ≤ f
rw₁ : comap id f ≤ f
⊢ comap φ (comap ψ f) ≤ f
have rw₂ : f ≤ f
Tactic: rw [comap_comap, eq, comap_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ map φ f = g
have refine : g ≤ map φ (map ψ g)
Tactic: refine le_antisymm hφ (le_trans ?_ (map_mono hψ))
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ g ≤ map φ (map ψ g)
have rw : g ≤ map (φ ∘ ψ) g
Tactic: rw [map_map, eq, map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
rw : g ≤ map (φ ∘ ψ) g
⊢ g ≤ map φ (map ψ g)
have rw₁ : g ≤ map id g
Tactic: rw [map_map, eq, map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
rw : g ≤ map (φ ∘ ψ) g
rw₁ : g ≤ map id g
⊢ g ≤ map φ (map ψ g)
have rw₂ : g ≤ g
Tactic: rw [map_map, eq, map_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : (x : α) → Decidable (p x)
h₀ : Tendsto f (l₁ ⊓ 𝓟 {x : α | p x}) l₂
h₁ : Tendsto g (l₁ ⊓ 𝓟 {x : α | ¬p x}) l₂
⊢ Tendsto (fun (x : α) ↦ if p x then f x else g x) l₁ l₂
have simp : ∀ (h₀ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | p x} x → x ∈ f ⁻¹' s} ∈ l₁)
  (h₁ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | ¬p x} x → x ∈ g ⁻¹' s} ∈ l₁),
  ∀ s ∈ l₂, (fun (x : α) ↦ if p x then f x else g x) ⁻¹' s ∈ l₁
Tactic: simp only [tendsto_def, mem_inf_principal] at *
Cleared hypotheses: h₀, h₁
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | p x} x → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | ¬p x} x → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
⊢ (fun (x : α) ↦ if p x then f x else g x) ⁻¹' s ∈ l₁
have h : ∀ (x : α) (hp₀ : p x → x ∈ f ⁻¹' s) (hp₁ : ¬p x → x ∈ g ⁻¹' s),
  Membership.mem (γ := Set α) ((fun (x : α) ↦ if p x then f x else g x) ⁻¹' s) x
Tactic: filter_upwards [h₀ s hs, h₁ s hs] with x hp₀ hp₁
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | p x} x → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | ¬p x} x → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
⊢ Membership.mem (γ := Set α) ((fun (x : α) ↦ if p x then f x else g x) ⁻¹' s) x
have h : (if p x then f x else g x) ∈ s
Tactic: rw [mem_preimage]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | p x} x → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | ¬p x} x → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
⊢ (if p x then f x else g x) ∈ s
have pos : ∀ (h : p x), f x ∈ s
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | p x} x → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x : α | Membership.mem (γ := Set α) {x : α | ¬p x} x → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
hp₁ : ¬p x → x ∈ g ⁻¹' s
pos : ∀ (h : p x), f x ∈ s
⊢ (if p x then f x else g x) ∈ s
have neg : ∀ (h : ¬p x), g x ∈ s
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ MapsTo m s t
have rw : Tendsto m (𝓟 s) (𝓟 t) ↔ MapsTo m s t
Tactic: rw [map_mapsTo_Iic_iff_tendsto, tendsto_principal_principal, MapsTo]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
rw : Tendsto m (𝓟 s) (𝓟 t) ↔ MapsTo m s t
⊢ MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ MapsTo m s t
have rw₁ : (∀ a ∈ s, m a ∈ t) ↔ MapsTo m s t
Tactic: rw [map_mapsTo_Iic_iff_tendsto, tendsto_principal_principal, MapsTo]
-- Lean 4 proof step from Mathlib.Order.Filter.Tendsto (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
rw : Tendsto m (𝓟 s) (𝓟 t) ↔ MapsTo m s t
rw₁ : (∀ a ∈ s, m a ∈ t) ↔ MapsTo m s t
⊢ MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ MapsTo m s t
have rw₂ : (∀ a ∈ s, m a ∈ t) ↔ ∀ ⦃x : α⦄, x ∈ s → m x ∈ t
Tactic: rw [map_mapsTo_Iic_iff_tendsto, tendsto_principal_principal, MapsTo]
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst : AddCommMonoid M
inst_1 : TendstoCofinite f
u v : α → M
⊢ mapDomain f (u + v) = mapDomain f u + mapDomain f v
have h : ∀ (x : β), mapDomain f (u + v) x = (mapDomain f u + mapDomain f v) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_5
f : α → β
inst : AddCommMonoid M
inst_1 : TendstoCofinite f
inst_2 : DistribSMul R M
r : R
v : α → M
⊢ mapDomain f (r • v) = r • mapDomain f v
have h : ∀ (x : β), mapDomain f (r • v) x = (r • mapDomain f v) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst : AddCommMonoid M
inst_1 : TendstoCofinite f
v : α → M
i : β
h' : i ∉ range f
⊢ mapDomain f v i = 0
have h'₁ : f ⁻¹' {i} = ∅
Tactic: rw [← Set.preimage_singleton_eq_empty] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
⊢ TendstoCofinite (α := α →₀ ℕ) (mapDomain f)
have refine : ∀ (x : β →₀ ℕ), Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
Tactic: refine (tendstoCofinite_iff_finite_preimage_singleton _).mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
⊢ Set.Finite (α := α →₀ ℕ) (mapDomain f ⁻¹' {x})
have refine : Subset (α := Set (α →₀ ℕ)) (mapDomain f ⁻¹' {x})
  (embDomain e ''
    {f : ↥s →₀ ℕ | LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) f : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)})
Tactic: refine Set.Finite.subset (Set.Finite.image (embDomain e) <| finite_of_degree_le (degree x)) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
⊢ ∀ (x_1 : α →₀ ℕ),
    mapDomain f x_1 = x →
      ∃ (x_2 : ↥s →₀ ℕ),
        LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) x_2 : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ) ∧
          embDomain e x_2 = x_1
have refine_1 : ∀ (y : α →₀ ℕ) (hy : mapDomain f y = x),
  LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) (comapDomain (⇑e : (a : ↥s) → α) y sorry) : ℕ)
    ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)
Tactic: refine fun y hy ↦ ⟨y.comapDomain e e.injective.injOn, ?_, embDomain_comapDomain ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
refine_1 :
  ∀ (y : α →₀ ℕ) (hy : mapDomain f y = x),
    LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) (comapDomain (⇑e : (a : ↥s) → α) y ⋯) : ℕ)
      ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)
⊢ ∀ (x_1 : α →₀ ℕ),
    mapDomain f x_1 = x →
      ∃ (x_2 : ↥s →₀ ℕ),
        LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) x_2 : ℕ) ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ) ∧
          embDomain e x_2 = x_1
have refine_2 : ∀ (y : α →₀ ℕ) (hy : mapDomain f y = x), (↑y.support : Set α) ⊆ range (ι := ↥s) (⇑e : (a : ↥s) → α)
Tactic: refine fun y hy ↦ ⟨y.comapDomain e e.injective.injOn, ?_, embDomain_comapDomain ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) (comapDomain (⇑e : (a : ↥s) → α) y ⋯) : ℕ)
    ((degree : (a : β →₀ ℕ) → ℕ) x : ℕ)
have refine_1 : LE.le (α := ℕ) ((degree : (a : ↥s →₀ ℕ) → ℕ) (comapDomain (⇑e : (a : ↥s) → α) y sorry) : ℕ)
  ((degree : (a : α →₀ ℕ) → ℕ) y : ℕ)
Tactic: rw [← hy, degree_mapDomain]
-- Lean 4 proof step from Mathlib.Order.Filter.TendstoCofinite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun (t : β) ↦ ⋯.toFinset (s := f ⁻¹' {t})
e : ↥s ↪ α := Function.Embedding.subtype fun (u : α) ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ (↑y.support : Set α) ⊆ range (ι := ↥s) (⇑e : (a : ↥s) → α)
have refine_2 : y.support ⊆ s
Tactic: suffices y.support ⊆ s by simpa [e]