internlm/Lean-Github huggingface dataset:
Theorem: LoVe.BackwardProofs.some_nonsense
Proof state before:
a b c : Prop
hg : a → b → c
ha : a
hf : a → c
hb : b
⊢ c
Tactic:
apply hg
Proof state after:
case a
a b c : Prop
hg : a → b → c
ha : a
hf : a → c
hb : b
⊢ a

case a
a b c : Prop
hg : a → b → c
ha : a
hf : a → c
hb : b
⊢ b
Theorem: LoVe.BackwardProofs.some_nonsense
Proof state before:
case a
a b c : Prop
hg : a → b → c
ha : a
hf : a → c
hb : b
⊢ a

case a
a b c : Prop
hg : a → b → c
ha : a
hf : a → c
hb : b
⊢ b
Tactic:
exact ha
Proof state after:
case a
a b c : Prop
hg : a → b → c
ha : a
hf : a → c
hb : b
⊢ b
Theorem: LoVe.BackwardProofs.some_nonsense
Proof state before:
case a
a b c : Prop
hg : a → b → c
ha : a
hf : a → c
hb : b
⊢ b
Tactic:
exact hb
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.contrapositive
Proof state before:
a b : Prop
⊢ (a → b) → ¬b → ¬a
Tactic:
intro hab hnb ha
Proof state after:
a b : Prop
hab : a → b
hnb : ¬b
ha : a
⊢ False
Theorem: LoVe.BackwardProofs.contrapositive
Proof state before:
a b : Prop
hab : a → b
hnb : ¬b
ha : a
⊢ False
Tactic:
apply hnb
Proof state after:
a b : Prop
hab : a → b
hnb : ¬b
ha : a
⊢ b
Theorem: LoVe.BackwardProofs.contrapositive
Proof state before:
a b : Prop
hab : a → b
hnb : ¬b
ha : a
⊢ b
Tactic:
apply hab
Proof state after:
a b : Prop
hab : a → b
hnb : ¬b
ha : a
⊢ a
Theorem: LoVe.BackwardProofs.contrapositive
Proof state before:
a b : Prop
hab : a → b
hnb : ¬b
ha : a
⊢ a
Tactic:
apply ha
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
α : Type
p q : α → Prop
⊢ (∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type
p q : α → Prop
⊢ (∀ (x : α), p x ∧ q x) → (∀ (x : α), p x) ∧ ∀ (x : α), q x

case mpr
α : Type
p q : α → Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mp
α : Type
p q : α → Prop
⊢ (∀ (x : α), p x ∧ q x) → (∀ (x : α), p x) ∧ ∀ (x : α), q x

case mpr
α : Type
p q : α → Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x
Tactic:
{ intro h
  apply And.intro
  { intro x
    apply And.left
    apply h }
  { intro x
    apply And.right
    apply h } }
Proof state after:
case mpr
α : Type
p q : α → Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mpr
α : Type
p q : α → Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x
Tactic:
{ intro h x
  apply And.intro
  { apply And.left h }
  { apply And.right h } }
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mp
α : Type
p q : α → Prop
⊢ (∀ (x : α), p x ∧ q x) → (∀ (x : α), p x) ∧ ∀ (x : α), q x
Tactic:
intro h
Proof state after:
case mp
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ (∀ (x : α), p x) ∧ ∀ (x : α), q x
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mp
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ (∀ (x : α), p x) ∧ ∀ (x : α), q x
Tactic:
apply And.intro
Proof state after:
case mp.left
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), p x

case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), q x
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mp.left
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), p x

case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), q x
Tactic:
{ intro x
  apply And.left
  apply h }
Proof state after:
case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), q x
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), q x
Tactic:
{ intro x
  apply And.right
  apply h }
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mp.left
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), p x
Tactic:
intro x
Proof state after:
case mp.left
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ p x
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mp.left
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ p x
Tactic:
apply And.left
Proof state after:
case mp.left.self
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ p x ∧ ?mp.left.b

case mp.left.b
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ Prop
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mp.left.self
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ p x ∧ ?mp.left.b

