awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h :
  (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * (c * c) +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c +
      -(↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
    0
simp :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0) 2 -
      4 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * -(↑g : Matrix (Fin 2) (Fin 2) K) 0 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ)
      (2 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0))
      2

Tactic:
simp only [← discrim_eq_sq_of_quadratic_eq_zero h, discr_fin_two, discrim, trace_fin_two,
        det_fin_two]

Premises used: Matrix.trace_fin_two, discrim, discrim_eq_sq_of_quadratic_eq_zero, Matrix.det_fin_two, Matrix.discr_fin_two
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h :
  (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * (c * c) +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c +
      -(↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
    0
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0) 2 -
      4 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * -(↑g : Matrix (Fin 2) (Fin 2) K) 0 1

Tactic:
grind
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • (↑c : OnePoint K) = (↑c : OnePoint K)
⊢ (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ)
      (2 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0))
      2

Tactic:
have : g.val.discr = (2 * g 1 0 * c + (g 1 1 + -g 0 0)) ^ 2 := by
      replace h : g 1 0 * (c * c) + (g 1 1 + -g 0 0) * c + -g 0 1 = 0 := by
        simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial, sq, sub_eq_add_neg]
          using h
      simp only [← discrim_eq_sq_of_quadratic_eq_zero h, discr_fin_two, discrim, trace_fin_two,
        det_fin_two]
      grind
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • (↑c : OnePoint K) = (↑c : OnePoint K)
this :
  (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ)
      (2 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0))
      2
coe :
  0 ≤
    HPow.hPow (β := ℕ)
      (2 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0))
      2
⊢ 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) K).discr

Tactic:
rw [this]
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • (↑c : OnePoint K) = (↑c : OnePoint K)
this :
  (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ)
      (2 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0))
      2
⊢ 0 ≤
    HPow.hPow (β := ℕ)
      (2 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0))
      2

Tactic:
apply sq_nonneg

Premises used: sq_nonneg
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : OnePoint K
infty : HSMul.hSMul (β := OnePoint K) g ∞ ≠ ∞
coe : ∀ (c : K), g • (↑c : OnePoint K) ≠ (↑c : OnePoint K)
⊢ g • c ≠ c

Tactic:
cases c with
  | infty =>
    rw [Ne, smul_infty_eq_self_iff]
    refine fun h ↦ not_le_of_gt hg ?_
    have : g.val.discr = (g 0 0 - g 1 1) ^ 2 := by
      simp only [discr_fin_two, trace_fin_two, det_fin_two]
      grind
    rw [this]
    apply sq_nonneg
  | coe c =>
    refine fun h ↦ not_le_of_gt hg ?_
    have : g.val.discr = (2 * g 1 0 * c + (g 1 1 + -g 0 0)) ^ 2 := by
      replace h : g 1 0 * (c * c) + (g 1 1 + -g 0 0) * c + -g 0 1 = 0 := by
        simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial, sq, sub_eq_add_neg]
          using h
      simp only [← discrim_eq_sq_of_quadratic_eq_zero h, discr_fin_two, discrim, trace_fin_two,
        det_fin_two]
      grind
    rw [this]
    apply sq_nonneg

Premises used: OnePoint.infty, OnePoint.smul_infty_eq_self_iff, Ne, sq_nonneg, not_le_of_gt
-- Module: Mathlib.Topology.Compactification.OnePoint.Sphere
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
⊢ 0 < Fintype.card ι

Tactic:
lia
-- Module: Mathlib.Topology.Compactification.OnePoint.Sphere
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
⊢ Nonempty ι

Tactic:
have : Nonempty ι := Fintype.card_pos_iff.mp <| by lia
-- Module: Mathlib.Topology.Compactification.OnePoint.Sphere
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
⊢ ‖v‖ = 1

Tactic:
simp [v]
-- Module: Mathlib.Topology.Compactification.OnePoint.Sphere
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
⊢ ‖v‖ = 1

Tactic:
have hv : ‖v‖ = 1 := by simp [v]
-- Module: Mathlib.Topology.Compactification.OnePoint.Sphere
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
contra : v = 0
⊢ False

Tactic:
simp [contra] at hv
-- Module: Mathlib.Topology.Compactification.OnePoint.Sphere
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
⊢ v ≠ 0

Tactic:
have hv₀ : v ≠ 0 := fun contra ↦ by simp [contra] at hv
-- Module: Mathlib.Topology.Compactification.OnePoint.Sphere
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
hv₀ : v ≠ 0
⊢ finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1

