internlm/Lean-Github huggingface dataset:
Theorem: MyNat.and_or_distrib_left
Proof state before:
P Q R : Prop
h : P ∧ Q ∨ P ∧ R
⊢ P ∧ (Q ∨ R)
Tactic:
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:
case inl
P Q R : Prop
hpq : P ∧ Q
⊢ P ∧ (Q ∨ R)
Tactic:
constructor
Proof state after:
case inl.left
P Q R : Prop
hpq : P ∧ Q
⊢ P

case inl.right
P Q R : Prop
hpq : P ∧ Q
⊢ Q ∨ R
Theorem: MyNat.and_or_distrib_left
Proof state before:
case inl.left
P Q R : Prop
hpq : P ∧ Q
⊢ P

case inl.right
P Q R : Prop
hpq : P ∧ Q
⊢ Q ∨ R
Tactic:
exact hpq.1
Proof state after:
case inl.right
P Q R : Prop
hpq : P ∧ Q
⊢ Q ∨ R
Theorem: MyNat.and_or_distrib_left
Proof state before:
case inl.right
P Q R : Prop
hpq : P ∧ Q
⊢ Q ∨ R
Tactic:
apply Or.inl
Proof state after:
case inl.right.h
P Q R : Prop
hpq : P ∧ Q
⊢ Q
Theorem: MyNat.and_or_distrib_left
Proof state before:
case inl.right.h
P Q R : Prop
hpq : P ∧ Q
⊢ Q
Tactic:
exact hpq.2
Proof state after:
no goals
Theorem: MyNat.and_or_distrib_left
Proof state before:
case inr
P Q R : Prop
hpr : P ∧ R
⊢ P ∧ (Q ∨ R)
Tactic:
constructor
Proof state after:
case inr.left
P Q R : Prop
hpr : P ∧ R
⊢ P

case inr.right
P Q R : Prop
hpr : P ∧ R
⊢ Q ∨ R
Theorem: MyNat.and_or_distrib_left
Proof state before:
case inr.left
P Q R : Prop
hpr : P ∧ R
⊢ P

case inr.right
P Q R : Prop
hpr : P ∧ R
⊢ Q ∨ R
Tactic:
exact hpr.1
Proof state after:
case inr.right
P Q R : Prop
hpr : P ∧ R
⊢ Q ∨ R
Theorem: MyNat.and_or_distrib_left
Proof state before:
case inr.right
P Q R : Prop
hpr : P ∧ R
⊢ Q ∨ R
Tactic:
apply Or.inr
Proof state after:
case inr.right.h
P Q R : Prop
hpr : P ∧ R
⊢ R
Theorem: MyNat.and_or_distrib_left
Proof state before:
case inr.right.h
P Q R : Prop
hpr : P ∧ R
⊢ R
Tactic:
exact hpr.2
Proof state after:
no goals
Theorem: MyNat.contra
Proof state before:
P Q : Prop
⊢ P ∧ ¬P → Q
Tactic:
intro h
Proof state after:
P Q : Prop
h : P ∧ ¬P
⊢ Q
Theorem: MyNat.contra
Proof state before:
P Q : Prop
h : P ∧ ¬P
⊢ Q
Tactic:
cases h with
| intro hp hnp => contradiction
Proof state after:
no goals
Theorem: MyNat.contra
Proof state before:
case intro
P Q : Prop
hp : P
hnp : ¬P
⊢ Q
Tactic:
contradiction
Proof state after:
no goals
Theorem: MyNat.contrapositive2
Proof state before:
P Q : Prop
⊢ (¬Q → ¬P) → P → Q
Tactic:
by_cases P <;> by_cases Q <;> simp [*]
Proof state after:
no goals
Theorem: MyNat.succ_inj'
Proof state before:
a b : Nat
hs : succ a = succ b
⊢ a = b
Tactic:
exact succ_inj hs
Proof state after:
no goals
Theorem: MyNat.succ_succ_inj
Proof state before:
a b : Nat
hs : succ (succ a) = succ (succ b)
⊢ a = b
Tactic:
exact succ_inj (succ_inj hs)
Proof state after:
no goals
Theorem: MyNat.succ_eq_succ_of_eq
Proof state before:
a b : Nat
⊢ a = b → succ a = succ b
Tactic:
intro h
Proof state after:
a b : Nat
h : a = b
⊢ succ a = succ b
Theorem: MyNat.succ_eq_succ_of_eq
Proof state before:
a b : Nat
h : a = b
⊢ succ a = succ b
Tactic:
rw [h]
Proof state after:
no goals
Theorem: MyNat.succ_eq_succ_iff
Proof state before:
a b : Nat
⊢ succ a = succ b ↔ a = b
Tactic:
constructor
Proof state after:
case mp
a b : Nat
⊢ succ a = succ b → a = b

