awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1
⊢ 0 < ‖c‖ / r

Tactic:
have hcr : 0 < ‖c‖ / r := div_pos (zero_lt_one.trans hc) hr
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1
hcr : 0 < ‖c‖ / r
⊢ ‖x'‖ ≤ ‖c‖ / r

Tactic:
ContinuousLinearMap.opNorm_le_of_shell hr hcr.le hc fun x h₁ h₂ => ?_

Premises used: LT.lt.le, ContinuousLinearMap.opNorm_le_of_shell
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1
hcr : 0 < ‖c‖ / r
refine : ∀ (x : E) (h₁ : r / ‖c‖ ≤ ‖x‖) (h₂ : ‖x‖ < r), norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) x : 𝕜) ≤ ‖c‖ / r * ‖x‖
⊢ ‖x'‖ ≤ ‖c‖ / r

Tactic:
refine ContinuousLinearMap.opNorm_le_of_shell hr hcr.le hc fun x h₁ h₂ => ?_

Premises used: LT.lt.le, ContinuousLinearMap.opNorm_le_of_shell
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1
hcr : 0 < ‖c‖ / r
x : E
h₁ : r / ‖c‖ ≤ ‖x‖
h₂ : ‖x‖ < r
⊢ norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) x : 𝕜) ≤ 1

Tactic:
hx' _ h₂
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1
hcr : 0 < ‖c‖ / r
x : E
h₁ : r / ‖c‖ ≤ ‖x‖
h₂ : ‖x‖ < r
rwa rwa₁ rwa₂ rwa₃ : r / ‖c‖ ≤ ‖x‖
⊢ (‖c‖ / r)⁻¹ ≤ ‖x‖

Tactic:
rwa [inv_div]

Premises used: inv_div
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1
hcr : 0 < ‖c‖ / r
x : E
h₁ : r / ‖c‖ ≤ ‖x‖
h₂ : ‖x‖ < r
⊢ norm.{u_1} (E := 𝕜) ((x' : (a : E) → 𝕜) x : 𝕜) ≤ ‖c‖ / r * ‖x‖

Tactic:
calc
    ‖x' x‖ ≤ 1 := hx' _ h₂
    _ ≤ ‖c‖ / r * ‖x‖ := (inv_le_iff_one_le_mul₀' hcr).1 (by rwa [inv_div])

Premises used: inv_le_iff_one_le_mul₀', Iff.mp, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
⊢ Subset (α := Set (StrongDual 𝕜 E)) (closedBall 0 r⁻¹ : Set (StrongDual 𝕜 E))
    (polar 𝕜 (closedBall 0 r) : Set (StrongDual 𝕜 E))

Tactic:
fun x' hx' x hx =>
  calc
    ‖x' x‖ ≤ ‖x'‖ * ‖x‖ := x'.le_opNorm x
    _ ≤ r⁻¹ * r :=
      (mul_le_mul (mem_closedBall_zero_iff.1 hx') (mem_closedBall_zero_iff.1 hx) (norm_nonneg _)
        (dist_nonneg.trans hx'))
    _ = r / r := inv_mul_eq_div _ _
    _ ≤ 1 := div_self_le_one r

Premises used: Trans.trans, Set.Mem, ContinuousLinearMap.le_opNorm, setOf, dist_nonneg, inv_mul_eq_div, StrongDual.polar, LinearMap.polar, div_self_le_one, Set.Subset, mul_le_mul, Iff.mp, LE.le.trans, mem_closedBall_zero_iff, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (closedBall 0 r)) (closedBall 0 r⁻¹)

Tactic:
Subset.antisymm ?_ (closedBall_inv_subset_polar_closedBall 𝕜)

Premises used: Set.Subset.antisymm, NormedSpace.closedBall_inv_subset_polar_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
refine : Subset (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (closedBall 0 r)) (closedBall 0 r⁻¹)
⊢ Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (closedBall 0 r)) (closedBall 0 r⁻¹)

Tactic:
refine Subset.antisymm ?_ (closedBall_inv_subset_polar_closedBall 𝕜)

Premises used: Set.Subset.antisymm, NormedSpace.closedBall_inv_subset_polar_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
h : Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 (closedBall 0 r)) x'
simp : ‖x'‖ ≤ r⁻¹
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (closedBall 0 r⁻¹) x'

Tactic:
simp only [mem_closedBall_zero_iff]

Premises used: mem_closedBall_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
h : Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 (closedBall 0 r)) x'
⊢ ‖x'‖ ≤ r⁻¹

Tactic:
ContinuousLinearMap.opNorm_le_of_ball hr (inv_nonneg.mpr hr.le) fun z _ => ?_

Premises used: Iff.mpr, LT.lt.le, ContinuousLinearMap.opNorm_le_of_ball, inv_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
h : Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 (closedBall 0 r)) x'
refine :
  ∀ (z : E), Membership.mem (γ := Set E) (ball 0 r) z → norm.{u_3} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ r⁻¹ * ‖z‖
⊢ ‖x'‖ ≤ r⁻¹

Tactic:
refine ContinuousLinearMap.opNorm_le_of_ball hr (inv_nonneg.mpr hr.le) fun z _ => ?_

Premises used: Iff.mpr, LT.lt.le, ContinuousLinearMap.opNorm_le_of_ball, inv_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : StrongDual 𝕜 E
h : Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 (closedBall 0 r)) x'
z : E
h_1 : Membership.mem (γ := Set E) (ball 0 r) z
⊢ norm.{u_3} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ r⁻¹ * ‖z‖

