How to find appropriate lib to import in Mathlib4

Stream: lean4

[Jaeboum Kim]

I am having a hard time getting used to Mathlib4, which is different structure from Mathlib3.
I have an error in the following code. "unknown tactic" at "mul_add".
How should I deal with problems that arise from not properly importing the lib?

import Mathlib.NumberTheory.ArithmeticFunction
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Real.Basic
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
import Mathlib.Logic.Equiv.Defs
import Mathlib.Tactic.Ring.Basic
import Mathlib.RingTheory.PowerSeries.Basic
import Mathlib.Algebra.Ring.Defs

theorem mathd_algebra
  (x : ℝ)
  (σ : Equiv ℝ ℝ)
  (h₀ : ∀ x, σ.1 x = 5 * x - 12)
  (h₁ : σ.1 (x + 1) = σ.2 x) :
  x = 47 / 24 :=
by
  mul_add

[Kevin Buzzard]

That looks like things are working fine. mul_add isn't a tactic so the error is expected.

[Jaeboum Kim]

Actually, I got "unexpected identifier; expected '['" errors at the last line.
While debugging, I found mul_add has an error.

theorem mathd_algebra
  (x : ℝ)
  (σ : Equiv ℝ ℝ)
  (h₀ : ∀ x, σ.1 x = 5 * x - 12)
  (h₁ : σ.1 (x + 1) = σ.2 x) :
  x = 47 / 24 :=
by
  field_simp [h₀, mul_add, add_mul, sub_add_cancel, mul_assoc, add_comm]
  have := congr_arg σ.to_fun h₁
  rw h₀ at this

[Yaël Dillies]

It should be rw [h₀] at this

[Jaeboum Kim]

@Yaël Dillies Yes, you're right! How can I find proper lib for import? ex) symmetry (unknown tactic)

[Yaël Dillies]

It's now called symm

[Jaeboum Kim]

How can I find these changes easily...?

[Yaël Dillies]

Ask here :smile:

[Kevin Buzzard]

Isn't there some "crash course to mathlib 4 for mathlib 3 users" somewhere? Maybe on the community website or the mathlib GitHub repo?

[Yaël Dillies]

https://github.com/leanprover-community/mathlib4/wiki/Lean-4-survival-guide-for-Lean-3-users