case mpr
a b : Nat
⊢ a = b → succ a = succ b
Theorem: MyNat.succ_eq_succ_iff
Proof state before:
a b : Nat
⊢ succ a = succ b → a = b
Tactic:
case mp =>
  apply succ_inj
Proof state after:
no goals
Theorem: MyNat.succ_eq_succ_iff
Proof state before:
a b : Nat
⊢ a = b → succ a = succ b
Tactic:
case mpr =>
  exact succ_eq_succ_of_eq
Proof state after:
no goals
Theorem: MyNat.succ_eq_succ_iff
Proof state before:
a b : Nat
⊢ succ a = succ b → a = b
Tactic:
apply succ_inj
Proof state after:
no goals
Theorem: MyNat.succ_eq_succ_iff
Proof state before:
a b : Nat
⊢ a = b → succ a = succ b
Tactic:
exact succ_eq_succ_of_eq
Proof state after:
no goals
Theorem: MyNat.add_right_cancel
Proof state before:
a b t : Nat
⊢ a + t = b + t → a = b
Tactic:
induction t with
| zero =>
  rw [add_zero, add_zero]
  intro h
  exact h
| succ t' ih =>
  rw [add_succ, add_succ]
  intro h
  have ihl : a + t' = b + t' := by exact (succ_inj h)
  exact (ih ihl)
Proof state after:
no goals
Theorem: MyNat.add_right_cancel
Proof state before:
case zero
a b : Nat
⊢ a + zero = b + zero → a = b
Tactic:
rw [add_zero, add_zero]
Proof state after:
case zero
a b : Nat
⊢ a = b → a = b
Theorem: MyNat.add_right_cancel
Proof state before:
case zero
a b : Nat
⊢ a = b → a = b
Tactic:
intro h
Proof state after:
case zero
a b : Nat
h : a = b
⊢ a = b
Theorem: MyNat.add_right_cancel
Proof state before:
case zero
a b : Nat
h : a = b
⊢ a = b
Tactic:
exact h
Proof state after:
no goals
Theorem: MyNat.add_right_cancel
Proof state before:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
⊢ a + succ t' = b + succ t' → a = b
Tactic:
rw [add_succ, add_succ]
Proof state after:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
⊢ succ (a + t') = succ (b + t') → a = b
Theorem: MyNat.add_right_cancel
Proof state before:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
⊢ succ (a + t') = succ (b + t') → a = b
Tactic:
intro h
Proof state after:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
h : succ (a + t') = succ (b + t')
⊢ a = b
Theorem: MyNat.add_right_cancel
Proof state before:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
h : succ (a + t') = succ (b + t')
⊢ a = b
Tactic:
have ihl : a + t' = b + t' := by exact (succ_inj h)
Proof state after:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
h : succ (a + t') = succ (b + t')
ihl : a + t' = b + t'
⊢ a = b
Theorem: MyNat.add_right_cancel
Proof state before:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
h : succ (a + t') = succ (b + t')
ihl : a + t' = b + t'
⊢ a = b
Tactic:
exact (ih ihl)
Proof state after:
no goals
Theorem: MyNat.add_right_cancel
Proof state before:
a b t' : Nat
ih : a + t' = b + t' → a = b
h : succ (a + t') = succ (b + t')
⊢ a + t' = b + t'
Tactic:
exact (succ_inj h)
Proof state after:
no goals
Theorem: MyNat.add_left_cancel
Proof state before:
t a b : Nat
⊢ t + a = t + b → a = b
Tactic:
rw [add_comm t a, add_comm t b]
Proof state after:
t a b : Nat
⊢ a + t = b + t → a = b
Theorem: MyNat.add_left_cancel
Proof state before:
t a b : Nat
⊢ a + t = b + t → a = b
Tactic:
exact add_right_cancel
Proof state after:
no goals
Theorem: MyNat.add_right_cancel_iff
Proof state before:
t a b : Nat
⊢ a + t = b + t ↔ a = b
Tactic:
constructor
Proof state after:
case mp
t a b : Nat
⊢ a + t = b + t → a = b

