internlm/Lean-Github huggingface dataset:
Theorem: abs_sub_le'
Proof state before:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ |a - c| ≤ |a - b| + |b - c|
Tactic:
apply abs_sub_le
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
⊢ seq_limit u l → seq_limit u l' → l = l'
Tactic:
intros hl hl'
Proof state after:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ l = l'
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ l = l'
Tactic:
apply eq_of_abs_sub_le_all
Proof state after:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ ∀ ε > 0, |l - l'| ≤ ε
Theorem: unique_limit
Proof state before:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ ∀ ε > 0, |l - l'| ≤ ε
Tactic:
intros ε ε_pos
Proof state after:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
⊢ |l - l'| ≤ ε
Theorem: unique_limit
Proof state before:
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
⊢ |l - l'| ≤ ε
Tactic:
rcases hl (ε/2) (by linarith) with ⟨N, hN⟩
Proof state after:
case a.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Theorem: unique_limit
Proof state before:
case a.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
rcases hl' (ε/2) (by linarith) with ⟨N', hN'⟩
Proof state after:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Theorem: unique_limit
Proof state before:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
specialize hN (max N N') (le_max_left _ _)
Proof state after:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
hN : |u (max N N') - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Theorem: unique_limit
Proof state before:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
hN : |u (max N N') - l| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
specialize hN' (max N N') (le_max_right _ _)
Proof state after:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Theorem: unique_limit
Proof state before:
case a.intro.intro
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
Tactic:
calc |l - l'| = |(l-u (max N N')) + (u (max N N') -l')| := by ring_nf
_ ≤ |l - u (max N N')| + |u (max N N') - l'| := by apply abs_add
_ = |u (max N N') - l| + |u (max N N') - l'| := by rw [abs_sub_comm]
_ ≤ ε/2 + ε/2 := by linarith
_ = ε := by ring
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
⊢ ε / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
⊢ ε / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - l'| = |l - u (max N N') + (u (max N N') - l')|
Tactic:
ring_nf
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - u (max N N') + (u (max N N') - l')| ≤ |l - u (max N N')| + |u (max N N') - l'|
Tactic:
apply abs_add
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |l - u (max N N')| + |u (max N N') - l'| = |u (max N N') - l| + |u (max N N') - l'|
Tactic:
rw [abs_sub_comm]
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ |u (max N N') - l| + |u (max N N') - l'| ≤ ε / 2 + ε / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: unique_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
N N' : ℕ
hN : |u (max N N') - l| ≤ ε / 2
hN' : |u (max N N') - l'| ≤ ε / 2
⊢ ε / 2 + ε / 2 = ε
Tactic:
ring
Proof state after:
no goals
Theorem: Finset.sum_univ_eq_single
Proof state before:
β : Type u
α : Type v
inst✝¹ : Fintype α
inst✝ : AddCommMonoid β
f : α → β
a : α
h : ∀ (b : α), b ≠ a → f b = 0
⊢ ∑ x : α, f x = f a
Tactic:
rw [Finset.sum_eq_single]
Proof state after:
case h₀
β : Type u
α : Type v
inst✝¹ : Fintype α
inst✝ : AddCommMonoid β
f : α → β
a : α
h : ∀ (b : α), b ≠ a → f b = 0
⊢ ∀ b ∈ univ, b ≠ a → f b = 0

case h₁
β : Type u
α : Type v
inst✝¹ : Fintype α
inst✝ : AddCommMonoid β
f : α → β
a : α
h : ∀ (b : α), b ≠ a → f b = 0
⊢ a ∉ univ → f a = 0
Theorem: Finset.sum_univ_eq_single
Proof state before:
case h₀
β : Type u
α : Type v
inst✝¹ : Fintype α
inst✝ : AddCommMonoid β
f : α → β
a : α
h : ∀ (b : α), b ≠ a → f b = 0
⊢ ∀ b ∈ univ, b ≠ a → f b = 0
Tactic:
tauto
Proof state after:
no goals
Theorem: Finset.sum_univ_eq_single
Proof state before:
case h₁
β : Type u
α : Type v
inst✝¹ : Fintype α
inst✝ : AddCommMonoid β
f : α → β
a : α
h : ∀ (b : α), b ≠ a → f b = 0
⊢ a ∉ univ → f a = 0
Tactic:
exact λ ha ↦ (ha <| Finset.mem_univ a).elim
Proof state after:
no goals
Theorem: Ideal.ker_mk
Proof state before:
R : Type u_1
S : Type ?u.14649
inst✝¹ : CommRing R
ι : Type ?u.14646
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker (Quotient.mk I) = I
Tactic:
ext x
Proof state after:
case h
R : Type u_1
S : Type ?u.14649
inst✝¹ : CommRing R
ι : Type ?u.14646
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
x : R
⊢ x ∈ ker (Quotient.mk I) ↔ x ∈ I
Theorem: Ideal.ker_mk
Proof state before:
case h
R : Type u_1
S : Type ?u.14649
inst✝¹ : CommRing R
ι : Type ?u.14646
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
x : R
⊢ x ∈ ker (Quotient.mk I) ↔ x ∈ I
Tactic:
rw [mem_ker, Quotient.eq_zero_iff_mem]
Proof state after:
no goals
Theorem: Ideal.ker_lift
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)
Tactic:
have : comap ((Quotient.lift I f H).comp (Quotient.mk I)) ⊥ = ker f := rfl
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : comap ((Quotient.lift I f H).comp (Quotient.mk I)) ⊥ = ker f
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)
Theorem: Ideal.ker_lift
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : comap ((Quotient.lift I f H).comp (Quotient.mk I)) ⊥ = ker f
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)
Tactic:
rw [← comap_comap] at this
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : comap (Quotient.mk I) (comap (Quotient.lift I f H) ⊥) = ker f
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)
Theorem: Ideal.ker_lift
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : comap (Quotient.mk I) (comap (Quotient.lift I f H) ⊥) = ker f
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)
Tactic:
apply_fun map (Quotient.mk I) at this
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : map (Quotient.mk I) (comap (Quotient.mk I) (comap (Quotient.lift I f H) ⊥)) = map (Quotient.mk I) (ker f)
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)
Theorem: Ideal.ker_lift
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.16994
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : map (Quotient.mk I) (comap (Quotient.mk I) (comap (Quotient.lift I f H) ⊥)) = map (Quotient.mk I) (ker f)
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)
Tactic:
rwa [map_comap_of_surjective _ Quotient.mk_surjective] at this
Proof state after:
no goals
Theorem: Ideal.injective_lift_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ Injective ⇑(Quotient.lift I f H) ↔ ker f = I
Tactic:
have : I ≤ ker f := H
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ Injective ⇑(Quotient.lift I f H) ↔ ker f = I
Theorem: Ideal.injective_lift_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ Injective ⇑(Quotient.lift I f H) ↔ ker f = I
Tactic:
rw [injective_iff_ker_eq_bot, ker_lift, map_eq_bot_iff_le_ker, ker_mk]
Proof state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ ker f ≤ I ↔ ker f = I
Theorem: Ideal.injective_lift_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ ker f ≤ I ↔ ker f = I
Tactic:
constructor
Proof state after:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ ker f ≤ I → ker f = I

