Unknown identifier `exp` Error code: lean.unknownIdentifier

Stream: new members

[Arthur Rats]

Hello everyone. How are you?

I recently used Lean4 and encountered this error (Unknown identifier exp
Error code: lean.unknownIdentifier). Could someone help me resolve this?

[Ilmārs Cīrulis]

Hello! :wave:

Can you tell us more about the problem, maybe even post #mwe?

[Arthur Rats]

I'm using Lean4 in VScode. I'm following Mathematics in Lean and got stuck at step 2.3, where there's an expression like (example (h : 1 ≤ a) (h' : b ≤ c) : 2 + a + exp b ≤ 3 * a + exp c := by
linarith). However, my VScode doesn't accept the 'exp' variable and gives the following error: Unknown identifier exp
Error code: lean.unknownIdentifier

[Aaron Liu]

did you mean docs#Real.exp

[Arthur Rats]

I'm using Lean4 in VScode. I'm following Mathematics in Lean and got stuck at step 2.3, where there's an expression like (example (h : 1 ≤ a) (h' : b ≤ c) : 2 + a + exp b ≤ 3 * a + exp c := by
linarith). However, my VScode doesn't accept the 'exp' variable and gives the following error: Unknown identifier exp
Error code: lean.unknownIdentifier

[Robin Arnez]

You might need to open Real before

[Notification Bot]

A message was moved here from #mathlib4 > The plan to remove induction' by Matthew Ballard.

[Matthew Ballard]

@Arthur Rats I've moved your message to a place where it will more attention.

[Arthur Rats]

error2.png

This is my error

[Notification Bot]

This topic was moved here from #lean4 > Unknown identifier `exp` Error code: lean.unknownIdentifier by Matthew Ballard.

[Notification Bot]

3 messages were moved here from #new members > request for help by Matthew Ballard.

[Notification Bot]

A message was moved here from #lean4 > Unknown identifier `exp` Error code: lean.unknownIdentifier by Matthew Ballard.

[Robin Arnez]

What does #where print

[Arthur Rats]

On the left side is where we can write our proof of the theorem. On the right side, we see the code executing in real time.

[Robin Arnez]

No I mean, can you put #where in your code somewhere (like the #checks you have there) and then copy its output here

[Kevin Buzzard]

My guess is that this is not a Lean file written in a correctly-formatted Lean project. Please follow the instructions on how to download and correctly install the Mathematics In Lean repository as a Lean project.

[Arthur Rats]

Here's the problem: I already have the Mathlib package downloaded in its entirety. I've tried importing several additional libraries, but it doesn't work.

[Aaron Liu]

but what does #where say?

[Arthur Rats]

On the right side you can see that the expression 'exp' appears as an error (Unknown identifier exp
Error code: lean.unknownIdentifier)

[Aaron Liu]

that's great but what does #where say?

[Aaron Liu]

it will help me understand your setup

[Arthur Rats]

Sorry my friend, I don't understand. Where is this #where you refer to?

[Matt Diamond]

you have to type it the same way you've typed #check

[Aaron Liu]

it's a command like #check and #print

[Aaron Liu]

you can tell because they all have the #

[Arthur Rats]

I'm using Lean as a proof assistant to prove theorems, following a risky approach outlined in this document: https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html#using-theorems-and-lemmas

The #check function is used to verify the type of argument being referenced.

[Matt Diamond]

(deleted)

[Aaron Liu]

yes and the #where function is used to print the open namespaces and the modified options

[Arthur Rats]

he said this:

namespace MyRing

variable (a b c d e f : ℝ) (R : Type) [Ring R] {R : Type} [Ring R] {G : Type*} [Group G]

set_option maxSynthPendingDepth 3
set_option linter.mathlibStandardSet true
set_option relaxedAutoImplicit false
set_option pp.unicode.fun true
set_option autoImplicit false
set_option Elab.inServer true

[Aaron Liu]

great that makes sense

[Aaron Liu]

you need an open Real

[Arthur Rats]

i need create a new real?

[Aaron Liu]

no you need to put open Real above your theorem statement

[Aaron Liu]

this is a command like #check and #print but it doesn't output any information

[Aaron Liu]

instead, it modifies the environment

[Aaron Liu]

you should also consider following the instructions here in order to correctly checkout the Mathematics in Lean book so you don't have these difficulties in the future

[Arthur Rats]

I really appreciate your support regarding my question. I wasn't able to solve what I wanted, but I'll still research it further.

[Ryan Smith]

Instead of a screenshot could you give us a copy and paste of the entire contents of your file? It sounds like you have a namespace issue but we can't diagnose that easily without the ability to copy your code into our editors

[Weiyi Wang]

Probably a silly question but... you have import Mathlib on the top, right?

[Arthur Rats]

Here is my complete code so far:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Order.Ring.Basic

set_option linter.style.cdot false
-- MATH IN LEAN
-- CAP: 2.1:
--1
example (a b c : ℝ) : a * b * c = b * (a * c) := by
  rw [← mul_assoc]
  rw [mul_comm a b]