case mpr
t a b : Nat
⊢ a = b → a + t = b + t
Theorem: MyNat.add_right_cancel_iff
Proof state before:
t a b : Nat
⊢ a + t = b + t → a = b
Tactic:
case mp =>
  exact add_right_cancel
Proof state after:
no goals
Theorem: MyNat.add_right_cancel_iff
Proof state before:
t a b : Nat
⊢ a = b → a + t = b + t
Tactic:
case mpr =>
  intro h
  rw [h]
Proof state after:
no goals
Theorem: MyNat.add_right_cancel_iff
Proof state before:
t a b : Nat
⊢ a + t = b + t → a = b
Tactic:
exact add_right_cancel
Proof state after:
no goals
Theorem: MyNat.add_right_cancel_iff
Proof state before:
t a b : Nat
⊢ a = b → a + t = b + t
Tactic:
intro h
Proof state after:
t a b : Nat
h : a = b
⊢ a + t = b + t
Theorem: MyNat.add_right_cancel_iff
Proof state before:
t a b : Nat
h : a = b
⊢ a + t = b + t
Tactic:
rw [h]
Proof state after:
no goals
Theorem: MyNat.eq_zero_of_add_right_eq_self
Proof state before:
a b : Nat
⊢ a + b = a → b = 0
Tactic:
intro h
Proof state after:
a b : Nat
h : a + b = a
⊢ b = 0
Theorem: MyNat.eq_zero_of_add_right_eq_self
Proof state before:
a b : Nat
h : a + b = a
⊢ b = 0
Tactic:
rw [← add_zero a] at h
Proof state after:
a b : Nat
h : a + zero + b = a + zero
⊢ b = 0
Theorem: MyNat.eq_zero_of_add_right_eq_self
Proof state before:
a b : Nat
h : a + zero + b = a + zero
⊢ b = 0
Tactic:
exact (add_left_cancel _ _ _ h)
Proof state after:
no goals
Theorem: MyNat.succ_ne_zero
Proof state before:
a : Nat
⊢ succ a ≠ 0
Tactic:
intro h
Proof state after:
a : Nat
h : succ a = 0
⊢ False
Theorem: MyNat.succ_ne_zero
Proof state before:
a : Nat
h : succ a = 0
⊢ False
Tactic:
exact zero_ne_succ a (Eq.symm h)
Proof state after:
no goals
Theorem: MyNat.add_left_eq_zero
Proof state before:
a b : Nat
h : a + b = zero
⊢ b = zero
Tactic:
cases b with
| zero => rfl
| succ d =>
  rw [add_succ] at h
  contradiction