Tactic:
simp [h]
-- Module: Mathlib.Topology.Compactification.OnePoint.Sphere
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
hv₀ : v ≠ 0
⊢ Fact (finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1)

Tactic:
have : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1) := ⟨by simp [h]⟩
-- Module: Mathlib.Topology.Compactification.OnePoint.Sphere
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this_1 : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
hv₀ : v ≠ 0
this : Fact (finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1)
⊢ finrank ℝ V = finrank.{0, u_1} ℝ ↥(ℝ ∙ v)ᗮ

Tactic:
have hV : finrank ℝ V = finrank ℝ (ℝ ∙ v)ᗮ := (finrank_orthogonal_span_singleton hv₀).symm
-- Module: Mathlib.Topology.Compactification.OnePoint.Sphere
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this_1 : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
hv₀ : v ≠ 0
this : Fact (finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1)
hV : finrank ℝ V = finrank.{0, u_1} ℝ ↥(ℝ ∙ v)ᗮ
e : Homeomorph.{u_2, u_1} V ↥(ℝ ∙ v)ᗮ := (↑(Nonempty.some ⋯) : V ≃ₜ ↥(ℝ ∙ v)ᗮ)
⊢ Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)

Tactic:
exact e.onePointCongr.trans <| onePointHyperplaneHomeoUnitSphere hv

Premises used: Homeomorph.onePointCongr, onePointHyperplaneHomeoUnitSphere, Homeomorph.trans
-- Module: Mathlib.Topology.Compactification.OnePoint.Sphere
Goal:
ι : Type u_1
V : Type u_2
inst : Fintype ι
inst_1 : AddCommGroup V
inst_2 : Module ℝ V
inst_3 : FiniteDimensional ℝ V
inst_4 : TopologicalSpace V
inst_5 : IsTopologicalAddGroup V
inst_6 : ContinuousSMul ℝ V
inst_7 : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
have have₁ have₂ have₃ : (this : Nonempty ι) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have₄ :
  (this : Nonempty ι) →
    let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
    (hv : ‖v‖ = 1) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have₅ :
  (this : Nonempty ι) →
    let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
    (hv : ‖v‖ = 1) → (hv₀ : v ≠ 0) → Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have₆ :
  (this : Nonempty ι) →
    let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
    (hv : ‖v‖ = 1) →
      (hv₀ : v ≠ 0) →
        (this : Fact (finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1)) →
          Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
have₇ have₈ :
  (this : Nonempty ι) →
    let v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1;
    (hv : ‖v‖ = 1) →
      (hv₀ : v ≠ 0) →
        (this : Fact (finrank.{0, u_1} ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1)) →
          (hV : finrank ℝ V = finrank.{0, u_1} ℝ ↥(ℝ ∙ v)ᗮ) →
            Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)
⊢ Homeomorph.{u_2, u_1} (OnePoint V) (↑(sphere 0 1) : Type u_1)

Tactic:
classical
  have : Nonempty ι := Fintype.card_pos_iff.mp <| by lia
  let v : EuclideanSpace ℝ ι := .single (Classical.arbitrary ι) 1
  have hv : ‖v‖ = 1 := by simp [v]
  have hv₀ : v ≠ 0 := fun contra ↦ by simp [contra] at hv
  have : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1) := ⟨by simp [h]⟩
  have hV : finrank ℝ V = finrank ℝ (ℝ ∙ v)ᗮ := (finrank_orthogonal_span_singleton hv₀).symm
  letI e : V ≃ₜ (ℝ ∙ v)ᗮ := (FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq hV).some
  exact e.onePointCongr.trans <| onePointHyperplaneHomeoUnitSphere hv
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
a b : Set α
u : Ultrafilter α
ua :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    u
ub :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    u
⊢ ∃ t₃ ∈ ultrafilterBasis α,
    u ∈ t₃ ∧
      t₃ ⊆
        (fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a ∩
          (fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b

Tactic:
⟨_, ⟨a ∩ b, rfl⟩, inter_mem ua ub, fun v hv ↦ ⟨?_, ?_⟩⟩

Premises used: Filter.inter_mem, Inter.inter, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
a b : Set α
u : Ultrafilter α
ua :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    u
ub :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    u
refine_1 :
  ∀ (v : Ultrafilter α)
    (hv :
      Membership.mem (γ := Set (Ultrafilter α))
        ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) (a ∩ b)) v),
    Membership.mem (γ := Set (Ultrafilter α))
      ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a) v
