awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
f : ι → Filter α
⊢ Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (i : ι), f i)) (⋃ (t : Finset ι), sets (⨅ i ∈ t, f i))
have h : Directed (fun (x1 x2 : Filter α) ↦ x1 ≥ x2) fun (t : Finset ι) ↦ ⨅ i ∈ t, f i
Tactic: rw [iInf_eq_iInf_finset, iInf_sets_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
⊢ Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (i : ι), f i)) (⋃ (t : Finset (PLift ι)), sets (⨅ i ∈ t, f i.down))
have rw : Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (i : ι), f i)) (sets (⨅ (i : PLift ι), f i.down))
Tactic: rw [← iInf_sets_eq_finite, ← Equiv.plift.surjective.iInf_comp, Equiv.plift_apply]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
rw : Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (i : ι), f i)) (sets (⨅ (i : PLift ι), f i.down))
⊢ Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (i : ι), f i)) (⋃ (t : Finset (PLift ι)), sets (⨅ i ∈ t, f i.down))
have rw₁ : Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (x : PLift ι), f ((Equiv.plift : (a : PLift ι) → ι) x)))
  (sets (⨅ (i : PLift ι), f i.down))
Tactic: rw [← iInf_sets_eq_finite, ← Equiv.plift.surjective.iInf_comp, Equiv.plift_apply]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Sort x
f : ι → Filter α
rw : Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (i : ι), f i)) (sets (⨅ (i : PLift ι), f i.down))
rw₁ :
  Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (x : PLift ι), f ((Equiv.plift : (a : PLift ι) → ι) x)))
    (sets (⨅ (i : PLift ι), f i.down))
⊢ Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (i : ι), f i)) (⋃ (t : Finset (PLift ι)), sets (⨅ i ∈ t, f i.down))
have rw₂ : Eq.{u + 1} (α := Set (Set α)) (sets (⨅ (x : PLift ι), f x.down)) (sets (⨅ (i : PLift ι), f i.down))
Tactic: rw [← iInf_sets_eq_finite, ← Equiv.plift.surjective.iInf_comp, Equiv.plift_apply]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ Membership.mem (γ := Filter β) (⨅ a ∈ s, f a) t ↔ ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a
have simp : Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t ↔
  ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
Tactic: simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t ↔
    ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
have refine_1 : ∀ (h : Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t),
  ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
refine_1 :
  ∀ (h : Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t),
    ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
⊢ Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t ↔
    ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
have refine_2 : (∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)) →
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
h : Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t
⊢ ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
have refine_1 : ∀ (p : Subtype (Membership.mem s) → Set β) (hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f (↑i : α))
  (h :
    Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α))
      (⋂ (i : Subtype (Membership.mem s)), p i)),
  ∃ (p_1 : α → Set β),
    (∀ a ∈ s, p_1 a ∈ f a) ∧
      Eq.{v + 1} (α := Set β) (⋂ (i : Subtype (Membership.mem s)), p i) (⋂ (x : (↑(↑s : Set α) : Type u)), p_1 (↑x : α))
Tactic: rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f (↑i : α)
h :
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α))
    (⋂ (i : Subtype (Membership.mem s)), p i)
⊢ ∃ (p_1 : α → Set β),
    (∀ a ∈ s, p_1 a ∈ f a) ∧
      Eq.{v + 1} (α := Set β) (⋂ (i : Subtype (Membership.mem s)), p i) (⋂ (x : (↑(↑s : Set α) : Type u)), p_1 (↑x : α))
have refine_1 : Eq.{v + 1} (α := Set β) (⋂ (i : Subtype (Membership.mem s)), p i)
  (⋂ (x : (↑(↑s : Set α) : Type u)),
    (fun (a : α) ↦ (if h : a ∈ s then p (Subtype.mk (p := Membership.mem s) a h) else univ : Set β)) (↑x : α))
Tactic: refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ,
            fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f (↑i : α)
h :
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α))
    (⋂ (i : Subtype (Membership.mem s)), p i)
⊢ Eq.{v + 1} (α := Set β) (⋂ (i : Subtype (Membership.mem s)), p i)
    (⋂ (x : (↑(↑s : Set α) : Type u)),
      (fun (a : α) ↦ (if h : a ∈ s then p (Subtype.mk (p := Membership.mem s) a h) else univ : Set β)) (↑x : α))