Tactic:
simpa only [one_div] using LinearMap.bound_of_ball_bound' hr 1 x'.toLinearMap h z

Premises used: ContinuousLinearMap.toLinearMap, LinearMap.bound_of_ball_bound', one_div, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
this : NormedSpace ℝ E := restrictScalars ℝ 𝕜 E
rw : Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r)) (polar 𝕜 (closedBall 0 r))
rw₁ :
  Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r))
    (polar 𝕜 (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 r)))
rw₂ rw₃ : Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r)) (polar 𝕜 (ball 0 r))
⊢ Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 (ball 0 r)) (closedBall 0 r⁻¹)

Tactic:
rw [← polar_closedBall hr, ← closure_ball _ hr.ne', polar_closure]

Premises used: NormedSpace.polar_closure, LT.lt.ne', closure_ball, NormedSpace.polar_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
s_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ ∃ (a : 𝕜), 1 < ‖a‖

Tactic:
NormedField.exists_one_lt_norm 𝕜

Premises used: NormedField.exists_one_lt_norm
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
s_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
obtain : ∀ (a : 𝕜) (ha : 1 < ‖a‖), IsBounded (α := StrongDual 𝕜 E) (polar 𝕜 s)
⊢ IsBounded (α := StrongDual 𝕜 E) (polar 𝕜 s)

Tactic:
obtain ⟨a, ha⟩ : ∃ a : 𝕜, 1 < ‖a‖ := NormedField.exists_one_lt_norm 𝕜

Premises used: NormedField.exists_one_lt_norm
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
s_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
a : 𝕜
ha : 1 < ‖a‖
⊢ ∃ (r : ℝ), 0 < r ∧ ball 0 r ⊆ s

Tactic:
Metric.mem_nhds_iff.1 s_nhds

Premises used: Metric.mem_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
s_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
a : 𝕜
ha : 1 < ‖a‖
obtain : ∀ (r : ℝ) (r_pos : 0 < r) (r_ball : ball 0 r ⊆ s), IsBounded (α := StrongDual 𝕜 E) (polar 𝕜 s)
⊢ IsBounded (α := StrongDual 𝕜 E) (polar 𝕜 s)

Tactic:
obtain ⟨r, r_pos, r_ball⟩ : ∃ r : ℝ, 0 < r ∧ ball 0 r ⊆ s := Metric.mem_nhds_iff.1 s_nhds

Premises used: Metric.mem_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
s_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
a : 𝕜
ha : 1 < ‖a‖
r : ℝ
r_pos : 0 < r
r_ball : ball 0 r ⊆ s
⊢ IsBounded (α := StrongDual 𝕜 E) (polar 𝕜 s)

Tactic:
isBounded_closedBall.subset
    (((topDualPairing 𝕜 E).flip.polar_antitone r_ball).trans <|
      polar_ball_subset_closedBall_div ha r_pos)

Premises used: Metric.isBounded_closedBall, LinearMap.polar_antitone, NormedSpace.polar_ball_subset_closedBall_div, topDualPairing, Bornology.IsBounded.subset, LinearMap.flip, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
s_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
a : 𝕜
ha : 1 < ‖a‖
r : ℝ
r_pos : 0 < r
r_ball : ball 0 r ⊆ s
⊢ IsBounded (α := StrongDual 𝕜 E) (polar 𝕜 s)

Tactic:
exact isBounded_closedBall.subset
    (((topDualPairing 𝕜 E).flip.polar_antitone r_ball).trans <|
      polar_ball_subset_closedBall_div ha r_pos)

Premises used: Metric.isBounded_closedBall, LinearMap.polar_antitone, NormedSpace.polar_ball_subset_closedBall_div, topDualPairing, Bornology.IsBounded.subset, LinearMap.flip, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
rw : closedBall 0 r⁻¹⁻¹
| closedBall 0 r

Tactic:
rw [← inv_inv r]

Premises used: inv_inv
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
conv_rhs :
  Eq (α := Set (StrongDual 𝕜 E)) (⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹})) (closedBall 0 r⁻¹⁻¹)
