internlm/Lean-Github huggingface dataset:
Theorem: Smt.Reconstruct.Arith.arithTransSineBounds
Proof state before:
case right
t : ℝ
⊢ t < 0 → t.sin > t
Tactic:
intro ht
Proof state after:
case right
t : ℝ
ht : t < 0
⊢ t.sin > t
Theorem: Smt.Reconstruct.Arith.arithTransSineBounds
Proof state before:
case right
t : ℝ
ht : t < 0
⊢ t.sin > t
Tactic:
rw [sin_neg']
Proof state after:
case right
t : ℝ
ht : t < 0
⊢ -(-t).sin > t
Theorem: Smt.Reconstruct.Arith.arithTransSineBounds
Proof state before:
case right
t : ℝ
ht : t < 0
⊢ -(-t).sin > t
Tactic:
apply lt_neg.mpr
Proof state after:
case right
t : ℝ
ht : t < 0
⊢ (-t).sin < -t
Theorem: Smt.Reconstruct.Arith.arithTransSineBounds
Proof state before:
case right
t : ℝ
ht : t < 0
⊢ (-t).sin < -t
Tactic:
apply sin_lt
Proof state after:
case right.h
t : ℝ
ht : t < 0
⊢ 0 < -t
Theorem: Smt.Reconstruct.Arith.arithTransSineBounds
Proof state before:
case right.h
t : ℝ
ht : t < 0
⊢ 0 < -t
Tactic:
linarith
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.Real.neg_lt_neg
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : a < b
⊢ -a > -b
Tactic:
simp
Proof state after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : a < b
⊢ a < b
Theorem: Smt.Reconstruct.Arith.Real.neg_lt_neg
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : a < b
⊢ a < b
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.Real.neg_le_neg
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : a ≤ b
⊢ -a ≥ -b
Tactic:
simp
Proof state after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : a ≤ b
⊢ a ≤ b
Theorem: Smt.Reconstruct.Arith.Real.neg_le_neg
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : a ≤ b
⊢ a ≤ b
Tactic:
exact h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.castLE'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ ∀ {a b : ℤ}, a ≤ b → ↑a ≤ ↑b
Tactic:
simp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.intTightLb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ ∀ {i : ℤ} {c : α}, ↑i > c → i ≥ ⌊c⌋ + 1
Tactic:
intros i c h
Proof state after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
⊢ i ≥ ⌊c⌋ + 1
Theorem: Smt.Reconstruct.Arith.intTightLb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
⊢ i ≥ ⌊c⌋ + 1
Tactic:
cases lt_trichotomy i (⌊c⌋ + 1) with
| inl iltc =>
  have ilec := (Int.lt_iff_add_one_le i (⌊c⌋ + 1)).mp iltc
  simp at ilec
  have c_le_floor := Int.floor_le c
  have cast_ilec := le_trans (castLE' ilec) c_le_floor
  have abs := lt_of_le_of_lt cast_ilec h
  simp at abs
| inr h' => cases h' with
            | inl ieqc => exact le_of_eq (Eq.symm ieqc)
            | inr igtc => exact le_of_lt igtc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.intTightLb'
Proof state before:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
⊢ i ≥ ⌊c⌋ + 1
Tactic:
have ilec := (Int.lt_iff_add_one_le i (⌊c⌋ + 1)).mp iltc
Proof state after:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i + 1 ≤ ⌊c⌋ + 1
⊢ i ≥ ⌊c⌋ + 1
Theorem: Smt.Reconstruct.Arith.intTightLb'
Proof state before:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i + 1 ≤ ⌊c⌋ + 1
⊢ i ≥ ⌊c⌋ + 1
Tactic:
simp at ilec
Proof state after:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
⊢ i ≥ ⌊c⌋ + 1
Theorem: Smt.Reconstruct.Arith.intTightLb'
Proof state before:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
⊢ i ≥ ⌊c⌋ + 1
Tactic:
have c_le_floor := Int.floor_le c
Proof state after:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
c_le_floor : ↑⌊c⌋ ≤ c
⊢ i ≥ ⌊c⌋ + 1
Theorem: Smt.Reconstruct.Arith.intTightLb'
Proof state before:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
c_le_floor : ↑⌊c⌋ ≤ c
⊢ i ≥ ⌊c⌋ + 1
Tactic:
have cast_ilec := le_trans (castLE' ilec) c_le_floor
Proof state after:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
c_le_floor : ↑⌊c⌋ ≤ c
cast_ilec : ↑i ≤ c
⊢ i ≥ ⌊c⌋ + 1
Theorem: Smt.Reconstruct.Arith.intTightLb'
Proof state before:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
c_le_floor : ↑⌊c⌋ ≤ c
cast_ilec : ↑i ≤ c
⊢ i ≥ ⌊c⌋ + 1
Tactic:
have abs := lt_of_le_of_lt cast_ilec h
Proof state after:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
c_le_floor : ↑⌊c⌋ ≤ c
cast_ilec : ↑i ≤ c
abs : ↑i < ↑i
⊢ i ≥ ⌊c⌋ + 1
Theorem: Smt.Reconstruct.Arith.intTightLb'
Proof state before:
case inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
iltc : i < ⌊c⌋ + 1
ilec : i ≤ ⌊c⌋
c_le_floor : ↑⌊c⌋ ≤ c
cast_ilec : ↑i ≤ c
abs : ↑i < ↑i
⊢ i ≥ ⌊c⌋ + 1
Tactic:
simp at abs
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.intTightLb'
Proof state before:
case inr
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
h' : i = ⌊c⌋ + 1 ∨ ⌊c⌋ + 1 < i
⊢ i ≥ ⌊c⌋ + 1
Tactic:
cases h' with
| inl ieqc => exact le_of_eq (Eq.symm ieqc)
| inr igtc => exact le_of_lt igtc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.intTightLb'
Proof state before:
case inr.inl
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
ieqc : i = ⌊c⌋ + 1
⊢ i ≥ ⌊c⌋ + 1
Tactic:
exact le_of_eq (Eq.symm ieqc)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.intTightLb'
Proof state before:
case inr.inr
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i > c
igtc : ⌊c⌋ + 1 < i
⊢ i ≥ ⌊c⌋ + 1
Tactic:
exact le_of_lt igtc
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.intTightUb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ ∀ {i : ℤ} {c : α}, ↑i < c → i ≤ ⌈c⌉ - 1
Tactic:
intros i c h
Proof state after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
⊢ i ≤ ⌈c⌉ - 1
Theorem: Smt.Reconstruct.Arith.intTightUb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
⊢ i ≤ ⌈c⌉ - 1
Tactic:
have neg_c_lt_neg_i := Real.neg_lt_neg h
Proof state after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
⊢ i ≤ ⌈c⌉ - 1
Theorem: Smt.Reconstruct.Arith.intTightUb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
⊢ i ≤ ⌈c⌉ - 1
Tactic:
have i_le_floor_neg_c: -i ≥ ⌊-c⌋ + 1 :=  by
  apply intTightLb'
  norm_cast at neg_c_lt_neg_i
Proof state after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ ⌊-c⌋ + 1
⊢ i ≤ ⌈c⌉ - 1
Theorem: Smt.Reconstruct.Arith.intTightUb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ ⌊-c⌋ + 1
⊢ i ≤ ⌈c⌉ - 1
Tactic:
rw [Int.floor_neg] at i_le_floor_neg_c
Proof state after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
⊢ i ≤ ⌈c⌉ - 1
Theorem: Smt.Reconstruct.Arith.intTightUb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
⊢ i ≤ ⌈c⌉ - 1
Tactic:
have i_plus_one_le_c := Int.neg_le_neg i_le_floor_neg_c
Proof state after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : - -i ≤ -(-⌈c⌉ + 1)
⊢ i ≤ ⌈c⌉ - 1
Theorem: Smt.Reconstruct.Arith.intTightUb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : - -i ≤ -(-⌈c⌉ + 1)
⊢ i ≤ ⌈c⌉ - 1
Tactic:
simp at i_plus_one_le_c
Proof state after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : 1 + i ≤ ⌈c⌉
⊢ i ≤ ⌈c⌉ - 1
Theorem: Smt.Reconstruct.Arith.intTightUb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : 1 + i ≤ ⌈c⌉
⊢ i ≤ ⌈c⌉ - 1
Tactic:
rw [add_comm] at i_plus_one_le_c
Proof state after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : i + 1 ≤ ⌈c⌉
⊢ i ≤ ⌈c⌉ - 1
Theorem: Smt.Reconstruct.Arith.intTightUb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : i + 1 ≤ ⌈c⌉
⊢ i ≤ ⌈c⌉ - 1
Tactic:
have pf: i + 1 - 1 ≤ ⌈c⌉ - 1 := Int.add_le_add i_plus_one_le_c le_rfl
Proof state after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : i + 1 ≤ ⌈c⌉
pf : i + 1 - 1 ≤ ⌈c⌉ - 1
⊢ i ≤ ⌈c⌉ - 1
Theorem: Smt.Reconstruct.Arith.intTightUb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : i + 1 ≤ ⌈c⌉
pf : i + 1 - 1 ≤ ⌈c⌉ - 1
⊢ i ≤ ⌈c⌉ - 1
Tactic:
simp at pf
Proof state after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : i + 1 ≤ ⌈c⌉
pf : i ≤ ⌈c⌉ - 1
⊢ i ≤ ⌈c⌉ - 1
Theorem: Smt.Reconstruct.Arith.intTightUb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
i_le_floor_neg_c : -i ≥ -⌈c⌉ + 1
i_plus_one_le_c : i + 1 ≤ ⌈c⌉
pf : i ≤ ⌈c⌉ - 1
⊢ i ≤ ⌈c⌉ - 1
Tactic:
exact pf
Proof state after:
no goals
Theorem: Smt.Reconstruct.Arith.intTightUb'
Proof state before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
⊢ -i ≥ ⌊-c⌋ + 1
Tactic:
apply intTightLb'
Proof state after:
case a
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
⊢ ↑(-i) > -c
Theorem: Smt.Reconstruct.Arith.intTightUb'
Proof state before:
case a
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
i : ℤ
c : α
h : ↑i < c
neg_c_lt_neg_i : -↑i > -c
⊢ ↑(-i) > -c
Tactic:
norm_cast at neg_c_lt_neg_i
Proof state after:
no goals
Theorem: modus_ponens
Proof state before:
p q : Bool
⊢ p = true → (p = true → q = true) → q = true
Tactic:
simp_all
Proof state after:
no goals
Theorem: Smt.Reconstruct.Quant.miniscopeN
Proof state before:
α : Type u
ps : List (α → Prop)
⊢ (∀ (x : α), andN (List.map (fun x_1 => x_1 x) [])) = andN (List.map (fun x => ∀ (x_1 : α), x x_1) [])
Tactic:
simp [andN]
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.ite_eq
Proof state before:
α : Sort u_1
c : Prop
h : Decidable c
x y : α
⊢ if c then (if c then x else y) = x else (if c then x else y) = y
Tactic:
cases h
Proof state after:
case isFalse
α : Sort u_1
c : Prop
x y : α
h✝ : ¬c
⊢ if c then (if c then x else y) = x else (if c then x else y) = y

case isTrue
α : Sort u_1
c : Prop
x y : α
h✝ : c
⊢ if c then (if c then x else y) = x else (if c then x else y) = y
Theorem: Smt.Reconstruct.Prop.ite_eq
Proof state before:
case isFalse
α : Sort u_1
c : Prop
x y : α
h✝ : ¬c
⊢ if c then (if c then x else y) = x else (if c then x else y) = y

case isTrue
α : Sort u_1
c : Prop
x y : α
h✝ : c
⊢ if c then (if c then x else y) = x else (if c then x else y) = y
Tactic:
all_goals simp_all
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.ite_eq
Proof state before:
case isTrue
α : Sort u_1
c : Prop
x y : α
h✝ : c
⊢ if c then (if c then x else y) = x else (if c then x else y) = y
Tactic:
simp_all
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notImplies1
Proof state before:
⊢ ∀ {P Q : Prop}, ¬(P → Q) → P
Tactic:
intros P Q h
Proof state after:
P Q : Prop
h : ¬(P → Q)
⊢ P
Theorem: Smt.Reconstruct.Prop.notImplies1
Proof state before:
P Q : Prop
h : ¬(P → Q)
⊢ P
Tactic:
cases Classical.em P with
| inl p  => exact p
| inr np => apply False.elim
            apply h
            intro p
            exact False.elim (np p)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notImplies1
Proof state before:
case inl
P Q : Prop
h : ¬(P → Q)
p : P
⊢ P
Tactic:
exact p
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notImplies1
Proof state before:
case inr
P Q : Prop
h : ¬(P → Q)
np : ¬P
⊢ P
Tactic:
apply False.elim
Proof state after:
case inr.h
P Q : Prop
h : ¬(P → Q)
np : ¬P
⊢ False
Theorem: Smt.Reconstruct.Prop.notImplies1
Proof state before:
case inr.h
P Q : Prop
h : ¬(P → Q)
np : ¬P
⊢ False
Tactic:
apply h
Proof state after:
case inr.h
P Q : Prop
h : ¬(P → Q)
np : ¬P
⊢ P → Q
Theorem: Smt.Reconstruct.Prop.notImplies1
Proof state before:
case inr.h
P Q : Prop
h : ¬(P → Q)
np : ¬P
⊢ P → Q
Tactic:
intro p
Proof state after:
case inr.h
P Q : Prop
h : ¬(P → Q)
np : ¬P
p : P
⊢ Q
Theorem: Smt.Reconstruct.Prop.notImplies1
Proof state before:
case inr.h
P Q : Prop
h : ¬(P → Q)
np : ¬P
p : P
⊢ Q
Tactic:
exact False.elim (np p)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notImplies2
Proof state before:
⊢ ∀ {P Q : Prop}, ¬(P → Q) → ¬Q
Tactic:
intros P Q h
Proof state after:
P Q : Prop
h : ¬(P → Q)
⊢ ¬Q
Theorem: Smt.Reconstruct.Prop.notImplies2
Proof state before:
P Q : Prop
h : ¬(P → Q)
⊢ ¬Q
Tactic:
cases Classical.em Q with
| inl q  => exact False.elim (h (λ _ => q))
| inr nq => exact nq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notImplies2
Proof state before:
case inl
P Q : Prop
h : ¬(P → Q)
q : Q
⊢ ¬Q
Tactic:
exact False.elim (h (λ _ => q))
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notImplies2
Proof state before:
case inr
P Q : Prop
h : ¬(P → Q)
nq : ¬Q
⊢ ¬Q
Tactic:
exact nq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.equivElim1
Proof state before:
⊢ ∀ {P Q : Prop}, P = Q → ¬P ∨ Q
Tactic:
intros P Q h
Proof state after:
P Q : Prop
h : P = Q
⊢ ¬P ∨ Q
Theorem: Smt.Reconstruct.Prop.equivElim1
Proof state before:
P Q : Prop
h : P = Q
⊢ ¬P ∨ Q
Tactic:
rewrite [h]
Proof state after:
P Q : Prop
h : P = Q
⊢ ¬Q ∨ Q
Theorem: Smt.Reconstruct.Prop.equivElim1
Proof state before:
P Q : Prop
h : P = Q
⊢ ¬Q ∨ Q
Tactic:
cases Classical.em Q with
| inl q  => exact Or.inr q
| inr nq => exact Or.inl nq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.equivElim1
Proof state before:
case inl
P Q : Prop
h : P = Q
q : Q
⊢ ¬Q ∨ Q
Tactic:
exact Or.inr q
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.equivElim1
Proof state before:
case inr
P Q : Prop
h : P = Q
nq : ¬Q
⊢ ¬Q ∨ Q
Tactic:
exact Or.inl nq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.equivElim2
Proof state before:
⊢ ∀ {P Q : Prop}, P = Q → P ∨ ¬Q
Tactic:
intros P Q h
Proof state after:
P Q : Prop
h : P = Q
⊢ P ∨ ¬Q
Theorem: Smt.Reconstruct.Prop.equivElim2
Proof state before:
P Q : Prop
h : P = Q
⊢ P ∨ ¬Q
Tactic:
rewrite [h]
Proof state after:
P Q : Prop
h : P = Q
⊢ Q ∨ ¬Q
Theorem: Smt.Reconstruct.Prop.equivElim2
Proof state before:
P Q : Prop
h : P = Q
⊢ Q ∨ ¬Q
Tactic:
cases Classical.em Q with
| inl q  => exact Or.inl q
| inr nq => exact Or.inr nq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.equivElim2
Proof state before:
case inl
P Q : Prop
h : P = Q
q : Q
⊢ Q ∨ ¬Q
Tactic:
exact Or.inl q
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.equivElim2
Proof state before:
case inr
P Q : Prop
h : P = Q
nq : ¬Q
⊢ Q ∨ ¬Q
Tactic:
exact Or.inr nq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notEquivElim1
Proof state before:
⊢ ∀ {P Q : Prop}, ¬P = Q → P ∨ Q
Tactic:
intros P Q h
Proof state after:
P Q : Prop
h : ¬P = Q
⊢ P ∨ Q
Theorem: Smt.Reconstruct.Prop.notEquivElim1
Proof state before:
P Q : Prop
h : ¬P = Q
⊢ P ∨ Q
Tactic:
exact match Classical.em P, Classical.em Q with
| Or.inl p, _ => Or.inl p
| _, Or.inl q => Or.inr q
| Or.inr np, Or.inr nq =>
  absurd (propext (Iff.intro (λ p => absurd p np) (λ q => absurd q nq))) h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.notEquivElim2
Proof state before:
⊢ ∀ {P Q : Prop}, ¬P = Q → ¬P ∨ ¬Q
Tactic:
intros P Q h
Proof state after:
P Q : Prop
h : ¬P = Q
⊢ ¬P ∨ ¬Q
Theorem: Smt.Reconstruct.Prop.notEquivElim2
Proof state before:
P Q : Prop
h : ¬P = Q
⊢ ¬P ∨ ¬Q
Tactic:
exact match Classical.em P, Classical.em Q with
| Or.inr np, _ => Or.inl np
| _, Or.inr nq => Or.inr nq
| Or.inl p, Or.inl q =>
  absurd (propext (Iff.intro (λ _ => q) (λ _ => p))) h
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orComm
Proof state before:
⊢ ∀ {P Q : Prop}, P ∨ Q → Q ∨ P
Tactic:
intros P Q h
Proof state after:
P Q : Prop
h : P ∨ Q
⊢ Q ∨ P
Theorem: Smt.Reconstruct.Prop.orComm
Proof state before:
P Q : Prop
h : P ∨ Q
⊢ Q ∨ P
Tactic:
cases h with
| inl hp => exact Or.inr hp
| inr hq => exact Or.inl hq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orComm
Proof state before:
case inl
P Q : Prop
hp : P
⊢ Q ∨ P
Tactic:
exact Or.inr hp
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orComm
Proof state before:
case inr
P Q : Prop
hq : Q
⊢ Q ∨ P
Tactic:
exact Or.inl hq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orAssocDir
Proof state before:
⊢ ∀ {P Q R : Prop}, P ∨ Q ∨ R → (P ∨ Q) ∨ R
Tactic:
intros P Q R h
Proof state after:
P Q R : Prop
h : P ∨ Q ∨ R
⊢ (P ∨ Q) ∨ R
Theorem: Smt.Reconstruct.Prop.orAssocDir
Proof state before:
P Q R : Prop
h : P ∨ Q ∨ R
⊢ (P ∨ Q) ∨ R
Tactic:
cases h with
| inl h₁ => exact Or.inl (Or.inl h₁)
| inr h₂ => cases h₂ with
            | inl h₃ => exact Or.inl (Or.inr h₃)
            | inr h₄ => exact Or.inr h₄
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orAssocDir
Proof state before:
case inl
P Q R : Prop
h₁ : P
⊢ (P ∨ Q) ∨ R
Tactic:
exact Or.inl (Or.inl h₁)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orAssocDir
Proof state before:
case inr
P Q R : Prop
h₂ : Q ∨ R
⊢ (P ∨ Q) ∨ R
Tactic:
cases h₂ with
| inl h₃ => exact Or.inl (Or.inr h₃)
| inr h₄ => exact Or.inr h₄
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orAssocDir
Proof state before:
case inr.inl
P Q R : Prop
h₃ : Q
⊢ (P ∨ Q) ∨ R
Tactic:
exact Or.inl (Or.inr h₃)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orAssocDir
Proof state before:
case inr.inr
P Q R : Prop
h₄ : R
⊢ (P ∨ Q) ∨ R
Tactic:
exact Or.inr h₄
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orAssocConv
Proof state before:
⊢ ∀ {P Q R : Prop}, (P ∨ Q) ∨ R → P ∨ Q ∨ R
Tactic:
intros P Q R h
Proof state after:
P Q R : Prop
h : (P ∨ Q) ∨ R
⊢ P ∨ Q ∨ R
Theorem: Smt.Reconstruct.Prop.orAssocConv
Proof state before:
P Q R : Prop
h : (P ∨ Q) ∨ R
⊢ P ∨ Q ∨ R
Tactic:
cases h with
| inl h₁ => cases h₁ with
            | inl h₃ => exact Or.inl h₃
            | inr h₄ => exact (Or.inr (Or.inl h₄))
| inr h₂ => exact Or.inr (Or.inr h₂)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orAssocConv
Proof state before:
case inl
P Q R : Prop
h₁ : P ∨ Q
⊢ P ∨ Q ∨ R
Tactic:
cases h₁ with
| inl h₃ => exact Or.inl h₃
| inr h₄ => exact (Or.inr (Or.inl h₄))
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orAssocConv
Proof state before:
case inl.inl
P Q R : Prop
h₃ : P
⊢ P ∨ Q ∨ R
Tactic:
exact Or.inl h₃
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orAssocConv
Proof state before:
case inl.inr
P Q R : Prop
h₄ : Q
⊢ P ∨ Q ∨ R
Tactic:
exact (Or.inr (Or.inl h₄))
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orAssocConv
Proof state before:
case inr
P Q R : Prop
h₂ : R
⊢ P ∨ Q ∨ R
Tactic:
exact Or.inr (Or.inr h₂)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.congOrRight
Proof state before:
⊢ ∀ {P Q R : Prop}, (P → Q) → P ∨ R → Q ∨ R
Tactic:
intros P Q R h₁ h₂
Proof state after:
P Q R : Prop
h₁ : P → Q
h₂ : P ∨ R
⊢ Q ∨ R
Theorem: Smt.Reconstruct.Prop.congOrRight
Proof state before:
P Q R : Prop
h₁ : P → Q
h₂ : P ∨ R
⊢ Q ∨ R
Tactic:
cases h₂ with
| inl h₃ => exact Or.inl (h₁ h₃)
| inr h₄ => exact Or.inr h₄
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.congOrRight
Proof state before:
case inl
P Q R : Prop
h₁ : P → Q
h₃ : P
⊢ Q ∨ R
Tactic:
exact Or.inl (h₁ h₃)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.congOrRight
Proof state before:
case inr
P Q R : Prop
h₁ : P → Q
h₄ : R
⊢ Q ∨ R
Tactic:
exact Or.inr h₄
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.congOrLeft
Proof state before:
⊢ ∀ {P Q R : Prop}, (P → Q) → R ∨ P → R ∨ Q
Tactic:
intros P Q R h₁ h₂
Proof state after:
P Q R : Prop
h₁ : P → Q
h₂ : R ∨ P
⊢ R ∨ Q
Theorem: Smt.Reconstruct.Prop.congOrLeft
Proof state before:
P Q R : Prop
h₁ : P → Q
h₂ : R ∨ P
⊢ R ∨ Q
Tactic:
apply orComm
Proof state after:
case a
P Q R : Prop
h₁ : P → Q
h₂ : R ∨ P
⊢ Q ∨ R
Theorem: Smt.Reconstruct.Prop.congOrLeft
Proof state before:
case a
P Q R : Prop
h₁ : P → Q
h₂ : R ∨ P
⊢ Q ∨ R
Tactic:
exact congOrRight h₁ (orComm h₂)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orImplies
Proof state before:
⊢ ∀ {p q : Prop}, (¬p → q) → p ∨ q
Tactic:
intros p q h
Proof state after:
p q : Prop
h : ¬p → q
⊢ p ∨ q
Theorem: Smt.Reconstruct.Prop.orImplies
Proof state before:
p q : Prop
h : ¬p → q
⊢ p ∨ q
Tactic:
exact match Classical.em p with
| Or.inl pp => Or.inl pp
| Or.inr npp => match Classical.em q with
                | Or.inl pq => Or.inr pq
                | Or.inr npq => False.elim (npq (h npp))
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orImplies₂
Proof state before:
⊢ ∀ {p q : Prop}, ¬p ∨ q → p → q
Tactic:
intros P Q h p
Proof state after:
P Q : Prop
h : ¬P ∨ Q
p : P
⊢ Q
Theorem: Smt.Reconstruct.Prop.orImplies₂
Proof state before:
P Q : Prop
h : ¬P ∨ Q
p : P
⊢ Q
Tactic:
cases h with
| inl np => exact False.elim (np p)
| inr q  => exact q
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orImplies₂
Proof state before:
case inl
P Q : Prop
p : P
np : ¬P
⊢ Q
Tactic:
exact False.elim (np p)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orImplies₂
Proof state before:
case inr
P Q : Prop
p : P
q : Q
⊢ Q
Tactic:
exact q
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orImplies₃
Proof state before:
⊢ ∀ {p q : Prop}, p ∨ q → ¬p → q
Tactic:
intros P Q h np
Proof state after:
P Q : Prop
h : P ∨ Q
np : ¬P
⊢ Q
Theorem: Smt.Reconstruct.Prop.orImplies₃
Proof state before:
P Q : Prop
h : P ∨ Q
np : ¬P
⊢ Q
Tactic:
cases h with
| inl p => exact False.elim (np p)
| inr q => exact q
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orImplies₃
Proof state before:
case inl
P Q : Prop
np : ¬P
p : P
⊢ Q
Tactic:
exact False.elim (np p)
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.orImplies₃
Proof state before:
case inr
P Q : Prop
np : ¬P
q : Q
⊢ Q
Tactic:
exact q
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorganSmall
Proof state before:
⊢ ∀ {p q : Prop}, ¬(p ∨ q) → ¬p ∧ ¬q
Tactic:
intros p q h
Proof state after:
p q : Prop
h : ¬(p ∨ q)
⊢ ¬p ∧ ¬q
Theorem: Smt.Reconstruct.Prop.deMorganSmall
Proof state before:
p q : Prop
h : ¬(p ∨ q)
⊢ ¬p ∧ ¬q
Tactic:
exact match Classical.em p, Classical.em q with
| Or.inl pp,  _          => False.elim (h (Or.inl pp))
| Or.inr _,   Or.inl pq  => False.elim (h (Or.inr pq))
| Or.inr npp, Or.inr npq => And.intro npp npq
Proof state after:
no goals
Theorem: Smt.Reconstruct.Prop.deMorganSmall₂
Proof state before:
⊢ ∀ {p q : Prop}, ¬p ∧ ¬q → ¬(p ∨ q)
Tactic:
intros p q h
Proof state after:
p q : Prop
h : ¬p ∧ ¬q
⊢ ¬(p ∨ q)