--2
example (a b c : ℝ) : c * b * a = b * (a * c) := by
  rw [← mul_assoc]
  rw [mul_comm c b]
  rw [mul_assoc]
  rw [mul_comm c a]
  rw [← mul_assoc]
--3
example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  rw [← mul_comm]
  rw [mul_assoc]
  rw [mul_comm c a]
--4
example (a b c : ℝ) : a * b * c = b * c * a := by
  rw [mul_assoc]
  rw [mul_comm]
--5
example (a b c : ℝ) : a * (b * c) = b * (c * a) := by
  rw [mul_comm]
  rw [mul_assoc]
--6

example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  rw [mul_comm a]
  rw [mul_assoc]
  rw [mul_comm c a]
--7
example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h']
  rw [← mul_assoc]
  rw [h]
  rw [mul_assoc]
--8
example (a b c d e f : ℝ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := by
  rw [mul_assoc a]
  rw [h]
  rw [← mul_assoc]
--9
example (a b c d : ℝ) (h : c = b * a - d) (h' : d = a * b) : c = 0 := by
  rw [mul_comm ] at h
  rw [h'] at h
  rw [sub_self] at h
  rw [h]
--10
example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h', ← mul_assoc, h, mul_assoc]
--11
variable (a b c d e f : ℝ)
example (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
  rw [h', ← mul_assoc, h, mul_assoc]
--12
section
#check mul_assoc
#check mul_assoc c a b
#check mul_add
end
--15
example (a b c : ℕ) (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := by
  nth_rw 2 [h]
  rw [add_mul]
-- CAP: 2.2:

variable (R : Type*) [Ring R]

#check (add_assoc : ∀ a b c : R, a + b + c = a + (b + c))
#check (add_comm : ∀ a b : R, a + b = b + a)
#check (zero_add : ∀ a : R, 0 + a = a)
#check (neg_add_cancel : ∀ a : R, -a + a = 0)
#check (mul_assoc : ∀ a b c : R, a * b * c = a * (b * c))
#check (mul_one : ∀ a : R, a * 1 = a)
#check (one_mul : ∀ a : R, 1 * a = a)
#check (mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c)
#check (add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c)

namespace MyRing
variable {R : Type*} [Ring R]

theorem add_zero (a : R) : a + 0 = a := by rw [add_comm, zero_add]

theorem add_neg_cancel (a : R) : a + -a = 0 := by rw [add_comm, neg_add_cancel]

theorem add_neg_left_cancel (a b : R) : -a + (a + b) = b := by
  rw [← add_assoc]
  rw [neg_add_cancel]
  rw [zero_add]

theorem add_neg_cancel_right (a b : R) : a + b + -b = a := by
  rw [add_comm]
  rw [add_comm a b]
  rw [← add_assoc]
  rw [neg_add_cancel]
  rw [zero_add]

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
  have ha : -a + (a + c) = b := by
    rw [← h, ← add_assoc, neg_add_cancel, zero_add]
  rw [← add_assoc, neg_add_cancel, zero_add] at ha
  symm at ha
  exact ha


theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c := by
  rw [add_comm a b, add_comm c b] at h
  rw [add_left_cancel h]


theorem mul_zero (a : R) : a * 0 = 0 := by
  have h : a * 0 + a * 0 = a * 0 + 0 := by
    rw [← mul_add, add_zero, add_zero]
  rw [add_left_cancel h]


theorem zero_mul (a : R) : 0 * a = 0 := by
  have h: 0 * a + 0 * a = 0 * a + 0 := by
    rw [← add_mul, add_zero, add_zero]
  apply add_left_cancel h


theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
  have h': -a + (a + b) = -a + 0 := by
    rw [h]
  rw [add_neg_left_cancel, add_zero] at h'
  symm
  exact h'


theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b := by
  have h': (a + b) + - b = 0 + -b := by
    rw [h]
  rw [add_assoc, add_neg_cancel, add_zero, zero_add] at h'
  exact h'


theorem neg_zero : (-0 : R) = 0 := by
  apply neg_eq_of_add_eq_zero
  rw [add_zero]
--DEBATER EM SALA
theorem neg_neg (a : R) : - -a = a := by
  apply neg_eq_of_add_eq_zero
  rw [neg_add_cancel]


example (a b : R) : a - b = a + -b :=
  sub_eq_add_neg a b

example (a b : ℝ) : a - b = a + -b :=
  rfl

example (a b : ℝ) : a - b = a + -b := by
  rfl

theorem self_sub (a : R) : a - a = 0 := by
  rw [sub_eq_add_neg, add_neg_cancel]


theorem one_add_one_eq_two : 1 + 1 = (2 : R) := by
  norm_num

theorem sum_square : 1 + 2 + 3 + 4  ≠  (1 : ℝ) := by
  norm_num
--Análise
theorem two_mul (a : R) : 2 * a = a + a := by
  rw [← one_add_one_eq_two, add_mul, one_mul]


variable {G : Type*} [Group G]

#check (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
#check (one_mul : ∀ a : G, 1 * a = a)
#check (inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1)
--Fazer em sala
theorem mul_inv_cancel (a : G) : a * a⁻¹  = 1 := by
  simp
--Fazer em sala
theorem mul_one (a : G) : a * 1 = a := by
  rw [← inv_mul_cancel a, ← mul_assoc, mul_inv_cancel, one_mul]
--Fazer em sala
theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
  simp
----------------------------------------------------------------------------------
-- CAP 2.3:
--Parte 1
#check (le_refl : ∀ a : ℝ, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
--Parte 2
example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans
  · apply h₀
  · apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans h₀
  apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z :=
  le_trans h₀ h₁

example (x : ℝ) : x ≤ x := by
  apply le_refl

example (x : ℝ) : x ≤ x :=
  le_refl x
--Parte3
#check (le_refl : ∀ a, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (lt_of_le_of_lt : a ≤ b → b < c → a < c)
#check (lt_of_lt_of_le : a < b → b ≤ c → a < c)
#check (lt_trans : a < b → b < c → a < c)

example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
  apply lt_trans
  . apply lt_of_le_of_lt
    . exact h₀
    . exact h₁
  . apply lt_of_le_of_lt
    . exact h₂
    . exact h₃




example (h : 1 ≤ a) (h' : b ≤ c) : 2 + a +  exp b ≤ 3 * a + exp c := by

----------------------------------------------------------------------------------
#check MyRing.add_zero
#check add_zero


end MyRing
--1
theorem teorema1 (a b : R) : -a + (a + b) = b := by
  rw [← add_assoc]
  rw [neg_add_cancel]
  rw [zero_add]
--2
theorem teorema2 (a b : R) : a + b + -b = a := by
  rw [add_comm]
  rw [add_comm a b]
  rw [← add_assoc]
  rw [neg_add_cancel]
  rw [zero_add]
--3
theorem teorema3 {a b c : R} (h : a + b = a + c) : b = c := by
  rw [add_left_cancel h]
--4
theorem teorema4 {a b c : R} (h : a + b = c + b) : a = c := by
  rw [add_right_cancel h]
--5
theorem teorema5 (a : R) : a * 0 = 0 := by
  have h : a * 0 + a * 0 = a * 0 + 0 := by
    rw [← mul_add, add_zero, add_zero]
  rw [add_left_cancel h]
--6
theorem teorema6 (a : R) : 0 * a = 0 := by
  have h : 0 * a + 0 * a = 0 * a + 0 := by
    rw [← add_mul, add_zero, add_zero]
  rw [add_left_cancel h]
--7

/-theorem teorema7 {a b : R} (h : a + b = 0) : -a = b := by
  have h1 : -a + 0 = b + 0 := by
    rw [add_zero, add_zero]
  rw [add_zero, add_zero] at h1
-/
--8
example (a b : R) : a - b = a + -b :=
  sub_eq_add_neg a b
--9
/-variable {G : Type} [AddGroup G] (a : G)

theorem self_sub : a - a = 0 := by
  rw [sub_eq_add_neg, add_right_neg]
-/
-- CAP: 2.3:

#check (le_refl : ∀ a : ℝ, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)

variable (h : a ≤ b) (h' : b ≤ c)

#check (le_refl : ∀ a : Real, a ≤ a)
#check (le_refl a : a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (le_trans h : b ≤ c → a ≤ c)
#check (le_trans h h' : a ≤ c)

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans
  · apply h₀
  · apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
  apply le_trans h₀
  apply h₁

example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z :=
  le_trans h₀ h₁

example (x : ℝ) : x ≤ x := by
  apply le_refl

example (x : ℝ) : x ≤ x :=
  le_refl x
--1
example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
  linarith


#check (exp_le_exp : exp a ≤ exp b ↔ a ≤ b)
#check (exp_lt_exp : exp a < exp b ↔ a < b)
#check (log_le_log : 0 < a → a ≤ b → log a ≤ log b)
#check (log_lt_log : 0 < a → a < b → log a < log b)
#check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
#check (add_le_add_left : a ≤ b → ∀ c, c + a ≤ c + b)
#check (add_le_add_right : a ≤ b → ∀ c, a + c ≤ b + c)
#check (add_lt_add_of_le_of_lt : a ≤ b → c < d → a + c < b + d)
#check (add_lt_add_of_lt_of_le : a < b → c ≤ d → a + c < b + d)
#check (add_lt_add_left : a < b → ∀ c, c + a < c + b)
#check (add_lt_add_right : a < b → ∀ c, a + c < b + c)
#check (add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b)
#check (add_pos : 0 < a → 0 < b → 0 < a + b)
#check (add_pos_of_pos_of_nonneg : 0 < a → 0 ≤ b → 0 < a + b)
#check (exp_pos : ∀ a, 0 < exp a)
#check add_le_add_left

[Arthur Rats]

some theorems have already been solved

[Aaron Liu]

try using the file in #mil

[Arthur Rats]

what is #mil?

[Aaron Liu]

it's a link and you can click on it

[Aaron Liu]

it linkifies to https://leanprover-community.github.io/mathematics_in_lean/

[Arthur Rats]

Sorry, continuous without understanding