case mp.left.b
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ Prop
Tactic:
apply h
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), q x
Tactic:
intro x
Proof state after:
case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ q x
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ q x
Tactic:
apply And.right
Proof state after:
case mp.right.self
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ ?mp.right.a ∧ q x

case mp.right.a
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ Prop
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mp.right.self
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ ?mp.right.a ∧ q x

case mp.right.a
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ Prop
Tactic:
apply h
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mpr
α : Type
p q : α → Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x
Tactic:
intro h x
Proof state after:
case mpr
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ p x ∧ q x
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mpr
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ p x ∧ q x
Tactic:
apply And.intro
Proof state after:
case mpr.left
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ p x

case mpr.right
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ q x
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mpr.left
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ p x

case mpr.right
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ q x
Tactic:
{ apply And.left h }
Proof state after:
case mpr.right
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ q x
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mpr.right
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ q x
Tactic:
{ apply And.right h }
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mpr.left
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ p x
Tactic:
apply And.left h
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.forall_and
Proof state before:
case mpr.right
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ q x
Tactic:
apply And.right h
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_zero
Proof state before:
n : ℕ
⊢ mul 0 n = 0
Tactic:
induction n with
| zero       => rfl
| succ n' ih => simp only [mul, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_zero
Proof state before:
case zero

⊢ mul 0 Nat.zero = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_zero
Proof state before:
case succ
n' : ℕ
ih : mul 0 n' = 0
⊢ mul 0 (Nat.succ n') = 0
Tactic:
simp only [mul, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_succ
Proof state before:
m n : ℕ
⊢ mul (Nat.succ m) n = add (mul m n) n
Tactic:
induction n with
| zero       => rfl
| succ n' ih => simp only [add, add_succ, add_assoc, mul, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_succ
Proof state before:
case zero
m : ℕ
⊢ mul (Nat.succ m) Nat.zero = add (mul m Nat.zero) Nat.zero
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_succ
Proof state before:
case succ
m n' : ℕ
ih : mul (Nat.succ m) n' = add (mul m n') n'
⊢ mul (Nat.succ m) (Nat.succ n') = add (mul m (Nat.succ n')) (Nat.succ n')
Tactic:
simp only [add, add_succ, add_assoc, mul, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_comm
Proof state before:
m n : ℕ
⊢ mul m n = mul n m
Tactic:
induction m with
| zero       => simp only [mul, mul_zero]
| succ m' ih =>
  simp only [mul_succ, ih]
  ac_rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_comm
Proof state before:
case zero
n : ℕ
⊢ mul Nat.zero n = mul n Nat.zero
Tactic:
simp only [mul, mul_zero]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_comm
Proof state before:
case succ
n m' : ℕ
ih : mul m' n = mul n m'
⊢ mul (Nat.succ m') n = mul n (Nat.succ m')
Tactic:
simp only [mul_succ, ih]
Proof state after:
case succ
n m' : ℕ
ih : mul m' n = mul n m'
⊢ add (mul n m') n = mul n (Nat.succ m')
Theorem: LoVe.BackwardProofs.mul_comm
Proof state before:
case succ
n m' : ℕ
ih : mul m' n = mul n m'
⊢ add (mul n m') n = mul n (Nat.succ m')
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_assoc
Proof state before:
l m n : ℕ
⊢ mul (mul l m) n = mul l (mul m n)
Tactic:
induction n with
| zero       => rfl
| succ n' ih => simp only [mul, mul_add, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_assoc
Proof state before:
case zero
l m : ℕ
⊢ mul (mul l m) Nat.zero = mul l (mul m Nat.zero)
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.mul_assoc
Proof state before:
case succ
l m n' : ℕ
ih : mul (mul l m) n' = mul l (mul m n')
⊢ mul (mul l m) (Nat.succ n') = mul l (mul m (Nat.succ n'))
Tactic:
simp only [mul, mul_add, ih]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.add_mul
Proof state before:
l m n : ℕ
⊢ mul (add l m) n = add (mul n l) (mul n m)
Tactic:
rw [mul_comm _ n]
Proof state after:
l m n : ℕ
⊢ mul n (add l m) = add (mul n l) (mul n m)
Theorem: LoVe.BackwardProofs.add_mul
Proof state before:
l m n : ℕ
⊢ mul n (add l m) = add (mul n l) (mul n m)
Tactic:
rw [mul_add]
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
⊢ ExcludedMiddle → Peirce
Tactic:
rw [ExcludedMiddle]
Proof state after:
⊢ (∀ (a : Prop), a ∨ ¬a) → Peirce
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
⊢ (∀ (a : Prop), a ∨ ¬a) → Peirce
Tactic:
rw [Peirce]
Proof state after:
⊢ (∀ (a : Prop), a ∨ ¬a) → ∀ (a b : Prop), ((a → b) → a) → a
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
⊢ (∀ (a : Prop), a ∨ ¬a) → ∀ (a b : Prop), ((a → b) → a) → a
Tactic:
intro hem
Proof state after:
hem : ∀ (a : Prop), a ∨ ¬a
⊢ ∀ (a b : Prop), ((a → b) → a) → a
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
hem : ∀ (a : Prop), a ∨ ¬a
⊢ ∀ (a b : Prop), ((a → b) → a) → a
Tactic:
intro a b haba
Proof state after:
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ a
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ a
Tactic:
apply Or.elim (hem a)
Proof state after:
case left
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ a → a