⊢ Eq (α := Set (StrongDual 𝕜 E)) (⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹})) (closedBall 0 r)

Tactic:
conv_rhs => rw [← inv_inv r]

Premises used: inv_inv
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
rw :
  Eq (α := Set (StrongDual 𝕜 E)) (⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}))
    (polar 𝕜 (closedBall 0 r⁻¹))
rw₁ :
  Eq (α := Set (StrongDual 𝕜 E))
    (⋂₀ (LinearMap.polar (LinearMap.flip (topDualPairing 𝕜 E)) '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}))
    (LinearMap.polar (LinearMap.flip (topDualPairing 𝕜 E)) (closedBall 0 r⁻¹))
rw₂ rw₃ :
  Eq (α := Set (StrongDual 𝕜 E))
    (LinearMap.polar (𝕜 := 𝕜) (E := E) (LinearMap.flip (topDualPairing 𝕜 E)) (closedBall 0 r⁻¹))
    (LinearMap.polar (LinearMap.flip (topDualPairing 𝕜 E)) (closedBall 0 r⁻¹))
⊢ Eq (α := Set (StrongDual 𝕜 E)) (⋂₀ (polar 𝕜 '' {F : Set E | F.Finite ∧ F ⊆ closedBall 0 r⁻¹})) (closedBall 0 r⁻¹⁻¹)

Tactic:
rw [← polar_closedBall (inv_pos_of_pos hr), StrongDual.polar,
    (topDualPairing 𝕜 E).flip.sInter_polar_finite_subset_eq_polar (closedBall (0 : E) r⁻¹)]

Premises used: StrongDual.polar, inv_pos_of_pos, LinearMap.sInter_polar_finite_subset_eq_polar, topDualPairing, Inv.inv, LinearMap.flip, Metric.closedBall, NormedSpace.polar_closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
rw :
  AbsConvex.{u_1, u_3} 𝕜 (E := F)
    (⋂ x ∈ s,
      Set.preimage.{u_3, u_1} (β := 𝕜) (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜)
        (Metric.closedBall 0 1))
⊢ AbsConvex.{u_1, u_3} 𝕜 (E := F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B s)

Tactic:
rw [polar_eq_biInter_preimage]

Premises used: LinearMap.polar_eq_biInter_preimage
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ AbsConvex.{u_1, u_3} 𝕜 (E := F)
    (⋂ x ∈ s,
      Set.preimage.{u_3, u_1} (β := 𝕜) (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜)
        (Metric.closedBall 0 1))

Tactic:
AbsConvex.iInter₂ fun i hi =>
    ⟨balanced_closedBall_zero.mulActionHom_preimage (f := (B i : (F →ₑ[(RingHom.id 𝕜)] 𝕜))),
      (convex_RCLike_iff_convex_real.mpr (convex_closedBall 0 1)).linear_preimage _⟩

Premises used: Iff.mpr, convex_RCLike_iff_convex_real, MulActionSemiHomClass.toMulActionHom, AbsConvex.iInter₂, And.intro, balanced_closedBall_zero, Balanced.mulActionHom_preimage, OfNat.ofNat, DFunLike.coe, convex_closedBall, Convex.linear_preimage
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ AbsConvex.{u_1, u_3} 𝕜 (E := F)
    (⋂ x ∈ s,
      Set.preimage.{u_3, u_1} (β := 𝕜) (⇑((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜)
        (Metric.closedBall 0 1))

Tactic:
exact AbsConvex.iInter₂ fun i hi =>
    ⟨balanced_closedBall_zero.mulActionHom_preimage (f := (B i : (F →ₑ[(RingHom.id 𝕜)] 𝕜))),
      (convex_RCLike_iff_convex_real.mpr (convex_closedBall 0 1)).linear_preimage _⟩

Premises used: Iff.mpr, convex_RCLike_iff_convex_real, MulActionSemiHomClass.toMulActionHom, AbsConvex.iInter₂, And.intro, balanced_closedBall_zero, Balanced.mulActionHom_preimage, OfNat.ofNat, DFunLike.coe, convex_closedBall, Convex.linear_preimage
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : ∀ (f : StrongDual 𝕜 E), Eq.{u_1 + 1} (α := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ x = 0

Tactic:
SeparatingDual.eq_zero_of_forall_dual_eq_zero h

Premises used: SeparatingDual.eq_zero_of_forall_dual_eq_zero
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ x = 0 ↔ ∀ (g : StrongDual 𝕜 E), Eq.{u_1 + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
SeparatingDual.eq_zero_iff_forall_dual_eq_zero x

Premises used: SeparatingDual.eq_zero_iff_forall_dual_eq_zero
-- Module: Mathlib.Analysis.Normed.Module.Dual
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
⊢ x = y ↔ ∀ (g : StrongDual 𝕜 E), Eq.{u_1 + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((g : (a : E) → 𝕜) y : 𝕜)

Tactic:
SeparatingDual.eq_iff_forall_dual_eq

Premises used: SeparatingDual.eq_iff_forall_dual_eq
-- Module: Mathlib.Analysis.Normed.Module.Extr
Goal:
α : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
l : Filter α
c : α
y : E
h : IsMaxFilter (norm ∘ f) l c
hy : SameRay ℝ (f c) y
x : α
hx : ‖f x‖ ≤ ‖f c‖
grw : ‖f x + y‖ ≤ ‖f c‖ + ‖y‖
grw₁ : ‖f x‖ + ‖y‖ ≤ ‖f c‖ + ‖y‖
grw₂ grw₃ : ‖f c‖ + ‖y‖ ≤ ‖f c‖ + ‖y‖
⊢ ‖f x + y‖ ≤ ‖f c + y‖

Tactic:
grw [hy.norm_add, norm_add_le, hx]

Premises used: norm_add_le, SameRay.norm_add
-- Module: Mathlib.Analysis.Normed.Module.Extr
Goal:
α : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
l : Filter α
c : α
h : IsMaxFilter (norm ∘ f) l c
⊢ IsMaxFilter (β := ℝ) (fun (x : α) ↦ ‖f x + f c‖) l c

Tactic:
IsMaxFilter.norm_add_sameRay h SameRay.rfl

Premises used: SameRay.rfl, IsMaxFilter.norm_add_sameRay
-- Module: Mathlib.Analysis.Normed.Module.Extr
Goal:
α : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
s : Set α
c : α
y : E
h : IsMaxOn (norm ∘ f) s c
hy : SameRay ℝ (f c) y
⊢ IsMaxOn (β := ℝ) (fun (x : α) ↦ ‖f x + y‖) s c

Tactic:
IsMaxFilter.norm_add_sameRay h hy

Premises used: IsMaxOn, IsMaxFilter.norm_add_sameRay
-- Module: Mathlib.Analysis.Normed.Module.Extr
Goal:
α : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → E
s : Set α
c : α
h : IsMaxOn (norm ∘ f) s c
⊢ IsMaxOn (β := ℝ) (fun (x : α) ↦ ‖f x + f c‖) s c

Tactic:
IsMaxFilter.norm_add_self h

Premises used: IsMaxOn, IsMaxFilter.norm_add_self
-- Module: Mathlib.Analysis.Normed.Module.Extr
Goal:
X : Type u_2
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
f : X → E
s : Set X
c : X
y : E
h : IsLocalMaxOn (norm ∘ f) s c
hy : SameRay ℝ (f c) y
⊢ IsLocalMaxOn (β := ℝ) (fun (x : X) ↦ ‖f x + y‖) s c

Tactic:
IsMaxFilter.norm_add_sameRay h hy

Premises used: IsLocalMaxOn, IsMaxFilter.norm_add_sameRay
-- Module: Mathlib.Analysis.Normed.Module.Extr
Goal:
X : Type u_2
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
f : X → E
s : Set X
c : X
h : IsLocalMaxOn (norm ∘ f) s c
⊢ IsLocalMaxOn (β := ℝ) (fun (x : X) ↦ ‖f x + f c‖) s c

Tactic:
IsMaxFilter.norm_add_self h

Premises used: IsLocalMaxOn, IsMaxFilter.norm_add_self
-- Module: Mathlib.Analysis.Normed.Module.Extr
Goal:
X : Type u_2
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
f : X → E
c : X
y : E
h : IsLocalMax (norm ∘ f) c
hy : SameRay ℝ (f c) y
⊢ IsLocalMax (β := ℝ) (fun (x : X) ↦ ‖f x + y‖) c

Tactic:
IsMaxFilter.norm_add_sameRay h hy

Premises used: IsLocalMax, IsMaxFilter.norm_add_sameRay
-- Module: Mathlib.Analysis.Normed.Module.Extr
Goal:
X : Type u_2
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
f : X → E
c : X
h : IsLocalMax (norm ∘ f) c
⊢ IsLocalMax (β := ℝ) (fun (x : X) ↦ ‖f x + f c‖) c

Tactic:
IsMaxFilter.norm_add_self h

Premises used: IsLocalMax, IsMaxFilter.norm_add_self
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
F : Type u_1
E₁ : Type u_2
inst : SeminormedAddCommGroup F
inst_1 : NormedAddCommGroup E₁
R₁ : Type u_3
inst_2 : Field R₁
inst_3 : Module R₁ E₁
inst_4 : Module R₁ F
inst_5 : FiniteDimensional R₁ E₁
inst_6 : FiniteDimensional R₁ F
li : E₁ →ₗᵢ[R₁] F
h : finrank R₁ E₁ = finrank R₁ F
⊢ Eq (α := (a : E₁) → F) (⇑(li.toLinearIsometryEquiv h) : (a : E₁) → F) (⇑li : (a : E₁) → F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
F : Type u_1
E₁ : Type u_2
inst : SeminormedAddCommGroup F
inst_1 : NormedAddCommGroup E₁
R₁ : Type u_3
inst_2 : Field R₁
inst_3 : Module R₁ E₁
inst_4 : Module R₁ F
inst_5 : FiniteDimensional R₁ E₁
inst_6 : FiniteDimensional R₁ F
li : E₁ →ₗᵢ[R₁] F
h : finrank R₁ E₁ = finrank R₁ F
x : E₁
⊢ Eq.{u_1 + 1} (α := F) ((li.toLinearIsometryEquiv h : (a : E₁) → F) x : F) ((li : (a : E₁) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u_1
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : NormedSpace 𝕜 V₁
inst_4 : NormedSpace 𝕜 V₂
inst_5 : MetricSpace P₁
inst_6 : PseudoMetricSpace P₂
inst_7 : NormedAddTorsor V₁ P₁
inst_8 : NormedAddTorsor V₂ P₂
inst_9 : FiniteDimensional 𝕜 V₁
inst_10 : FiniteDimensional 𝕜 V₂
inst_11 : Inhabited P₁
li : P₁ →ᵃⁱ[𝕜] P₂
h : finrank 𝕜 V₁ = finrank 𝕜 V₂
p : P₁
⊢ (li : (a : P₁) → P₂) p =
    HVAdd.hVAdd.{u_3, u_5, u_5} (α := V₂) (β := P₂)
      ((li.linearIsometry.toLinearIsometryEquiv h : (a : V₁) → V₂) (p -ᵥ default) : V₂)
      ((li : (a : P₁) → P₂) default : P₂)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u_1
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : NormedSpace 𝕜 V₁
inst_4 : NormedSpace 𝕜 V₂
inst_5 : MetricSpace P₁
inst_6 : PseudoMetricSpace P₂
inst_7 : NormedAddTorsor V₁ P₁
inst_8 : NormedAddTorsor V₂ P₂
inst_9 : FiniteDimensional 𝕜 V₁
inst_10 : FiniteDimensional 𝕜 V₂
inst_11 : Inhabited P₁
li : P₁ →ᵃⁱ[𝕜] P₂
h : finrank 𝕜 V₁ = finrank 𝕜 V₂
⊢ Eq (α := (a : P₁) → P₂) (⇑(li.toAffineIsometryEquiv h) : (a : P₁) → P₂) (⇑li : (a : P₁) → P₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u_1
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : NormedSpace 𝕜 V₁
inst_4 : NormedSpace 𝕜 V₂
inst_5 : MetricSpace P₁
inst_6 : PseudoMetricSpace P₂
inst_7 : NormedAddTorsor V₁ P₁
inst_8 : NormedAddTorsor V₂ P₂
inst_9 : FiniteDimensional 𝕜 V₁
inst_10 : FiniteDimensional 𝕜 V₂
inst_11 : Inhabited P₁
li : P₁ →ᵃⁱ[𝕜] P₂
h : finrank 𝕜 V₁ = finrank 𝕜 V₂
x : P₁
⊢ Eq.{u_5 + 1} (α := P₂) ((li.toAffineIsometryEquiv h : (a : P₁) → P₂) x : P₂) ((li : (a : P₁) → P₂) x : P₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
PE : Type u_1
PF : Type u_2
inst_6 : MetricSpace PE
inst_7 : NormedAddTorsor E PE
inst_8 : MetricSpace PF
inst_9 : NormedAddTorsor F PF
inst_10 : FiniteDimensional 𝕜 E
f : PE →ᵃ[𝕜] PF
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : PE) → PF)

Tactic:
AffineMap.continuous_linear_iff.1 f.linear.continuous_of_finiteDimensional

Premises used: LinearMap.continuous_of_finiteDimensional, AffineMap.linear, Iff.mp, AffineMap.continuous_linear_iff
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
PE : Type u_1
PF : Type u_2
inst_6 : MetricSpace PE
inst_7 : NormedAddTorsor E PE
inst_8 : MetricSpace PF
inst_9 : NormedAddTorsor F PF
inst_10 : FiniteDimensional 𝕜 E
f : PE ≃ᵃ[𝕜] PF
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : PE) → PF)

Tactic:
f.toAffineMap.continuous_of_finiteDimensional

Premises used: AffineEquiv.toAffineMap, AffineMap.continuous_of_finiteDimensional
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
PE : Type u_1
PF : Type u_2
inst_6 : MetricSpace PE
inst_7 : NormedAddTorsor E PE
inst_8 : MetricSpace PF
inst_9 : NormedAddTorsor F PF
inst_10 : FiniteDimensional 𝕜 E
f : PE ≃ᵃ[𝕜] PF
⊢ Eq (α := (a : PE) → PF) (⇑f.toHomeomorphOfFiniteDimensional : (a : PE) → PF) (⇑f : (a : PE) → PF)

Tactic:
rfl

Premises used: rfl