case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ ker f = I → ker f ≤ I
Theorem: Ideal.injective_lift_iff
Proof state before:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ ker f ≤ I → ker f = I
Tactic:
exact fun h ↦ le_antisymm h this
Proof state after:
no goals
Theorem: Ideal.injective_lift_iff
Proof state before:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
this : I ≤ ker f
⊢ ker f = I → ker f ≤ I
Tactic:
rintro rfl
Proof state after:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
f : R →+* S
H : ∀ a ∈ ker f, f a = 0
this : ker f ≤ ker f
⊢ ker f ≤ ker f
Theorem: Ideal.injective_lift_iff
Proof state before:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
ι : Type ?u.22043
inst✝ : CommRing S
f : R →+* S
H : ∀ a ∈ ker f, f a = 0
this : ker f ≤ ker f
⊢ ker f ≤ ker f
Tactic:
rfl
Proof state after:
no goals
Theorem: lowerBounds_range
Proof state before:
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
⊢ x ∈ lowerBounds (Set.range s) ↔ ∀ (i : ι), x ≤ s i
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
⊢ x ∈ lowerBounds (Set.range s) → ∀ (i : ι), x ≤ s i

case mpr
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
⊢ (∀ (i : ι), x ≤ s i) → x ∈ lowerBounds (Set.range s)
Theorem: lowerBounds_range
Proof state before:
case mp
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
⊢ x ∈ lowerBounds (Set.range s) → ∀ (i : ι), x ≤ s i
Tactic:
intros hx i
Proof state after:
case mp
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : x ∈ lowerBounds (Set.range s)
i : ι
⊢ x ≤ s i
Theorem: lowerBounds_range
Proof state before:
case mp
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : x ∈ lowerBounds (Set.range s)
i : ι
⊢ x ≤ s i
Tactic:
apply hx
Proof state after:
case mp.a
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : x ∈ lowerBounds (Set.range s)
i : ι
⊢ s i ∈ Set.range s
Theorem: lowerBounds_range
Proof state before:
case mp.a
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : x ∈ lowerBounds (Set.range s)
i : ι
⊢ s i ∈ Set.range s
Tactic:
exact Set.mem_range_self i
Proof state after:
no goals
Theorem: lowerBounds_range
Proof state before:
case mpr
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
⊢ (∀ (i : ι), x ≤ s i) → x ∈ lowerBounds (Set.range s)
Tactic:
rintro hx y ⟨i, rfl⟩
Proof state after:
case mpr.intro
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : ∀ (i : ι), x ≤ s i
i : ι
⊢ x ≤ s i
Theorem: lowerBounds_range
Proof state before:
case mpr.intro
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : ∀ (i : ι), x ≤ s i
i : ι
⊢ x ≤ s i
Tactic:
exact hx i
Proof state after:
no goals
Theorem: Tutorial.isOpen_empty
Proof state before:
X : Type
T : Topology X
⊢ T.isOpen ∅
Tactic:
have : (∅ : Set X) = ⋃ i : Empty, i.rec := by
  rw [Set.iUnion_of_empty]
