Confusion about tactic exact and have

Stream: lean4

[aprilgrimoire]

Hi!

            have h5 := Complex.exp_neg (↑φ * Complex.I)
            exact h5
            -- exact Complex.exp_neg (↑φ * Complex.I)

Here why can't 'have, exact' be replaced with 'exact' directly?

Here is the full code:

import Mathlib

def cyclotomic_degree_real_2 (n : ℕ) :=
  let φ : ℝ := 2 * Real.pi / n
  let α : ℂ := Complex.exp (φ * Complex.I)
  let β : ℂ := Real.cos φ

  let ℚ_in_ℂ := Subfield.closure {(1 : Complex)}
  let F := Subfield.closure (ℚ_in_ℂ ∪ {α})
  let G := Subfield.closure (ℚ_in_ℂ ∪ {β})

  have h1 : (G ≤ F) := by
    have h2 : (ℚ_in_ℂ ∪ {β} : Set ℂ) ⊆ (↑F : Set ℂ)
    . apply Set.union_subset_iff.mpr
      apply And.intro
      case left =>
        unfold F
        have h3 : (ℚ_in_ℂ : Set ℂ) ⊆ (ℚ_in_ℂ ∪ {α} : Set ℂ)
        apply Set.subset_union_left
        apply subset_trans h3
        apply Subfield.subset_closure

      case right =>
        unfold F
        apply Set.singleton_subset_iff.mpr
        have h3 : β = (α + α⁻¹) / 2
        . unfold β
          have h4 : α⁻¹ = Complex.exp (-φ * Complex.I)
          . unfold α
            symm
            conv =>
              lhs
              arg 1
              apply neg_mul


            have h5 := Complex.exp_neg (↑φ * Complex.I)
            exact h5
            -- exact Complex.exp_neg (↑φ * Complex.I)
          rw [h4]
          unfold α
          repeat rw [← Complex.cos_add_sin_I]
          rw [Complex.ofReal_cos]
          simp
          ring
        rw [h3]
        have h4 : α ∈ F
        . have h5 : α ∈ (↑ℚ_in_ℂ ∪ {α} : Set ℂ)
          . apply Set.mem_union_right
            exact Set.mem_singleton α
          apply Subfield.subset_closure
          exact h5

        have h5 : α⁻¹ ∈ F
        . apply Subfield.inv_mem'
          exact h4

        have h6 : α + α⁻¹ ∈ F
        . apply Subfield.add_mem
          exact h4
          exact h5

        apply Subfield.div_mem
        exact h6

        apply Subfield.subset_closure
        apply (Set.mem_union 2 ↑ℚ_in_ℂ {α}).mpr
        apply Or.inl

        have h7 : 1 ∈ ℚ_in_ℂ
        . apply Subfield.subset_closure
          apply Set.mem_singleton

        have h8 : (2 : ℂ) = 1 + 1
        . ring

        rw [h8]

        apply Subfield.add_mem ℚ_in_ℂ h7 h7
    unfold G
    apply Subfield.closure_le.mpr
    exact h2

  let G' := Subfield.comap (Subfield.subtype F) G

  have h2 : (Module.Free G' F) :=
    Module.Free.of_basis (Basis.ofVectorSpace G' F)

  let F_span : Set F :=
    have one_in_F : ((1 : ℂ) ∈ F) := by
      have h1 : 1 ∈ (↑ℚ_in_ℂ : Set ℂ) ∪ {α}
      . apply Set.mem_union_left
        unfold ℚ_in_ℂ
        apply Set.mem_of_subset_of_mem Subfield.subset_closure
        simp
      unfold F
      apply Set.mem_of_subset_of_mem Subfield.subset_closure
      exact h1
    have sinφI_in_F : ((Real.sin φ) * Complex.I ∈ F) := by
      have h1 : (Real.sin φ) * Complex.I = (α - α⁻¹) / 2
      . sorry
      sorry

    {⟨1, one_in_F⟩, ⟨(Real.sin φ) * Complex.I, sorry⟩}
  let wtf : F := ⟨(1 : ℂ), sorry⟩
  let wtf2 : F := ⟨(Real.sin φ) * Complex.I, sorry⟩
  h1

#help tactic

Thanks.

[David Renshaw]

Looks like definitional equality is going down a bad path somehow. It works if I do this:

            with_reducible exact Complex.exp_neg (↑φ * Complex.I)

[aprilgrimoire]

David Renshaw said:

Looks like definitional equality is going down a bad path somehow. It works if I do this:

            with_reducible exact Complex.exp_neg (↑φ * Complex.I)

Thanks. Is this a bug or a feature? I think definitional equality should be checked along all paths, with limited depth for each one.

[David Renshaw]

It also works if I explicitly indicate the type for the coercion:

            exact Complex.exp_neg ((φ:ℂ) * Complex.I)

[Kim Morrison]

It is neither a bug nor a feature. Efficiently checking definitional equality is hard, and Lean does its best. Backtracking quickly becomes infeasibly slow.