internlm/Lean-Github huggingface dataset:
Theorem: algebra.grble_eq_true_of_grlex
Proof state before:
case inr.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
split at h
Proof state after:
case inr.inl.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : Order.lex v₁ v₂
h : True
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : ¬Order.lex v₁ v₂
h : False
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Theorem: algebra.grble_eq_true_of_grlex
Proof state before:
case inr.inl.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : Order.lex v₁ v₂
h : True
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : ¬Order.lex v₁ v₂
h : False
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
intros _ hh
Proof state after:
case inr.inl.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : Order.lex v₁ v₂
h : True
a✝ : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁
hh : ¬Order.lex v₁ v₂
⊢ False

case inr.inl.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : ¬Order.lex v₁ v₂
h : False
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Theorem: algebra.grble_eq_true_of_grlex
Proof state before:
case inr.inl.inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : Order.lex v₁ v₂
h : True
a✝ : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁
hh : ¬Order.lex v₁ v₂
⊢ False

case inr.inl.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝³ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝² : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h✝¹ : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h✝ : ¬Order.lex v₁ v₂
h : False
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inr.inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝² : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝¹ : Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : if Order.lex v₁ v₂ then True else False
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
repeat contradiction
Proof state after:
no goals
Theorem: algebra.grble_eq_true_of_grlex
Proof state before:
case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: toChar_aux
Proof state before:
n : Nat
h : n < UInt8.size
⊢ Nat.isValidChar (UInt32.ofNat n).val.val
Tactic:
rw [UInt32.val_eq_of_lt]
Proof state after:
n : Nat
h : n < UInt8.size
⊢ Nat.isValidChar n

n : Nat
h : n < UInt8.size
⊢ n < UInt32.size
Theorem: toChar_aux
Proof state before:
n : Nat
h : n < UInt8.size
⊢ Nat.isValidChar n

n : Nat
h : n < UInt8.size
⊢ n < UInt32.size
Tactic:
exact Or.inl (Nat.lt_trans h (by decide))
Proof state after:
n : Nat
h : n < UInt8.size
⊢ n < UInt32.size
Theorem: toChar_aux
Proof state before:
n : Nat
h : n < UInt8.size
⊢ n < UInt32.size
Tactic:
exact Nat.lt_trans h (by decide)
Proof state after:
no goals
Theorem: toChar_aux
Proof state before:
n : Nat
h : n < UInt8.size
⊢ UInt8.size < 55296
Tactic:
decide
Proof state after:
no goals
Theorem: toChar_aux
Proof state before:
n : Nat
h : n < UInt8.size
⊢ UInt8.size < UInt32.size
Tactic:
decide
Proof state after:
no goals
Theorem: Char.utf8Size_pos
Proof state before:
c : Char
foo : ∀ {c : Prop} {t e : UInt32} [inst : Decidable c], 0 < t → 0 < e → 0 < if c then t else e :=
  fun {c} {t e} x x_1 x_2 =>
    match x, x_1, x_2 with
    | isTrue h, h_1, x => h_1
    | isFalse h, x, h_1 => h_1
⊢ 0 < UInt32.ofNatCore 1 utf8Size.proof_2
Tactic:
decide
Proof state after:
no goals
Theorem: Char.utf8Size_pos
Proof state before:
c : Char
foo : ∀ {c : Prop} {t e : UInt32} [inst : Decidable c], 0 < t → 0 < e → 0 < if c then t else e :=
  fun {c} {t e} x x_1 x_2 =>
    match x, x_1, x_2 with
    | isTrue h, h_1, x => h_1
    | isFalse h, x, h_1 => h_1
⊢ 0 < UInt32.ofNatCore 2 utf8Size.proof_4
Tactic:
decide
Proof state after:
no goals
Theorem: Char.utf8Size_pos
Proof state before:
c : Char
foo : ∀ {c : Prop} {t e : UInt32} [inst : Decidable c], 0 < t → 0 < e → 0 < if c then t else e :=
  fun {c} {t e} x x_1 x_2 =>
    match x, x_1, x_2 with
    | isTrue h, h_1, x => h_1
    | isFalse h, x, h_1 => h_1