Proof state after:
X : Type
T : Topology X
this : ∅ = ⋃ i, Empty.rec (fun x => Set X) i
⊢ T.isOpen ∅
Theorem: Tutorial.isOpen_empty
Proof state before:
X : Type
T : Topology X
this : ∅ = ⋃ i, Empty.rec (fun x => Set X) i
⊢ T.isOpen ∅
Tactic:
rw [this]
Proof state after:
X : Type
T : Topology X
this : ∅ = ⋃ i, Empty.rec (fun x => Set X) i
⊢ T.isOpen (⋃ i, Empty.rec (fun x => Set X) i)
Theorem: Tutorial.isOpen_empty
Proof state before:
X : Type
T : Topology X
this : ∅ = ⋃ i, Empty.rec (fun x => Set X) i
⊢ T.isOpen (⋃ i, Empty.rec (fun x => Set X) i)
Tactic:
exact T.isOpen_iUnion Empty.rec
Proof state after:
no goals
Theorem: Tutorial.isOpen_empty
Proof state before:
X : Type
T : Topology X
⊢ ∅ = ⋃ i, Empty.rec (fun x => Set X) i
Tactic:
rw [Set.iUnion_of_empty]
Proof state after:
no goals
Theorem: Tutorial.isOpen_univ
Proof state before:
X : Type
T : Topology X
⊢ T.isOpen Set.univ
Tactic:
have : (Set.univ : Set X) = ⋂ i : Empty, i.rec := by
  rw [Set.iInter_of_empty]
