internlm/Lean-Github huggingface dataset:
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
A₁ : adjunction (lWZ ∘ lZX) (uXY ∘ uYW)
⊢ lWZ ∘ lZX = lWY ∘ lYX
Tactic:
exact unique_left A₁ (hXY.compose hWY)
Proof state after:
no goals
Theorem: Tutorial.left_comm_of_right_comm
Proof state before:
case A₁
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
⊢ ?m.150838
Tactic:
exact hXZ.compose hZW
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:
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
Theorem: Tutorial.Subgroups.push_generate
Proof state before:
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
Tactic:
apply generate_forget_adjunction
Proof state after:
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 ∘ forget

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 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 ∘ forget

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G
Tactic:
apply generate_forget_adjunction
Proof state after:
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ forget ∘ pull f = Set.preimage ↑f ∘ forget
Theorem: Tutorial.Subgroups.push_generate
Proof state before:
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ forget ∘ pull f = Set.preimage ↑f ∘ forget
Tactic:
ext H
Proof state after:
case h.h.h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
H : Subgroup G'
x✝ : G
⊢ x✝ ∈ (forget ∘ pull f) H ↔ x✝ ∈ (Set.preimage ↑f ∘ forget) H
Theorem: Tutorial.Subgroups.push_generate
Proof state before:
case h.h.h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
H : Subgroup G'
x✝ : G
⊢ x✝ ∈ (forget ∘ pull f) H ↔ x✝ ∈ (Set.preimage ↑f ∘ forget) H
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: uniq_limit
Proof state before:
u : ℕ → ℝ
l l' : ℝ
⊢ seq_limit u l → seq_limit u l' → l = l'
Tactic:
sorry
Proof state after:
no goals
Theorem: id_le_extraction'
Proof state before:
φ : ℕ → ℕ
⊢ extraction φ → ∀ (n : ℕ), n ≤ φ n
Tactic:
intros hyp n
Proof state after:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
⊢ n ≤ φ n
Theorem: id_le_extraction'
Proof state before:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
⊢ n ≤ φ n
Tactic:
induction n with
| zero =>  exact Nat.zero_le _
| succ n ih => exact Nat.succ_le_of_lt (by linarith [hyp n (n+1) (by linarith)])
Proof state after:
no goals
Theorem: id_le_extraction'
Proof state before:
case zero
φ : ℕ → ℕ
hyp : extraction φ
⊢ Nat.zero ≤ φ Nat.zero
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: id_le_extraction'
Proof state before:
case succ
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
ih : n ≤ φ n
⊢ Nat.succ n ≤ φ (Nat.succ n)
Tactic:
exact Nat.succ_le_of_lt (by linarith [hyp n (n+1) (by linarith)])
Proof state after:
no goals
Theorem: id_le_extraction'
Proof state before:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
ih : n ≤ φ n
⊢ n < φ (Nat.succ n)
Tactic:
linarith [hyp n (n+1) (by linarith)]
Proof state after:
no goals
Theorem: id_le_extraction'
Proof state before:
φ : ℕ → ℕ
hyp : extraction φ
n : ℕ
ih : n ≤ φ n
⊢ n < n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: extraction_ge
Proof state before:
φ : ℕ → ℕ
⊢ extraction φ → ∀ (N N' : ℕ), ∃ n ≥ N', φ n ≥ N
Tactic:
sorry
Proof state after:
no goals
Theorem: near_cluster
Proof state before:
u : ℕ → ℝ
a : ℝ
⊢ cluster_point u a → ∀ ε > 0, ∀ (N : ℕ), ∃ n ≥ N, |u n - a| ≤ ε
Tactic:
sorry
Proof state after:
no goals
Theorem: subseq_tendsto_of_tendsto'
Proof state before:
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
⊢ seq_limit (u ∘ φ) l
Tactic:
sorry
Proof state after:
no goals
Theorem: cluster_limit
Proof state before:
u : ℕ → ℝ
l a : ℝ
hl : seq_limit u l
ha : cluster_point u a
⊢ a = l
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.isInf.lowerBound
Proof state before:
X : Type u_1
inst✝ : PartialOrder X
s : Set X
x₀ : X
h : isInf s x₀
⊢ x₀ ∈ lowerBounds s
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.isSup_of_isInf
Proof state before:
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
⊢ isSupFun fun s => I (upperBounds s)
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Inf_subset
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
s t : Set X
h : s ⊆ t
⊢ Inf t ≤ Inf s
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Inf_pair
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x x' : X
⊢ x ≤ x' ↔ Inf {x, x'} = x
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Inf_self_le
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
x : X
⊢ Inf {x' | x ≤ x'} = x
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.isInfInter
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
⊢ isInf S (⋂₀ S)
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.isSupUnion
Proof state before:
X : Type
inst✝¹ : PartialOrder X
inst✝ : CompleteLattice X
Y : Type
S : Set (Set Y)
⊢ isSup S (⋃₀ S)
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.adjunction.dual
Proof state before:
X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
l : X → Y
r : Y → X
h : adjunction l r
⊢ adjunction r l
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.adjunction_of_Sup
Proof state before:
X Y : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
h : ∀ (s : Set X), l (Sup s) = Sup (l '' s)
⊢ adjunction l (mk_right l)
Tactic:
sorry
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:
sorry
Proof state after:
no goals
Theorem: Tutorial.ContinuousProductTopIff
Proof state before:
ι : Type
X : ι → Type
T : Π (i : ι), Topology (X i)
Z : Type
TZ : Topology Z
f : Z → Π (i : ι), X i
⊢ Continuous TZ (ProductTopology T) f ↔ ∀ (i : ι), Continuous TZ (T i) fun z => f z i
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Subgroups.SubgroupInf_is_Inf
Proof state before:
G : Type
inst✝ : Group G
⊢ isInfFun SubgroupInf
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Subgroups.generate_forget_adjunction
Proof state before:
G : Type
inst✝ : Group G
⊢ adjunction generate forget
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Subgroups.push_pull_adjunction
Proof state before:
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) (pull f)
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.unique_left
Proof state before:
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l l' : X → Y
r : Y → X
h : adjunction l r
h' : adjunction l' r
⊢ l = l'
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.unique_right
Proof state before:
X : Type
inst✝³ : PartialOrder X
inst✝² : CompleteLattice X
Y : Type
inst✝¹ : PartialOrder Y
inst✝ : CompleteLattice Y
l : X → Y
r r' : Y → X
h : adjunction l r
h' : adjunction l r'
⊢ r = r'
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.adjunction.compose
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
l : X → Y
r : Y → X
h : adjunction l r
l' : Y → Z
r' : Z → Y
h' : adjunction l' r'
⊢ adjunction (l' ∘ l) (r ∘ r')
Tactic:
sorry
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: ClassicalPropositionalLogic.isTrue_neg
Proof state before:
v : Variable → Prop
A B : Formula
⊢ IsTrue v ~A ↔ ¬IsTrue v A
Tactic:
simp
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.isTrue_top
Proof state before:
v : Variable → Prop
A B : Formula
⊢ IsTrue v ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.isTrue_equiv
Proof state before:
v : Variable → Prop
A B : Formula
⊢ IsTrue v (A ⇔ B) ↔ (IsTrue v A ↔ IsTrue v B)
Tactic:
simp
Proof state after:
v : Variable → Prop
A B : Formula
⊢ (IsTrue v A → IsTrue v B) ∧ (IsTrue v B → IsTrue v A) ↔ (IsTrue v A ↔ IsTrue v B)
Theorem: ClassicalPropositionalLogic.isTrue_equiv
Proof state before:
v : Variable → Prop
A B : Formula
⊢ (IsTrue v A → IsTrue v B) ∧ (IsTrue v B → IsTrue v A) ↔ (IsTrue v A ↔ IsTrue v B)
Tactic:
tauto
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.satisfies_insert_iff
Proof state before:
v : Variable → Prop
A B : Formula
Γ : Set Formula
⊢ Satisfies v (insert A Γ) ↔ IsTrue v A ∧ Satisfies v Γ
Tactic:
simp [Satisfies]
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
h2 : Γ ⊆ Δ
⊢ Δ ⊢ A
Tactic:
induction h generalizing Δ
Proof state after:
case ax
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