case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ ¬a → a
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
case left
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ a → a

case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ ¬a → a
Tactic:
{ intro ha
  assumption }
Proof state after:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ ¬a → a
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ ¬a → a
Tactic:
{ intro hna
  apply haba
  intro ha
  apply False.elim
  apply hna
  assumption }
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
case left
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ a → a
Tactic:
intro ha
Proof state after:
case left
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
ha : a
⊢ a
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
case left
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
ha : a
⊢ a
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ ¬a → a
Tactic:
intro hna
Proof state after:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
⊢ a
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
⊢ a
Tactic:
apply haba
Proof state after:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
⊢ a → b
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
⊢ a → b
Tactic:
intro ha
Proof state after:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
ha : a
⊢ b
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
ha : a
⊢ b
Tactic:
apply False.elim
Proof state after:
case right.h
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
ha : a
⊢ False
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
case right.h
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
ha : a
⊢ False
Tactic:
apply hna
Proof state after:
case right.h
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
ha : a
⊢ a
Theorem: LoVe.BackwardProofs.Peirce_of_EM
Proof state before:
case right.h
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
ha : a
⊢ a
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.DN_of_Peirce
Proof state before:
⊢ Peirce → DoubleNegation
Tactic:
rw [Peirce]
Proof state after:
⊢ (∀ (a b : Prop), ((a → b) → a) → a) → DoubleNegation
Theorem: LoVe.BackwardProofs.DN_of_Peirce
Proof state before:
⊢ (∀ (a b : Prop), ((a → b) → a) → a) → DoubleNegation
Tactic:
rw [DoubleNegation]
Proof state after:
⊢ (∀ (a b : Prop), ((a → b) → a) → a) → ∀ (a : Prop), ¬¬a → a
Theorem: LoVe.BackwardProofs.DN_of_Peirce
Proof state before:
⊢ (∀ (a b : Prop), ((a → b) → a) → a) → ∀ (a : Prop), ¬¬a → a
Tactic:
intro hpeirce a hnna
Proof state after:
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
⊢ a
Theorem: LoVe.BackwardProofs.DN_of_Peirce
Proof state before:
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
⊢ a
Tactic:
apply hpeirce a False
Proof state after:
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
⊢ (a → False) → a
Theorem: LoVe.BackwardProofs.DN_of_Peirce
Proof state before:
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
⊢ (a → False) → a
Tactic:
intro hna
Proof state after:
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
hna : a → False
⊢ a
Theorem: LoVe.BackwardProofs.DN_of_Peirce
Proof state before:
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
hna : a → False
⊢ a
Tactic:
apply False.elim
Proof state after:
case h
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
hna : a → False
⊢ False
Theorem: LoVe.BackwardProofs.DN_of_Peirce
Proof state before:
case h
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
hna : a → False
⊢ False
Tactic:
apply hnna
Proof state after:
case h
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
hna : a → False
⊢ ¬a
Theorem: LoVe.BackwardProofs.DN_of_Peirce
Proof state before:
case h
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
hna : a → False
⊢ ¬a
Tactic:
exact hna
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_Iff
Proof state before:
a b : Fraction
⊢ a ≈ b ↔ a.num * b.denom = b.num * a.denom
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.add_num
Proof state before:
a b : Fraction
⊢ (a + b).num = a.num * b.denom + b.num * a.denom
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.add_denom
Proof state before:
a b : Fraction
⊢ (a + b).denom = a.denom * b.denom
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_add
Proof state before:
a a' b b' : Fraction
ha : a ≈ a'
hb : b ≈ b'
⊢ a + b ≈ a' + b'
Tactic:
simp [Setoid_Iff, add_denom, add_num] at *
Proof state after:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ (a.num * b.denom + b.num * a.denom) * (a'.denom * b'.denom) =
    (a'.num * b'.denom + b'.num * a'.denom) * (a.denom * b.denom)