have refine_1 : ∀ (x : Subtype (Membership.mem s)),
  (fun (a : α) ↦ (if h : a ∈ s then p (Subtype.mk (p := Membership.mem s) a h) else univ : Set β)) (↑(id x) : α) = p x
Tactic: refine iInter_congr_of_surjective id surjective_id ?_
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ Membership.mem (γ := Filter β) (⨅ a ∈ s, f a) t ↔ ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a
have simp : Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t ↔
  ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
Tactic: classical
  simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']
  refine ⟨fun h => ?_, ?_⟩
  · rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩
    refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ,
            fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩
    refine iInter_congr_of_surjective id surjective_id ?_
    rintro ⟨a, ha⟩
    simp [ha]
  · rintro ⟨p, hpf, rfl⟩
    exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
simp :
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t ↔
    ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
⊢ Membership.mem (γ := Filter β) (⨅ a ∈ s, f a) t ↔ ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a
have refine_1 : ∀ (h : Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t),
  ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
Tactic: classical
  simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']
  refine ⟨fun h => ?_, ?_⟩
  · rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩
    refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ,
            fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩
    refine iInter_congr_of_surjective id surjective_id ?_
    rintro ⟨a, ha⟩
    simp [ha]
  · rintro ⟨p, hpf, rfl⟩
    exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
simp :
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t ↔
    ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
refine_1 :
  ∀ (h : Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t),
    ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)
⊢ Membership.mem (γ := Filter β) (⨅ a ∈ s, f a) t ↔ ∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a
have refine_2 : (∃ (p : α → Set β), (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ (x : (↑(↑s : Set α) : Type u)), p (↑x : α)) →
  Membership.mem (γ := Filter β) (⨅ (x : Subtype (Membership.mem s)), f (↑x : α)) t
Tactic: classical
  simp only [← Finset.set_biInter_coe, biInter_eq_iInter, iInf_subtype']
  refine ⟨fun h => ?_, ?_⟩
  · rcases (mem_iInf_of_finite _).1 h with ⟨p, hp, rfl⟩
    refine ⟨fun a => if h : a ∈ s then p ⟨a, h⟩ else univ,
            fun a ha => by simpa [ha] using hp ⟨a, ha⟩, ?_⟩
    refine iInter_congr_of_surjective id surjective_id ?_
    rintro ⟨a, ha⟩
    simp [ha]
  · rintro ⟨p, hpf, rfl⟩
    exact iInter_mem.2 fun a => mem_iInf_of_mem a (hpf a a.2)
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
h : i ∉ s
hs : Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))
⊢ Eq.{u + 1} (α := Filter α) (⨅ i_1 ∈ insert i s, 𝓟 (f i_1)) (𝓟 (⋂ i_1 ∈ insert i s, f i_1))
have insert : 𝓟 (f i) ⊓ ⨅ x ∈ s, 𝓟 (f x) = 𝓟 (⋂ i_1 ∈ insert i s, f i_1)
Tactic: rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
h : i ∉ s
hs : Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))
insert : 𝓟 (f i) ⊓ ⨅ x ∈ s, 𝓟 (f x) = 𝓟 (⋂ i_1 ∈ Insert.insert i s, f i_1)
⊢ Eq.{u + 1} (α := Filter α) (⨅ i_1 ∈ Insert.insert i s, 𝓟 (f i_1)) (𝓟 (⋂ i_1 ∈ Insert.insert i s, f i_1))
have insert₁ : 𝓟 (f i) ⊓ ⨅ x ∈ s, 𝓟 (f x) = 𝓟 (f i ∩ ⋂ x ∈ s, f x)
Tactic: rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
h : i ∉ s
hs : Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))
insert : 𝓟 (f i) ⊓ ⨅ x ∈ s, 𝓟 (f x) = 𝓟 (⋂ i_1 ∈ Insert.insert i s, f i_1)
insert₁ : 𝓟 (f i) ⊓ ⨅ x ∈ s, 𝓟 (f x) = 𝓟 (f i ∩ ⋂ x ∈ s, f x)
⊢ Eq.{u + 1} (α := Filter α) (⨅ i_1 ∈ Insert.insert i s, 𝓟 (f i_1)) (𝓟 (⋂ i_1 ∈ Insert.insert i s, f i_1))
have insert₂ : 𝓟 (f i) ⊓ 𝓟 (⋂ i ∈ s, f i) = 𝓟 (f i ∩ ⋂ x ∈ s, f x)
Tactic: rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
h : i ∉ s
hs : Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))
insert : 𝓟 (f i) ⊓ ⨅ x ∈ s, 𝓟 (f x) = 𝓟 (⋂ i_1 ∈ Insert.insert i s, f i_1)
insert₁ : 𝓟 (f i) ⊓ ⨅ x ∈ s, 𝓟 (f x) = 𝓟 (f i ∩ ⋂ x ∈ s, f x)
insert₂ : 𝓟 (f i) ⊓ 𝓟 (⋂ i ∈ s, f i) = 𝓟 (f i ∩ ⋂ x ∈ s, f x)
⊢ Eq.{u + 1} (α := Filter α) (⨅ i_1 ∈ Insert.insert i s, 𝓟 (f i_1)) (𝓟 (⋂ i_1 ∈ Insert.insert i s, f i_1))
have insert₃ : 𝓟 (f i ∩ ⋂ i ∈ s, f i) = 𝓟 (f i ∩ ⋂ x ∈ s, f x)
Tactic: rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type w
s : Finset ι
f : ι → Set α
⊢ Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))
have empty : Eq.{u + 1} (α := Filter α) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), 𝓟 (f i))
  (𝓟 (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i))
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs => rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type w
s : Finset ι
f : ι → Set α
empty :
  Eq.{u + 1} (α := Filter α) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), 𝓟 (f i))
    (𝓟 (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i))
