internlm/Lean-Github huggingface dataset:
Theorem: MyNat.mul_assoc
Proof state before:
case succ
a b c' : Nat
ih : a * b * c' = a * (b * c')
⊢ a * b * c' + a * b = a * (b * c' + b)
Tactic:
rw [mul_add]
Proof state after:
case succ
a b c' : Nat
ih : a * b * c' = a * (b * c')
⊢ a * b * c' + a * b = a * (b * c') + a * b
Theorem: MyNat.mul_assoc
Proof state before:
case succ
a b c' : Nat
ih : a * b * c' = a * (b * c')
⊢ a * b * c' + a * b = a * (b * c') + a * b
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: MyNat.mul_assoc
Proof state before:
case succ
a b c' : Nat
ih : a * b * c' = a * (b * c')
⊢ a * b * c' + a * b = a * (b * succ c')
Tactic:
(rw [mul_succ])
Proof state after:
case succ
a b c' : Nat
ih : a * b * c' = a * (b * c')
⊢ a * b * c' + a * b = a * (b * c' + b)
Theorem: MyNat.mul_assoc
Proof state before:
case succ
a b c' : Nat
ih : a * b * c' = a * (b * c')
⊢ a * b * c' + a * b = a * (b * succ c')
Tactic:
rw [mul_succ]
Proof state after:
case succ
a b c' : Nat
ih : a * b * c' = a * (b * c')
⊢ a * b * c' + a * b = a * (b * c' + b)
Theorem: MyNat.succ_mul
Proof state before:
a b : Nat
⊢ succ a * b = a * b + b
Tactic:
induction b with
| zero =>
  rw [mul_zero, mul_zero, add_zero]
| succ b' ih =>
  show succ a * succ b' = a * succ b' + succ b'
  exact
    calc
      succ a * succ b' = succ a * (b' + one) := by rw [succ_eq_add_one b']
      _                = succ a * b' + succ a * one := by rw [mul_add]
      _                = succ a * b' + succ a := by rw [mul_one]
      _                = a * b' + b' + succ a := by rw [ih]
      _                = a * b' + succ a + b' := by rw [add_comm_right]
      _                = a * b' + (a + one) + b' := by rw [succ_eq_add_one]
      _                = a * b' + a + one + b' := by simp only [add_assoc]
      _                = a * succ b' + one + b' := by rw [← mul_succ]
      _                = a * succ b' + b' + one := by rw [add_comm_right]
      _                = a * succ b' + (b' + one) := by rw [add_assoc]
      _                = a * succ b' + succ b' := by rw [succ_eq_add_one]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
case zero
a : Nat
⊢ succ a * zero = a * zero + zero
Tactic:
rw [mul_zero, mul_zero, add_zero]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
case succ
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ succ a * succ b' = a * succ b' + succ b'
Tactic:
exact
  calc
    succ a * succ b' = succ a * (b' + one) := by rw [succ_eq_add_one b']
    _                = succ a * b' + succ a * one := by rw [mul_add]
    _                = succ a * b' + succ a := by rw [mul_one]
    _                = a * b' + b' + succ a := by rw [ih]
    _                = a * b' + succ a + b' := by rw [add_comm_right]
    _                = a * b' + (a + one) + b' := by rw [succ_eq_add_one]
    _                = a * b' + a + one + b' := by simp only [add_assoc]
    _                = a * succ b' + one + b' := by rw [← mul_succ]
    _                = a * succ b' + b' + one := by rw [add_comm_right]
    _                = a * succ b' + (b' + one) := by rw [add_assoc]
    _                = a * succ b' + succ b' := by rw [succ_eq_add_one]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ succ a * succ b' = succ a * (b' + one)
Tactic:
rw [succ_eq_add_one b']
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ succ a * (b' + one) = succ a * b' + succ a * one
Tactic:
rw [mul_add]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ succ a * b' + succ a * one = succ a * b' + succ a
Tactic:
rw [mul_one]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ succ a * b' + succ a = a * b' + b' + succ a
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * b' + b' + succ a = a * b' + succ a + b'
Tactic:
rw [add_comm_right]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * b' + succ a + b' = a * b' + (a + one) + b'
Tactic:
rw [succ_eq_add_one]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * b' + (a + one) + b' = a * b' + a + one + b'
Tactic:
simp only [add_assoc]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * b' + a + one + b' = a * succ b' + one + b'
Tactic:
rw [← mul_succ]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * succ b' + one + b' = a * succ b' + b' + one
Tactic:
rw [add_comm_right]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * succ b' + b' + one = a * succ b' + (b' + one)
Tactic:
rw [add_assoc]
Proof state after:
no goals
Theorem: MyNat.succ_mul
Proof state before:
a b' : Nat
ih : succ a * b' = a * b' + b'
⊢ a * succ b' + (b' + one) = a * succ b' + succ b'
Tactic:
rw [succ_eq_add_one]
Proof state after:
no goals
Theorem: MyNat.add_mul
Proof state before:
a b t : Nat
⊢ (a + b) * t = a * t + b * t
Tactic:
induction t with
| zero =>
  simp
| succ t' ih =>
  rw [mul_succ, ih, mul_succ, mul_succ]
  simp
Proof state after:
no goals
Theorem: MyNat.add_mul
Proof state before:
case zero
a b : Nat
⊢ (a + b) * zero = a * zero + b * zero
Tactic:
simp
Proof state after:
no goals
Theorem: MyNat.add_mul
Proof state before:
case succ
a b t' : Nat
ih : (a + b) * t' = a * t' + b * t'
⊢ (a + b) * succ t' = a * succ t' + b * succ t'
Tactic:
rw [mul_succ, ih, mul_succ, mul_succ]
Proof state after:
case succ
a b t' : Nat
ih : (a + b) * t' = a * t' + b * t'
⊢ a * t' + b * t' + (a + b) = a * t' + a + (b * t' + b)
Theorem: MyNat.add_mul
Proof state before:
case succ
a b t' : Nat
ih : (a + b) * t' = a * t' + b * t'
⊢ a * t' + b * t' + (a + b) = a * t' + a + (b * t' + b)
Tactic:
simp
Proof state after:
no goals
Theorem: MyNat.mul_comm
Proof state before:
a b : Nat
⊢ a * b = b * a
Tactic:
induction b with
| zero => simp
| succ b' ih => rw [mul_succ, succ_mul, ih]
Proof state after:
no goals
Theorem: MyNat.mul_comm
Proof state before:
case zero
a : Nat
⊢ a * zero = zero * a
Tactic:
simp
Proof state after:
no goals
Theorem: MyNat.mul_comm
Proof state before:
case succ
a b' : Nat
ih : a * b' = b' * a
⊢ a * succ b' = succ b' * a
Tactic:
rw [mul_succ, succ_mul, ih]
Proof state after:
no goals
Theorem: MyNat.mul_left_comm
Proof state before:
a b c : Nat
⊢ a * (b * c) = b * (a * c)
Tactic:
rw [← mul_assoc]
Proof state after:
a b c : Nat
⊢ a * b * c = b * (a * c)
Theorem: MyNat.mul_left_comm
Proof state before:
a b c : Nat
⊢ a * b * c = b * (a * c)
Tactic:
rw [mul_comm a b]
Proof state after:
a b c : Nat
⊢ b * a * c = b * (a * c)
Theorem: MyNat.mul_left_comm
Proof state before:
a b c : Nat
⊢ b * a * c = b * (a * c)
Tactic:
rw [mul_assoc]
Proof state after:
no goals
Theorem: MyNat.zero_pow_succ
Proof state before:
n : Nat
⊢ zero ^ succ n = zero
Tactic:
rw [pow_succ, mul_zero]
Proof state after:
no goals
Theorem: MyNat.pow_one
Proof state before:
m : Nat
⊢ m ^ one = m
Tactic:
rw [one_eq_succ_zero, pow_succ, pow_zero, one_mul]
Proof state after:
no goals
Theorem: MyNat.one_pow
Proof state before:
n : Nat
⊢ one ^ n = one
Tactic:
induction n with
| zero => rw [pow_zero]
| succ n' ih =>
  rw [pow_succ, ih, mul_one]
Proof state after:
no goals
Theorem: MyNat.one_pow
Proof state before:
case zero

