awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ Eq (α := ℝ)
    (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              ⋯ :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        I :
      ℝ)
    (0 : ℝ)

Tactic:
h.I_re_ax

Premises used: RCLike.I_re_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ Eq (α := ℝ)
    (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              ⋯ :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        I :
      ℝ)
    (0 : ℝ)

Tactic:
exact h.I_re_ax

Premises used: RCLike.I_re_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst : Eq.{u_3 + 1} (α := 𝕜) I 0 ∨ HMul.hMul (α := 𝕜) I I = -1
⊢ Eq.{u_3 + 1} (α := 𝕜) I 0 ∨ HMul.hMul (α := 𝕜) I I = -1

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ Eq.{u_3 + 1} (α := 𝕜) I 0 ∨ HMul.hMul (α := 𝕜) I I = -1

Tactic:
h.I_mul_I_ax

Premises used: RCLike.I_mul_I_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ Eq.{u_3 + 1} (α := 𝕜) I 0 ∨ HMul.hMul (α := 𝕜) I I = -1

Tactic:
exact h.I_mul_I_ax

Premises used: RCLike.I_mul_I_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst :
  ∀ (z : 𝕜),
    HAdd.hAdd (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                      let __spread.0 := hk;
                      𝕜 →+ ℝ)
                      (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                      re)
                      ⋯ :
                    let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    𝕜 →+ ℝ) :
                  (a : 𝕜) → ℝ)
                z :
              ℝ) :
          𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜)
          (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                  ℝ →+* 𝕜 } :
                (a : ℝ) → 𝕜)
              (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                        let __spread.0 := hk;
                        𝕜 →+ ℝ)
                        (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                        im)
                        ⋯ :
                      let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                      𝕜 →+ ℝ) :
                    (a : 𝕜) → ℝ)
                  z :
                ℝ) :
            𝕜)
          (I : 𝕜)) =
      z
⊢ ∀ (z : 𝕜),
    HAdd.hAdd (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                      let __spread.0 := hk;
                      𝕜 →+ ℝ)
                      (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                      re)
                      ⋯ :
                    let __spread.0 := hk;
                    𝕜 →+ ℝ) :
                  (a : 𝕜) → ℝ)
                z :
              ℝ) :
          𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜)
          (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                  ℝ →+* 𝕜 } :
                (a : ℝ) → 𝕜)
              (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                        let __spread.0 := hk;
                        𝕜 →+ ℝ)
                        (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                        im)
                        ⋯ :
                      let __spread.0 := hk;
                      𝕜 →+ ℝ) :
                    (a : 𝕜) → ℝ)
                  z :
                ℝ) :
            𝕜)
          (I : 𝕜)) =
      z

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (z : 𝕜),
    HAdd.hAdd (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                      let __spread.0 := hk;
                      𝕜 →+ ℝ)
                      (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                      re)
                      ⋯ :
                    let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    𝕜 →+ ℝ) :
                  (a : 𝕜) → ℝ)
                z :
              ℝ) :
          𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜)
          (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                  ℝ →+* 𝕜 } :
                (a : ℝ) → 𝕜)
              (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                        let __spread.0 := hk;
                        𝕜 →+ ℝ)
                        (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                        im)
                        ⋯ :
                      let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                      𝕜 →+ ℝ) :
                    (a : 𝕜) → ℝ)
                  z :
                ℝ) :
            𝕜)
          (I : 𝕜)) =
      z

Tactic:
h.re_add_im_ax

Premises used: RCLike.re_add_im_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (z : 𝕜),
    HAdd.hAdd (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                      let __spread.0 := hk;
                      𝕜 →+ ℝ)
                      (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                      re)
                      ⋯ :
                    let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    𝕜 →+ ℝ) :
                  (a : 𝕜) → ℝ)
                z :
              ℝ) :
          𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜)
          (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                  ℝ →+* 𝕜 } :
                (a : ℝ) → 𝕜)
              (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                        let __spread.0 := hk;
                        𝕜 →+ ℝ)
                        (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                        im)
                        ⋯ :
                      let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                      𝕜 →+ ℝ) :
                    (a : 𝕜) → ℝ)
                  z :
                ℝ) :
            𝕜)
          (I : 𝕜)) =
      z

Tactic:
exact h.re_add_im_ax

Premises used: RCLike.re_add_im_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst :
  ∀ (r : ℝ),
    ((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              ⋯ :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜) =
      r
⊢ ∀ (r : ℝ),
    ((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              ⋯ :
            let __spread.0 := hk;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜) =
      r

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ),
    ((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              ⋯ :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜) =
      r

Tactic:
h.ofReal_re_ax

Premises used: RCLike.ofReal_re_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ),
    ((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              ⋯ :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜) =
      r

Tactic:
exact h.ofReal_re_ax

Premises used: RCLike.ofReal_re_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst :
  ∀ (r : ℝ),
    Eq (α := ℝ)
      (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                im)
                ⋯ :
              let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                  ℝ →+* 𝕜 } :
                (a : ℝ) → 𝕜)
              r :
            𝕜) :
        ℝ)
      (0 : ℝ)
⊢ ∀ (r : ℝ),
    Eq (α := ℝ)
      (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                im)
                ⋯ :
              let __spread.0 := hk;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                  ℝ →+* 𝕜 } :
                (a : ℝ) → 𝕜)
              r :
            𝕜) :
        ℝ)
      (0 : ℝ)

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ),
    Eq (α := ℝ)
      (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                im)
                ⋯ :
              let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                  ℝ →+* 𝕜 } :
                (a : ℝ) → 𝕜)
              r :
            𝕜) :
        ℝ)
      (0 : ℝ)

Tactic:
h.ofReal_im_ax

Premises used: RCLike.ofReal_im_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ),
    Eq (α := ℝ)
      (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                im)
                ⋯ :
              let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                  ℝ →+* 𝕜 } :
                (a : ℝ) → 𝕜)
              r :
            𝕜) :
        ℝ)
      (0 : ℝ)

Tactic:
exact h.ofReal_im_ax

Premises used: RCLike.ofReal_im_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (z w : 𝕜),
    ((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              ⋯ :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        (z * w) =
      HMul.hMul (α := ℝ) (β := ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              w :
            ℝ) -
        HMul.hMul (α := ℝ) (β := ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    im)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    im)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              w :
            ℝ)

Tactic:
h.mul_re_ax

Premises used: RCLike.mul_re_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (z w : 𝕜),
    ((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              ⋯ :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        (z * w) =
      HMul.hMul (α := ℝ) (β := ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              w :
            ℝ) -
        HMul.hMul (α := ℝ) (β := ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    im)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    im)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              w :
            ℝ)

Tactic:
exact h.mul_re_ax

Premises used: RCLike.mul_re_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (z w : 𝕜),
    ((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              im)
              ⋯ :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        (z * w) =
      HMul.hMul (α := ℝ) (β := ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    im)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              w :
            ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    im)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    ⋯ :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              w :
            ℝ)

Tactic:
h.mul_im_ax

Premises used: RCLike.mul_im_ax