refine_2 :
  ∀ (v : Ultrafilter α)
    (hv :
      Membership.mem (γ := Set (Ultrafilter α))
        ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) (a ∩ b)) v),
    Membership.mem (γ := Set (Ultrafilter α))
      ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b) v
⊢ ∃ t₃ ∈ ultrafilterBasis α,
    u ∈ t₃ ∧
      t₃ ⊆
        (fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a ∩
          (fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b

Tactic:
refine ⟨_, ⟨a ∩ b, rfl⟩, inter_mem ua ub, fun v hv ↦ ⟨?_, ?_⟩⟩
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
a b : Set α
u : Ultrafilter α
ua :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    u
ub :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    u
v : Ultrafilter α
hv :
  Membership.mem (γ := Set (Ultrafilter α))
    ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) (a ∩ b)) v
refine_1 : a ∩ b ⊆ a
⊢ Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    v

Tactic:
apply mem_of_superset hv

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
a b : Set α
u : Ultrafilter α
ua :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    u
ub :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    u
v : Ultrafilter α
hv :
  Membership.mem (γ := Set (Ultrafilter α))
    ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) (a ∩ b)) v
refine_2 : a ∩ b ⊆ b
⊢ Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    v

Tactic:
apply mem_of_superset hv

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
a b : Set α
u : Ultrafilter α
ua :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    u
ub :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    u
v : Ultrafilter α
hv :
  Membership.mem (γ := Set (Ultrafilter α))
    ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) (a ∩ b)) v
⊢ a ∩ b ⊆ a

Tactic:
simp [inter_subset_right]

Premises used: Set.inter_subset_right
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
a b : Set α
u : Ultrafilter α
ua :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    u
ub :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) b)
    u
v : Ultrafilter α
hv :
  Membership.mem (γ := Set (Ultrafilter α))
    ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) (a ∩ b)) v
⊢ a ∩ b ⊆ b

Tactic:
simp [inter_subset_right]

Premises used: Set.inter_subset_right
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
s : Set α
⊢ IsOpen.{u} (X := Ultrafilter α) {u : Ultrafilter α | s ∈ u}

Tactic:
ultrafilterBasis_is_basis.isOpen ⟨s, rfl⟩

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, ultrafilterBasis_is_basis, Exists.intro, rfl
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
s : Set α
rw : IsOpen.{u} (X := Ultrafilter α) {u : Ultrafilter α | s ∈ u}ᶜ
⊢ IsClosed.{u} (X := Ultrafilter α) {u : Ultrafilter α | s ∈ u}

Tactic:
rw [← isOpen_compl_iff]

Premises used: isOpen_compl_iff
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
s : Set α
⊢ IsOpen.{u} (X := Ultrafilter α) {u : Ultrafilter α | sᶜ ∈ u}

Tactic:
ultrafilter_isOpen_basic sᶜ

Premises used: Compl.compl, ultrafilter_isOpen_basic
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
s : Set α
h : Eq.{u + 1} (α := Set (Ultrafilter α)) {u : Ultrafilter α | s ∈ u}ᶜ {u : Ultrafilter α | sᶜ ∈ u}
⊢ IsOpen.{u} (X := Ultrafilter α) {u : Ultrafilter α | s ∈ u}ᶜ

Tactic:
convert! ultrafilter_isOpen_basic sᶜ using 1

Premises used: Compl.compl, ultrafilter_isOpen_basic
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
s : Set α
h :
  ∀ (u : Ultrafilter α),
    Membership.mem (γ := Set (Ultrafilter α)) {u : Ultrafilter α | s ∈ u}ᶜ u ↔
      Membership.mem (γ := Set (Ultrafilter α)) {u : Ultrafilter α | sᶜ ∈ u} u
⊢ Eq.{u + 1} (α := Set (Ultrafilter α)) {u : Ultrafilter α | s ∈ u}ᶜ {u : Ultrafilter α | sᶜ ∈ u}

Tactic:
ext u
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
s : Set α
u : Ultrafilter α
⊢ Membership.mem (γ := Set (Ultrafilter α)) {u : Ultrafilter α | s ∈ u}ᶜ u ↔
    Membership.mem (γ := Set (Ultrafilter α)) {u : Ultrafilter α | sᶜ ∈ u} u

Tactic:
Ultrafilter.compl_mem_iff_notMem.symm

Premises used: Set.Mem, setOf, Ultrafilter.compl_mem_iff_notMem, Not, Iff.symm
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
s : Set α
u : Ultrafilter α
⊢ Membership.mem (γ := Set (Ultrafilter α)) {u : Ultrafilter α | s ∈ u}ᶜ u ↔
    Membership.mem (γ := Set (Ultrafilter α)) {u : Ultrafilter α | sᶜ ∈ u} u

