-- Mathlib/Analysis/LocallyConvex/Polar.lean
theorem polar_subMulAction {S : Type*} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) :
    B.polar m = { y | ∀ x ∈ m, B x y = 0 }

Proof state:
case h.mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
h : y ∈ {y | ∀ x ∈ m, (B x) y = 0}
x : E
hx : x ∈ ↑m
⊢ ‖(B x) y‖ ≤ 1

Tactic:
simp [h x hx]

Result:
no goals

Proof state:
case h.mp.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
hy : y ∈ B.polar ↑m
x : E
hx : x ∈ m
r : 𝕜
hr : ‖(B x) y‖⁻¹ < ‖r‖
⊢ (B x) y = 0

Tactic:
contrapose! hr

Result:
case h.mp.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
hy : y ∈ B.polar ↑m
x : E
hx : x ∈ m
r : 𝕜
hr : (B x) y ≠ 0
⊢ ‖r‖ ≤ ‖(B x) y‖⁻¹

Proof state:
case h.mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
⊢ y ∈ {y | ∀ x ∈ m, (B x) y = 0} → y ∈ B.polar ↑m

Tactic:
intro h x hx

Result:
case h.mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
h : y ∈ {y | ∀ x ∈ m, (B x) y = 0}
x : E
hx : x ∈ ↑m
⊢ ‖(B x) y‖ ≤ 1

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
⊢ y ∈ B.polar ↑m ↔ y ∈ {y | ∀ x ∈ m, (B x) y = 0}

Tactic:
constructor

Result:
case h.mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
⊢ y ∈ B.polar ↑m → y ∈ {y | ∀ x ∈ m, (B x) y = 0}

case h.mpr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
⊢ y ∈ {y | ∀ x ∈ m, (B x) y = 0} → y ∈ B.polar ↑m

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
⊢ B.polar ↑m = {y | ∀ x ∈ m, (B x) y = 0}

Tactic:
ext y

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
⊢ y ∈ B.polar ↑m ↔ y ∈ {y | ∀ x ∈ m, (B x) y = 0}

Proof state:
case h.mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
⊢ y ∈ B.polar ↑m → y ∈ {y | ∀ x ∈ m, (B x) y = 0}

Tactic:
intro hy x hx

Result:
case h.mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
hy : y ∈ B.polar ↑m
x : E
hx : x ∈ m
⊢ (B x) y = 0

Proof state:
case h.mp.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
hy : y ∈ B.polar ↑m
x : E
hx : x ∈ m
r : 𝕜
hr : (B x) y ≠ 0
⊢ ‖r‖ * ‖(B x) y‖ ≤ 1

Tactic:
simpa using hy _ (SMulMemClass.smul_mem r hx)

Result:
no goals

Proof state:
case h.mp.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
hy : y ∈ B.polar ↑m
x : E
hx : x ∈ m
r : 𝕜
hr : (B x) y ≠ 0
⊢ ‖r‖ ≤ ‖(B x) y‖⁻¹

Tactic:
rw [← one_div, le_div_iff₀ (norm_pos_iff.2 hr)]

Result:
case h.mp.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
hy : y ∈ B.polar ↑m
x : E
hx : x ∈ m
r : 𝕜
hr : (B x) y ≠ 0
⊢ ‖r‖ * ‖(B x) y‖ ≤ 1

Proof state:
case h.mp
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
hy : y ∈ B.polar ↑m
x : E
hx : x ∈ m
⊢ (B x) y = 0

Tactic:
obtain ⟨r, hr⟩ := NormedField.exists_lt_norm 𝕜 ‖B x y‖⁻¹

Result:
case h.mp.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : F
hy : y ∈ B.polar ↑m
x : E
hx : x ∈ m
r : 𝕜
hr : ‖(B x) y‖⁻¹ < ‖r‖
⊢ (B x) y = 0