Proof state after:
no goals
Theorem: MyNat.add_left_eq_zero
Proof state before:
case zero
a : Nat
h : a + zero = zero
⊢ zero = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_left_eq_zero
Proof state before:
case succ
a d : Nat
h : a + succ d = zero
⊢ succ d = zero
Tactic:
rw [add_succ] at h
Proof state after:
case succ
a d : Nat
h : succ (a + d) = zero
⊢ succ d = zero
Theorem: MyNat.add_left_eq_zero
Proof state before:
case succ
a d : Nat
h : succ (a + d) = zero
⊢ succ d = zero
Tactic:
contradiction
Proof state after:
no goals
Theorem: MyNat.add_right_eq_zero
Proof state before:
a b : Nat
h : a + b = zero
⊢ a = zero
Tactic:
rw [add_comm] at h
Proof state after:
a b : Nat
h : b + a = zero
⊢ a = zero
Theorem: MyNat.add_right_eq_zero
Proof state before:
a b : Nat
h : b + a = zero
⊢ a = zero
Tactic:
apply add_left_eq_zero h
Proof state after:
no goals
Theorem: MyNat.add_one_eq_succ
Proof state before:
d : Nat
⊢ d + one = succ d
Tactic:
rw [succ_eq_add_one]
Proof state after:
no goals
Theorem: MyNat.ne_succ_self
Proof state before:
n : Nat
⊢ n ≠ succ n
Tactic:
induction n with
| zero => apply zero_ne_succ
| succ n' ih =>
  intro (h : succ n' = succ (succ n'))
  have hn : n' = succ n' := by exact succ_inj h
  exact ih hn
Proof state after:
no goals
Theorem: MyNat.ne_succ_self
Proof state before:
case zero

⊢ zero ≠ succ zero
Tactic:
apply zero_ne_succ
Proof state after:
no goals
Theorem: MyNat.ne_succ_self
Proof state before:
case succ
n' : Nat
ih : n' ≠ succ n'
⊢ succ n' ≠ succ (succ n')
Tactic:
intro (h : succ n' = succ (succ n'))
Proof state after:
case succ
n' : Nat
ih : n' ≠ succ n'
h : succ n' = succ (succ n')
⊢ False
Theorem: MyNat.ne_succ_self
Proof state before:
case succ
n' : Nat
ih : n' ≠ succ n'
h : succ n' = succ (succ n')
⊢ False
Tactic:
have hn : n' = succ n' := by exact succ_inj h
Proof state after:
case succ
n' : Nat
ih : n' ≠ succ n'
h : succ n' = succ (succ n')
hn : n' = succ n'
⊢ False
Theorem: MyNat.ne_succ_self
Proof state before:
case succ
n' : Nat
ih : n' ≠ succ n'
h : succ n' = succ (succ n')
hn : n' = succ n'
⊢ False
Tactic:
exact ih hn
Proof state after:
no goals
Theorem: MyNat.ne_succ_self
Proof state before:
n' : Nat
ih : n' ≠ succ n'
h : succ n' = succ (succ n')
⊢ n' = succ n'
Tactic:
exact succ_inj h
Proof state after:
no goals
Theorem: MyNat.mul_pos
Proof state before:
a b : Nat
⊢ a ≠ zero → b ≠ zero → a * b ≠ zero
Tactic:
intro ha hb hab
Proof state after:
a b : Nat
ha : a ≠ zero
hb : b ≠ zero
hab : a * b = zero
⊢ False
Theorem: MyNat.mul_pos
Proof state before:
a b : Nat
ha : a ≠ zero
hb : b ≠ zero
hab : a * b = zero
⊢ False
Tactic:
cases a with
| zero => exact ha (Eq.refl zero)  | succ a' =>
  rw [succ_mul] at hab
  have hbz : b = 0 := add_left_eq_zero hab
  exact hb hbz