⊢ Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))
have insert : ∀ (i : ι) (s : Finset ι),
  i ∉ s →
    ∀ (hs : Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))),
      Eq.{u + 1} (α := Filter α) (⨅ i_1 ∈ insert i s, 𝓟 (f i_1)) (𝓟 (⋂ i_1 ∈ insert i s, f i_1))
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs => rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type w
s : Finset ι
f : ι → Set α
⊢ Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))
have empty : Eq.{u + 1} (α := Filter α) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), 𝓟 (f i))
  (𝓟 (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i))
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs => rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type w
s : Finset ι
f : ι → Set α
empty :
  Eq.{u + 1} (α := Filter α) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), 𝓟 (f i))
    (𝓟 (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i))
⊢ Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))
have insert : ∀ (i : ι) (s : Finset ι),
  i ∉ s →
    ∀ (hs : Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))),
      Eq.{u + 1} (α := Filter α) (⨅ i_1 ∈ insert i s, 𝓟 (f i_1)) (𝓟 (⋂ i_1 ∈ insert i s, f i_1))
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s _ hs => rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Sort w
inst : Finite ι
f : ι → Set α
⊢ Eq.{u + 1} (α := Filter α) (⨅ (i : ι), 𝓟 (f i)) (𝓟 (⋂ (i : ι), f i))
have intro : ∀ (val : Fintype (PLift ι)), Eq.{u + 1} (α := Filter α) (⨅ (i : ι), 𝓟 (f i)) (𝓟 (⋂ (i : ι), f i))
Tactic: cases nonempty_fintype (PLift ι)
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Sort w
inst : Finite ι
f : ι → Set α
val : Fintype (PLift ι)
⊢ Eq.{u + 1} (α := Filter α) (⨅ (i : ι), 𝓟 (f i)) (𝓟 (⋂ (i : ι), f i))
have intro : Eq.{u + 1} (α := Filter α) (⨅ (i : PLift ι), 𝓟 (f i.down)) (𝓟 (⋂ (i : PLift ι), f i.down))
Tactic: rw [← iInf_plift_down, ← iInter_plift_down]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type w
s : Set ι
hs : s.Finite
f : ι → Set α
⊢ Eq.{u + 1} (α := Filter α) (⨅ i ∈ s, 𝓟 (f i)) (𝓟 (⋂ i ∈ s, f i))
have lift : ∀ (s : Finset ι), Eq.{u + 1} (α := Filter α) (⨅ i ∈ (↑s : Set ι), 𝓟 (f i)) (𝓟 (⋂ i ∈ (↑s : Set ι), f i))
Tactic: lift s to Finset ι using hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Sort u_2
inst : Finite ι
l : Filter α
p : ι → α → Prop
⊢ (∃ᶠ (x : α) in l, ∃ (i : ι), p i x) ↔ ∃ (i : ι), ∃ᶠ (x : α) in l, p i x
have rw : (¬∃ᶠ (x : α) in l, ∃ (i : ι), p i x) ↔ ¬∃ (i : ι), ∃ᶠ (x : α) in l, p i x
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
ι : Type u_2
I : Set ι
hI : I.Finite
l : Filter α
p : ι → α → Prop
⊢ (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
have rw : (¬∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ¬∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (hypothesis)
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
⊢ ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i
have this : Finite.{u_2 + 1} (↑s : Type u_2)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i
have rw : ⋃ (x : (↑s : Type u_2)), f (↑x : ι) ≤ᶠ[l] ⋃ (x : (↑s : Type u_2)), g (↑x : ι)
Tactic: rw [biUnion_eq_iUnion, biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (hypothesis)
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i
have this : Finite.{u_2 + 1} (↑s : Type u_2)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i
have rw : ⋂ (x : (↑s : Type u_2)), f (↑x : ι) ≤ᶠ[l] ⋂ (x : (↑s : Type u_2)), g (↑x : ι)
Tactic: rw [biInter_eq_iInter, biInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l_1 : Filter α
f g h : α → β
l : Filter α
P : l.Germ β
⊢ ∀ (a b : α → β),
    a ≈ b →
      Eq (α := Prop) ((fun (f : α → β) ↦ ∃ (b : β), f =ᶠ[l] fun (x : α) ↦ b) a)
        ((fun (f : α → β) ↦ ∃ (b : β), f =ᶠ[l] fun (x : α) ↦ b) b)
have suffices : ∀ (f g : α → β) (b : β), f =ᶠ[l] g → (f =ᶠ[l] fun (x : α) ↦ b) → g =ᶠ[l] fun (x : α) ↦ b
Tactic: suffices ∀ f g : α → β, ∀ b : β, f =ᶠ[l] g → (f =ᶠ[l] fun _ ↦ b) → (g =ᶠ[l] fun _ ↦ b) from
      fun f g h ↦ propext ⟨fun ⟨b, hb⟩ ↦ ⟨b, this f g b h hb⟩, fun ⟨b, hb⟩ ↦ ⟨b, h.trans hb⟩⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
b w : β
⊢ IsConstant.{u_1, u_2} (α := α) (β := β) (l := l) (↑fun (x : α) ↦ b : l.Germ β)
have h : EventuallyEq.{u_1, u_2} (β := β) l (fun (x : α) ↦ b) fun (x : α) ↦ b
Tactic: use b
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
g : β → γ
h : IsConstant (l := l) (↑f : l.Germ β)
⊢ IsConstant (l := l) (↑(g ∘ f) : l.Germ γ)
have obtain : ∀ (b : β) (hb : f =ᶠ[l] fun (x : α) ↦ b), IsConstant (l := l) (↑(g ∘ f) : l.Germ γ)
Tactic: obtain ⟨b, hb⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
l : Filter α
⊢ Eq (α := l.Germ β → l.Germ β) (map id) id
have h : ∀ (x : l.Germ β) (f : α → β),
  Eq (α := l.Germ β) (map id (Quot.mk (⇑(l.germSetoid β) : (α → β) → (α → β) → Prop) f))
    (id (Quot.mk (⇑(l.germSetoid β) : (α → β) → (α → β) → Prop) f))
Tactic: ext ⟨f⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
lc : Filter γ
g : γ → α
hf : IsConstant (l := l) (↑f : l.Germ β)
hg : Tendsto g lc l
⊢ IsConstant (l := lc) (↑(f ∘ g) : lc.Germ β)
have rcases : ∀ (b : β) (hb : f =ᶠ[l] fun (x : α) ↦ b), IsConstant (l := lc) (↑(f ∘ g) : lc.Germ β)
Tactic: rcases hf with ⟨b, hb⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : l.Germ β
lc : Filter γ
g : γ → α
hf : f.IsConstant
hg : Tendsto g lc l
⊢ (f.compTendsto g hg).IsConstant
have h : ∀ (f : α → β) (hf : IsConstant ⟦f⟧), (compTendsto ⟦f⟧ g hg).IsConstant
Tactic: induction f using Quotient.inductionOn with | _ f => ?_
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : AddMonoidWithOne M
⊢ Eq (α := α → M) (↑0 : α → M) fun (x : α) ↦ 0
have simp : Eq (α := α → M) 0 fun (x : α) ↦ 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : AddMonoidWithOne M
x : ℕ
⊢ Eq (α := α → M) (↑(x + 1) : α → M)
    ((fun (f g : α → M) (x : α) ↦ ((fun (x1 x2 : M) ↦ x1 + x2) (f x) (g x) : M)) (↑x : α → M) fun (x : α) ↦ 1)
have simp : HAdd.hAdd (α := α → M) (↑x : α → M) 1 = fun (x_1 : α) ↦ HAdd.hAdd (α := M) (↑x : M) 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst : AddGroupWithOne G
x : ℕ
⊢ Eq (α := α → G) (↑(Int.negSucc x) : α → G) ((fun (x : α → G) ↦ Neg.neg ∘ x) (↑(x + 1) : α → G))
have simp : HAdd.hAdd (α := α → G) (-1) (-(↑x : α → G)) = fun (x_1 : α) ↦ HAdd.hAdd (α := G) (-1) (-(↑x : G))
Tactic: simp [Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : MulAction M β
c₁ c₂ : M
f_2 : l.Germ β
f : α → β
⊢ HSMul.hSMul (β := l.Germ β) (c₁ * c₂) (↑f : l.Germ β) = c₁ • HSMul.hSMul (β := l.Germ β) c₂ (↑f : l.Germ β)
have norm_cast : (c₁ * c₂) • f =ᶠ[l] c₁ • c₂ • f
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : MulAction M β
f_2 : l.Germ β
f : α → β
⊢ HSMul.hSMul (α := M) (β := l.Germ β) 1 (↑f : l.Germ β) = (↑f : l.Germ β)
have norm_cast : HSMul.hSMul (α := M) 1 f =ᶠ[l] f
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : MulAction M β
c₁_1 c₂_1 : l.Germ M
f_2 : l.Germ β
c₁ c₂ : α → M
f : α → β
⊢ HSMul.hSMul (β := l.Germ β) (HMul.hMul (α := l.Germ M) (↑c₁ : l.Germ M) (↑c₂ : l.Germ M)) (↑f : l.Germ β) =
    HSMul.hSMul (α := l.Germ M) (↑c₁ : l.Germ M)
      (HSMul.hSMul (α := l.Germ M) (β := l.Germ β) (↑c₂ : l.Germ M) (↑f : l.Germ β))
have norm_cast : (c₁ * c₂) • f =ᶠ[l] c₁ • c₂ • f
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : AddMonoid N
inst_2 : DistribMulAction M N
c : M
f_2 g_2 : l.Germ N
f g : α → N
⊢ c • HAdd.hAdd (α := l.Germ N) (↑f : l.Germ N) (↑g : l.Germ N) =
    HSMul.hSMul (β := l.Germ N) c (↑f : l.Germ N) + HSMul.hSMul (β := l.Germ N) c (↑g : l.Germ N)
have norm_cast : c • (f + g) =ᶠ[l] c • f + c • g
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g_1 h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Monoid M
inst_1 : AddMonoid N
inst_2 : DistribMulAction M N
c_1 : l.Germ M
f_2 g_2 : l.Germ N
c : α → M
f g : α → N
⊢ HSMul.hSMul (α := l.Germ M) (↑c : l.Germ M) (HAdd.hAdd (α := l.Germ N) (↑f : l.Germ N) (↑g : l.Germ N)) =
    HSMul.hSMul (α := l.Germ M) (β := l.Germ N) (↑c : l.Germ M) (↑f : l.Germ N) +
      HSMul.hSMul (α := l.Germ M) (β := l.Germ N) (↑c : l.Germ M) (↑g : l.Germ N)
have norm_cast : c • (f + g) =ᶠ[l] c • f + c • g
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Order.Filter.Germ.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f_1 g h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c₁ c₂ : R
f_2 : l.Germ M
f : α → M
⊢ HSMul.hSMul (β := l.Germ M) (c₁ + c₂) (↑f : l.Germ M) =
    HSMul.hSMul (β := l.Germ M) c₁ (↑f : l.Germ M) + HSMul.hSMul (β := l.Germ M) c₂ (↑f : l.Germ M)
have norm_cast : (c₁ + c₂) • f =ᶠ[l] c₁ • f + c₂ • f
Tactic: norm_cast