ToFun.lean

import Mathlib.Tactic.ToFun
import Mathlib.Analysis.Normed.Ring.Basic

set_option pp.unicode.fun true

/--
warning: `to_fun` correctly autogenerated the provided name `fun_id_eq'`.
You may remove it.
-/
#guard_msgs in
@[to_fun fun_id_eq']
lemma id_eq' {R : Type*} : (@id R) = id := id_eq _

@[to_fun baz]
lemma Foo.bar (f g : ℝ → ℝ) : f * g = g * f := mul_comm f g

/-- info: Foo.baz (f g : ℝ → ℝ) : (fun i ↦ f i * g i) = fun i ↦ g i * f i -/
#guard_msgs in #check Foo.baz

@[to_fun baz']
lemma _root_.Foo.bar' (f g : ℝ → ℝ) : f * g = g * f := mul_comm f g
/-- info: Foo.baz' (f g : ℝ → ℝ) : (fun i ↦ f i * g i) = fun i ↦ g i * f i -/
#guard_msgs in #check Foo.baz'

namespace Test

@[to_fun baz]
lemma Foo.bar (f g : ℝ → ℝ) : f * g = g * f := mul_comm f g
/-- info: Test.Foo.baz (f g : ℝ → ℝ) : (fun i ↦ f i * g i) = fun i ↦ g i * f i -/
#guard_msgs in #check Test.Foo.baz

@[to_fun baz'']
lemma _root_.Foo.bar'' (f g : ℝ → ℝ) : f * g = g * f := mul_comm f g
/-- info: Foo.baz'' (f g : ℝ → ℝ) : (fun i ↦ f i * g i) = fun i ↦ g i * f i -/
#guard_msgs in #check Foo.baz''

end Test

@[to_fun Bars.baz]
lemma Foo.Bar.baz (f g : ℝ → ℝ) : f * g = g * f := mul_comm f g
/-- info: Foo.Bars.baz (f g : ℝ → ℝ) : (fun i ↦ f i * g i) = fun i ↦ g i * f i -/
#guard_msgs in #check Foo.Bars.baz

@[to_fun Baz.Bars.baz]
lemma Foo.Bar.baz' (f g : ℝ → ℝ) : f * g = g * f := mul_comm f g
/-- info: Baz.Bars.baz (f g : ℝ → ℝ) : (fun i ↦ f i * g i) = fun i ↦ g i * f i -/
#guard_msgs in #check Baz.Bars.baz

-- Specifying more components than the original lemma is fine.
@[to_fun Bar.Bars.Bazzz.baz]
lemma Foo.Bar.baz'' (f g : ℝ → ℝ) : f * g = g * f := mul_comm f g
/-- info: Bar.Bars.Bazzz.baz (f g : ℝ → ℝ) : (fun i ↦ f i * g i) = fun i ↦ g i * f i -/
#guard_msgs in #check Bar.Bars.Bazzz.baz

@[to_fun]
theorem Function.mul_comm (f g : ℝ → ℝ) : f * g = g * f := _root_.mul_comm f g

/-- info: Function.fun_mul_comm (f g : ℝ → ℝ) : (fun i ↦ f i * g i) = fun i ↦ g i * f i -/
#guard_msgs in
#check Function.fun_mul_comm

/--
warning: `to_fun` correctly autogenerated the provided name `fun_bar`.
You may remove it.
-/
#guard_msgs in
@[to_fun fun_bar]
theorem bar (f g : ℝ → ℝ) : f * g = g * f := _root_.mul_comm f g

/-- Look I am the doc-string of `foo`. -/
@[to_fun]
theorem foo : (1 : Nat → Nat) = 1 := rfl

open Lean in
/--
info: Eta-expanded form of `foo`

---

Look I am the doc-string of `foo`.
-/
#guard_msgs in
run_meta
  let some doc  ← findDocString? (← getEnv) ``fun_foo | throwError "no docstring found"
  logInfo doc


-- Test that it also works when the generated proof is not a `rfl` proof:

@[to_additive (attr := push ← high)]
lemma Pi.mul_def' {ι : Type*} {M : ι → Type*} [∀ i, Mul (M i)] (f g : ∀ i, M i) :
    f * g = fun i ↦ f i * g i := (rfl)

@[to_fun]
theorem Function.mul_comm' (f g : ℝ → ℝ) : f * g = g * f := _root_.mul_comm f g

/-- info: Function.fun_mul_comm' (f g : ℝ → ℝ) : (fun i ↦ f i * g i) = fun i ↦ g i * f i -/
#guard_msgs in
#check Function.fun_mul_comm'