Proof state after:
no goals
Theorem: MyNat.mul_pos
Proof state before:
case zero
b : Nat
hb : b ≠ zero
ha : zero ≠ zero
hab : zero * b = zero
⊢ False
Tactic:
exact ha (Eq.refl zero)
Proof state after:
no goals
Theorem: MyNat.mul_pos
Proof state before:
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : succ a' * b = zero
⊢ False
Tactic:
rw [succ_mul] at hab
Proof state after:
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : a' * b + b = zero
⊢ False
Theorem: MyNat.mul_pos
Proof state before:
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : a' * b + b = zero
⊢ False
Tactic:
have hbz : b = 0 := add_left_eq_zero hab
Proof state after:
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : a' * b + b = zero
hbz : b = 0
⊢ False
Theorem: MyNat.mul_pos
Proof state before:
case succ
b : Nat
hb : b ≠ zero
a' : Nat
ha : succ a' ≠ zero
hab : a' * b + b = zero
hbz : b = 0
⊢ False
Tactic:
exact hb hbz
Proof state after:
no goals
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
a b : Nat
x✝ : zero * zero = zero
⊢ zero = 0 ∨ zero = 0
Tactic:
apply Or.inl
Proof state after:
case h
a b : Nat
x✝ : zero * zero = zero
⊢ zero = 0
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
case h
a b : Nat
x✝ : zero * zero = zero
⊢ zero = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
a b b' : Nat
x✝ : zero * succ b' = zero
⊢ zero = 0 ∨ succ b' = 0
Tactic:
apply Or.inl
Proof state after:
case h
a b b' : Nat
x✝ : zero * succ b' = zero
⊢ zero = 0
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
case h
a b b' : Nat
x✝ : zero * succ b' = zero
⊢ zero = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
a b a' : Nat
x✝ : succ a' * zero = zero
⊢ succ a' = 0 ∨ zero = 0
Tactic:
apply Or.inr
Proof state after:
case h
a b a' : Nat
x✝ : succ a' * zero = zero
⊢ zero = 0
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
case h
a b a' : Nat
x✝ : succ a' * zero = zero
⊢ zero = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
⊢ succ a' = 0 ∨ succ b' = 0
Tactic:
have ha' : succ a' ≠ zero := by exact succ_ne_zero _
Proof state after:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0
Tactic:
have hb' : succ b' ≠ zero := by exact succ_ne_zero _
Proof state after:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
hb' : succ b' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
hb' : succ b' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0
Tactic:
have _ : succ a' * succ b' ≠ zero := by
  apply mul_pos <;> assumption
Proof state after:
a b a' b' : Nat
x✝¹ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
hb' : succ b' ≠ zero
x✝ : succ a' * succ b' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
a b a' b' : Nat
x✝¹ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
hb' : succ b' ≠ zero
x✝ : succ a' * succ b' ≠ zero
⊢ succ a' = 0 ∨ succ b' = 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
⊢ succ a' ≠ zero
Tactic:
exact succ_ne_zero _
Proof state after:
no goals
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
⊢ succ b' ≠ zero
Tactic:
exact succ_ne_zero _
Proof state after:
no goals
Theorem: MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
Proof state before:
a b a' b' : Nat
x✝ : succ a' * succ b' = zero
ha' : succ a' ≠ zero
hb' : succ b' ≠ zero
⊢ succ a' * succ b' ≠ zero
Tactic:
apply mul_pos <;> assumption
Proof state after:
no goals
Theorem: MyNat.mul_eq_zero_iff
Proof state before:
a b : Nat
⊢ a * b = zero ↔ a = zero ∨ b = zero
Tactic:
constructor
Proof state after:
case mp
a b : Nat
⊢ a * b = zero → a = zero ∨ b = zero

case mpr
a b : Nat
⊢ a = zero ∨ b = zero → a * b = zero
Theorem: MyNat.mul_eq_zero_iff
Proof state before:
a b : Nat
⊢ a * b = zero → a = zero ∨ b = zero
Tactic:
case mp =>
  intro
  apply eq_zero_or_eq_zero_of_mul_eq_zero
  assumption
Proof state after:
no goals
Theorem: MyNat.mul_eq_zero_iff
Proof state before:
a b : Nat
⊢ a = zero ∨ b = zero → a * b = zero
Tactic:
case mpr =>
  intro
  | Or.inl ha => rw [ha, zero_mul]
  | Or.inr hb => rw [hb, mul_zero]
