mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
⊢ x ∈ affineSpan k s → x ∈ ↑(Submodule.span k s)

Tactic:
hx

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
hx : x ∈ affineSpan k s
⊢ x ∈ ↑(Submodule.span k s)
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
⊢ 𝓝 (σ 0) = 𝓝 0

Tactic:
map_zero

Goal state after:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst✝⁹ : NormedDivisionRing 𝕜₁
inst✝⁸ : NormedDivisionRing 𝕜₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜₁ E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
⊢ 𝓝 0 = 𝓝 0
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
x : E
⊢ x ∈ s ∩ t →
    ∀ ⦃y : E⦄,
      y ∈ s ∩ t → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior (s ∩ t)) x y

Tactic:
hx

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
x : E
hx : x ∈ s ∩ t
⊢ ∀ ⦃y : E⦄,
    y ∈ s ∩ t → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior (s ∩ t)) x y
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕜] F
hf : Continuous ⇑f
hfinj : Injective ⇑f
x : E
⊢ x ∈ ⇑f ⁻¹' s →
    ∀ ⦃y : E⦄,
      y ∈ ⇑f ⁻¹' s →
        x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior (⇑f ⁻¹' s)) x y

Tactic:
hx

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕜] F
hf : Continuous ⇑f
hfinj : Injective ⇑f
x : E
hx : x ∈ ⇑f ⁻¹' s
⊢ ∀ ⦃y : E⦄,
    y ∈ ⇑f ⁻¹' s → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior (⇑f ⁻¹' s)) x y
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
⊢ x ∈ (fun x ↦ z + x) ⁻¹' s →
    ∀ ⦃y : E⦄,
      y ∈ (fun x ↦ z + x) ⁻¹' s →
        x ≠ y →
          (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior ((fun x ↦ z + x) ⁻¹' s)) x y

Tactic:
hx

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x ↦ z + x) ⁻¹' s
⊢ ∀ ⦃y : E⦄,
    y ∈ (fun x ↦ z + x) ⁻¹' s →
      x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior ((fun x ↦ z + x) ⁻¹' s)) x y
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : Continuous ⇑f
hfinj : Injective ⇑f
x : E
⊢ x ∈ ⇑f ⁻¹' s →
    ∀ ⦃y : E⦄,
      y ∈ ⇑f ⁻¹' s →
        x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior (⇑f ⁻¹' s)) x y

Tactic:
hx

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : Continuous ⇑f
hfinj : Injective ⇑f
x : E
hx : x ∈ ⇑f ⁻¹' s
⊢ ∀ ⦃y : E⦄,
    y ∈ ⇑f ⁻¹' s → x ≠ y → (fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior (⇑f ⁻¹' s)) x y
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun x1 x2 ↦ x1 -ᵥ x2) p₁ p₂ = v
⊢ v ∈ ↑(Submodule.span k ((fun x ↦ x -ᵥ p) '' s))

Tactic:
simp_rw [← vsub_sub_vsub_cancel_right p₁ p₂ p] at hv

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p₁ -ᵥ p - (p₂ -ᵥ p) = v
⊢ v ∈ ↑(Submodule.span k ((fun x ↦ x -ᵥ p) '' s))
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case a.f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
| fun x ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)

Tactic:
· ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
⊢ x ∈ s →
    ∀ ⦃y : E⦄,
      y ∈ s →
        ∀ ⦃a b : 𝕜⦄,
          0 ≤ a →
            0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y

Tactic:
hx

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
⊢ ∀ ⦃y : E⦄,
    y ∈ s →
      ∀ ⦃a b : 𝕜⦄,
        0 ≤ a →
          0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s →
          ∀ ⦃a b : 𝕜⦄,
            0 ≤ a →
              0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y
x : E
⊢ x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
hx

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s →
          ∀ ⦃a b : 𝕜⦄,
            0 ≤ a →
              0 ≤ b → 0 < a + b → f ((a / (a + b)) • x + (b / (a + b)) • y) ≤ (a / (a + b)) • f x + (b / (a + b)) • f y
x : E
hx : x ∈ s
⊢ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Finset P
w : P → k
⊢ (affineCombination k s.attach Subtype.val) (w ∘ Subtype.val) = (affineCombination k s id) w

Tactic:
by
  classical rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
      univ_eq_attach, attach_image_val]

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y
x : E
⊢ x ∈ s →
    ∀ ⦃y : E⦄,
      y ∈ s →
        x ≠ y →
          ∀ ⦃a b : 𝕜⦄,
            0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y

