awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup Fₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
inst_7 : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f_1 g : E →SL[σ₁₂] F
E' : Type u_6
inst_8 : SeminormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
inst_10 : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf :
  Membership.mem (γ := Set ((a : E') → F)) (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' s)) f
⊢ Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (range (ι := E' →ₛₗ[σ₁₂] F) (DFunLike.coe (β := fun (x : E') ↦ F)))) f
have refine_1 : ∀ g ∈ s,
  Membership.mem (γ := Set (E' →SL[σ₁₂] F))
    (preimage (β := E' → F) (DFunLike.coe (β := fun (x : E') ↦ F))
      (range (ι := E' →ₛₗ[σ₁₂] F) (DFunLike.coe (β := fun (x : E') ↦ F))))
    g
Tactic: refine closure_mono (image_subset_iff.2 fun g _ => ?_) hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup Fₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
inst_7 : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f_1 g : E →SL[σ₁₂] F
E' : Type u_6
inst_8 : SeminormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
inst_10 : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf :
  Membership.mem (γ := Set ((a : E') → F)) (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' s)) f
⊢ ∃ (C : ℝ), ∀ (x : E'), Norm.norm.{u_4} (E := F) ((linearMapOfMemClosureRangeCoe f ⋯ : (a : E') → F) x : F) ≤ C * ‖x‖
have refine_2 : ∀ (C : ℝ) (hC : ∀ x ∈ s, ‖x‖ ≤ C),
  ∃ (C : ℝ), ∀ (x : E'), Norm.norm.{u_4} (E := F) ((linearMapOfMemClosureRangeCoe f sorry : (a : E') → F) x : F) ≤ C * ‖x‖