Proof state after:
no goals
Theorem: MyNat.mul_eq_zero_iff
Proof state before:
a b : Nat
⊢ a * b = zero → a = zero ∨ b = zero
Tactic:
intro
Proof state after:
a b : Nat
a✝ : a * b = zero
⊢ a = zero ∨ b = zero
Theorem: MyNat.mul_eq_zero_iff
Proof state before:
a b : Nat
a✝ : a * b = zero
⊢ a = zero ∨ b = zero
Tactic:
apply eq_zero_or_eq_zero_of_mul_eq_zero
Proof state after:
case x
a b : Nat
a✝ : a * b = zero
⊢ a * b = zero
Theorem: MyNat.mul_eq_zero_iff
Proof state before:
case x
a b : Nat
a✝ : a * b = zero
⊢ a * b = zero
Tactic:
assumption
Proof state after:
no goals
Theorem: MyNat.mul_eq_zero_iff
Proof state before:
a b : Nat
⊢ a = zero ∨ b = zero → a * b = zero
Tactic:
intro
| Or.inl ha => rw [ha, zero_mul]
| Or.inr hb => rw [hb, mul_zero]
Proof state after:
no goals
Theorem: MyNat.mul_eq_zero_iff
Proof state before:
a b : Nat
x✝ : a = zero ∨ b = zero
ha : a = zero
⊢ a * b = zero
Tactic:
rw [ha, zero_mul]
Proof state after:
no goals
Theorem: MyNat.mul_eq_zero_iff
Proof state before:
a b : Nat
x✝ : a = zero ∨ b = zero
hb : b = zero
⊢ a * b = zero
Tactic:
rw [hb, mul_zero]
Proof state after:
no goals
Theorem: MyNat.mul_left_cancel
Proof state before:
a b c : Nat
ha : a ≠ zero
⊢ a * b = a * c → b = c
Tactic:
revert c
Proof state after:
a b : Nat
ha : a ≠ zero
⊢ ∀ (c : Nat), a * b = a * c → b = c
Theorem: MyNat.mul_left_cancel
Proof state before:
a b : Nat
ha : a ≠ zero
⊢ ∀ (c : Nat), a * b = a * c → b = c
Tactic:
induction b with
| zero =>
  intro c h
  rw [mul_zero] at h
  apply Eq.symm
  show c = 0
  cases eq_zero_or_eq_zero_of_mul_eq_zero (Eq.symm h) with
  | inl ha0 => contradiction
  | inr hc0 => assumption
| succ b' ihb =>
  intro
  | zero =>
    intro h
    rw [mul_zero] at h
    cases eq_zero_or_eq_zero_of_mul_eq_zero h with
    | inl ha => contradiction
    | inr hb => assumption  | succ c' =>
    intro h
    apply succ_eq_succ_of_eq
    show b' = c'
    rw [mul_succ, mul_succ] at h
    have habax : a*b' = a*c' := add_right_cancel h
    have ihbc : a*b' = a*c' → b' = c' := ihb c'
    apply ihbc
    exact habax
Proof state after:
no goals
Theorem: MyNat.mul_left_cancel
Proof state before:
case zero
a : Nat
ha : a ≠ zero
⊢ ∀ (c : Nat), a * zero = a * c → zero = c
Tactic:
intro c h
Proof state after:
case zero
a : Nat
ha : a ≠ zero
c : Nat
h : a * zero = a * c
⊢ zero = c
Theorem: MyNat.mul_left_cancel
Proof state before:
case zero
a : Nat
ha : a ≠ zero
c : Nat
h : a * zero = a * c
⊢ zero = c
Tactic:
rw [mul_zero] at h
Proof state after:
case zero
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
⊢ zero = c
Theorem: MyNat.mul_left_cancel
Proof state before:
case zero
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
⊢ zero = c
Tactic:
apply Eq.symm
Proof state after:
case zero.h
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
⊢ c = zero
Theorem: MyNat.mul_left_cancel
Proof state before:
case zero.h
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
⊢ c = zero
Tactic:
show c = 0
Proof state after:
case zero.h
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
⊢ c = 0
Theorem: MyNat.mul_left_cancel
Proof state before:
case zero.h
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
⊢ c = 0
Tactic:
cases eq_zero_or_eq_zero_of_mul_eq_zero (Eq.symm h) with
| inl ha0 => contradiction
| inr hc0 => assumption
Proof state after:
no goals
Theorem: MyNat.mul_left_cancel
Proof state before:
case zero.h.inl
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
ha0 : a = 0
⊢ c = 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: MyNat.mul_left_cancel
Proof state before:
case zero.h.inr
a : Nat
ha : a ≠ zero
c : Nat
h : zero = a * c
hc0 : c = 0
⊢ c = 0
Tactic:
assumption
Proof state after:
no goals
Theorem: MyNat.mul_left_cancel
Proof state before:
case succ
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
⊢ ∀ (c : Nat), a * succ b' = a * c → succ b' = c
Tactic:
intro
| zero =>
  intro h
  rw [mul_zero] at h
  cases eq_zero_or_eq_zero_of_mul_eq_zero h with
  | inl ha => contradiction
  | inr hb => assumption  | succ c' =>
  intro h
  apply succ_eq_succ_of_eq
  show b' = c'
  rw [mul_succ, mul_succ] at h
  have habax : a*b' = a*c' := add_right_cancel h
  have ihbc : a*b' = a*c' → b' = c' := ihb c'
  apply ihbc
  exact habax