Tactic:
hx

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y
x : E
hx : x ∈ s
⊢ ∀ ⦃y : E⦄,
    y ∈ s →
      x ≠ y →
        ∀ ⦃a b : 𝕜⦄,
          0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s →
          x ≠ y →
            ∀ ⦃a b : 𝕜⦄,
              0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y
x : E
⊢ x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y

Tactic:
hx

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h :
  ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s →
          x ≠ y →
            ∀ ⦃a b : 𝕜⦄,
              0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y
x : E
hx : x ∈ s
⊢ ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p) w = p i

Tactic:
classical
    rw [← @vsub_eq_zero_iff_eq V, ← hw,
      ← s.affineCombination_sdiff_sub (singleton_subset_iff.2 his), sdiff_singleton_eq_erase,
      ← filter_ne']
    congr
    refine (affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_singleton_self _) ?_ ?_).symm
    · simp [hwi]
    · simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
v : V
x : k
s : Set ι
p : ι → P
b : P
⊢ (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint p b) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint (fun i ↦ p ↑i) b) w

Tactic:
simp_rw [weightedVSubOfPoint_apply]
    constructor
    · rintro ⟨fs, hfs, w, rfl, rfl⟩
      exact ⟨fs.subtype (· ∈ s), fun i => w i, sum_subtype_of_mem _ hfs,
        (sum_subtype_of_mem _ hfs).symm⟩
    · rintro ⟨fs, w, rfl, rfl⟩
      refine ⟨fs.map (Function.Embedding.subtype _), map_subtype_subset _, fun i =>
        if h : i ∈ s then w ⟨i, h⟩ else 0, ?_, ?_⟩ <;> simp

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
⊢ BddAbove (range (DFunLike.coe ∘ p)) ↔ ∀ (x : E), BddAbove (range fun i ↦ (p i) x)

Tactic:
bddAbove_range_pi

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
⊢ (∀ (a : E), BddAbove (range fun i ↦ (DFunLike.coe ∘ p) i a)) ↔ ∀ (x : E), BddAbove (range fun i ↦ (p i) x)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x : E
⊢ (c • p).closedBall x r = p.closedBall x (r / ↑c)

Tactic:
by
  ext
  rw [mem_closedBall, mem_closedBall, smul_apply, NNReal.smul_def, smul_eq_mul, mul_comm,
    le_div_iff₀ (NNReal.coe_pos.mpr hc)]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ)

Tactic:
exact convex_iInter₂ fun _ _ => convex_ball _ _ _

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕝 : Type u_6
E : Type u_7
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : Seminorm 𝕝 E
hp : ∀ r > 0, ⇑p ⁻¹' Metric.closedBall 0 r ∈ 𝓝 0
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : E) in 𝓝 0, p x ∈ Metric.closedBall (p 0) i

Tactic:
map_zero

Goal state after:
𝕝 : Type u_6
E : Type u_7
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : Seminorm 𝕝 E
hp : ∀ r > 0, ⇑p ⁻¹' Metric.closedBall 0 r ∈ 𝓝 0
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : E) in 𝓝 0, p x ∈ Metric.closedBall 0 i
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : DivisionRing k
inst✝¹ : Module k V
inst✝ : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
⊢ (b.coord i) (Finset.centroid k s ⇑b) = (↑s.card)⁻¹

Tactic:
by
  rw [Finset.centroid,
    b.coord_apply_combination_of_mem hi (s.sum_centroidWeights_eq_one_of_nonempty _ ⟨i, hi⟩),
    Finset.centroidWeights, Function.const_apply]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
xεpos : 0 < p x / ε
n : ℤ
hn : p x / ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ p (c ^ (-(n + 1)) • x) < ε

Tactic:
show p ((c ^ (-(n + 1))) • x) < ε

Goal state after:
case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
xεpos : 0 < p x / ε
n : ℤ
hn : p x / ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ p (c ^ (-(n + 1)) • x) < ε
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: 𝕜 : Type ?u.3
inst✝² : Ring 𝕜
inst✝¹ : PartialOrder 𝕜
inst✝ : IsOrderedRing 𝕜
f : ↑(stdSimplex 𝕜 (Fin 2))
⊢ ↑((fun x ↦ ⟨![1 - ↑x, ↑x], ⋯⟩) ((fun f ↦ ⟨↑f 1, ⋯⟩) f)) 0 = ↑f 0 ∧
    ↑((fun x ↦ ⟨![1 - ↑x, ↑x], ⋯⟩) ((fun f ↦ ⟨↑f 1, ⋯⟩) f)) 1 = ↑f 1