⊢ 0 < UInt32.ofNatCore 3 utf8Size.proof_6
Tactic:
decide
Proof state after:
no goals
Theorem: Char.utf8Size_pos
Proof state before:
c : Char
foo : ∀ {c : Prop} {t e : UInt32} [inst : Decidable c], 0 < t → 0 < e → 0 < if c then t else e :=
  fun {c} {t e} x x_1 x_2 =>
    match x, x_1, x_2 with
    | isTrue h, h_1, x => h_1
    | isFalse h, x, h_1 => h_1
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
Tactic:
decide
Proof state after:
no goals
Theorem: Metamath.Expr.subst_append
Proof state before:
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ subst σ (const c :: e₁ ++ e₂) = subst σ (const c :: e₁) ++ subst σ e₂
Tactic:
simp only [subst, List.append_eq]
Proof state after:
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ const c :: subst σ (e₁ ++ e₂) = const c :: subst σ e₁ ++ subst σ e₂
Theorem: Metamath.Expr.subst_append
Proof state before:
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ const c :: subst σ (e₁ ++ e₂) = const c :: subst σ e₁ ++ subst σ e₂
Tactic:
rw [subst_append ..]
Proof state after:
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ const c :: (subst σ e₁ ++ subst σ e₂) = const c :: subst σ e₁ ++ subst σ e₂
Theorem: Metamath.Expr.subst_append
Proof state before:
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ const c :: (subst σ e₁ ++ subst σ e₂) = const c :: subst σ e₁ ++ subst σ e₂
Tactic:
rfl
Proof state after:
no goals
Theorem: Metamath.Expr.subst_append
Proof state before:
σ : VR → Expr
v : VR
e : List Sym
e₂ : Expr
⊢ subst σ (var v :: e ++ e₂) = subst σ (var v :: e) ++ subst σ e₂
Tactic:
rw [List.cons_append]
Proof state after:
σ : VR → Expr
v : VR
e : List Sym
e₂ : Expr
⊢ subst σ (var v :: (e ++ e₂)) = subst σ (var v :: e) ++ subst σ e₂
Theorem: Metamath.Expr.subst_append
Proof state before:
σ : VR → Expr
v : VR
e : List Sym
e₂ : Expr
⊢ subst σ (var v :: (e ++ e₂)) = subst σ (var v :: e) ++ subst σ e₂
Tactic:
simp only [Expr.subst]
Proof state after:
σ : VR → Expr
v : VR
e : List Sym
e₂ : Expr
⊢ σ v ++ subst σ (e ++ e₂) = σ v ++ subst σ e ++ subst σ e₂
Theorem: Metamath.Expr.subst_append
Proof state before:
σ : VR → Expr
v : VR
e : List Sym
e₂ : Expr
⊢ σ v ++ subst σ (e ++ e₂) = σ v ++ subst σ e ++ subst σ e₂
Tactic:
rw [List.append_assoc, subst_append ..]
Proof state after:
no goals
Theorem: Metamath.Expr.subst_tr
Proof state before:
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst (subst.trans σ σ') (var v :: e) = subst σ' (subst σ (var v :: e))
Tactic:
simp only [subst]
Proof state after:
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst.trans σ σ' v ++ subst (subst.trans σ σ') e = subst σ' (σ v ++ subst σ e)
Theorem: Metamath.Expr.subst_tr
Proof state before:
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst.trans σ σ' v ++ subst (subst.trans σ σ') e = subst σ' (σ v ++ subst σ e)
Tactic:
rw [subst_append, subst_tr _ _ e]
Proof state after:
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst.trans σ σ' v ++ subst σ' (subst σ e) = subst σ' (σ v) ++ subst σ' (subst σ e)
Theorem: Metamath.Expr.subst_tr
Proof state before:
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst.trans σ σ' v ++ subst σ' (subst σ e) = subst σ' (σ v) ++ subst σ' (subst σ e)
Tactic:
rfl
Proof state after:
no goals
Theorem: Metamath.DJ.ne
Proof state before:
dj : DJ
a b : VR
h : disj dj a b
e : a = b
⊢ False
Tactic:
cases e
Proof state after:
case refl
dj : DJ
a : VR
h : disj dj a a
⊢ False
Theorem: Metamath.DJ.ne
Proof state before:
case refl
dj : DJ
a : VR
h : disj dj a a
⊢ False
Tactic:
exact dj.irr h
Proof state after:
no goals
Theorem: Metamath.DJ.ext
Proof state before:
dj₁ : VR → VR → Prop
irr✝¹ : ∀ {x : VR}, ¬dj₁ x x
symm✝¹ : ∀ {x y : VR}, dj₁ x y → dj₁ y x
dj₂ : VR → VR → Prop
irr✝ : ∀ {x : VR}, ¬dj₂ x x
symm✝ : ∀ {x y : VR}, dj₂ x y → dj₂ y x
h :
  ∀ (a b : VR),
    disj { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } a b ↔ disj { disj := dj₂, irr := irr✝, symm := symm✝ } a b
this : dj₁ = dj₂
⊢ { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } = { disj := dj₂, irr := irr✝, symm := symm✝ }
Tactic:
cases this
Proof state after:
case refl
dj₁ : VR → VR → Prop
irr✝¹ : ∀ {x : VR}, ¬dj₁ x x
symm✝¹ : ∀ {x y : VR}, dj₁ x y → dj₁ y x
irr✝ : ∀ {x : VR}, ¬dj₁ x x
symm✝ : ∀ {x y : VR}, dj₁ x y → dj₁ y x
h :
  ∀ (a b : VR),
    disj { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } a b ↔ disj { disj := dj₁, irr := irr✝, symm := symm✝ } a b
⊢ { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } = { disj := dj₁, irr := irr✝, symm := symm✝ }
Theorem: Metamath.DJ.ext
Proof state before:
case refl
dj₁ : VR → VR → Prop
irr✝¹ : ∀ {x : VR}, ¬dj₁ x x
symm✝¹ : ∀ {x y : VR}, dj₁ x y → dj₁ y x
irr✝ : ∀ {x : VR}, ¬dj₁ x x
symm✝ : ∀ {x y : VR}, dj₁ x y → dj₁ y x
h :
  ∀ (a b : VR),
    disj { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } a b ↔ disj { disj := dj₁, irr := irr✝, symm := symm✝ } a b
⊢ { disj := dj₁, irr := irr✝¹, symm := symm✝¹ } = { disj := dj₁, irr := irr✝, symm := symm✝ }
Tactic:
rfl
Proof state after:
no goals
Theorem: Metamath.Statement.vars.mono'
Proof state before:
s₁ s₂ : Statement
H : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ s₂.ctx.hyps
H₂ : s₁.fmla = s₂.fmla
v : VR
⊢ v ∈ vars s₁ → v ∈ vars s₂
Tactic:
simp only [vars, List.mem_bind, List.mem_cons, H₂]
Proof state after:
s₁ s₂ : Statement
H : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ s₂.ctx.hyps
H₂ : s₁.fmla = s₂.fmla
v : VR
⊢ (∃ a, (a = s₂.fmla ∨ a ∈ s₁.ctx.hyps) ∧ v ∈ Expr.vars a.snd) →
    ∃ a, (a = s₂.fmla ∨ a ∈ s₂.ctx.hyps) ∧ v ∈ Expr.vars a.snd
Theorem: Metamath.Statement.vars.mono'
Proof state before:
s₁ s₂ : Statement
H : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ s₂.ctx.hyps
H₂ : s₁.fmla = s₂.fmla
v : VR
⊢ (∃ a, (a = s₂.fmla ∨ a ∈ s₁.ctx.hyps) ∧ v ∈ Expr.vars a.snd) →
    ∃ a, (a = s₂.fmla ∨ a ∈ s₂.ctx.hyps) ∧ v ∈ Expr.vars a.snd
