awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
inr :
  {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ a • s} =
    HSMul.hSMul (β := Set ℝ) a⁻¹ {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s}
⊢ sInf {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ a • s} =
    sInf (HSMul.hSMul (β := Set ℝ) a⁻¹ {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s})

Tactic:
congr 1
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
inr :
  ∀ (r : ℝ),
    Membership.mem (γ := Set ℝ) {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ a • s} r ↔
      r ∈ HSMul.hSMul (β := Set ℝ) a⁻¹ {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s}
⊢ {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ a • s} =
    HSMul.hSMul (β := Set ℝ) a⁻¹ {r : ℝ | Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ r⁻¹ • x ∈ s}

Tactic:
ext r
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
inr :
  (Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ ∃ y ∈ s, a • y = r⁻¹ • x) →
    ∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r
inr₁ :
  (∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r) →
    Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ ∃ y ∈ s, a • y = r⁻¹ • x
⊢ (Membership.mem (γ := Set ℝ) (Ioi 0) r ∧ ∃ y ∈ s, a • y = r⁻¹ • x) ↔
    ∃ (y : ℝ), (Membership.mem (γ := Set ℝ) (Ioi 0) y ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
y : E
hy : y ∈ s
h : a • y = r⁻¹ • x
⊢ 0 < r

Tactic:
simp_rw [mem_Ioi] at hr ⊢

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
y : E
hy : y ∈ s
h : a • y = r⁻¹ • x
hr : 0 < r
⊢ ∃ (y : ℝ), (0 < y ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r

Tactic:
⟨a • r, ⟨smul_pos ha' hr, ?_⟩, inv_smul_smul₀ ha'.ne' _⟩

Premises used: inv_smul_smul₀, LT.lt.ne', And.intro, Exists.intro, HSMul.hSMul, smul_pos
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
y : E
hy : y ∈ s
h : a • y = r⁻¹ • x
hr : 0 < r
inr : (a • r)⁻¹ • x ∈ s
⊢ ∃ (y : ℝ), (0 < y ∧ y⁻¹ • x ∈ s) ∧ a⁻¹ • y = r

Tactic:
refine ⟨a • r, ⟨smul_pos ha' hr, ?_⟩, inv_smul_smul₀ ha'.ne' _⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
y : E
hy : y ∈ s
h : a • y = r⁻¹ • x
hr : 0 < r
inr : (a⁻¹ • r⁻¹) • x ∈ s
inr₁ : a⁻¹ • r⁻¹ • x ∈ s
inr₂ : a⁻¹ • a • y ∈ s
inr₃ inr₄ inr₅ inr₆ : y ∈ s
⊢ (a • r)⁻¹ • x ∈ s

Tactic:
rwa [smul_inv₀, smul_assoc, ← h, inv_smul_smul₀ ha'.ne']

Premises used: inv_smul_smul₀, smul_assoc, LT.lt.ne', smul_inv₀
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hx : r⁻¹ • x ∈ s
⊢ 0 < r

Tactic:
rw [mem_Ioi] at hr ⊢

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hx : r⁻¹ • x ∈ s
hr₁ : 0 < r
⊢ r⁻¹ • x ∈ s

Tactic:
rw [mem_Ioi] at hr ⊢

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : 0 < r
hx : r⁻¹ • x ∈ s
⊢ 0 < a⁻¹ • r ∧ ∃ y ∈ s, a • y = (a⁻¹ • r)⁻¹ • x

Tactic:
⟨smul_pos (inv_pos.2 ha') hr, r⁻¹ • x, hx, ?_⟩

Premises used: Iff.mpr, inv_pos, Inv.inv, And.intro, Exists.intro, HSMul.hSMul, smul_pos
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : 0 < r
hx : r⁻¹ • x ∈ s
inr : a • r⁻¹ • x = (a⁻¹ • r)⁻¹ • x
⊢ 0 < a⁻¹ • r ∧ ∃ y ∈ s, a • y = (a⁻¹ • r)⁻¹ • x

Tactic:
refine ⟨smul_pos (inv_pos.2 ha') hr, r⁻¹ • x, hx, ?_⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : 0 < r
hx : r⁻¹ • x ∈ s
inr : a • r⁻¹ • x = (a⁻¹⁻¹ • r⁻¹) • x
inr₁ : a • r⁻¹ • x = a⁻¹⁻¹ • r⁻¹ • x
inr₂ inr₃ : a • r⁻¹ • x = a • r⁻¹ • x
⊢ a • r⁻¹ • x = (a⁻¹ • r)⁻¹ • x

Tactic:
rw [smul_inv₀, smul_assoc, inv_inv]

Premises used: smul_assoc, inv_inv, smul_inv₀
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
rw : gauge (a • s) = gauge (|a| • s)
⊢ gauge (a • s) = |a|⁻¹ • gauge s

Tactic:
rw [← gauge_smul_left_of_nonneg (abs_nonneg a)]

Premises used: gauge_smul_left_of_nonneg, abs_nonneg
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
inl : ∀ (h : |a| = a), gauge (a • s) = gauge (|a| • s)
inr : ∀ (h : |a| = -a), gauge (a • s) = gauge (|a| • s)
⊢ gauge (a • s) = gauge (|a| • s)

Tactic:
obtain h | h := abs_choice a

Premises used: abs_choice
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = a
inl inl₁ : gauge (a • s) = gauge (a • s)
⊢ gauge (a • s) = gauge (|a| • s)

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
inr : gauge (a • s) = gauge (a • -s)
⊢ gauge (a • s) = gauge (|a| • s)

Tactic:
rw [h, Set.neg_smul_set, ← Set.smul_set_neg]

Premises used: Set.smul_set_neg, Set.neg_smul_set
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
inr : s = -s
⊢ gauge (a • s) = gauge (a • -s)

Tactic:
congr
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
inr : ∀ (y : E), y ∈ s ↔ y ∈ -s
⊢ s = -s

Tactic:
ext y
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
y : E
⊢ y ∈ s ↔ y ∈ -s

Tactic:
⟨symmetric _, fun hy => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
y : E
inr : ∀ (hy : y ∈ -s), y ∈ s
⊢ y ∈ s ↔ y ∈ -s

Tactic:
refine ⟨symmetric _, fun hy => ?_⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
y : E
hy : y ∈ -s
inr : - -y ∈ s
⊢ y ∈ s

Tactic:
rw [← neg_neg y]

Premises used: neg_neg
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
y : E
hy : y ∈ -s
⊢ - -y ∈ s

Tactic:
symmetric _ hy

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
y : E
hy : y ∈ -s
⊢ - -y ∈ s

Tactic:
exact symmetric _ hy
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
e_a : ∀ (θ : ℝ), 0 < θ ∧ ‖r‖ • x ∈ θ • s ↔ 0 < θ ∧ r • x ∈ θ • s
⊢ Eq (α := ℝ) (sInf {r_1 : ℝ | 0 < r_1 ∧ ‖r‖ • x ∈ r_1 • s}) (sInf {r_1 : ℝ | 0 < r_1 ∧ r • x ∈ r_1 • s})

Tactic:
congr with θ
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
e_a : 0 < θ ∧ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖r‖ : 𝕜) x ∈ θ • s ↔ 0 < θ ∧ r • x ∈ θ • s
⊢ 0 < θ ∧ ‖r‖ • x ∈ θ • s ↔ 0 < θ ∧ r • x ∈ θ • s

Tactic:
rw [@RCLike.real_smul_eq_coe_smul 𝕜]

Premises used: RCLike.real_smul_eq_coe_smul
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
⊢ 0 < θ ∧ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖r‖ : 𝕜) x ∈ θ • s ↔ 0 < θ ∧ r • x ∈ θ • s

Tactic:
and_congr_right fun hθ => (hs.smul _).smul_mem_iff ?_

Premises used: Balanced.smul_mem_iff, and_congr_right, Balanced.smul
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
e_a : ∀ (hθ : 0 < θ), norm.{u_1} (E := 𝕜) (↑‖r‖ : 𝕜) = ‖r‖
⊢ 0 < θ ∧ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖r‖ : 𝕜) x ∈ θ • s ↔ 0 < θ ∧ r • x ∈ θ • s

Tactic:
refine and_congr_right fun hθ => (hs.smul _).smul_mem_iff ?_

Premises used: Balanced.smul_mem_iff, and_congr_right, Balanced.smul
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
hθ : 0 < θ
e_a : |‖r‖| = ‖r‖
e_a₁ e_a₂ : ‖r‖ = ‖r‖
⊢ norm.{u_1} (E := 𝕜) (↑‖r‖ : 𝕜) = ‖r‖

Tactic:
rw [RCLike.norm_ofReal, abs_norm]

Premises used: RCLike.norm_ofReal, abs_norm
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
rw : gauge s (r • x) = ‖r‖ • gauge s x
rw₁ : gauge s (r • x) = gauge s (‖r‖ • x)
rw₂ rw₃ : gauge s (r • x) = gauge s (r • x)
⊢ gauge s (r • x) = ‖r‖ * gauge s x

Tactic:
rw [← smul_eq_mul, ← gauge_smul_of_nonneg (norm_nonneg r), gauge_norm_smul hs]

Premises used: gauge_smul_of_nonneg, gauge_norm_smul, smul_eq_mul, norm_nonneg
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
rcases : ∀ (r : ℝ) (hr₀ : r > 0) (hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u), u ∈ comap (gauge s) (𝓝 0)
⊢ u ∈ comap (gauge s) (𝓝 0)

Tactic:
rcases (hb hu).exists_pos with ⟨r, hr₀, hr⟩

Premises used: Absorbs.exists_pos
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
x : E
h : ∀ (hx : gauge s x < r⁻¹), x ∈ u
⊢ x ∈ gauge s ⁻¹' {x : ℝ | x < r⁻¹} → x ∈ u

Tactic:
(hx : gauge s x < r⁻¹)
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
h : ∀ (x : E) (hx : gauge s x < r⁻¹), x ∈ u
⊢ u ∈ comap (gauge s) (𝓝 0)

Tactic:
filter_upwards [preimage_mem_comap (gt_mem_nhds (inv_pos.2 hr₀))] with x (hx : gauge s x < r⁻¹)

Premises used: Iff.mpr, gt_mem_nhds, inv_pos, Filter.preimage_mem_comap
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
x : E
hx : gauge s x < r⁻¹
h :
  ∀ (c : ℝ) (hc₀ : 0 < c) (hcr : c < r⁻¹) (y : E) (hy : y ∈ s) (hx : gauge s ((fun (x : E) ↦ c • x) y) < r⁻¹),
    (fun (x : E) ↦ c • x) y ∈ u
⊢ x ∈ u

Tactic:
rcases exists_lt_of_gauge_lt ha hx with ⟨c, hc₀, hcr, y, hy, rfl⟩

Premises used: exists_lt_of_gauge_lt, rfl
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
y : E
hy : y ∈ s
hx : gauge s ((fun (x : E) ↦ c • x) y) < r⁻¹
⊢ r < c⁻¹

Tactic:
have hrc := (lt_inv_comm₀ hr₀ hc₀).2 hcr
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
y : E
hy : y ∈ s
hx : gauge s ((fun (x : E) ↦ c • x) y) < r⁻¹
hrc : r < c⁻¹
h :
  ∀ (z : E) (hz : z ∈ u) (hy : (fun (x : E) ↦ c⁻¹ • x) z ∈ s)
    (hx : gauge s ((fun (x : E) ↦ c • x) ((fun (x : E) ↦ c⁻¹ • x) z)) < r⁻¹),
    (fun (x : E) ↦ c • x) ((fun (x : E) ↦ c⁻¹ • x) z) ∈ u
⊢ (fun (x : E) ↦ c • x) y ∈ u

Tactic:
rcases hr c⁻¹ (hrc.le.trans (le_abs_self _)) hy with ⟨z, hz, rfl⟩

Premises used: le_abs_self, LT.lt.le, Inv.inv, LE.le.trans, rfl
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
hrc : r < c⁻¹
z : E
hz : z ∈ u
hy : (fun (x : E) ↦ c⁻¹ • x) z ∈ s
hx : gauge s ((fun (x : E) ↦ c • x) ((fun (x : E) ↦ c⁻¹ • x) z)) < r⁻¹
⊢ (fun (x : E) ↦ c • x) ((fun (x : E) ↦ c⁻¹ • x) z) ∈ u

Tactic:
simpa only [smul_inv_smul₀ hc₀.ne']

Premises used: smul_inv_smul₀, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
⊢ gauge s x = 0 ↔ x = 0

Tactic:
⟨fun h₀ ↦ by_contra fun (hne : x ≠ 0) ↦ ?_, fun h ↦ h.symm ▸ gauge_zero⟩

Premises used: Eq.rec, Iff.intro, by_contra, Eq.symm, gauge_zero
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
refine : ∀ (h₀ : gauge s x = 0) (hne : x ≠ 0), False
⊢ gauge s x = 0 ↔ x = 0

Tactic:
refine ⟨fun h₀ ↦ by_contra fun (hne : x ≠ 0) ↦ ?_, fun h ↦ h.symm ▸ gauge_zero⟩
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
⊢ {x}ᶜ ∈ comap (gauge s) (𝓝 0)

Tactic:
have : {x}ᶜ ∈ comap (gauge s) (𝓝 0) :=
    comap_gauge_nhds_zero_le hs hb (isOpen_compl_singleton.mem_nhds hne.symm)
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)
rcases : ∀ (r : ℝ) (hr₀ : 0 < r) (hr : gauge s ⁻¹' {b : ℝ | |b| < r} ⊆ {x}ᶜ), False
⊢ False

Tactic:
rcases ((nhds_basis_zero_abs_lt _).comap _).mem_iff.1 this with ⟨r, hr₀, hr⟩

Premises used: Filter.HasBasis.mem_iff, nhds_basis_zero_abs_lt, Filter.HasBasis.comap, Iff.mp
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)
r : ℝ
hr₀ : 0 < r
hr : gauge s ⁻¹' {b : ℝ | |b| < r} ⊆ {x}ᶜ
⊢ x ∈ gauge s ⁻¹' {b : ℝ | |b| < r}

Tactic:
simpa [h₀]
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)
r : ℝ
hr₀ : 0 < r
hr : gauge s ⁻¹' {b : ℝ | |b| < r} ⊆ {x}ᶜ
⊢ False

Tactic:
exact hr (by simpa [h₀]) rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
⊢ 0 < gauge s x ↔ x ≠ 0

Tactic:
simp only [(gauge_nonneg _).lt_iff_ne', Ne, gauge_eq_zero hs hb]

Premises used: gauge_eq_zero, Ne, gauge_nonneg, LE.le.lt_iff_ne'
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
⊢ Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 (HSMul.hSMul (α := ℝ) 1⁻¹ x))

Tactic:
have H₁ : Tendsto (fun r : ℝ ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 ((1 : ℝ)⁻¹ • x)) :=
    ((tendsto_id.inv₀ one_ne_zero).smul tendsto_const_nhds).mono_left inf_le_left
-- Module: Mathlib.Analysis.Convex.Gauge
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 (HSMul.hSMul (α := ℝ) 1⁻¹ x))
⊢ Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)

Tactic:
rw [inv_one, one_smul] at H₁

Premises used: inv_one, one_smul