Tactic:
by
    simp [← (show f.1 0 + f.1 1 = 1 by simpa using f.2.2)]

Goal state after:
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: S : Type u_1
inst✝⁶ : Semiring S
inst✝⁵ : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : Fintype X
inst✝³ : Fintype Y
inst✝² : Fintype Z
inst✝¹ : IsOrderedRing S
inst✝ : Subsingleton X
s t : ↑(stdSimplex S X)
⊢ s = t

Tactic:
ext i
    have (u : stdSimplex S X) : u i = 1 := by
      rw [← sum_eq_one u, Finset.sum_eq_single i _ (by simp)]
      intro j _ hj
      exact (hj (Subsingleton.elim j i)).elim
    simp [this]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_2
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
p : P
x✝ : p ∈ Simplex.setInterior I s
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h : (affineCombination k univ s.points) w = p
⊢ p ∈ Simplex.setInterior I (s.reindex e)

Tactic:
· subst h
    rw [← Function.comp_id w, ← Function.comp_id s.points, ← e.symm_comp_self,
      ← Function.comp_assoc, ← Function.comp_assoc, ← e.coe_toEmbedding,
      ← Finset.univ.affineCombination_map e.toEmbedding, map_univ_equiv]
    change Finset.univ.affineCombination k (s.reindex e).points _ ∈ _
    have hw' : ∑ i, (w ∘ e.symm) i = 1 := by rwa [sum_comp_equiv, map_univ_equiv]
    rw [affineCombination_mem_setInterior_iff hw']
    exact fun i ↦ hwI (e.symm i)

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : TopologicalSpace V
inst✝² : Torsor V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
p : P
| Continuous[instTopologicalSpaceProd, inst✝³] fun p ↦ p.1 * p.2

Tactic:
enter [1, x]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : TopologicalSpace V
inst✝² : Torsor V P
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
p : P
x : V × V
| x.1 * x.2
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ∃ c, (lineMap x y) c ∈ interior s
x : E
⊢ x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → (fun x y ↦ openSegment 𝕜 x y ⊆ interior s) x y

Tactic:
hx

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y ↦ ∃ c, (lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
⊢ ∀ ⦃y : E⦄, y ∈ s → x ≠ y → (fun x y ↦ openSegment 𝕜 x y ⊆ interior s) x y
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
⊢ x ∈ s → StarConvex R x s

Tactic:
hx

Goal state after:
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
⊢ StarConvex R x s
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
u : Set X
x✝ : IsOpen[inst✝] u
⊢ (∀ (x : X), IsOpen[inst✝] (pathComponentIn u x)) ↔ ∀ x ∈ u, pathComponentIn u x ∈ 𝓝 x

Tactic:
exact ⟨fun h x hxu ↦ (h x).mem_nhds (mem_pathComponentIn_self hxu),
    fun h x ↦ isOpen_iff_mem_nhds.mpr fun y hy ↦
      pathComponentIn_congr hy ▸ h y <| pathComponentIn_subset hy⟩

Goal state after:
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_1
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
x : E
⊢ x ∈ Set.range v → x ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}

Tactic:
hx

Goal state after:
case refine_1
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
x : E
hx : x ∈ Set.range v
⊢ x ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_1
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Set E
x : E
⊢ x ∈ s → x ∈ {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}

Tactic:
hx

Goal state after:
case refine_1
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Set E
x : E
hx : x ∈ s
⊢ x ∈ {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : ∑ i ∈ sx, wx i = 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : ∑ i ∈ sy, wy i = 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • sx.centerMass wx zx + b • sy.centerMass wy zy ∈
    {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}

Tactic:
rw [Finset.centerMass_segment' _ _ _ _ _ _ hwx₁ hwy₁ _ _ hab]

Goal state after:
case refine_2
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : ∑ i ∈ sx, wx i = 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : ∑ i ∈ sy, wy i = 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (sx.disjSum sy).centerMass (Sum.elim (fun i ↦ a * wx i) fun j ↦ b * wy j) (Sum.elim zx zy) ∈
    {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

Tactic:
by
  rw [inf_eq_iInf]
  refine .iInf fun b => ?_
  cases b <;> assumption

Goal state after: