internlm/Lean-Github huggingface dataset:
Theorem: product_of_two_primes_neq_zero
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
⊢ p * q ≠ 0
Tactic:
have h1 : p ≠ 0 := by
  apply Nat.Prime.ne_zero hp
Proof state after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
⊢ p * q ≠ 0
Theorem: product_of_two_primes_neq_zero
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
⊢ p * q ≠ 0
Tactic:
have h2 : q ≠ 0 := by
  apply Nat.Prime.ne_zero hq
Proof state after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
h2 : q ≠ 0
⊢ p * q ≠ 0
Theorem: product_of_two_primes_neq_zero
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
h2 : q ≠ 0
⊢ p * q ≠ 0
Tactic:
have h3 : p*q ≠ 0 := by
  apply Nat.mul_ne_zero h1 h2
Proof state after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
h2 : q ≠ 0
h3 : p * q ≠ 0
⊢ p * q ≠ 0
Theorem: product_of_two_primes_neq_zero
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
h2 : q ≠ 0
h3 : p * q ≠ 0
⊢ p * q ≠ 0
Tactic:
apply h3
Proof state after:
no goals
Theorem: product_of_two_primes_neq_zero
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
⊢ p ≠ 0
Tactic:
apply Nat.Prime.ne_zero hp
Proof state after:
no goals
Theorem: product_of_two_primes_neq_zero
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
⊢ q ≠ 0
Tactic:
apply Nat.Prime.ne_zero hq
Proof state after:
no goals
Theorem: product_of_two_primes_neq_zero
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
h1 : p ≠ 0
h2 : q ≠ 0
⊢ p * q ≠ 0
Tactic:
apply Nat.mul_ne_zero h1 h2
Proof state after:
no goals
Theorem: lagrange_theorem
Proof state before:
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this : orderOf a > 0
x✝ : { x // x ∈ H }
x : α
h : x ∈ H
⊢ { val := x, property := h } ∈
    {
      val :=
        Quotient.mk'
          (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
            (Lean.Internal.coeM (range (orderOf a)))),
      nodup :=
        (_ :
          Multiset.Nodup
            (Quotient.mk'
              (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
                (Lean.Internal.coeM (range (orderOf a)))))) }
Tactic:
obtain ⟨n, h⟩ := Subgroup.mem_closure_singleton.mp h
Proof state after:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this : orderOf a > 0
x✝ : { x // x ∈ H }
x : α
h✝ : x ∈ H
n : ℤ
h : a ^ n = x
⊢ { val := x, property := h✝ } ∈
    {
      val :=
        Quotient.mk'
          (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
            (Lean.Internal.coeM (range (orderOf a)))),
      nodup :=
        (_ :
          Multiset.Nodup
            (Quotient.mk'
              (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
                (Lean.Internal.coeM (range (orderOf a)))))) }
Theorem: lagrange_theorem
Proof state before:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this : orderOf a > 0
x✝ : { x // x ∈ H }
x : α
h✝ : x ∈ H
n : ℤ
h : a ^ n = x
⊢ { val := x, property := h✝ } ∈
    {
      val :=
        Quotient.mk'
          (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
            (Lean.Internal.coeM (range (orderOf a)))),
      nodup :=
        (_ :
          Multiset.Nodup
            (Quotient.mk'
              (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
                (Lean.Internal.coeM (range (orderOf a)))))) }
Tactic:
subst h
Proof state after:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this : orderOf a > 0
x✝ : { x // x ∈ H }
n : ℤ
h : a ^ n ∈ H
⊢ { val := a ^ n, property := h } ∈
    {
      val :=
        Quotient.mk'
          (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
            (Lean.Internal.coeM (range (orderOf a)))),
      nodup :=
        (_ :
          Multiset.Nodup
            (Quotient.mk'
              (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
                (Lean.Internal.coeM (range (orderOf a)))))) }
Theorem: lagrange_theorem
Proof state before:
case intro
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this : orderOf a > 0
x✝ : { x // x ∈ H }
n : ℤ
h : a ^ n ∈ H
⊢ { val := a ^ n, property := h } ∈
    {
      val :=
        Quotient.mk'
          (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
            (Lean.Internal.coeM (range (orderOf a)))),
      nodup :=
        (_ :
          Multiset.Nodup
            (Quotient.mk'
              (map (fun n => { val := a ^ n, property := (_ : a ^ n ∈ Subgroup.closure {a}) })
                (Lean.Internal.coeM (range (orderOf a)))))) }
Tactic:
sorry
Proof state after:
no goals
Theorem: lagrange_theorem
Proof state before:
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this✝¹ : orderOf a > 0
this✝ : Fintype { x // x ∈ H }
this : Fintype.card { x // x ∈ H } = orderOf a
⊢ orderOf a ∣ Fintype.card α
Tactic:
rw [←this]
Proof state after:
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this✝¹ : orderOf a > 0
this✝ : Fintype { x // x ∈ H }
this : Fintype.card { x // x ∈ H } = orderOf a
⊢ Fintype.card { x // x ∈ H } ∣ Fintype.card α
Theorem: lagrange_theorem
Proof state before:
α : Type u_1
inst✝¹ : Group α
inst✝ : Fintype α
a : α
H : Subgroup α := Subgroup.closure {a}
this✝¹ : orderOf a > 0
this✝ : Fintype { x // x ∈ H }
this : Fintype.card { x // x ∈ H } = orderOf a
⊢ Fintype.card { x // x ∈ H } ∣ Fintype.card α
Tactic:
apply Subgroup.card_subgroup_dvd_card
Proof state after:
no goals
Theorem: euler_theorem
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
⊢ ∀ (t : (ZMod (p * q))ˣ), t ^ φ (p * q) = 1
Tactic:
have h2: NeZero (p*q) := by
  apply ne_zero_product_of_primes hp hq
Proof state after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
⊢ ∀ (t : (ZMod (p * q))ˣ), t ^ φ (p * q) = 1
Theorem: euler_theorem
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
⊢ ∀ (t : (ZMod (p * q))ˣ), t ^ φ (p * q) = 1
Tactic:
have h1: Fintype.card (ZMod (p*q))ˣ = Nat.totient (p*q) := by
  rw [ZMod.card_units_eq_totient]
Proof state after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
⊢ ∀ (t : (ZMod (p * q))ˣ), t ^ φ (p * q) = 1
Theorem: euler_theorem
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
⊢ ∀ (t : (ZMod (p * q))ˣ), t ^ φ (p * q) = 1
Tactic:
intro t
Proof state after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
t : (ZMod (p * q))ˣ
⊢ t ^ φ (p * q) = 1
Theorem: euler_theorem
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
t : (ZMod (p * q))ˣ
⊢ t ^ φ (p * q) = 1
Tactic:
rw [←orderOf_dvd_iff_pow_eq_one, ←h1]
Proof state after:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
t : (ZMod (p * q))ˣ
⊢ orderOf t ∣ Fintype.card (ZMod (p * q))ˣ
Theorem: euler_theorem
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
h1 : Fintype.card (ZMod (p * q))ˣ = φ (p * q)
t : (ZMod (p * q))ˣ
⊢ orderOf t ∣ Fintype.card (ZMod (p * q))ˣ
Tactic:
apply lagrange_theorem
Proof state after:
no goals
Theorem: euler_theorem
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
⊢ NeZero (p * q)
Tactic:
apply ne_zero_product_of_primes hp hq
Proof state after:
no goals
Theorem: euler_theorem
Proof state before:
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
⊢ Fintype.card (ZMod (p * q))ˣ = φ (p * q)
Tactic:
rw [ZMod.card_units_eq_totient]
Proof state after:
no goals
Theorem: atleast_two_primes_in_range
Proof state before:
⊢ 3 ∈ List.remove 2 (rangeFrom1ToN MAX)
Tactic:
rw[List.mem_remove_iff]
Proof state after:
⊢ 3 ∈ rangeFrom1ToN MAX ∧ 3 ≠ 2
Theorem: atleast_two_primes_in_range
Proof state before:
⊢ 3 ∈ rangeFrom1ToN MAX ∧ 3 ≠ 2
Tactic:
simp
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_principal_def
Proof state before:
α : Type u_1
s t : Set α
⊢ s ∈ 𝓟 t ↔ t ⊆ s
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_principal_self
Proof state before:
α : Type u_1
s : Set α
⊢ s ∈ 𝓟 s
Tactic:
exact (mem_principal_def _ _).mpr subset_rfl
Proof state after:
no goals
Theorem: FilterGame.Filter.le_principal_iff
Proof state before:
α : Type u_1
s : Set α
f : Filter α
⊢ f ≤ 𝓟 s ↔ s ∈ f
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
s : Set α
f : Filter α
⊢ f ≤ 𝓟 s → s ∈ f

case mpr
α : Type u_1
s : Set α
f : Filter α
⊢ s ∈ f → f ≤ 𝓟 s
Theorem: FilterGame.Filter.le_principal_iff
Proof state before:
case mp
α : Type u_1
s : Set α
f : Filter α
⊢ f ≤ 𝓟 s → s ∈ f

case mpr
α : Type u_1
s : Set α
f : Filter α
⊢ s ∈ f → f ≤ 𝓟 s
Tactic:
. intros h
  exact h _ (mem_principal_self s)
Proof state after:
case mpr
α : Type u_1
s : Set α
f : Filter α
⊢ s ∈ f → f ≤ 𝓟 s
Theorem: FilterGame.Filter.le_principal_iff
Proof state before:
case mpr
α : Type u_1
s : Set α
f : Filter α
⊢ s ∈ f → f ≤ 𝓟 s
Tactic:
. intros h t ht
  rw [mem_principal_def] at ht
  exact superset_mem h ht
Proof state after:
no goals
Theorem: FilterGame.Filter.le_principal_iff
Proof state before:
case mp
α : Type u_1
s : Set α
f : Filter α
⊢ f ≤ 𝓟 s → s ∈ f
Tactic:
intros h
Proof state after:
case mp
α : Type u_1
s : Set α
f : Filter α
h : f ≤ 𝓟 s
⊢ s ∈ f
Theorem: FilterGame.Filter.le_principal_iff
Proof state before:
case mp
α : Type u_1
s : Set α
f : Filter α
h : f ≤ 𝓟 s
⊢ s ∈ f
Tactic:
exact h _ (mem_principal_self s)
Proof state after:
no goals
Theorem: FilterGame.Filter.le_principal_iff
Proof state before:
case mpr
α : Type u_1
s : Set α
f : Filter α
⊢ s ∈ f → f ≤ 𝓟 s
Tactic:
intros h t ht
Proof state after:
case mpr
α : Type u_1
s : Set α
f : Filter α
h : s ∈ f
t : Set α
ht : t ∈ 𝓟 s
⊢ t ∈ f
Theorem: FilterGame.Filter.le_principal_iff
Proof state before:
case mpr
α : Type u_1
s : Set α
f : Filter α
h : s ∈ f
t : Set α
ht : t ∈ 𝓟 s
⊢ t ∈ f
Tactic:
rw [mem_principal_def] at ht
Proof state after:
case mpr
α : Type u_1
s : Set α
f : Filter α
h : s ∈ f
t : Set α
ht : s ⊆ t
⊢ t ∈ f
Theorem: FilterGame.Filter.le_principal_iff
Proof state before:
case mpr
α : Type u_1
s : Set α
f : Filter α
h : s ∈ f
t : Set α
ht : s ⊆ t
⊢ t ∈ f
Tactic:
exact superset_mem h ht
Proof state after:
no goals
Theorem: FilterGame.Filter.principal_mono
Proof state before:
α : Type u_1
s t : Set α
⊢ 𝓟 s ≤ 𝓟 t ↔ s ⊆ t
Tactic:
rw [le_principal_iff, mem_principal_def]
Proof state after:
no goals
Theorem: FilterGame.Filter.principal_eq_iff_eq
Proof state before:
α : Type u_1
s t : Set α
⊢ 𝓟 s = 𝓟 t ↔ s = t
Tactic:
simp only [le_antisymm_iff, le_principal_iff, mem_principal_def]
Proof state after:
α : Type u_1
s t : Set α
⊢ s ⊆ t ∧ t ⊆ s ↔ s ≤ t ∧ t ≤ s
Theorem: FilterGame.Filter.principal_eq_iff_eq
Proof state before:
α : Type u_1
s t : Set α
⊢ s ⊆ t ∧ t ⊆ s ↔ s ≤ t ∧ t ≤ s
Tactic:
rfl
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_top_def
Proof state before:
α : Type u_1
s : Set α
⊢ s ∈ ⊤ ↔ ∀ (x : α), x ∈ s
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_top_iff_eq_univ
Proof state before:
α : Type u_1
s : Set α
⊢ s ∈ ⊤ ↔ s = Set.univ
Tactic:
rw [mem_top_def, Set.eq_univ_iff_forall]
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_bot
Proof state before:
α : Type u_1
s : Set α
⊢ s ∈ ⊥
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
α : Type u_1
f : Filter α
⊢ ∅ ∈ f ↔ f = ⊥
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
f : Filter α
⊢ ∅ ∈ f → f = ⊥

case mpr
α : Type u_1
f : Filter α
⊢ f = ⊥ → ∅ ∈ f
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mp
α : Type u_1
f : Filter α
⊢ ∅ ∈ f → f = ⊥

case mpr
α : Type u_1
f : Filter α
⊢ f = ⊥ → ∅ ∈ f
Tactic:
. intros h
  apply ext
  intros s
  apply Iff.intro
  . intros _; exact True.intro
  . intros _; exact superset_mem h (Set.empty_subset _)
Proof state after:
case mpr
α : Type u_1
f : Filter α
⊢ f = ⊥ → ∅ ∈ f
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mpr
α : Type u_1
f : Filter α
⊢ f = ⊥ → ∅ ∈ f
Tactic:
. intros h
  rw [h]
  exact Set.mem_univ _
Proof state after:
no goals
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mp
α : Type u_1
f : Filter α
⊢ ∅ ∈ f → f = ⊥
Tactic:
intros h
Proof state after:
case mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
⊢ f = ⊥
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
⊢ f = ⊥
Tactic:
apply ext
Proof state after:
case mp.a
α : Type u_1
f : Filter α
h : ∅ ∈ f
⊢ ∀ (s : Set α), s ∈ f ↔ s ∈ ⊥
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mp.a
α : Type u_1
f : Filter α
h : ∅ ∈ f
⊢ ∀ (s : Set α), s ∈ f ↔ s ∈ ⊥
Tactic:
intros s
Proof state after:
case mp.a
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ f ↔ s ∈ ⊥
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mp.a
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ f ↔ s ∈ ⊥
Tactic:
apply Iff.intro
Proof state after:
case mp.a.mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ f → s ∈ ⊥

case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ ⊥ → s ∈ f
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mp.a.mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ f → s ∈ ⊥

case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ ⊥ → s ∈ f
Tactic:
. intros _; exact True.intro
Proof state after:
case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ ⊥ → s ∈ f
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ ⊥ → s ∈ f
Tactic:
. intros _; exact superset_mem h (Set.empty_subset _)
Proof state after:
no goals
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mp.a.mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ f → s ∈ ⊥
Tactic:
intros _
Proof state after:
case mp.a.mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
a✝ : s ∈ f
⊢ s ∈ ⊥
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mp.a.mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
a✝ : s ∈ f
⊢ s ∈ ⊥
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ ⊥ → s ∈ f
Tactic:
intros _
Proof state after:
case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
a✝ : s ∈ ⊥
⊢ s ∈ f
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
a✝ : s ∈ ⊥
⊢ s ∈ f
Tactic:
exact superset_mem h (Set.empty_subset _)
Proof state after:
no goals
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mpr
α : Type u_1
f : Filter α
⊢ f = ⊥ → ∅ ∈ f
Tactic:
intros h
Proof state after:
case mpr
α : Type u_1
f : Filter α
h : f = ⊥
⊢ ∅ ∈ f
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mpr
α : Type u_1
f : Filter α
h : f = ⊥
⊢ ∅ ∈ f
Tactic:
rw [h]
Proof state after:
case mpr
α : Type u_1
f : Filter α
h : f = ⊥
⊢ ∅ ∈ ⊥
Theorem: FilterGame.Filter.empty_mem_iff_eq_bot
Proof state before:
case mpr
α : Type u_1
f : Filter α
h : f = ⊥
⊢ ∅ ∈ ⊥
Tactic:
exact Set.mem_univ _
Proof state after:
no goals
Theorem: FilterGame.Filter.principal_univ_eq_top
Proof state before:
α : Type u_1
⊢ 𝓟 Set.univ = ⊤
Tactic:
apply top_unique
Proof state after:
case h
α : Type u_1
⊢ ⊤ ≤ 𝓟 Set.univ
Theorem: FilterGame.Filter.principal_univ_eq_top
Proof state before:
case h
α : Type u_1
⊢ ⊤ ≤ 𝓟 Set.univ
Tactic:
rw [le_principal_iff, mem_top_def]
Proof state after:
case h
α : Type u_1
⊢ ∀ (x : α), x ∈ Set.univ
Theorem: FilterGame.Filter.principal_univ_eq_top
Proof state before:
case h
α : Type u_1
⊢ ∀ (x : α), x ∈ Set.univ
Tactic:
intros x
Proof state after:
case h
α : Type u_1
x : α
⊢ x ∈ Set.univ
Theorem: FilterGame.Filter.principal_univ_eq_top
Proof state before:
case h
α : Type u_1
x : α
⊢ x ∈ Set.univ
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: FilterGame.Filter.principal_empty_eq_bot
Proof state before:
α : Type u_1
⊢ 𝓟 ∅ = ⊥
Tactic:
apply bot_unique
Proof state after:
case h
α : Type u_1
⊢ 𝓟 ∅ ≤ ⊥
Theorem: FilterGame.Filter.principal_empty_eq_bot
Proof state before:
case h
α : Type u_1
⊢ 𝓟 ∅ ≤ ⊥
Tactic:
intros s hs
Proof state after:
case h
α : Type u_1
s : Set α
hs : s ∈ ⊥
⊢ s ∈ 𝓟 ∅
Theorem: FilterGame.Filter.principal_empty_eq_bot
Proof state before:
case h
α : Type u_1
s : Set α
hs : s ∈ ⊥
⊢ s ∈ 𝓟 ∅
Tactic:
exact Set.empty_subset s
Proof state after:
no goals
Theorem: FilterGame.Filter.compl_not_mem
Proof state before:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
⊢ ¬sᶜ ∈ f
Tactic:
intros h'
Proof state after:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ False
Theorem: FilterGame.Filter.compl_not_mem
Proof state before:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ False
Tactic:
apply hf
Proof state after:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ f = ⊥
Theorem: FilterGame.Filter.compl_not_mem
Proof state before:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ f = ⊥
Tactic:
rw [← empty_mem_iff_eq_bot, ← Set.compl_inter_self s]
Proof state after:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ sᶜ ∩ s ∈ f
Theorem: FilterGame.Filter.compl_not_mem
Proof state before:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ sᶜ ∩ s ∈ f
Tactic:
exact inter_mem h' h
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_def
Proof state before:
α : Type u_1
f : Filter α
s : Set α
⊢ s ∈ f ↔ s ∈ f.sets
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: FilterGame.Filter.eq_def
Proof state before:
α : Type u_1
f g : Filter α
⊢ f = g ↔ f.sets = g.sets
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
f g : Filter α
⊢ f = g → f.sets = g.sets

case mpr
α : Type u_1
f g : Filter α
⊢ f.sets = g.sets → f = g
Theorem: FilterGame.Filter.eq_def
Proof state before:
case mp
α : Type u_1
f g : Filter α
⊢ f = g → f.sets = g.sets

case mpr
α : Type u_1
f g : Filter α
⊢ f.sets = g.sets → f = g
Tactic:
. intro h; rw [h]
Proof state after:
case mpr
α : Type u_1
f g : Filter α
⊢ f.sets = g.sets → f = g
Theorem: FilterGame.Filter.eq_def
Proof state before:
case mpr
α : Type u_1
f g : Filter α
⊢ f.sets = g.sets → f = g
Tactic:
. intro h; cases f; cases g; congr
Proof state after:
no goals
Theorem: FilterGame.Filter.eq_def
Proof state before:
case mp
α : Type u_1
f g : Filter α
⊢ f = g → f.sets = g.sets
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
f g : Filter α
h : f = g
⊢ f.sets = g.sets
Theorem: FilterGame.Filter.eq_def
Proof state before:
case mp
α : Type u_1
f g : Filter α
h : f = g
⊢ f.sets = g.sets
Tactic:
rw [h]
Proof state after:
no goals
Theorem: FilterGame.Filter.eq_def
Proof state before:
case mpr
α : Type u_1
f g : Filter α
⊢ f.sets = g.sets → f = g
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
f g : Filter α
h : f.sets = g.sets
⊢ f = g
Theorem: FilterGame.Filter.eq_def
Proof state before:
case mpr
α : Type u_1
f g : Filter α
h : f.sets = g.sets
⊢ f = g
Tactic:
cases f
Proof state after:
case mpr.mk
α : Type u_1
g : Filter α
sets✝ : Set (Set α)
univ_mem_sets✝ : Set.univ ∈ sets✝
superset_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h :
  { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
        inter_mem_sets := inter_mem_sets✝ }.sets =
    g.sets
⊢ { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ } =
    g
Theorem: FilterGame.Filter.eq_def
Proof state before:
case mpr.mk
α : Type u_1
g : Filter α
sets✝ : Set (Set α)
univ_mem_sets✝ : Set.univ ∈ sets✝
superset_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h :
  { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
        inter_mem_sets := inter_mem_sets✝ }.sets =
    g.sets
⊢ { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ } =
    g
Tactic:
cases g
Proof state after:
case mpr.mk.mk
α : Type u_1
sets✝¹ : Set (Set α)
univ_mem_sets✝¹ : Set.univ ∈ sets✝¹
superset_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → s ⊆ t → t ∈ sets✝¹
inter_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → s ∩ t ∈ sets✝¹
sets✝ : Set (Set α)
univ_mem_sets✝ : Set.univ ∈ sets✝
superset_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h :
  { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
        inter_mem_sets := inter_mem_sets✝¹ }.sets =
    { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
        inter_mem_sets := inter_mem_sets✝ }.sets
⊢ { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
      inter_mem_sets := inter_mem_sets✝¹ } =
    { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ }
Theorem: FilterGame.Filter.eq_def
Proof state before:
case mpr.mk.mk
α : Type u_1
sets✝¹ : Set (Set α)
univ_mem_sets✝¹ : Set.univ ∈ sets✝¹
superset_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → s ⊆ t → t ∈ sets✝¹
inter_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → s ∩ t ∈ sets✝¹
sets✝ : Set (Set α)
univ_mem_sets✝ : Set.univ ∈ sets✝
superset_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → s ⊆ t → t ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → s ∩ t ∈ sets✝
h :
  { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
        inter_mem_sets := inter_mem_sets✝¹ }.sets =
    { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
        inter_mem_sets := inter_mem_sets✝ }.sets
⊢ { sets := sets✝¹, univ_mem_sets := univ_mem_sets✝¹, superset_mem_sets := superset_mem_sets✝¹,
      inter_mem_sets := inter_mem_sets✝¹ } =
    { sets := sets✝, univ_mem_sets := univ_mem_sets✝, superset_mem_sets := superset_mem_sets✝,
      inter_mem_sets := inter_mem_sets✝ }
Tactic:
congr
Proof state after:
no goals
Theorem: FilterGame.Filter.ext_iff
Proof state before:
α : Type u_1
f g : Filter α
⊢ f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
Tactic:
sorry
Proof state after:
no goals
Theorem: FilterGame.Filter.ext
Proof state before:
α : Type u_1
f g : Filter α
⊢ (∀ (s : Set α), s ∈ f ↔ s ∈ g) → f = g
Tactic:
sorry
Proof state after:
no goals
Theorem: FilterGame.Filter.univ_mem
Proof state before:
α : Type u_1
f : Filter α
⊢ Set.univ ∈ f
Tactic:
exact f.univ_mem_sets
Proof state after:
no goals
Theorem: FilterGame.Filter.superset_mem
Proof state before:
α : Type u_1
f : Filter α
s t : Set α
hs : s ∈ f
h : s ⊆ t
⊢ t ∈ f
Tactic:
exact f.superset_mem_sets hs h
Proof state after:
no goals
Theorem: FilterGame.Filter.inter_mem
Proof state before:
α : Type u_1
f : Filter α
s t : Set α
hs : s ∈ f
ht : t ∈ f
⊢ s ∩ t ∈ f
Tactic:
exact f.inter_mem_sets hs ht
Proof state after:
no goals