Tactic:
exact fun ⟨a, b, c⟩ => ⟨a, b.imp_right (H _), c⟩
Proof state after:
no goals
Theorem: Metamath.Statement.untrim.mono
Proof state before:
s₁ s₂ : Statement
H : s₁.ctx.hyps = s₂.ctx.hyps
h : s₁ ≤ s₂
⊢ ∀ (a : Formula), a ∈ s₂.ctx.hyps → a ∈ s₁.ctx.hyps
Tactic:
rw [H]
Proof state after:
s₁ s₂ : Statement
H : s₁.ctx.hyps = s₂.ctx.hyps
h : s₁ ≤ s₂
⊢ ∀ (a : Formula), a ∈ s₂.ctx.hyps → a ∈ s₂.ctx.hyps
Theorem: Metamath.Statement.untrim.mono
Proof state before:
s₁ s₂ : Statement
H : s₁.ctx.hyps = s₂.ctx.hyps
h : s₁ ≤ s₂
⊢ ∀ (a : Formula), a ∈ s₂.ctx.hyps → a ∈ s₂.ctx.hyps
Tactic:
exact fun _ => id
Proof state after:
no goals
Theorem: Metamath.Statement.trim_untrim
Proof state before:
s : Statement
⊢ trim (untrim s) = trim s
Tactic:
simp only [trim, untrim_vars]
Proof state after:
s : Statement
⊢ { ctx := { hyps := (untrim s).ctx.hyps, dj := DJ.trim (untrim s).ctx.dj fun v => v ∈ vars s },
      fmla := (untrim s).fmla } =
    { ctx := { hyps := s.ctx.hyps, dj := DJ.trim s.ctx.dj fun v => v ∈ vars s }, fmla := s.fmla }
Theorem: Metamath.Statement.trim_untrim
Proof state before:
s : Statement
⊢ { ctx := { hyps := (untrim s).ctx.hyps, dj := DJ.trim (untrim s).ctx.dj fun v => v ∈ vars s },
      fmla := (untrim s).fmla } =
    { ctx := { hyps := s.ctx.hyps, dj := DJ.trim s.ctx.dj fun v => v ∈ vars s }, fmla := s.fmla }