Theorem: LoVe.Fraction.Setoid_add
Proof state before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ (a.num * b.denom + b.num * a.denom) * (a'.denom * b'.denom) =
    (a'.num * b'.denom + b'.num * a'.denom) * (a.denom * b.denom)
Tactic:
calc
  (num a * denom b + num b * denom a)
      * (denom a' * denom b')
  = num a * denom a' * denom b * denom b'
    + num b * denom b' * denom a * denom a' :=
    by
      simp [add_mul, mul_add]
      ac_rfl
  _ = num a' * denom a * denom b * denom b'
        + num b' * denom b * denom a * denom a' :=
    by simp [*]
  _ = (num a' * denom b' + num b' * denom a')
        * (denom a * denom b) :=
    by
      simp [add_mul, mul_add]
      ac_rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_add
Proof state before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ (a.num * b.denom + b.num * a.denom) * (a'.denom * b'.denom) =
    a.num * a'.denom * b.denom * b'.denom + b.num * b'.denom * a.denom * a'.denom
Tactic:
simp [add_mul, mul_add]
Proof state after:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a.num * b.denom * (a'.denom * b'.denom) + b.num * a.denom * (a'.denom * b'.denom) =
    a.num * a'.denom * b.denom * b'.denom + b.num * b'.denom * a.denom * a'.denom
Theorem: LoVe.Fraction.Setoid_add
Proof state before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a.num * b.denom * (a'.denom * b'.denom) + b.num * a.denom * (a'.denom * b'.denom) =
    a.num * a'.denom * b.denom * b'.denom + b.num * b'.denom * a.denom * a'.denom
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_add
Proof state before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a.num * a'.denom * b.denom * b'.denom + b.num * b'.denom * a.denom * a'.denom =
    a'.num * a.denom * b.denom * b'.denom + b'.num * b.denom * a.denom * a'.denom
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_add
Proof state before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a'.num * a.denom * b.denom * b'.denom + b'.num * b.denom * a.denom * a'.denom =
    (a'.num * b'.denom + b'.num * a'.denom) * (a.denom * b.denom)
Tactic:
simp [add_mul, mul_add]
Proof state after:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a'.num * a.denom * b.denom * b'.denom + b'.num * b.denom * a.denom * a'.denom =
    a'.num * b'.denom * (a.denom * b.denom) + b'.num * a'.denom * (a.denom * b.denom)