Tactic:
exact Ultrafilter.compl_mem_iff_notMem.symm

Premises used: Ultrafilter.compl_mem_iff_notMem, Iff.symm
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
rw : (↑u : Filter (Ultrafilter α)) ≤ 𝓝 x ↔ (↑(joinM u) : Filter α) ≤ (↑x : Filter α)
⊢ (↑u : Filter (Ultrafilter α)) ≤ 𝓝 x ↔ x = joinM u

Tactic:
rw [eq_comm, ← Ultrafilter.coe_le_coe]

Premises used: Ultrafilter.coe_le_coe, eq_comm
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
change : (↑u : Filter (Ultrafilter α)) ≤ 𝓝 x ↔ ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
⊢ (↑u : Filter (Ultrafilter α)) ≤ 𝓝 x ↔ (↑(joinM u) : Filter α) ≤ (↑x : Filter α)

Tactic:
change ↑u ≤ 𝓝 x ↔ ∀ s ∈ x, { v : Ultrafilter α | s ∈ v } ∈ u

Premises used: nhds, Ultrafilter
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
simp :
  (∀ (i : Set (Ultrafilter α))
      (i_1 :
        x ∈ i ∧
          Membership.mem (γ := Set (Set (Ultrafilter α))) (range fun (s : Set α) ↦ {u : Ultrafilter α | s ∈ u}) i),
      i ∈ (↑u : Filter (Ultrafilter α))) ↔
    ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
⊢ (↑u : Filter (Ultrafilter α)) ≤ 𝓝 x ↔ ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u

Tactic:
simp only [TopologicalSpace.nhds_generateFrom, le_iInf_iff, ultrafilterBasis, le_principal_iff,
    mem_setOf_eq]

Premises used: Filter.le_principal_iff, le_iInf_iff, TopologicalSpace.nhds_generateFrom, Set.mem_setOf_eq, ultrafilterBasis
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
mp :
  (∀ (i : Set (Ultrafilter α))
      (i_1 :
        x ∈ i ∧
          Membership.mem (γ := Set (Set (Ultrafilter α))) (range fun (s : Set α) ↦ {u : Ultrafilter α | s ∈ u}) i),
      i ∈ (↑u : Filter (Ultrafilter α))) →
    ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
mpr :
  (∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u) →
    ∀ (i : Set (Ultrafilter α))
      (i_1 :
        x ∈ i ∧
          Membership.mem (γ := Set (Set (Ultrafilter α))) (range fun (s : Set α) ↦ {u : Ultrafilter α | s ∈ u}) i),
      i ∈ (↑u : Filter (Ultrafilter α))
⊢ (∀ (i : Set (Ultrafilter α))
      (i_1 :
        x ∈ i ∧
          Membership.mem (γ := Set (Set (Ultrafilter α))) (range fun (s : Set α) ↦ {u : Ultrafilter α | s ∈ u}) i),
      i ∈ (↑u : Filter (Ultrafilter α))) ↔
    ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u

Tactic:
constructor
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h :
  ∀ (i : Set (Ultrafilter α))
    (i_1 :
      x ∈ i ∧ Membership.mem (γ := Set (Set (Ultrafilter α))) (range fun (s : Set α) ↦ {u : Ultrafilter α | s ∈ u}) i),
    i ∈ (↑u : Filter (Ultrafilter α))
a : Set α
ha : a ∈ x
⊢ {v : Ultrafilter α | a ∈ v} ∈ u

Tactic:
h _ ⟨ha, a, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h :
  ∀ (i : Set (Ultrafilter α))
    (i_1 :
      x ∈ i ∧ Membership.mem (γ := Set (Set (Ultrafilter α))) (range fun (s : Set α) ↦ {u : Ultrafilter α | s ∈ u}) i),
    i ∈ (↑u : Filter (Ultrafilter α))
a : Set α
ha : a ∈ x
⊢ {v : Ultrafilter α | a ∈ v} ∈ u

Tactic:
exact h _ ⟨ha, a, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Compactification.StoneCech
Goal:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
h : ∀ s ∈ x, {v : Ultrafilter α | s ∈ v} ∈ u
a : Set α
xi :
  Membership.mem (γ := Set (Ultrafilter α)) ((fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a)
    x
⊢ (fun (s : Set α) ↦ ({u : Ultrafilter α | s ∈ u} : Set (Ultrafilter α))) a ∈ (↑u : Filter (Ultrafilter α))

Tactic:
h _ xi

Premises used: Set.Mem