tactic `by exact` vs proof term

Stream: new members

[Nicolas Rolland]

Is there any difference between by exact foo and foo ?

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

variable (f g : ℝ → ℝ) (a b : ℝ)


-- OK
example (hfa : FnUb f a) (hgb : FnUb g b) (nng : FnLb g 0) (nna : 0 ≤ a) :
    FnUb (fun x ↦ f x * g x) (a * b) := fun x ↦
    show f x * g x <= a * b by
    have h := (mul_le_mul_of_nonneg_right (hfa x) (nng x) : f x * g x ≤ a * g x)
    calc
      f x * g x  <= a * g x := by exact  h
               _ <= a * b :=  mul_le_mul_of_nonneg_left (hgb x) nna

-- NOT OK
example (hfa : FnUb f a) (hgb : FnUb g b) (nng : FnLb g 0) (nna : 0 ≤ a) :
    FnUb (fun x ↦ f x * g x) (a * b) := fun x ↦
    show f x * g x <= a * b by
    have h := (mul_le_mul_of_nonneg_right (hfa x) (nng x) : f x * g x ≤ a * g x)
    calc
      /-
      function expected at
        h
      term has type
        f x * g x ≤ a * g x
      -/
      f x * g x  <= a * g x := h
               _ <= a * b :=  mul_le_mul_of_nonneg_left (hgb x) nna

[Alex J. Best]

by exact changes the order in which the terms are elaborated, which can be helpful, or a bad thing depending on the context. In by exact the term is elaborated independently of the type that it should be in context. So in this example a coercion is not inserted and the definition fails

axiom A : Type
axiom B : Type
instance : Coe A B := sorry

variable (a : A)
def foo : B := a
def bar : B := by exact a

[Nicolas Rolland]

Ok. The behaviour a bit surprising in my example. I wonder if I can get a rule of thumb.

It might be best to use by exact and only give the proof term when it fails to allow coercions ?

[Eric Rodriguez]

there is examples where rfl fails but by exact rfl works