case impI
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ ⇒ B✝

case impE
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ ⇒ B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝

case andI
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ && B✝

case andE1
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

case andE2
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝

case orI1
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝

case orI2
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝

case orE
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
a_ih✝² : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ || B✝
a_ih✝¹ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
a_ih✝ : ∀ {Δ : Set Formula}, insert B✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ C✝

case botC
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
a_ih✝ : ∀ {Δ : Set Formula}, insert (~A✝) Γ✝ ⊆ Δ → Δ ⊢ ⊥
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
case ax => apply ax; solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ ⇒ B✝
Tactic:
case impI ih => apply impI; solve_by_elim [insert_subset_insert]
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ ⇒ B✝
ih₂ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
Tactic:
case impE ih₁ ih₂ => apply impE <;> solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
ih₂ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ && B✝
Tactic:
case andI ih₁ ih₂ => apply andI <;> solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
case andE1 ih => apply andE1 <;> solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
Tactic:
case andE2 ih => apply andE2 <;> solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝
Tactic:
case orI1 ih => apply orI1; solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝
Tactic:
case orI2 ih => apply orI2; solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ || B✝
ih₂ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
ih₃ : ∀ {Δ : Set Formula}, insert B✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ C✝
Tactic:
case orE ih₁ ih₂ ih₃ => apply orE <;> solve_by_elim [insert_subset_insert]
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : ∀ {Δ : Set Formula}, insert (~A✝) Γ✝ ⊆ Δ → Δ ⊢ ⊥
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
case botC ih => apply botC; solve_by_elim [insert_subset_insert]
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
apply ax
Proof state after:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ A✝ ∈ Δ
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ A✝ ∈ Δ
Tactic:
solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ ⇒ B✝
Tactic:
apply impI
Proof state after:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ insert A✝ Δ ⊢ B✝
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ insert A✝ Δ ⊢ B✝
Tactic:
solve_by_elim [insert_subset_insert]
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ ⇒ B✝
ih₂ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
Tactic:
apply impE <;> solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
ih₂ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ && B✝
Tactic:
apply andI <;> solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
apply andE1 <;> solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
Tactic:
apply andE2 <;> solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝
Tactic:
apply orI1
Proof state after:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
solve_by_elim
Proof state after:
no goals
Theorem: ClassicalPropositionalLogic.weakening
Proof state before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝
Tactic:
apply orI2
Proof state after:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