⊢ one ^ zero = one
Tactic:
rw [pow_zero]
Proof state after:
no goals
Theorem: MyNat.one_pow
Proof state before:
case succ
n' : Nat
ih : one ^ n' = one
⊢ one ^ succ n' = one
Tactic:
rw [pow_succ, ih, mul_one]
Proof state after:
no goals
Theorem: MyNat.pow_add
Proof state before:
a m n : Nat
⊢ a ^ (m + n) = a ^ m * a ^ n
Tactic:
induction n with
| zero => rw [add_zero, pow_zero, mul_one]
| succ n' ih =>
  rw [add_succ, pow_succ, pow_succ, ih, mul_assoc]
Proof state after:
no goals
Theorem: MyNat.pow_add
Proof state before:
case zero
a m : Nat
⊢ a ^ (m + zero) = a ^ m * a ^ zero
Tactic:
rw [add_zero, pow_zero, mul_one]
Proof state after:
no goals
Theorem: MyNat.pow_add
Proof state before:
case succ
a m n' : Nat
ih : a ^ (m + n') = a ^ m * a ^ n'
⊢ a ^ (m + succ n') = a ^ m * a ^ succ n'
Tactic:
rw [add_succ, pow_succ, pow_succ, ih, mul_assoc]
Proof state after:
no goals
Theorem: MyNat.mul_pow
Proof state before:
a b n : Nat
⊢ (a * b) ^ n = a ^ n * b ^ n
Tactic:
induction n with
| zero =>
  repeat (rw [pow_zero])
  rw [mul_one]
| succ n' ih =>
  rw [pow_succ, ih]
  repeat (rw [pow_succ])
  simp
Proof state after:
no goals
Theorem: MyNat.mul_pow
Proof state before:
case zero
a b : Nat
⊢ (a * b) ^ zero = a ^ zero * b ^ zero
Tactic:
repeat (rw [pow_zero])
Proof state after:
case zero
a b : Nat
⊢ one = one * one
Theorem: MyNat.mul_pow
Proof state before:
case zero
a b : Nat
⊢ one = one * one
Tactic:
rw [mul_one]
Proof state after:
no goals
Theorem: MyNat.mul_pow
Proof state before:
case zero
a b : Nat
⊢ one = one * b ^ zero
Tactic:
(rw [pow_zero])
Proof state after:
case zero
a b : Nat
⊢ one = one * one
Theorem: MyNat.mul_pow
Proof state before:
case zero
a b : Nat
⊢ one = one * b ^ zero
Tactic:
rw [pow_zero]
Proof state after:
case zero
a b : Nat
⊢ one = one * one
Theorem: MyNat.mul_pow
Proof state before:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ (a * b) ^ succ n' = a ^ succ n' * b ^ succ n'
Tactic:
rw [pow_succ, ih]
Proof state after:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ succ n' * b ^ succ n'
Theorem: MyNat.mul_pow
Proof state before:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ succ n' * b ^ succ n'
Tactic:
repeat (rw [pow_succ])
Proof state after:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * (b ^ n' * b)
Theorem: MyNat.mul_pow
Proof state before:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * (b ^ n' * b)
Tactic:
simp
Proof state after:
no goals
Theorem: MyNat.mul_pow
Proof state before:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * b ^ succ n'
Tactic:
(rw [pow_succ])
Proof state after:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * (b ^ n' * b)
Theorem: MyNat.mul_pow
Proof state before:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * b ^ succ n'
Tactic:
rw [pow_succ]
Proof state after:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * (b ^ n' * b)
Theorem: MyNat.pow_pow
Proof state before:
a m n : Nat
⊢ (a ^ m) ^ n = a ^ (m * n)
Tactic:
induction n with
| zero => rw [pow_zero, mul_zero, pow_zero]
| succ n' ih => rw [pow_succ, ih, mul_succ, pow_add]
Proof state after:
no goals
Theorem: MyNat.pow_pow
Proof state before:
case zero
a m : Nat
⊢ (a ^ m) ^ zero = a ^ (m * zero)
Tactic:
rw [pow_zero, mul_zero, pow_zero]
Proof state after:
no goals
Theorem: MyNat.pow_pow
Proof state before:
case succ
a m n' : Nat
ih : (a ^ m) ^ n' = a ^ (m * n')
⊢ (a ^ m) ^ succ n' = a ^ (m * succ n')
Tactic:
rw [pow_succ, ih, mul_succ, pow_add]
Proof state after:
no goals
Theorem: MyNat.add_squared
Proof state before:
a b : Nat
⊢ (a + b) ^ two = a ^ two + b ^ two + two * a * b
Tactic:
rw [two_eq_succ_one]
Proof state after:
a b : Nat
⊢ (a + b) ^ succ one = a ^ succ one + b ^ succ one + succ one * a * b
Theorem: MyNat.add_squared
Proof state before:
a b : Nat
⊢ (a + b) ^ succ one = a ^ succ one + b ^ succ one + succ one * a * b
Tactic:
rw [one_eq_succ_zero]
Proof state after:
a b : Nat
⊢ (a + b) ^ succ (succ zero) = a ^ succ (succ zero) + b ^ succ (succ zero) + succ (succ zero) * a * b
Theorem: MyNat.add_squared
Proof state before:
a b : Nat
⊢ (a + b) ^ succ (succ zero) = a ^ succ (succ zero) + b ^ succ (succ zero) + succ (succ zero) * a * b
Tactic:
rw [pow_succ, pow_succ, pow_succ, pow_succ, pow_succ, pow_succ]
Proof state after:
a b : Nat
⊢ (a + b) ^ zero * (a + b) * (a + b) = a ^ zero * a * a + b ^ zero * b * b + succ (succ zero) * a * b
Theorem: MyNat.add_squared
Proof state before:
a b : Nat
⊢ (a + b) ^ zero * (a + b) * (a + b) = a ^ zero * a * a + b ^ zero * b * b + succ (succ zero) * a * b
Tactic:
rw [pow_zero, pow_zero, pow_zero]
Proof state after:
a b : Nat
⊢ one * (a + b) * (a + b) = one * a * a + one * b * b + succ (succ zero) * a * b
Theorem: MyNat.add_squared
Proof state before:
a b : Nat
⊢ one * (a + b) * (a + b) = one * a * a + one * b * b + succ (succ zero) * a * b
Tactic:
rw [one_mul, one_mul, one_mul]
Proof state after:
a b : Nat
⊢ (a + b) * (a + b) = a * a + b * b + succ (succ zero) * a * b
Theorem: MyNat.add_squared
Proof state before:
a b : Nat
⊢ (a + b) * (a + b) = a * a + b * b + succ (succ zero) * a * b
Tactic:
rw [add_mul, mul_add, mul_add]
Proof state after:
a b : Nat
⊢ a * a + a * b + (b * a + b * b) = a * a + b * b + succ (succ zero) * a * b
Theorem: MyNat.add_squared
Proof state before:
a b : Nat
⊢ a * a + a * b + (b * a + b * b) = a * a + b * b + succ (succ zero) * a * b
Tactic:
rw [succ_mul, succ_mul, zero_mul, zero_add, add_mul]
Proof state after:
a b : Nat
⊢ a * a + a * b + (b * a + b * b) = a * a + b * b + (a * b + a * b)
Theorem: MyNat.add_squared
Proof state before:
a b : Nat
⊢ a * a + a * b + (b * a + b * b) = a * a + b * b + (a * b + a * b)
Tactic:
rw [add_assoc]
Proof state after:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + b * b + (a * b + a * b)
Theorem: MyNat.add_squared
Proof state before:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + b * b + (a * b + a * b)
Tactic:
rw [add_assoc (a*a) _ _]
Proof state after:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + (b * b + (a * b + a * b))
Theorem: MyNat.add_squared
Proof state before:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + (b * b + (a * b + a * b))
Tactic:
rw [add_left_comm (b*b) (a*b) (a*b)]
Proof state after:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + (a * b + (b * b + a * b))
Theorem: MyNat.add_squared
Proof state before:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + (a * b + (b * b + a * b))
Tactic:
rw [add_comm (b*b) (a*b)]
Proof state after:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + (a * b + (a * b + b * b))
Theorem: MyNat.add_squared
Proof state before:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + (a * b + (a * b + b * b))
Tactic:
rw [mul_comm a b]
Proof state after:
no goals
Theorem: MyNat.imp_self
Proof state before:
P : Prop
⊢ P → P
Tactic:
intro p
Proof state after:
P : Prop
p : P
⊢ P
Theorem: MyNat.imp_self
Proof state before:
P : Prop
p : P
⊢ P
Tactic:
exact p
Proof state after:
no goals
Theorem: MyNat.maze
Proof state before:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ U
Tactic:
apply l
Proof state after:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ T
Theorem: MyNat.maze
Proof state before:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ T
Tactic:
apply j
Proof state after:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ Q
Theorem: MyNat.maze
Proof state before:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ Q
Tactic:
apply h
Proof state after:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ P
Theorem: MyNat.maze
Proof state before:
P Q R S T U : Prop
p : P
h : P → Q
i : Q → R
j : Q → T
k : S → T
l : T → U
⊢ P
Tactic:
exact p
Proof state after:
no goals
Theorem: MyNat.imp_trans
Proof state before:
P Q F : Prop
⊢ (P → Q) → (Q → F) → P → F
Tactic:
intro f g _
Proof state after:
P Q F : Prop
f : P → Q
g : Q → F
a✝ : P
⊢ F
Theorem: MyNat.imp_trans
Proof state before:
P Q F : Prop
f : P → Q
g : Q → F
a✝ : P
⊢ F
Tactic:
apply g
Proof state after:
P Q F : Prop
f : P → Q
g : Q → F
a✝ : P
⊢ Q
Theorem: MyNat.imp_trans
Proof state before:
P Q F : Prop
f : P → Q
g : Q → F
a✝ : P
⊢ Q
Tactic:
apply f
Proof state after:
P Q F : Prop
f : P → Q
g : Q → F
a✝ : P
⊢ P
Theorem: MyNat.imp_trans
Proof state before:
P Q F : Prop
f : P → Q
g : Q → F
a✝ : P
⊢ P
Tactic:
assumption
Proof state after:
no goals
Theorem: MyNat.not_iff_imp_false
Proof state before:
P : Prop
⊢ ¬P → P → False
Tactic:
intros
Proof state after:
P : Prop
a✝¹ : ¬P
a✝ : P
⊢ False
Theorem: MyNat.not_iff_imp_false
Proof state before:
P : Prop
a✝¹ : ¬P
a✝ : P
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: MyNat.not_iff_imp_false
Proof state before:
P : Prop
⊢ (P → False) → ¬P
Tactic:
intro f
Proof state after:
P : Prop
f : P → False
⊢ ¬P
Theorem: MyNat.not_iff_imp_false
Proof state before:
P : Prop
f : P → False
⊢ ¬P
Tactic:
exact f
Proof state after:
no goals
Theorem: MyNat.contrapositive
Proof state before:
P Q : Prop
⊢ (P → Q) → ¬Q → ¬P
Tactic:
repeat (rw [not_iff_imp_false])
Proof state after:
P Q : Prop
⊢ (P → Q) → (Q → False) → P → False
Theorem: MyNat.contrapositive
Proof state before:
P Q : Prop
⊢ (P → Q) → (Q → False) → P → False
Tactic:
exact imp_trans P Q False
Proof state after:
no goals
Theorem: MyNat.contrapositive
Proof state before:
P Q : Prop
⊢ (P → Q) → (Q → False) → ¬P
Tactic:
(rw [not_iff_imp_false])
Proof state after:
P Q : Prop
⊢ (P → Q) → (Q → False) → P → False
Theorem: MyNat.contrapositive
Proof state before:
P Q : Prop
⊢ (P → Q) → (Q → False) → ¬P
Tactic:
rw [not_iff_imp_false]
Proof state after:
P Q : Prop
⊢ (P → Q) → (Q → False) → P → False
Theorem: MyNat.and_symm
Proof state before:
P Q : Prop
⊢ P ∧ Q → Q ∧ P
Tactic:
intro h
Proof state after:
P Q : Prop
h : P ∧ Q
⊢ Q ∧ P
Theorem: MyNat.and_symm
Proof state before:
P Q : Prop
h : P ∧ Q
⊢ Q ∧ P
Tactic:
exact ⟨ h.right, h.left ⟩
Proof state after:
no goals
Theorem: MyNat.and_trans
Proof state before:
P Q R : Prop
⊢ P ∧ Q → Q ∧ R → P ∧ R
Tactic:
intro hpq hqr
Proof state after:
P Q R : Prop
hpq : P ∧ Q
hqr : Q ∧ R
⊢ P ∧ R
Theorem: MyNat.and_trans
Proof state before:
P Q R : Prop
hpq : P ∧ Q
hqr : Q ∧ R
⊢ P ∧ R
Tactic:
exact ⟨hpq.left, hqr.right⟩
Proof state after:
no goals
Theorem: MyNat.iff_trans
Proof state before:
P Q R : Prop
⊢ (P ↔ Q) → (Q ↔ R) → (P ↔ R)
Tactic:
intro hpq hqr
Proof state after:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ P ↔ R
Theorem: MyNat.iff_trans
Proof state before:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ P ↔ R
Tactic:
constructor
Proof state after:
case mp
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ P → R

case mpr
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ R → P
Theorem: MyNat.iff_trans
Proof state before:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ P → R
Tactic:
case mp =>
  intro hp
  exact hqr.mp (hpq.mp hp)
Proof state after:
no goals
Theorem: MyNat.iff_trans
Proof state before:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ R → P
Tactic:
case mpr =>
  intro hr
  cases hqr with
  | intro hqr_mp hqr_mpr =>
    cases hpq with
    | intro hpq_mp hpq_mpr =>
      apply hpq_mpr
      apply hqr_mpr
      exact hr
Proof state after:
no goals
Theorem: MyNat.iff_trans
Proof state before:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ P → R
Tactic:
intro hp
Proof state after:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
hp : P
⊢ R
Theorem: MyNat.iff_trans
Proof state before:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
hp : P
⊢ R
Tactic:
exact hqr.mp (hpq.mp hp)
Proof state after:
no goals
Theorem: MyNat.iff_trans
Proof state before:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ R → P
Tactic:
intro hr
Proof state after:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
hr : R
⊢ P
Theorem: MyNat.iff_trans
Proof state before:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
hr : R
⊢ P
Tactic:
cases hqr with
| intro hqr_mp hqr_mpr =>
  cases hpq with
  | intro hpq_mp hpq_mpr =>
    apply hpq_mpr
    apply hqr_mpr
    exact hr
Proof state after:
no goals
Theorem: MyNat.iff_trans
Proof state before:
case intro
P Q R : Prop
hpq : P ↔ Q
hr : R
hqr_mp : Q → R
hqr_mpr : R → Q
⊢ P
Tactic:
cases hpq with
| intro hpq_mp hpq_mpr =>
  apply hpq_mpr
  apply hqr_mpr
  exact hr
Proof state after:
no goals
Theorem: MyNat.iff_trans
Proof state before:
case intro.intro
P Q R : Prop
hr : R
hqr_mp : Q → R
hqr_mpr : R → Q
hpq_mp : P → Q
hpq_mpr : Q → P
⊢ P
Tactic:
apply hpq_mpr
Proof state after:
case intro.intro
P Q R : Prop
hr : R
hqr_mp : Q → R
hqr_mpr : R → Q
hpq_mp : P → Q
hpq_mpr : Q → P
⊢ Q
Theorem: MyNat.iff_trans
Proof state before:
case intro.intro
P Q R : Prop
hr : R
hqr_mp : Q → R
hqr_mpr : R → Q
hpq_mp : P → Q
hpq_mpr : Q → P
⊢ Q
Tactic:
apply hqr_mpr
Proof state after:
case intro.intro
P Q R : Prop
hr : R
hqr_mp : Q → R
hqr_mpr : R → Q
hpq_mp : P → Q
hpq_mpr : Q → P
⊢ R
Theorem: MyNat.iff_trans
Proof state before:
case intro.intro
P Q R : Prop
hr : R
hqr_mp : Q → R
hqr_mpr : R → Q
hpq_mp : P → Q
hpq_mpr : Q → P
⊢ R
Tactic:
exact hr
Proof state after:
no goals
Theorem: MyNat.or_symm
Proof state before:
P Q : Prop
⊢ P ∨ Q → Q ∨ P
Tactic:
intro h
Proof state after:
P Q : Prop
h : P ∨ Q
⊢ Q ∨ P
Theorem: MyNat.or_symm
Proof state before:
P Q : Prop
h : P ∨ Q
⊢ Q ∨ P
Tactic:
cases h with
| inl hp => apply Or.inr; exact hp
| inr hq =>  apply Or.inl; exact hq
Proof state after:
no goals
Theorem: MyNat.or_symm
Proof state before:
case inl
P Q : Prop
hp : P
⊢ Q ∨ P
Tactic:
apply Or.inr
Proof state after:
case inl.h
P Q : Prop
hp : P
⊢ P
Theorem: MyNat.or_symm
Proof state before:
case inl.h
P Q : Prop
hp : P
⊢ P
Tactic:
exact hp
Proof state after:
no goals
Theorem: MyNat.or_symm
Proof state before:
case inr
P Q : Prop
hq : Q
⊢ Q ∨ P
Tactic:
apply Or.inl
Proof state after:
case inr.h
P Q : Prop
hq : Q
⊢ Q
Theorem: MyNat.or_symm
Proof state before:
case inr.h
P Q : Prop
hq : Q
⊢ Q
Tactic:
exact hq
Proof state after:
no goals
Theorem: MyNat.and_or_distrib_left
Proof state before:
P Q R : Prop
⊢ P ∧ (Q ∨ R) ↔ P ∧ Q ∨ P ∧ R
Tactic:
constructor
Proof state after:
case mp
P Q R : Prop
⊢ P ∧ (Q ∨ R) → P ∧ Q ∨ P ∧ R

case mpr
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
Theorem: MyNat.and_or_distrib_left
Proof state before:
P Q R : Prop
⊢ P ∧ (Q ∨ R) → P ∧ Q ∨ P ∧ R
Tactic:
case mp =>
  intro h
  have _ : P := h.left
  cases h.right with
  | inl hq => apply Or.inl; constructor <;> assumption
  | inr rq => apply Or.inr; constructor <;> assumption
Proof state after:
no goals
Theorem: MyNat.and_or_distrib_left
Proof state before:
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
Tactic:
case mpr =>
  intro h
  cases h with
  | inl hpq =>
    constructor
    exact hpq.1
    apply Or.inl
    exact hpq.2
    | inr hpr =>
    constructor
    exact hpr.1
    apply Or.inr
    exact hpr.2
Proof state after:
no goals
Theorem: MyNat.and_or_distrib_left
Proof state before:
P Q R : Prop
⊢ P ∧ (Q ∨ R) → P ∧ Q ∨ P ∧ R
Tactic:
intro h
Proof state after:
P Q R : Prop
h : P ∧ (Q ∨ R)
⊢ P ∧ Q ∨ P ∧ R
Theorem: MyNat.and_or_distrib_left
Proof state before:
P Q R : Prop
h : P ∧ (Q ∨ R)
⊢ P ∧ Q ∨ P ∧ R
Tactic:
have _ : P := h.left
Proof state after:
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
⊢ P ∧ Q ∨ P ∧ R
Theorem: MyNat.and_or_distrib_left
Proof state before:
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
⊢ P ∧ Q ∨ P ∧ R
Tactic:
cases h.right with
| inl hq => apply Or.inl; constructor <;> assumption
| inr rq => apply Or.inr; constructor <;> assumption
Proof state after:
no goals
Theorem: MyNat.and_or_distrib_left
Proof state before:
case inl
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
hq : Q
⊢ P ∧ Q ∨ P ∧ R
Tactic:
apply Or.inl
Proof state after:
case inl.h
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
hq : Q
⊢ P ∧ Q
Theorem: MyNat.and_or_distrib_left
Proof state before:
case inl.h
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
hq : Q
⊢ P ∧ Q
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: MyNat.and_or_distrib_left
Proof state before:
case inr
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
rq : R
⊢ P ∧ Q ∨ P ∧ R
Tactic:
apply Or.inr
Proof state after:
case inr.h
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
rq : R
⊢ P ∧ R
Theorem: MyNat.and_or_distrib_left
Proof state before:
case inr.h
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
rq : R
⊢ P ∧ R
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: MyNat.and_or_distrib_left
Proof state before:
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
Tactic:
intro h
Proof state after:
P Q R : Prop
h : P ∧ Q ∨ P ∧ R
⊢ P ∧ (Q ∨ R)