Proof state after:
X : Type
T : Topology X
this : Set.univ = ⋂ i, Empty.rec (fun x => Set X) i
⊢ T.isOpen Set.univ
Theorem: Tutorial.isOpen_univ
Proof state before:
X : Type
T : Topology X
this : Set.univ = ⋂ i, Empty.rec (fun x => Set X) i
⊢ T.isOpen Set.univ
Tactic:
rw [this]
Proof state after:
X : Type
T : Topology X
this : Set.univ = ⋂ i, Empty.rec (fun x => Set X) i
⊢ T.isOpen (⋂ i, Empty.rec (fun x => Set X) i)
Theorem: Tutorial.isOpen_univ
Proof state before:
X : Type
T : Topology X
this : Set.univ = ⋂ i, Empty.rec (fun x => Set X) i
⊢ T.isOpen (⋂ i, Empty.rec (fun x => Set X) i)
Tactic:
exact T.isOpen_iInter  Empty.rec (Finite.of_fintype Empty)
Proof state after:
no goals
Theorem: Tutorial.isOpen_univ
Proof state before:
X : Type
T : Topology X
⊢ Set.univ = ⋂ i, Empty.rec (fun x => Set X) i
Tactic:
rw [Set.iInter_of_empty]
Proof state after:
no goals
Theorem: Tutorial.push_push
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
T : Topology X
⊢ g⁎ (f⁎ T) = (g ∘ f)⁎ T
Tactic:
ext V
Proof state after:
case isOpen.h.a
X Y Z : Type
f : X → Y
g : Y → Z
T : Topology X
V : Set Z
⊢ (g⁎ (f⁎ T)).isOpen V ↔ ((g ∘ f)⁎ T).isOpen V
Theorem: Tutorial.push_push
Proof state before:
case isOpen.h.a
X Y Z : Type
f : X → Y
g : Y → Z
T : Topology X
V : Set Z
⊢ (g⁎ (f⁎ T)).isOpen V ↔ ((g ∘ f)⁎ T).isOpen V
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: Tutorial.Subgroups.push_generate
Proof state before:
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ push f ∘ generate = generate ∘ Set.image ⇑f
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.weakening
Proof state before:
H : Type ?u.21661
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
h2 : Γ ⊆ Δ
⊢ Δ ⊢ A
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.ProvableFrom.insert
Proof state before:
H : Type ?u.21714
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Insert.insert B Γ ⊢ A
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.deduction_theorem
Proof state before:
H : Type ?u.21772
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ B
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.Provable.mp
Proof state before:
H : Type ?u.21830
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ B
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.soundness_theorem
Proof state before:
H : Type ?u.21865
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊨ A
Tactic:
sorry
Proof state after:
no goals
Theorem: IntuitionisticPropositionalLogic.valid_of_provable
Proof state before:
H : Type ?u.21898
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Provable A
⊢ Valid A
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.isSupUnion
Proof state before:
case mpr.a
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
t : Set Y
ht : ⋃₀ S ≤ t
u : Set Y
hu : u ∈ S
x : Y
hx : x ∈ u
⊢ x ∈ ⋃₀ S
Tactic:
use u
Proof state after:
no goals
Theorem: Tutorial.push_Sup
Proof state before:
X Y : Type
f : X → Y
t : Set (Topology X)
⊢ f⁎ (Sup t) = Sup (f⁎ '' t)
Tactic:
ext V
Proof state after:
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ (f⁎ (Sup t)).isOpen V ↔ (Sup (f⁎ '' t)).isOpen V
Theorem: Tutorial.push_Sup
Proof state before:
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ (f⁎ (Sup t)).isOpen V ↔ (Sup (f⁎ '' t)).isOpen V
Tactic:
rw [isOpen_Sup, Set.forall_mem_image]
Proof state after:
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ (f⁎ (Sup t)).isOpen V ↔ ∀ ⦃x : Topology X⦄, x ∈ t → (f⁎ x).isOpen V
Theorem: Tutorial.push_Sup
Proof state before:
case isOpen.h.a
X Y : Type
f : X → Y
t : Set (Topology X)
V : Set Y
⊢ (f⁎ (Sup t)).isOpen V ↔ ∀ ⦃x : Topology X⦄, x ∈ t → (f⁎ x).isOpen V
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: Tutorial.left_comm_of_right_comm
Proof state before:
X : Type
inst✝⁷ : PartialOrder X
inst✝⁶ : CompleteLattice X
Y : Type
inst✝⁵ : PartialOrder Y
inst✝⁴ : CompleteLattice Y
Z✝ : Type
inst✝³ : PartialOrder Z✝
inst✝² : CompleteLattice Z✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
⊢ lWZ ∘ lZX = lWY ∘ lYX
Tactic:
have A₁ := hXZ.compose hZW
Proof state after:
X : Type
inst✝⁷ : PartialOrder X
inst✝⁶ : CompleteLattice X
Y : Type
inst✝⁵ : PartialOrder Y
inst✝⁴ : CompleteLattice Y
Z✝ : Type
inst✝³ : PartialOrder Z✝
inst✝² : CompleteLattice Z✝
W : Type
inst✝¹ : PartialOrder W
Z : Type
inst✝ : PartialOrder Z
lYX : X → Y
uXY : Y → X
hXY : adjunction lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : adjunction lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : adjunction lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : adjunction lZX uXZ
h : uXZ ∘ uZW = uXY ∘ uYW
A₁ : adjunction (lWZ ∘ lZX) (uXZ ∘ uZW)
⊢ lWZ ∘ lZX = lWY ∘ lYX
Theorem: Tutorial.Subgroups.push_generate
Proof state before:
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ push f ∘ generate = generate ∘ Set.image ⇑f
Tactic:
apply left_comm_of_right_comm
Proof state after:
case hXY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (Set.image ⇑f) ?uXY

case hZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) ?uZW

case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ ?uZW = ?uXY ∘ ?uYW

case uXY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Set G' → Set G

case uZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Subgroup G

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G
Theorem: Tutorial.Subgroups.push_generate
Proof state before:
case hXY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (Set.image ⇑f) ?uXY

case hZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) ?uZW

case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ ?uZW = ?uXY ∘ ?uYW

case uXY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Set G' → Set G

case uZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Subgroup G

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G
Tactic:
apply image_preimage_adjunction
Proof state after:
case hZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) ?uZW

case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ ?uZW = Set.preimage ⇑f ∘ ?uYW

case uZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Subgroup G

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G
Theorem: Tutorial.Subgroups.push_generate
Proof state before:
case hZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) ?uZW

case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ ?uZW = Set.preimage ⇑f ∘ ?uYW

case uZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Subgroup G

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G
Tactic:
apply push_pull_adjunction
Proof state after:
case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ pull f = Set.preimage ⇑f ∘ ?uYW

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G