internlm/Lean-Github huggingface dataset:
Theorem: LoVe.mmap_append
Proof state before:
m : Type → Type
inst✝ : LawfulMonad m
α β : Type
f : α → m β
a : α
as as' : List α
⊢ mmap f (a :: as ++ as') = do
    let bs ← mmap f (a :: as)
    let bs' ← mmap f as'
    pure (bs ++ bs')
Tactic:
simp [mmap, mmap_append _ as as', LawfulMonad.pure_bind,
LawfulMonad.bind_assoc]
Proof state after:
no goals
Theorem: LoVe.List.length_add
Proof state before:
⊢ List.length [] = List.length [] → List.length (add [] []) = List.length []
Tactic:
simp [List.add]
Proof state after:
no goals
Theorem: LoVe.List.length_add
Proof state before:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ List.length (x :: xs) = List.length (y :: ys) → List.length (add (x :: xs) (y :: ys)) = List.length (x :: xs)
Tactic:
simp [List.add, List.length]
Proof state after:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ List.length xs = List.length ys → List.length (add xs ys) = List.length xs
Theorem: LoVe.List.length_add
Proof state before:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ List.length xs = List.length ys → List.length (add xs ys) = List.length xs
Tactic:
intro hsame
Proof state after:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
hsame : List.length xs = List.length ys
⊢ List.length (add xs ys) = List.length xs
Theorem: LoVe.List.length_add
Proof state before:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
hsame : List.length xs = List.length ys
⊢ List.length (add xs ys) = List.length xs
Tactic:
rw [List.length_add xs ys hsame]
Proof state after:
no goals
Theorem: LoVe.List.length_add
Proof state before:
y : ℤ
ys : List ℤ
⊢ List.length [] = List.length (y :: ys) → List.length (add [] (y :: ys)) = List.length []
Tactic:
intro hsame
Proof state after:
y : ℤ
ys : List ℤ
hsame : List.length [] = List.length (y :: ys)
⊢ List.length (add [] (y :: ys)) = List.length []
Theorem: LoVe.List.length_add
Proof state before:
y : ℤ
ys : List ℤ
hsame : List.length [] = List.length (y :: ys)
⊢ List.length (add [] (y :: ys)) = List.length []
Tactic:
cases hsame
Proof state after:
no goals
Theorem: LoVe.List.length_add
Proof state before:
x : ℤ
xs : List ℤ
⊢ List.length (x :: xs) = List.length [] → List.length (add (x :: xs) []) = List.length (x :: xs)
Tactic:
intro hsame
Proof state after:
x : ℤ
xs : List ℤ
hsame : List.length (x :: xs) = List.length []
⊢ List.length (add (x :: xs) []) = List.length (x :: xs)
Theorem: LoVe.List.length_add
Proof state before:
x : ℤ
xs : List ℤ
hsame : List.length (x :: xs) = List.length []
⊢ List.length (add (x :: xs) []) = List.length (x :: xs)
Tactic:
cases hsame
Proof state after:
no goals
Theorem: LoVe.List.add.comm
Proof state before:
⊢ add [] [] = add [] []
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.List.add.comm
Proof state before:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ add (x :: xs) (y :: ys) = add (y :: ys) (x :: xs)
Tactic:
simp [List.add, add_comm]
Proof state after:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ add xs ys = add ys xs
Theorem: LoVe.List.add.comm
Proof state before:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ add xs ys = add ys xs
Tactic:
exact List.add.comm xs ys
Proof state after:
no goals
Theorem: LoVe.List.add.comm
Proof state before:
y : ℤ
ys : List ℤ
⊢ add [] (y :: ys) = add (y :: ys) []
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.List.add.comm
Proof state before:
x : ℤ
xs : List ℤ
⊢ add (x :: xs) [] = add [] (x :: xs)
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.Vector.add.comm
Proof state before:
n : ℕ
u v : Vector ℤ n
⊢ add u v = add v u
Tactic:
apply Subtype.eq
Proof state after:
case a
n : ℕ
u v : Vector ℤ n
⊢ ↑(add u v) = ↑(add v u)
Theorem: LoVe.Vector.add.comm
Proof state before:
case a
n : ℕ
u v : Vector ℤ n
⊢ ↑(add u v) = ↑(add v u)
Tactic:
simp [Vector.add]
Proof state after:
case a
n : ℕ
u v : Vector ℤ n
⊢ List.add ↑u ↑v = List.add ↑v ↑u
Theorem: LoVe.Vector.add.comm
Proof state before:
case a
n : ℕ
u v : Vector ℤ n
⊢ List.add ↑u ↑v = List.add ↑v ↑u
Tactic:
apply List.add.comm
Proof state after:
no goals
Theorem: LoVe.Int.neg_eq
Proof state before:
p n : ℕ
⊢ neg (Quotient.mk Setoid (p, n)) = Quotient.mk Setoid (n, p)
Tactic:
rfl
Proof state after:
no goals
Theorem: LoVe.int.neg_neg
Proof state before:
a : Int
⊢ Int.neg (Int.neg a) = a
Tactic:
induction a using Quotient.inductionOn with
| h pn =>
  cases pn with
  | mk p n => apply Int.neg_eq
Proof state after:
no goals
Theorem: LoVe.int.neg_neg
Proof state before:
case h
pn : ℕ × ℕ
⊢ Int.neg (Int.neg (Quotient.mk Int.Setoid pn)) = Quotient.mk Int.Setoid pn
Tactic:
cases pn with
| mk p n => apply Int.neg_eq
Proof state after:
no goals
Theorem: LoVe.int.neg_neg
Proof state before:
case h.mk
p n : ℕ
⊢ Int.neg (Int.neg (Quotient.mk Int.Setoid (p, n))) = Quotient.mk Int.Setoid (p, n)
Tactic:
apply Int.neg_eq
Proof state after:
no goals
Theorem: LoVe.quarter_pos
Proof state before:
x : ℚ
hx : 0 < x
⊢ 0 < x / 4
Tactic:
have hx2 : 0 < x / 2 := half_pos hx
Proof state after:
x : ℚ
hx : 0 < x
hx2 : 0 < x / 2
⊢ 0 < x / 4
Theorem: LoVe.quarter_pos
Proof state before:
x : ℚ
hx : 0 < x
hx2 : 0 < x / 2
⊢ 0 < x / 4
Tactic:
calc 0 < (x / 2) / 2 := half_pos hx2
     _ = x / 4 := by ring
Proof state after:
no goals
Theorem: LoVe.quarter_pos
Proof state before:
x : ℚ
hx : 0 < x
hx2 : 0 < x / 2
⊢ x / 2 / 2 = x / 4
Tactic:
ring
Proof state after:
no goals
Theorem: normalize_correct
Proof state before:
b : bexpr
⊢ normalize b = true ↔ interp b
Tactic:
induction b with
| atom a => cases' a <;> simp [normalize, interp]
| and a b iha ihb => simp [normalize, interp, *]
| or a b iha ihb => simp [normalize, interp, *]
| not b ih =>
  simp [normalize, interp]
  rw [Bool.eq_false_iff]
  tauto
| imp a b iha ihb =>
  simp [normalize, interp, ← iha, ← ihb]
  rw [Bool.eq_false_iff]
  tauto
Proof state after:
no goals
Theorem: normalize_correct
Proof state before:
case atom
a : Bool
⊢ normalize (atom a) = true ↔ interp (atom a)
Tactic:
cases' a <;> simp [normalize, interp]
Proof state after:
no goals
Theorem: normalize_correct
Proof state before:
case and
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize (bexpr.and a b) = true ↔ interp (bexpr.and a b)
Tactic:
simp [normalize, interp, *]
Proof state after:
no goals
Theorem: normalize_correct
Proof state before:
case or
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize (bexpr.or a b) = true ↔ interp (bexpr.or a b)
Tactic:
simp [normalize, interp, *]
Proof state after:
no goals
Theorem: normalize_correct
Proof state before:
case not
b : bexpr
ih : normalize b = true ↔ interp b
⊢ normalize (bexpr.not b) = true ↔ interp (bexpr.not b)
Tactic:
simp [normalize, interp]
Proof state after:
case not
b : bexpr
ih : normalize b = true ↔ interp b
⊢ normalize b = false ↔ ¬interp b
Theorem: normalize_correct
Proof state before:
case not
b : bexpr
ih : normalize b = true ↔ interp b
⊢ normalize b = false ↔ ¬interp b
Tactic:
rw [Bool.eq_false_iff]
Proof state after:
case not
b : bexpr
ih : normalize b = true ↔ interp b
⊢ normalize b ≠ true ↔ ¬interp b
Theorem: normalize_correct
Proof state before:
case not
b : bexpr
ih : normalize b = true ↔ interp b
⊢ normalize b ≠ true ↔ ¬interp b
Tactic:
tauto
Proof state after:
no goals
Theorem: normalize_correct
Proof state before:
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize (imp a b) = true ↔ interp (imp a b)
Tactic:
simp [normalize, interp, ← iha, ← ihb]
Proof state after:
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize a = false ∨ normalize b = true ↔ normalize a = true → normalize b = true
Theorem: normalize_correct
Proof state before:
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize a = false ∨ normalize b = true ↔ normalize a = true → normalize b = true
Tactic:
rw [Bool.eq_false_iff]
Proof state after:
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize a ≠ true ∨ normalize b = true ↔ normalize a = true → normalize b = true
Theorem: normalize_correct
Proof state before:
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize a ≠ true ∨ normalize b = true ↔ normalize a = true → normalize b = true
Tactic:
tauto
Proof state after:
no goals
Theorem: new.to_and_from
Proof state before:
p : Polar
hpmag : p.magnitude > 0
hpangle1 : -(Real.pi / 2) < p.angle
hpangle2 : p.angle < Real.pi / 2
⊢ Complex.toPolar (Polar.toComplex p) = p
Tactic:
cases' p with pangle pmag
Proof state after:
case mk
pangle pmag : ℝ
hpmag : { angle := pangle, magnitude := pmag }.magnitude > 0
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
⊢ Complex.toPolar (Polar.toComplex { angle := pangle, magnitude := pmag }) = { angle := pangle, magnitude := pmag }
Theorem: new.to_and_from
Proof state before:
case mk
pangle pmag : ℝ
hpmag : { angle := pangle, magnitude := pmag }.magnitude > 0
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
⊢ Complex.toPolar (Polar.toComplex { angle := pangle, magnitude := pmag }) = { angle := pangle, magnitude := pmag }
Tactic:
simp at hpmag
Proof state after:
case mk
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Complex.toPolar (Polar.toComplex { angle := pangle, magnitude := pmag }) = { angle := pangle, magnitude := pmag }
Theorem: new.to_and_from
Proof state before:
case mk
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Complex.toPolar (Polar.toComplex { angle := pangle, magnitude := pmag }) = { angle := pangle, magnitude := pmag }
Tactic:
simp [Complex.toPolar, Polar.toComplex]
Proof state after:
case mk
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (pmag * Real.sin pangle / (pmag * Real.cos pangle)) = pangle ∧
    Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag
Theorem: new.to_and_from
Proof state before:
case mk
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (pmag * Real.sin pangle / (pmag * Real.cos pangle)) = pangle ∧
    Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag
Tactic:
constructor
Proof state after:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (pmag * Real.sin pangle / (pmag * Real.cos pangle)) = pangle

case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag
Theorem: new.to_and_from
Proof state before:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (pmag * Real.sin pangle / (pmag * Real.cos pangle)) = pangle

case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag
Tactic:
{ rw [mul_div_mul_left]
  rw [← Real.tan_eq_sin_div_cos]
  rw [Real.arctan_tan]
  all_goals aesop }
Proof state after:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag
Theorem: new.to_and_from
Proof state before:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag
Tactic:
{ suffices : (pmag * Real.cos pangle)^2 + (pmag * Real.sin pangle)^2 = pmag^2
  rw [this]
  rw [Real.sqrt_sq] 
  linarith
  have h : (Real.sin pangle)^2 + (Real.cos pangle)^2 = 1 :=
    Real.sin_sq_add_cos_sq pangle
  linear_combination pmag ^ 2 * h }
Proof state after:
no goals
Theorem: new.to_and_from
Proof state before:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (pmag * Real.sin pangle / (pmag * Real.cos pangle)) = pangle
Tactic:
rw [mul_div_mul_left]
Proof state after:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (Real.sin pangle / Real.cos pangle) = pangle

case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0
Theorem: new.to_and_from
Proof state before:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (Real.sin pangle / Real.cos pangle) = pangle

case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0
Tactic:
rw [← Real.tan_eq_sin_div_cos]
Proof state after:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (Real.tan pangle) = pangle

case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0
Theorem: new.to_and_from
Proof state before:
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (Real.tan pangle) = pangle

case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0
Tactic:
rw [Real.arctan_tan]
Proof state after:
case mk.left.hx₁
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ -(Real.pi / 2) < pangle

case mk.left.hx₂
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pangle < Real.pi / 2

case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0
Theorem: new.to_and_from
Proof state before:
case mk.left.hx₁
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ -(Real.pi / 2) < pangle

case mk.left.hx₂
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pangle < Real.pi / 2

case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0
Tactic:
all_goals aesop
Proof state after:
no goals
Theorem: new.to_and_from
Proof state before:
case mk.left.hc
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ pmag ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: new.to_and_from
Proof state before:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag
Tactic:
suffices : (pmag * Real.cos pangle)^2 + (pmag * Real.sin pangle)^2 = pmag^2
Proof state after:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
this : (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag

case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Theorem: new.to_and_from
Proof state before:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
this : (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag

case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Tactic:
rw [this]
Proof state after:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
this : (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
⊢ Real.sqrt (pmag ^ 2) = pmag

case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Theorem: new.to_and_from
Proof state before:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
this : (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
⊢ Real.sqrt (pmag ^ 2) = pmag

case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Tactic:
rw [Real.sqrt_sq]
Proof state after:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
this : (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
⊢ 0 ≤ pmag

case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Theorem: new.to_and_from
Proof state before:
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
this : (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
⊢ 0 ≤ pmag

case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Tactic:
linarith
Proof state after:
case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Theorem: new.to_and_from
Proof state before:
case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Tactic:
have h : (Real.sin pangle)^2 + (Real.cos pangle)^2 = 1 :=
  Real.sin_sq_add_cos_sq pangle
Proof state after:
case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
h : Real.sin pangle ^ 2 + Real.cos pangle ^ 2 = 1
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Theorem: new.to_and_from
Proof state before:
case this
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
h : Real.sin pangle ^ 2 + Real.cos pangle ^ 2 = 1
⊢ (pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2 = pmag ^ 2
Tactic:
linear_combination pmag ^ 2 * h
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.I
Proof state before:
a : Prop
⊢ a → a
Tactic:
intro ha
Proof state after:
a : Prop
ha : a
⊢ a
Theorem: LoVe.BackwardProofs.I
Proof state before:
a : Prop
ha : a
⊢ a
Tactic:
exact ha
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.K
Proof state before:
a b : Prop
⊢ a → b → b
Tactic:
intro ha hb
Proof state after:
a b : Prop
ha : a
hb : b
⊢ b
Theorem: LoVe.BackwardProofs.K
Proof state before:
a b : Prop
ha : a
hb : b
⊢ b
Tactic:
exact hb
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.C
Proof state before:
a b c : Prop
⊢ (a → b → c) → b → a → c
Tactic:
intro hg hb ha
Proof state after:
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ c
Theorem: LoVe.BackwardProofs.C
Proof state before:
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ c
Tactic:
apply hg
Proof state after:
case a
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ a

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

case a
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ b
Tactic:
exact ha
Proof state after:
case a
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ b
Theorem: LoVe.BackwardProofs.C
Proof state before:
case a
a b c : Prop
hg : a → b → c
hb : b
ha : a
⊢ b
Tactic:
exact hb
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.proj_fst
Proof state before:
a : Prop
⊢ a → a → a
Tactic:
intro ha ha'
Proof state after:
a : Prop
ha ha' : a
⊢ a
Theorem: LoVe.BackwardProofs.proj_fst
Proof state before:
a : Prop
ha ha' : a
⊢ a
Tactic:
exact ha
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.proj_snd
Proof state before:
a : Prop
⊢ a → a → a
Tactic:
intro ha ha'
Proof state after:
a : Prop
ha ha' : a
⊢ a
Theorem: LoVe.BackwardProofs.proj_snd
Proof state before:
a : Prop
ha ha' : a
⊢ a
Tactic:
exact ha'
Proof state after:
no goals
Theorem: LoVe.BackwardProofs.some_nonsense
Proof state before:
a b c : Prop
⊢ (a → b → c) → a → (a → c) → b → c
Tactic:
intro hg ha hf hb
Proof state after:
a b c : Prop
hg : a → b → c
ha : a
hf : a → c
hb : b
⊢ c