Proof state after:
no goals
Theorem: MyNat.mul_left_cancel
Proof state before:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
⊢ a * succ b' = a * zero → succ b' = zero
Tactic:
intro h
Proof state after:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = a * zero
⊢ succ b' = zero
Theorem: MyNat.mul_left_cancel
Proof state before:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = a * zero
⊢ succ b' = zero
Tactic:
rw [mul_zero] at h
Proof state after:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = zero
⊢ succ b' = zero
Theorem: MyNat.mul_left_cancel
Proof state before:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = zero
⊢ succ b' = zero
Tactic:
cases eq_zero_or_eq_zero_of_mul_eq_zero h with
| inl ha => contradiction
| inr hb => assumption
Proof state after:
no goals
Theorem: MyNat.mul_left_cancel
Proof state before:
case inl
a : Nat
ha✝ : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = zero
ha : a = 0
⊢ succ b' = zero
Tactic:
contradiction
Proof state after:
no goals
Theorem: MyNat.mul_left_cancel
Proof state before:
case inr
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ : Nat
h : a * succ b' = zero
hb : succ b' = 0
⊢ succ b' = zero
Tactic:
assumption
Proof state after:
no goals
Theorem: MyNat.mul_left_cancel
Proof state before:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
⊢ a * succ b' = a * succ c' → succ b' = succ c'
Tactic:
intro h
Proof state after:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * succ b' = a * succ c'
⊢ succ b' = succ c'
Theorem: MyNat.mul_left_cancel
Proof state before:
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * succ b' = a * succ c'
⊢ succ b' = succ c'
Tactic:
apply succ_eq_succ_of_eq
Proof state after:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * succ b' = a * succ c'
⊢ b' = c'
Theorem: MyNat.mul_left_cancel
Proof state before:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * succ b' = a * succ c'
⊢ b' = c'
Tactic:
rw [mul_succ, mul_succ] at h
Proof state after:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
⊢ b' = c'
Theorem: MyNat.mul_left_cancel
Proof state before:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
⊢ b' = c'
Tactic:
have habax : a*b' = a*c' := add_right_cancel h
Proof state after:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
habax : a * b' = a * c'
⊢ b' = c'
Theorem: MyNat.mul_left_cancel
Proof state before:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
habax : a * b' = a * c'
⊢ b' = c'
Tactic:
have ihbc : a*b' = a*c' → b' = c' := ihb c'
Proof state after:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
habax : a * b' = a * c'
ihbc : a * b' = a * c' → b' = c'
⊢ b' = c'
Theorem: MyNat.mul_left_cancel
Proof state before:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
habax : a * b' = a * c'
ihbc : a * b' = a * c' → b' = c'
⊢ b' = c'
Tactic:
apply ihbc
Proof state after:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
habax : a * b' = a * c'
ihbc : a * b' = a * c' → b' = c'
⊢ a * b' = a * c'
Theorem: MyNat.mul_left_cancel
Proof state before:
case a
a : Nat
ha : a ≠ zero
b' : Nat
ihb : ∀ (c : Nat), a * b' = a * c → b' = c
x✝ c' : Nat
h : a * b' + a = a * c' + a
habax : a * b' = a * c'
ihbc : a * b' = a * c' → b' = c'
⊢ a * b' = a * c'
Tactic:
exact habax
Proof state after:
no goals