Tactic:
simp only [untrim, untrim', DJ.trim_untrim]
Proof state after:
no goals
Theorem: Metamath.Statement.untrim_trim
Proof state before:
s : Statement
⊢ untrim (trim s) = untrim s
Tactic:
simp only [untrim, untrim', trim_vars]
Proof state after:
s : Statement
⊢ { ctx := { hyps := (trim s).ctx.hyps, dj := DJ.untrim (trim s).ctx.dj fun v => v ∈ vars s }, fmla := (trim s).fmla } =
    { ctx := { hyps := s.ctx.hyps, dj := DJ.untrim s.ctx.dj fun v => v ∈ vars s }, fmla := s.fmla }
Theorem: Metamath.Statement.untrim_trim
Proof state before:
s : Statement
⊢ { ctx := { hyps := (trim s).ctx.hyps, dj := DJ.untrim (trim s).ctx.dj fun v => v ∈ vars s }, fmla := (trim s).fmla } =
    { ctx := { hyps := s.ctx.hyps, dj := DJ.untrim s.ctx.dj fun v => v ∈ vars s }, fmla := s.fmla }
Tactic:
simp only [trim, DJ.untrim_trim]
Proof state after:
no goals
Theorem: Metamath.Statement.trim_le
Proof state before:
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : (trim s₁).ctx ≤ s₂.ctx
h₁ : ∀ (a : Formula), a ∈ (trim s₁).ctx.hyps → a ∈ s₂.ctx.hyps
h₂ : (trim s₁).ctx.dj ≤ s₂.ctx.dj
⊢ (DJ.trim s₁.ctx.dj fun x => (fun v => v ∈ vars s₂) x) ≤ s₂.ctx.dj
Tactic:
rw [← e]
Proof state after:
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : (trim s₁).ctx ≤ s₂.ctx
h₁ : ∀ (a : Formula), a ∈ (trim s₁).ctx.hyps → a ∈ s₂.ctx.hyps
h₂ : (trim s₁).ctx.dj ≤ s₂.ctx.dj
⊢ (DJ.trim s₁.ctx.dj fun x => (fun v => v ∈ vars s₁) x) ≤ s₂.ctx.dj
Theorem: Metamath.Statement.trim_le
Proof state before:
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : (trim s₁).ctx ≤ s₂.ctx
h₁ : ∀ (a : Formula), a ∈ (trim s₁).ctx.hyps → a ∈ s₂.ctx.hyps
h₂ : (trim s₁).ctx.dj ≤ s₂.ctx.dj
⊢ (DJ.trim s₁.ctx.dj fun x => (fun v => v ∈ vars s₁) x) ≤ s₂.ctx.dj
Tactic:
exact h₂
Proof state after:
no goals
Theorem: Metamath.Statement.trim_le
Proof state before:
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : s₁.ctx ≤ (untrim s₂).ctx
h₁ : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ (untrim s₂).ctx.hyps
h₂ : s₁.ctx.dj ≤ (untrim s₂).ctx.dj
⊢ s₁.ctx.dj ≤ DJ.untrim s₂.ctx.dj fun x => (fun v => v ∈ vars s₁) x
Tactic:
rw [e]
Proof state after:
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : s₁.ctx ≤ (untrim s₂).ctx
h₁ : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ (untrim s₂).ctx.hyps
h₂ : s₁.ctx.dj ≤ (untrim s₂).ctx.dj
⊢ s₁.ctx.dj ≤ DJ.untrim s₂.ctx.dj fun x => (fun v => v ∈ vars s₂) x
Theorem: Metamath.Statement.trim_le
Proof state before:
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : s₁.ctx ≤ (untrim s₂).ctx
h₁ : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ (untrim s₂).ctx.hyps
h₂ : s₁.ctx.dj ≤ (untrim s₂).ctx.dj
⊢ s₁.ctx.dj ≤ DJ.untrim s₂.ctx.dj fun x => (fun v => v ∈ vars s₂) x
Tactic:
exact h₂
Proof state after:
no goals
Theorem: Metamath.Statement.trimmed.trim_eq
Proof state before:
a : List Formula
b : DJ
c : Formula
h : trimmed { ctx := { hyps := a, dj := b }, fmla := c }
⊢ trim { ctx := { hyps := a, dj := b }, fmla := c } = { ctx := { hyps := a, dj := b }, fmla := c }
Tactic:
simp only [trim]
Proof state after:
a : List Formula
b : DJ
c : Formula
h : trimmed { ctx := { hyps := a, dj := b }, fmla := c }
⊢ { ctx := { hyps := a, dj := DJ.trim b fun v => v ∈ vars { ctx := { hyps := a, dj := b }, fmla := c } }, fmla := c } =
    { ctx := { hyps := a, dj := b }, fmla := c }
Theorem: Metamath.Statement.trimmed.trim_eq
Proof state before:
a : List Formula
b : DJ
c : Formula
h : trimmed { ctx := { hyps := a, dj := b }, fmla := c }
⊢ { ctx := { hyps := a, dj := DJ.trim b fun v => v ∈ vars { ctx := { hyps := a, dj := b }, fmla := c } }, fmla := c } =
    { ctx := { hyps := a, dj := b }, fmla := c }
Tactic:
rw [DJ.trimmed.trim_eq h]
Proof state after:
no goals
Theorem: Metamath.Provable.mono
Proof state before:
axs₁ axs₂ : Statement → Prop
haxs : ∀ (a : Statement), axs₁ a → axs₂ a
Γ₁ Γ₂ : Context
hΓ : Γ₁ ≤ Γ₂
e : Formula
pr : Provable axs₁ Γ₁ e
⊢ Provable axs₂ Γ₂ e
Tactic:
induction pr with
| hyp e h => exact hyp e (hΓ.1 _ h)
| var v => exact var v
| ax σ ha h₁ _ IH =>
  exact ax σ (haxs _ ha) (h₁.mono (DJ.refl _) hΓ.2) fun e h => IH _ h
Proof state after:
no goals
Theorem: Metamath.Provable.mono
Proof state before:
case hyp
axs₁ axs₂ : Statement → Prop
haxs : ∀ (a : Statement), axs₁ a → axs₂ a
Γ₁ Γ₂ : Context
hΓ : Γ₁ ≤ Γ₂
e✝ e : Formula
h : e ∈ Γ₁.hyps
⊢ Provable axs₂ Γ₂ e
Tactic:
exact hyp e (hΓ.1 _ h)
Proof state after:
no goals
Theorem: Metamath.Provable.mono
Proof state before:
case var
axs₁ axs₂ : Statement → Prop
haxs : ∀ (a : Statement), axs₁ a → axs₂ a
Γ₁ Γ₂ : Context
hΓ : Γ₁ ≤ Γ₂
e : Formula
v : VR
⊢ Provable axs₂ Γ₂ (VR.vhyp v)
Tactic:
exact var v
Proof state after:
no goals
Theorem: Metamath.Provable.mono
Proof state before:
case ax
axs₁ axs₂ : Statement → Prop
haxs : ∀ (a : Statement), axs₁ a → axs₂ a
Γ₁ Γ₂ : Context
hΓ : Γ₁ ≤ Γ₂
e : Formula
σ : VR → Expr
ax✝ : Statement
ha : axs₁ ax✝
h₁ : DJ.subst σ ax✝.ctx.dj Γ₁.dj
a✝ : ∀ (h : Formula), (h ∈ ax✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs₁ Γ₁ (Formula.subst σ h)
IH : ∀ (h : Formula), (h ∈ ax✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs₂ Γ₂ (Formula.subst σ h)
⊢ Provable axs₂ Γ₂ (Formula.subst σ ax✝.fmla)
Tactic:
exact ax σ (haxs _ ha) (h₁.mono (DJ.refl _) hΓ.2) fun e h => IH _ h
Proof state after:
no goals
Theorem: Metamath.Statement.provable.trim
Proof state before:
axs : Statement → Prop
s : Statement
⊢ provable axs (Statement.trim s) ↔ provable axs s
Tactic:
simp only [provable, untrim_trim]
Proof state after:
no goals
Theorem: Metamath.Provable.ax_self
Proof state before:
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ Statement.provable' axs ax
Tactic:
have := Provable.ax (Γ := ax.ctx) VR.expr H ?disj ?hyp
Proof state after:
axs : Statement → Prop
ax : Statement
H : axs ax
this : Provable axs ax.ctx (Formula.subst VR.expr ax.fmla)
⊢ Statement.provable' axs ax

case disj
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj

case hyp
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)
Theorem: Metamath.Provable.ax_self
Proof state before:
axs : Statement → Prop
ax : Statement
H : axs ax
this : Provable axs ax.ctx (Formula.subst VR.expr ax.fmla)
⊢ Statement.provable' axs ax

case disj
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj

case hyp
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)
Tactic:
rw [Formula.subst_id] at this
Proof state after:
axs : Statement → Prop
ax : Statement
H : axs ax
this : Provable axs ax.ctx ax.fmla
⊢ Statement.provable' axs ax

case disj
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj

case hyp
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)
Theorem: Metamath.Provable.ax_self
Proof state before:
axs : Statement → Prop
ax : Statement
H : axs ax
this : Provable axs ax.ctx ax.fmla
⊢ Statement.provable' axs ax

case disj
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj

case hyp
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)
Tactic:
exact this
Proof state after:
case disj
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj

case hyp
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)
Theorem: Metamath.Provable.ax_self
Proof state before:
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj
Tactic:
case disj =>
  intro a b h a' b' h₁ h₂
  match a', b', h₁, h₂ with | _, _, .head _, .head _ => ?_
  exact h
Proof state after:
no goals
Theorem: Metamath.Provable.ax_self
Proof state before:
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)
Tactic:
case hyp =>
  intro fmla h
  match fmla, h with
  | fmla, Or.inl h => rw [Formula.subst_id]; exact Provable.hyp _ h
  | _, Or.inr ⟨v, rfl⟩ => exact Provable.var v
Proof state after:
no goals
Theorem: Metamath.Provable.ax_self
Proof state before:
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj
Tactic:
intro a b h a' b' h₁ h₂
Proof state after:
axs : Statement → Prop
ax : Statement
H : axs ax
a b : VR
h : DJ.disj ax.ctx.dj a b
a' b' : VR
h₁ : a' ∈' VR.expr a
h₂ : b' ∈' VR.expr b
⊢ DJ.disj ax.ctx.dj a' b'