Theorem: LoVe.Fraction.Setoid_add
Proof state before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a'.num * a.denom * b.denom * b'.denom + b'.num * b.denom * a.denom * a'.denom =
    a'.num * b'.denom * (a.denom * b.denom) + b'.num * a'.denom * (a.denom * b.denom)
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.neg_num
Proof state before:
a : Fraction
⊢ (-a).num = -a.num
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.neg_denom
Proof state before:
a : Fraction
⊢ (-a).denom = a.denom
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_neg
Proof state before:
a a' : Fraction
hab : a ≈ a'
⊢ -a ≈ -a'
Tactic:
simp [Setoid_Iff] at *
Proof state after:
a a' : Fraction
hab : a.num * a'.denom = a'.num * a.denom
⊢ a.num * a'.denom = a'.num * a.denom
Theorem: LoVe.Fraction.Setoid_neg
Proof state before:
a a' : Fraction
hab : a.num * a'.denom = a'.num * a.denom
⊢ a.num * a'.denom = a'.num * a.denom
Tactic:
exact hab
Proof state after:
no goals
Theorem: LoVe.Fraction.mul_num
Proof state before:
a b : Fraction
⊢ (a * b).num = a.num * b.num
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.mul_denom
Proof state before:
a b : Fraction
⊢ (a * b).denom = a.denom * b.denom
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_mul
Proof state before:
a a' b b' : Fraction
ha : a ≈ a'
hb : b ≈ b'
⊢ a * b ≈ a' * b'
Tactic:
simp [Setoid_Iff] at *
Proof state after:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a.num * b.num * (a'.denom * b'.denom) = a'.num * b'.num * (a.denom * b.denom)
Theorem: LoVe.Fraction.Setoid_mul
Proof state before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a.num * b.num * (a'.denom * b'.denom) = a'.num * b'.num * (a.denom * b.denom)
Tactic:
calc
  num a * num b * (denom a' * denom b')
  = (num a * denom a') * (num b * denom b') :=
    by ac_rfl
  _ = (num a' * denom a) * (num b' * denom b) :=
    by simp [*]
  _ = num a' * num b' * (denom a * denom b) :=
    by ac_rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_mul
Proof state before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a.num * b.num * (a'.denom * b'.denom) = a.num * a'.denom * (b.num * b'.denom)
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_mul
Proof state before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a.num * a'.denom * (b.num * b'.denom) = a'.num * a.denom * (b'.num * b.denom)
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_mul
Proof state before:
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a'.num * a.denom * (b'.num * b.denom) = a'.num * b'.num * (a.denom * b.denom)
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: LoVe.Fraction.inv_num
Proof state before:
a : Fraction
ha : a.num ≠ 0
⊢ a⁻¹.num = a.denom
Tactic:
rw [inv_def a ha]
Proof state after:
no goals
Theorem: LoVe.Fraction.inv_denom
Proof state before:
a : Fraction
ha : a.num ≠ 0
⊢ a⁻¹.denom = a.num
Tactic:
rw [inv_def a ha]
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_inv
Proof state before:
a a' : Fraction
ha : a ≈ a'
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
cases Classical.em (num a = 0) with
| inl ha0 =>
  cases Classical.em (num a' = 0) with
  | inl ha'0 =>
    simp [ha0, ha'0, inv_zero]
  | inr ha'0 =>
    simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
| inr ha0 =>
  cases Classical.em (num a' = 0) with
  | inl ha'0 =>
    simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
  | inr ha'0 =>
    simp [Setoid_Iff, ha0, ha'0] at *
    linarith
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_inv
Proof state before:
case inl
a a' : Fraction
ha : a ≈ a'
ha0 : a.num = 0
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
cases Classical.em (num a' = 0) with
| inl ha'0 =>
  simp [ha0, ha'0, inv_zero]
| inr ha'0 =>
  simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_inv
Proof state before:
case inl.inl
a a' : Fraction
ha : a ≈ a'
ha0 : a.num = 0
ha'0 : a'.num = 0
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
simp [ha0, ha'0, inv_zero]
Proof state after:
no goals
Theorem: LoVe.Fraction.Setoid_inv
Proof state before:
case inl.inr
a a' : Fraction
ha : a ≈ a'
ha0 : a.num = 0
ha'0 : ¬a'.num = 0
⊢ a⁻¹ ≈ a'⁻¹
Tactic:
simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
Proof state after:
no goals