awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Icc a c
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Icc b c)
x : α
hx : x ∈ Icc a c
pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have neg : ∀ (g₀ : b < x), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ioi a
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ioi a
pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have neg : ∀ (g₀ : b < x), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ici a
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Icc a b)
h₁ : AntitoneOn f (Ici b)
x : α
hx : x ∈ Ici a
pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have neg : ∀ (g₀ : b < x), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have neg : ∀ (g₀ : b < x), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Icc b a)
x : α
hx : x ∈ Iic a
pos : ∀ (g₀ : x ≤ b), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have neg : ∀ (g₀ : b < x), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: by_cases! g₀ : x ≤ b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
h : Membership.mem (γ := Set α) univ x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have inl : x ≤ b → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: rcases le_total x b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type u_1
inst : LinearOrder α
inst_1 : Preorder β
b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ici b)
x : α
h : Membership.mem (γ := Set α) univ x
inl : x ≤ b → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
have inr : b ≤ x → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
Tactic: rcases le_total x b
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
⊢ IsMaxFilter g l a
have refine : ∀ (x : α) (hf : f x ≤ f a) (hgf : g x ≤ f x), g x ≤ g a
Tactic: refine hle.mp (h.mono fun x hf hgf => ?_)
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
x : α
hf : f x ≤ f a
hgf : g x ≤ f x
⊢ g x ≤ g a
have rw : g x ≤ f a
Tactic: rw [← hfga]
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : α → β
a : α
l : Filter α
h : IsExtrFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsExtrFilter g l a
have h₁ : IsMinFilter f l a ∨ IsMaxFilter f l a
Tactic: rw [IsExtrFilter] at *
Cleared hypotheses: h, heq, hfga
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
f g : α → β
a : α
l : Filter α
h : IsMinFilter f l a ∨ IsMaxFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsMinFilter g l a ∨ IsMaxFilter g l a
have rwa : IsMinFilter g l a ∨ IsMaxFilter f l a
Tactic: rwa [← heq.isMaxFilter_iff hfga, ← heq.isMinFilter_iff hfga]
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
inst_1 : OrderBot β
D : α → β
s : Finset α
inst_2 : Nonempty α
b : β
hb : b ∈ range D
hmem : Function.invFun D b ∈ s
hmax : ∀ a ∈ s, D a ≤ b
⊢ s.sup D = b
have obtain : ∀ (a : α) (hmem : Function.invFun D (D a) ∈ s) (hmax : ∀ a_1 ∈ s, D a_1 ≤ D a), s.sup D = D a
Tactic: obtain ⟨a, rfl⟩ := hb
Cleared hypotheses: b, hb, hmem, hmax
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
inst_1 : OrderBot β
D : α → β
s : Finset α
inst_2 : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
⊢ s.sup D = D a
have rw : s.sup D = D (Function.invFun D (D a))
Tactic: rw [← Function.apply_invFun_apply (f := D)]
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
inst_1 : OrderBot β
D : α → β
s : Finset α
inst_2 : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
⊢ s.sup D = D (Function.invFun D (D a))
have apply : IsMaxOn D (↑s : Set α) (Function.invFun D (D a))
Tactic: apply sup_eq_of_isMaxOn hmem
-- Lean 4 proof step from Mathlib.Order.Filter.Extr (goal)
Goal:
α : Type u
β : Type v
inst : SemilatticeSup β
inst_1 : OrderBot β
D : α → β
s : Finset α
inst_2 : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_2 ∈ s, D a_2 ≤ D a
a_1 : α
⊢ a_1 ∈ (↑s : Set α) → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ D x ≤ D (Function.invFun D (D a))) x} a_1
have rw : a_1 ∈ (↑s : Set α) → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ D x ≤ D a) x} a_1
Tactic: rw [Function.apply_invFun_apply (f := D)]
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : Preorder β
⊢ Eq (α := (↑φ : Filter α).Germ β → (↑φ : Filter α).Germ β → Prop) (fun (x1 x2 : (↑φ : Filter α).Germ β) ↦ x1 < x2)
    (LiftRel fun (x1 x2 : β) ↦ x1 < x2)
