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
⊢ ∀ (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:
exact h.mul_im_ax

Premises used: RCLike.mul_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 :
  ∀ (z : 𝕜),
    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 : 𝕜) → ℝ)
          ((starRingEnd 𝕜 : (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 : 𝕜) → ℝ)
          z :
        ℝ)
⊢ ∀ (z : 𝕜),
    Eq (α := ℝ)
      (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                re)
                ⋯ :
              let __spread.0 := hk;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) :
        ℝ)
      (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                re)
                ⋯ :
              let __spread.0 := hk;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          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 : 𝕜),
    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 : 𝕜) → ℝ)
          ((starRingEnd 𝕜 : (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 : 𝕜) → ℝ)
          z :
        ℝ)

Tactic:
h.conj_re_ax

Premises used: RCLike.conj_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 : 𝕜),
    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 : 𝕜) → ℝ)
          ((starRingEnd 𝕜 : (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 : 𝕜) → ℝ)
          z :
        ℝ)

Tactic:
exact h.conj_re_ax

Premises used: RCLike.conj_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 :
  ∀ (z : 𝕜),
    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 : 𝕜) → ℝ)
          ((starRingEnd 𝕜 : (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 : 𝕜) → ℝ)
            z :
        ℝ)
⊢ ∀ (z : 𝕜),
    Eq (α := ℝ)
      (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                let __spread.0 := hk;
                𝕜 →+ ℝ)
                (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                im)
                ⋯ :
              let __spread.0 := hk;
              𝕜 →+ ℝ) :
            (a : 𝕜) → ℝ)
          ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) :
        ℝ)
      (-((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                  let __spread.0 := hk;
                  𝕜 →+ ℝ)
                  (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  im)
                  ⋯ :
                let __spread.0 := hk;
                𝕜 →+ ℝ) :
              (a : 𝕜) → ℝ)
            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 : 𝕜),
    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 : 𝕜) → ℝ)
          ((starRingEnd 𝕜 : (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 : 𝕜) → ℝ)
            z :
        ℝ)

Tactic:
h.conj_im_ax

Premises used: RCLike.conj_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 : 𝕜),
    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 : 𝕜) → ℝ)
          ((starRingEnd 𝕜 : (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 : 𝕜) → ℝ)
            z :
        ℝ)

Tactic:
exact h.conj_im_ax

Premises used: RCLike.conj_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 : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) I : 𝕜) (-I : 𝕜)
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) I : 𝕜) (-I : 𝕜)

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 (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) I : 𝕜) (-I : 𝕜)

Tactic:
h.conj_I_ax

Premises used: RCLike.conj_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 (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) I : 𝕜) (-I : 𝕜)

Tactic:
exact h.conj_I_ax

Premises used: RCLike.conj_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
⊢ ∀ (z : 𝕜),
    HPow.hPow (β := ℕ) ‖z‖ 2 =
      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 : 𝕜) → ℝ)
              z :
            ℝ) +
        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 : 𝕜) → ℝ)
              z :
            ℝ)

Tactic:
h.norm_sq_eq_def_ax

Premises used: RCLike.norm_sq_eq_def_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 : 𝕜),
    HPow.hPow (β := ℕ) ‖z‖ 2 =
      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 : 𝕜) → ℝ)
              z :
            ℝ) +
        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 : 𝕜) → ℝ)
              z :
            ℝ)

Tactic:
exact h.norm_sq_eq_def_ax

Premises used: RCLike.norm_sq_eq_def_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 : 𝕜),
    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 : 𝕜) → ℝ)
            I :
          ℝ) =
      ((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
⊢ ∀ (z : 𝕜),
    HMul.hMul (α := ℝ) (β := ℝ)
        (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                  let __spread.0 := hk;
                  𝕜 →+ ℝ)
                  (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  im)
                  ⋯ :
                let __spread.0 := hk;
                𝕜 →+ ℝ) :
              (a : 𝕜) → ℝ)
            z :
          ℝ)
        (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                  let __spread.0 := hk;
                  𝕜 →+ ℝ)
                  (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  im)
                  ⋯ :
                let __spread.0 := hk;
                𝕜 →+ ℝ) :
              (a : 𝕜) → ℝ)
            I :
          ℝ) =
      ((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              im)
              ⋯ :
            let __spread.0 := hk;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        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 : 𝕜),
    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 : 𝕜) → ℝ)
            I :
          ℝ) =
      ((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

Tactic:
h.mul_im_I_ax

Premises used: RCLike.mul_im_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
⊢ ∀ (z : 𝕜),
    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 : 𝕜) → ℝ)
            I :
          ℝ) =
      ((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

Tactic:
exact h.mul_im_I_ax

Premises used: RCLike.mul_im_I_ax