Tactic: rcases isBounded_iff_forall_norm_le.1 hs with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup Fₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
inst_7 : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f_1 g : E →SL[σ₁₂] F
E' : Type u_6
inst_8 : SeminormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
inst_10 : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf :
  Membership.mem (γ := Set ((a : E') → F)) (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' s)) f
C : ℝ
hC : ∀ x ∈ s, ‖x‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (x : E'), Norm.norm.{u_4} (E := F) ((linearMapOfMemClosureRangeCoe f ⋯ : (a : E') → F) x : F) ≤ C * ‖x‖
have this : ∀ (x : E'), IsClosed[Pi.topologicalSpace] {g : E' → F | ‖g x‖ ≤ C * ‖x‖}
Tactic: have : ∀ x, IsClosed { g : E' → F | ‖g x‖ ≤ C * ‖x‖ } := fun x =>
      isClosed_Iic.preimage (@continuous_apply E' (fun _ => F) _ x).norm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup Fₗ
inst_3 : NontriviallyNormedField 𝕜
inst_4 : NontriviallyNormedField 𝕜₂
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
inst_7 : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f_1 g : E →SL[σ₁₂] F
E' : Type u_6
inst_8 : SeminormedAddCommGroup E'
inst_9 : NormedSpace 𝕜 E'
inst_10 : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf :
  Membership.mem (γ := Set ((a : E') → F)) (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' s)) f
C : ℝ
hC : ∀ x ∈ s, ‖x‖ ≤ C
this : ∀ (x : E'), IsClosed[Pi.topologicalSpace] {g : E' → F | ‖g x‖ ≤ C * ‖x‖}
⊢ ∃ (C : ℝ), ∀ (x : E'), Norm.norm.{u_4} (E := F) ((linearMapOfMemClosureRangeCoe f ⋯ : (a : E') → F) x : F) ≤ C * ‖x‖
have refine_2 : ∀ (x : E') (g : E' →SL[σ₁₂] F) (hg : g ∈ s),
  Membership.mem (γ := Set (E' →SL[σ₁₂] F))
    (preimage (β := E' → F) (DFunLike.coe (β := fun (x : E') ↦ F)) {g : E' → F | ‖g x‖ ≤ C * ‖x‖}) g
Tactic: refine ⟨C, fun x => (this x).closure_subset_iff.2 (image_subset_iff.2 fun g hg => ?_) hf⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
⊢ Tendsto f atTop (𝓝 g)
have rcases : ∀ (b : ℕ → ℝ) (hb₀ : ∀ (n : ℕ), 0 ≤ b n) (hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N)
  (hb_lim : Tendsto b atTop (𝓝 0)), Tendsto f atTop (𝓝 g)
Tactic: rcases cauchySeq_iff_le_tendsto_0.1 hf with ⟨b, hb₀, hfb, hb_lim⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
hb_lim : Tendsto b atTop (𝓝 0)
⊢ Tendsto f atTop (𝓝 g)
have hfb₁ : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
Tactic: simp_rw [dist_eq_norm] at hfb
Cleared hypotheses: hfb
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
⊢ Tendsto f atTop (𝓝 g)
have suffices : ∀ (n : ℕ) (x : E'), ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖ ≤ b n * ‖x‖
Tactic: suffices ∀ n x, ‖f n x - g x‖ ≤ b n * ‖x‖ from
    tendsto_iff_norm_sub_tendsto_zero.2
    (squeeze_zero (fun n => norm_nonneg _) (fun n => opNorm_le_bound _ (hb₀ n) (this n)) hb_lim)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
n : ℕ
x : E'
⊢ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖ ≤ b n * ‖x‖
have this : Tendsto (fun (m : ℕ) ↦ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((f m : (a : E') → F) x : F)‖) atTop
  (𝓝 ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖)
Tactic: have : Tendsto (fun m => ‖f n x - f m x‖) atTop (𝓝 ‖f n x - g x‖) :=
    (tendsto_const_nhds.sub <| tendsto_pi_nhds.1 hg _).norm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f : ℕ → E' →SL[σ₁₂] F
g : E' →SL[σ₁₂] F
hg : Tendsto (β := (x : E') → F) (fun (n : ℕ) (x : E') ↦ (f n : (a : E') → F) x) atTop (𝓝 (⇑g : (a : E') → F))
hf : CauchySeq f
b : ℕ → ℝ
hb₀ : ∀ (n : ℕ), 0 ≤ b n
hb_lim : Tendsto b atTop (𝓝 0)
hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → ‖f n - f m‖ ≤ b N
n : ℕ
x : E'
this :
  Tendsto (fun (m : ℕ) ↦ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((f m : (a : E') → F) x : F)‖) atTop
    (𝓝 ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖)
⊢ ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((g : (a : E') → F) x : F)‖ ≤ b n * ‖x‖
have refine : ∀ (m : ℕ) (hm : m ≥ n),
  ‖HSub.hSub (α := F) (β := F) ((f n : (a : E') → F) x : F) ((f m : (a : E') → F) x : F)‖ ≤ b n * ‖x‖
Tactic: refine le_of_tendsto this (eventually_atTop.2 ⟨n, fun m hm => ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' closedBall f₀ r)) (⇑f : (a : E') → F)
⊢ f ∈ closedBall f₀ r
have hr : 0 ≤ r
Tactic: have hr : 0 ≤ r := nonempty_closedBall.1 (closure_nonempty_iff.1 ⟨_, hf⟩).of_image
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' closedBall f₀ r)) (⇑f : (a : E') → F)
hr : 0 ≤ r
⊢ f ∈ closedBall f₀ r
have refine : ∀ (x : E'), Norm.norm.{u_4} (E := F) ((f - f₀ : (a : E') → F) x : F) ≤ r * ‖x‖
Tactic: refine mem_closedBall_iff_norm.2 (opNorm_le_bound _ hr fun x => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' closedBall f₀ r)) (⇑f : (a : E') → F)
hr : 0 ≤ r
x : E'
⊢ Norm.norm.{u_4} (E := F) ((f - f₀ : (a : E') → F) x : F) ≤ r * ‖x‖
have this : IsClosed[Pi.topologicalSpace] {g : E' → F | ‖HSub.hSub (β := F) (g x) ((f₀ : (a : E') → F) x : F)‖ ≤ r * ‖x‖}
Tactic: have : IsClosed { g : E' → F | ‖g x - f₀ x‖ ≤ r * ‖x‖ } :=
    isClosed_Iic.preimage ((@continuous_apply E' (fun _ => F) _ x).sub continuous_const).norm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Completeness (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NontriviallyNormedField 𝕜
inst_2 : NontriviallyNormedField 𝕜₂
inst_3 : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
E' : Type u_6
inst_4 : SeminormedAddCommGroup E'
inst_5 : NormedSpace 𝕜 E'
inst_6 : RingHomIsometric σ₁₂
f₀ : E' →SL[σ₁₂] F
r : ℝ
f : E' →SL[σ₁₂] F
hf :
  Membership.mem (γ := Set ((a : E') → F))
    (closure[Pi.topologicalSpace] (DFunLike.coe (β := fun (x : E') ↦ F) '' closedBall f₀ r)) (⇑f : (a : E') → F)
hr : 0 ≤ r
x : E'
this : IsClosed[Pi.topologicalSpace] {g : E' → F | ‖HSub.hSub (β := F) (g x) ((f₀ : (a : E') → F) x : F)‖ ≤ r * ‖x‖}
⊢ Norm.norm.{u_4} (E := F) ((f - f₀ : (a : E') → F) x : F) ≤ r * ‖x‖
have refine : ∀ (g : E' →SL[σ₁₂] F) (hg : g ∈ closedBall f₀ r),
  Membership.mem (γ := Set (E' →SL[σ₁₂] F))
    (preimage (β := E' → F) (DFunLike.coe (β := fun (x : E') ↦ F))
      {g : E' → F | ‖HSub.hSub (β := F) (g x) ((f₀ : (a : E') → F) x : F)‖ ≤ r * ‖x‖})
    g
Tactic: refine this.closure_subset_iff.2 (image_subset_iff.2 fun g hg => ?_) hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Conformal (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : NormedSpace R M
inst_4 : NormedSpace R N
f : M →L[R] N
hf : IsConformalMap f
c : R
hc : c ≠ 0
⊢ IsConformalMap (c • f)
have rcases : ∀ (c' : R) (hc' : c' ≠ 0) (li : M →ₗᵢ[R] N), IsConformalMap (c • c' • li.toContinuousLinearMap)
Tactic: rcases hf with ⟨c', hc', li, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Conformal (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace R M
inst_5 : NormedSpace R N
inst_6 : NormedSpace R G
f : M →L[R] N
g : N →L[R] G
hg : IsConformalMap g
hf : IsConformalMap f
⊢ IsConformalMap (g ∘SL f)
have rcases : ∀ (cf : R) (hcf : cf ≠ 0) (lif : M →ₗᵢ[R] N), IsConformalMap (g ∘SL (cf • lif.toContinuousLinearMap))
Tactic: rcases hf with ⟨cf, hcf, lif, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Conformal (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace R M
inst_5 : NormedSpace R N
inst_6 : NormedSpace R G
g : N →L[R] G
hg : IsConformalMap g
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
⊢ IsConformalMap (g ∘SL (cf • lif.toContinuousLinearMap))
have rcases : ∀ (cg : R) (hcg : cg ≠ 0) (lig : N →ₗᵢ[R] G),
  IsConformalMap ((cg • lig.toContinuousLinearMap) ∘SL (cf • lif.toContinuousLinearMap))
Tactic: rcases hg with ⟨cg, hcg, lig, rfl⟩
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Conformal (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace R M
inst_5 : NormedSpace R N
inst_6 : NormedSpace R G
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ IsConformalMap ((cg • lig.toContinuousLinearMap) ∘SL (cf • lif.toContinuousLinearMap))
have refine : (cg • lig.toContinuousLinearMap) ∘SL (cf • lif.toContinuousLinearMap) = (cg * cf) • (lig.comp lif).toContinuousLinearMap
Tactic: refine ⟨cg * cf, mul_ne_zero hcg hcf, lig.comp lif, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Conformal (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace R M
inst_5 : NormedSpace R N
inst_6 : NormedSpace R G
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ (cg • lig.toContinuousLinearMap) ∘SL (cf • lif.toContinuousLinearMap) =
    (cg * cf) • (lig.comp lif).toContinuousLinearMap
have rw : cg • cf • lig.toContinuousLinearMap ∘SL lif.toContinuousLinearMap = cg • cf • (lig.comp lif).toContinuousLinearMap
Tactic: rw [smul_comp, comp_smul, mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Conformal (goal)
Goal:
R : Type u_1
N : Type u_3
M' : Type u_5
inst : NormedField R
inst_1 : SeminormedAddCommGroup N
inst_2 : NormedSpace R N
inst_3 : NormedAddCommGroup M'
inst_4 : NormedSpace R M'
f : M' →L[R] N
h : IsConformalMap f
⊢ Injective.{u_5 + 1, u_3 + 1} (α := M') (β := N) (⇑f : (a : M') → N)
have rcases : ∀ (c : R) (hc : c ≠ 0) (li : M' →ₗᵢ[R] N),
  Injective.{u_5 + 1, u_3 + 1} (α := M') (β := N) (⇑(c • li.toContinuousLinearMap) : (a : M') → N)
Tactic: rcases h with ⟨c, hc, li, rfl⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Conformal (goal)
Goal:
R : Type u_1
N : Type u_3
M' : Type u_5
inst : NormedField R
inst_1 : SeminormedAddCommGroup N
inst_2 : NormedSpace R N
inst_3 : NormedAddCommGroup M'
inst_4 : NormedSpace R M'
inst_5 : Nontrivial M'
hf' : IsConformalMap.{u_1, u_5, u_3} (R := R) (X := M') (Y := N) 0
⊢ False
have rcases : ∀ (a : M') (ha : a ≠ 0), False
Tactic: rcases exists_ne (0 : M') with ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
⊢ ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
have pos : ∀ (hV : Subsingleton V), ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
Tactic: by_cases! hV : Subsingleton V
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
pos : ∀ (hV : Subsingleton V), ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
⊢ ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
have neg : ∀ (hV : Nontrivial V), ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
Tactic: by_cases! hV : Subsingleton V
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Subsingleton V
⊢ ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
have pos : ∀ (hV : Subsingleton W), ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
Tactic: by_cases! hV : Subsingleton W
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Subsingleton V
pos : ∀ (hV : Subsingleton W), ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
⊢ ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
have neg : ∀ (hV : Nontrivial W), ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
Tactic: by_cases! hV : Subsingleton W
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
⊢ ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
have neg : ∃ (U : V ≃L[𝕜] W),
  ∀ (x : V →L[𝕜] V),
    comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
Tactic: simp_rw [ContinuousAlgEquiv.ext_iff, funext_iff, conjContinuousAlgEquiv_apply, ← comp_assoc,
    eq_comp_toContinuousLinearMap_symm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
⊢ ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
have neg : ∀ (u : V) (hu : u ≠ 0),
  ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
Tactic: obtain ⟨u, hu⟩ := exists_ne (0 : V)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
⊢ ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
have neg : ∀ (v : StrongDual 𝕜 V) (huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)),
  ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
Tactic: obtain ⟨v, huv⟩ := SeparatingDual.exists_ne_zero (R := 𝕜) hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
⊢ ∃ (z : W),
    ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
        ((0 : (a : W) → W) z : W)
have simp_rw : ∃ (x : V), ¬Eq.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) x : 𝕜) (0 : 𝕜)
Tactic: simp_rw [← not_forall, ← ContinuousLinearMap.ext_iff, map_eq_zero_iff,
      ContinuousLinearMap.ext_iff, not_forall, smulRight_apply, zero_apply,
      smul_eq_zero_iff_left hu]