have h : ∀ (x : (↑φ : Filter α).Germ β) (f : α → β) (x : (↑φ : Filter α).Germ β) (g : α → β),
  LT.lt (α := (↑φ : Filter α).Germ β) (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) f)
      (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) g) ↔
    LiftRel (l := (↑φ : Filter α)) (fun (x1 x2 : β) ↦ x1 < x2)
      (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) f)
      (Quot.mk (⇑((↑φ : Filter α).germSetoid β) : (α → β) → (α → β) → Prop) g)
Tactic: ext ⟨f⟩ ⟨g⟩
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
⊢ Eq (α := (↑φ : Filter α).Germ β) (max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
have inl : ∀ (h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)),
  Eq (α := (↑φ : Filter α).Germ β) (max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
Tactic: rcases le_total (a : β*) b with h | h
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
inl :
  ∀ (h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)),
    Eq (α := (↑φ : Filter α).Germ β) (max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
      (map₂ max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
⊢ Eq (α := (↑φ : Filter α).Germ β) (max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
have inr : ∀ (h : LE.le (α := (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β)),
  Eq (α := (↑φ : Filter α).Germ β) (max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
Tactic: rcases le_total (a : β*) b with h | h
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)
⊢ Eq (α := (↑φ : Filter α).Germ β) (max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
have inl : b =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ max (a x) (b x)
Tactic: rw [max_eq_right h, map₂_coe, coe_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β)
⊢ Eq (α := (↑φ : Filter α).Germ β) (max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ max (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
have inr : a =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ max (a x) (b x)
Tactic: rw [max_eq_left h, map₂_coe, coe_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
⊢ Eq (α := (↑φ : Filter α).Germ β) (min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
have inl : ∀ (h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)),
  Eq (α := (↑φ : Filter α).Germ β) (min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
Tactic: rcases le_total (a : β*) b with h | h
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
inl :
  ∀ (h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)),
    Eq (α := (↑φ : Filter α).Germ β) (min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
      (map₂ min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
⊢ Eq (α := (↑φ : Filter α).Germ β) (min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
have inr : ∀ (h : LE.le (α := (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β)),
  Eq (α := (↑φ : Filter α).Germ β) (min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
Tactic: rcases le_total (a : β*) b with h | h
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β)
⊢ Eq (α := (↑φ : Filter α).Germ β) (min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
have inl : a =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ min (a x) (b x)
Tactic: rw [min_eq_left h, map₂_coe, coe_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
K : LinearOrder β
x y : (↑φ : Filter α).Germ β
a b : α → β
h : LE.le (α := (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β) (↑a : (↑φ : Filter α).Germ β)
⊢ Eq (α := (↑φ : Filter α).Germ β) (min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
    (map₂ min (↑a : (↑φ : Filter α).Germ β) (↑b : (↑φ : Filter α).Germ β))
have inr : b =ᶠ[(↑φ : Filter α)] fun (x : α) ↦ min (a x) (b x)
Tactic: rw [min_eq_right h, map₂_coe, coe_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : β
⊢ Eq (α := (↑φ : Filter α).Germ β) (↑(max x y) : (↑φ : Filter α).Germ β)
    (max (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β))
have rw : Eq (α := (↑φ : Filter α).Germ β) (↑(max x y) : (↑φ : Filter α).Germ β)
  (map₂ max (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β))
Tactic: rw [max_def, map₂_const]
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : β
rw :
  Eq (α := (↑φ : Filter α).Germ β) (↑(max x y) : (↑φ : Filter α).Germ β)
    (map₂ max (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β))
⊢ Eq (α := (↑φ : Filter α).Germ β) (↑(max x y) : (↑φ : Filter α).Germ β)
    (max (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β))
have rw₁ : Eq (α := (↑φ : Filter α).Germ β) (↑(max x y) : (↑φ : Filter α).Germ β) (↑(max x y) : (↑φ : Filter α).Germ β)
Tactic: rw [max_def, map₂_const]
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : β
⊢ Eq (α := (↑φ : Filter α).Germ β) (↑(min x y) : (↑φ : Filter α).Germ β)
    (min (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β))
have rw : Eq (α := (↑φ : Filter α).Germ β) (↑(min x y) : (↑φ : Filter α).Germ β)
  (map₂ min (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β))
Tactic: rw [min_def, map₂_const]
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : LinearOrder β
x y : β
rw :
  Eq (α := (↑φ : Filter α).Germ β) (↑(min x y) : (↑φ : Filter α).Germ β)
    (map₂ min (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β))
⊢ Eq (α := (↑φ : Filter α).Germ β) (↑(min x y) : (↑φ : Filter α).Germ β)
    (min (↑x : (↑φ : Filter α).Germ β) (↑y : (↑φ : Filter α).Germ β))
have rw₁ : Eq (α := (↑φ : Filter α).Germ β) (↑(min x y) : (↑φ : Filter α).Germ β) (↑(min x y) : (↑φ : Filter α).Germ β)
Tactic: rw [min_def, map₂_const]
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : AddCommGroup β
inst_1 : LinearOrder β
x : β
⊢ Eq (α := (↑φ : Filter α).Germ β) (↑|x| : (↑φ : Filter α).Germ β) |(↑x : (↑φ : Filter α).Germ β)|
have rw : Eq (α := (↑φ : Filter α).Germ β) (↑|x| : (↑φ : Filter α).Germ β) (map abs (↑x : (↑φ : Filter α).Germ β))
Tactic: rw [abs_def, map_const]
-- Lean 4 proof step from Mathlib.Order.Filter.FilterProduct (goal)
Goal:
α : Type u
β : Type v
φ : Ultrafilter α
inst : AddCommGroup β
inst_1 : LinearOrder β
x : β
rw : Eq (α := (↑φ : Filter α).Germ β) (↑|x| : (↑φ : Filter α).Germ β) (map abs (↑x : (↑φ : Filter α).Germ β))
⊢ Eq (α := (↑φ : Filter α).Germ β) (↑|x| : (↑φ : Filter α).Germ β) |(↑x : (↑φ : Filter α).Germ β)|
have rw₁ : Eq (α := (↑φ : Filter α).Germ β) (↑|x| : (↑φ : Filter α).Germ β) (↑|x| : (↑φ : Filter α).Germ β)
Tactic: rw [abs_def, map_const]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Finite
⊢ ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f
have empty : ⋂ (i : β), ⋂ (_ : Membership.mem (γ := Set β) ∅ i), s i ∈ f ↔ ∀ (i : β), Membership.mem (γ := Set β) ∅ i → s i ∈ f
Tactic: induction is, hf using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hs => simp [hs]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Finite
empty :
  ⋂ (i : β), ⋂ (_ : Membership.mem (γ := Set β) ∅ i), s i ∈ f ↔ ∀ (i : β), Membership.mem (γ := Set β) ∅ i → s i ∈ f
⊢ ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f
have insert : ∀ {a : β} {s_1 : Set β},
  a ∉ s_1 →
    s_1.Finite →
      ∀ (hs : ⋂ i ∈ s_1, s i ∈ f ↔ ∀ i ∈ s_1, s i ∈ f), ⋂ i ∈ insert a s_1, s i ∈ f ↔ ∀ i ∈ insert a s_1, s i ∈ f
Tactic: induction is, hf using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hs => simp [hs]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
f : Filter α
s : Set (Set α)
hfin : s.Finite
⊢ ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f
have rw : ⋂ i ∈ s, i ∈ f ↔ ∀ U ∈ s, U ∈ f
Tactic: rw [sInter_eq_biInter, biInter_mem hfin]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
f : Filter α
s : Set (Set α)
hfin : s.Finite
rw : ⋂ i ∈ s, i ∈ f ↔ ∀ U ∈ s, U ∈ f
⊢ ⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f
have rw₁ : (∀ i ∈ s, i ∈ f) ↔ ∀ U ∈ s, U ∈ f
Tactic: rw [sInter_eq_biInter, biInter_mem hfin]
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
s : Set (Set α)
U : Set α
⊢ U ∈ generate s ↔ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
have mp : U ∈ generate s → ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
s : Set (Set α)
U : Set α
mp : U ∈ generate s → ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
⊢ U ∈ generate s ↔ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
have mpr : (∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U) → U ∈ generate s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
s : Set (Set α)
U s_1 t : Set α
h : GenerateSets s s_1
hVW : s_1 ⊆ t
hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s_1
⊢ ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ t
have mp : ∀ (t_1 : Set (Set α)) (hts : t_1 ⊆ s) (ht : t_1.Finite) (htV : ⋂₀ t_1 ⊆ s_1), ∃ t_2 ⊆ s, t_2.Finite ∧ ⋂₀ t_2 ⊆ t
Tactic: rcases hV with ⟨t, hts, ht, htV⟩
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
s : Set (Set α)
U s_1 t : Set α
h : GenerateSets s s_1
h_1 : GenerateSets s t
hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s_1
hW : ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ t
⊢ ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ s_1 ∩ t
have mp : ∀ (t_1 : Set (Set α)) (hts : t_1 ⊆ s) (ht : t_1.Finite) (htV : ⋂₀ t_1 ⊆ s_1) (u : Set (Set α)) (hus : u ⊆ s)
  (hu : u.Finite) (huW : ⋂₀ u ⊆ t), ∃ t_2 ⊆ s, t_2.Finite ∧ ⋂₀ t_2 ⊆ s_1 ∩ t
Tactic: rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
Cleared hypotheses: hV, hW
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
s : Set (Set α)
U : Set α
h : U ∈ generate s
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
have mp : ∀ {V : Set α} (V_in : V ∈ s), ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ V
Tactic: induction h with
    | @basic V V_in =>
      exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
    | univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
    | superset _ hVW hV =>
      rcases hV with ⟨t, hts, ht, htV⟩
      exact ⟨t, hts, ht, htV.trans hVW⟩
    | inter _ _ hV hW =>
      rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
      exact
        ⟨t ∪ u, union_subset hts hus, ht.union hu,
          (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
s : Set (Set α)
U : Set α
h : U ∈ generate s
mp : ∀ {V : Set α} (V_in : V ∈ s), ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ V
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
have mp₁ : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ univ
Tactic: induction h with
    | @basic V V_in =>
      exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
    | univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
    | superset _ hVW hV =>
      rcases hV with ⟨t, hts, ht, htV⟩
      exact ⟨t, hts, ht, htV.trans hVW⟩
    | inter _ _ hV hW =>
      rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
      exact
        ⟨t ∪ u, union_subset hts hus, ht.union hu,
          (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.Finite (goal)
Goal:
α : Type u
s : Set (Set α)
U : Set α
h : U ∈ generate s
mp : ∀ {V : Set α} (V_in : V ∈ s), ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ V
mp₁ : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ univ
⊢ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
have mp₂ : ∀ {s_1 t : Set α},
  GenerateSets s s_1 → ∀ (hVW : s_1 ⊆ t) (hV : ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ s_1), ∃ t_1 ⊆ s, t_1.Finite ∧ ⋂₀ t_1 ⊆ t
Tactic: induction h with
    | @basic V V_in =>
      exact ⟨{V}, singleton_subset_iff.2 V_in, finite_singleton _, (sInter_singleton _).subset⟩
    | univ => exact ⟨∅, empty_subset _, finite_empty, subset_univ _⟩
    | superset _ hVW hV =>
      rcases hV with ⟨t, hts, ht, htV⟩
      exact ⟨t, hts, ht, htV.trans hVW⟩
    | inter _ _ hV hW =>
      rcases hV, hW with ⟨⟨t, hts, ht, htV⟩, u, hus, hu, huW⟩
      exact
        ⟨t ∪ u, union_subset hts hus, ht.union hu,
          (sInter_union _ _).subset.trans <| inter_subset_inter htV huW⟩
Cleared hypotheses: h