mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
⊢ ∃ r V, 0 < r ∧ V ∈ 𝓝 0 ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U

Tactic:
have h : Filter.Tendsto (fun x : 𝕜 × E => x.fst • x.snd) (𝓝 (0, 0)) (𝓝 0) :=
      continuous_smul.tendsto' (0, 0) _ (smul_zero _)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
h : Tendsto (fun x ↦ x.1 • x.2) (𝓝 (0, 0)) (𝓝 0)
⊢ ∃ r V, 0 < r ∧ V ∈ 𝓝 0 ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
S : Set (Set E)
hS : S.Finite
⊢ IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s

Tactic:
sUnion_eq_biUnion,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
S : Set (Set E)
hS : S.Finite
⊢ IsVonNBounded 𝕜 (⋃ i ∈ S, i) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s
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
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ affineSpan k A
y : P
hy : y ∈ A
⊢ ⟨y, ⋯⟩ ∈ affineSpan k (Subtype.val ⁻¹' A)

Tactic:
exact subset_affineSpan _ _ hy

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
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ((s.erase i).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
  apply sum_erase
  rw [vsub_self, smul_zero]

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
s : Finset ι
w : ι → k
p : P
h : ∑ i ∈ s, w i = 0
⊢ (s.weightedVSub fun x ↦ p) w = 0

Tactic:
by
  rw [weightedVSub, weightedVSubOfPoint_apply_const, h, zero_smul]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddGroup E
inst✝ : SMul 𝕜 E
g : Seminorm 𝕜 E
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le'✝ : ∀ (r s : E), toFun✝ (r + s) ≤ toFun✝ r + toFun✝ s
neg'✝ : ∀ (r : E), toFun✝ (-r) = toFun✝ r
smul'✝ :
  ∀ (a : 𝕜) (x : E),
    { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝ }.toFun (a • x) =
      ‖a‖ * { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝ }.toFun x
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝, smul' := smul'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝, smul' := smul'✝ } = g

Tactic:
rcases g with ⟨⟨_⟩⟩

Goal state after:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddGroup E
inst✝ : SMul 𝕜 E
toFun✝¹ : E → ℝ
map_zero'✝¹ : toFun✝¹ 0 = 0
add_le'✝¹ : ∀ (r s : E), toFun✝¹ (r + s) ≤ toFun✝¹ r + toFun✝¹ s
neg'✝¹ : ∀ (r : E), toFun✝¹ (-r) = toFun✝¹ r
smul'✝¹ :
  ∀ (a : 𝕜) (x : E),
    { toFun := toFun✝¹, map_zero' := map_zero'✝¹, add_le' := add_le'✝¹, neg' := neg'✝¹ }.toFun (a • x) =
      ‖a‖ * { toFun := toFun✝¹, map_zero' := map_zero'✝¹, add_le' := add_le'✝¹, neg' := neg'✝¹ }.toFun x
toFun✝ : E → ℝ
map_zero'✝ : toFun✝ 0 = 0
add_le'✝ : ∀ (r s : E), toFun✝ (r + s) ≤ toFun✝ r + toFun✝ s
neg'✝ : ∀ (r : E), toFun✝ (-r) = toFun✝ r
smul'✝ :
  ∀ (a : 𝕜) (x : E),
    { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝ }.toFun (a • x) =
      ‖a‖ * { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝ }.toFun x
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, map_zero' := map_zero'✝¹, add_le' := add_le'✝¹, neg' := neg'✝¹, smul' := smul'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝, smul' := smul'✝ }
⊢ { toFun := toFun✝¹, map_zero' := map_zero'✝¹, add_le' := add_le'✝¹, neg' := neg'✝¹, smul' := smul'✝¹ } =
    { toFun := toFun✝, map_zero' := map_zero'✝, add_le' := add_le'✝, neg' := neg'✝, smul' := smul'✝ }
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₁ w₂ : ι → k
p : ι → P
⊢ (s.weightedVSub p) w₁ +ᵥ (affineCombination k s p) w₂ = (affineCombination k s p) (w₁ + w₂)

Tactic:
by
  rw [← vadd_eq_add, AffineMap.map_vadd, affineCombination_linear]

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
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 =
    (affineCombination k (s \ {i}) p) w -ᵥ (affineCombination k {i} p) (-w)

Tactic:
sdiff_singleton_eq_erase,

Goal state after:
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 =
    (affineCombination k (s.erase i) p) w -ᵥ (affineCombination k {i} p) (-w)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case e_a.refine_1
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
⊢ (-w) i = 1

Tactic:
simp [hwi]

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

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
⊢ map f (affineSpan k s) = affineSpan k (⇑f '' s)

Tactic:
by
  rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)
  · simp
  apply ext_of_direction_eq
  · simp [direction_affineSpan]
  · exact ⟨f p, mem_image_of_mem f (subset_affineSpan k _ hp),
          subset_affineSpan k _ (mem_image_of_mem f hp)⟩

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
a : 𝕜
x : E
⊢ ⨆ i, ↑i (a • x) = ‖a‖ * ⨆ i, ↑i x

Tactic:
← smul_eq_mul,

Goal state after:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
a : 𝕜
x : E
⊢ ⨆ i, ↑i (a • x) = ‖a‖ • ⨆ i, ↑i x
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case inr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
i0 : ι
⊢ (s.weightedVSub p) w ∈ vectorSpan k (Set.range p)

Tactic:
vectorSpan_range_eq_span_range_vsub_right k p i0,

Goal state after:
case inr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
i0 : ι
⊢ (s.weightedVSub p) w ∈ Submodule.span k (Set.range fun i ↦ p i -ᵥ p i0)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: 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
s₁ s₂ s₃ : AffineSubspace k P
h₁₂ : s₁ ∥ s₂
h₂₃ : s₂ ∥ s₃
⊢ s₁ ∥ s₃

Tactic:
rcases h₁₂ with ⟨v₁₂, rfl⟩

Goal state after:
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
s₁ s₃ : AffineSubspace k P
v₁₂ : V
h₂₃ : map (↑(constVAdd k P v₁₂)) s₁ ∥ s₃
⊢ s₁ ∥ s₃
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case mp.inr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
⊢ v ∈ vectorSpan k (Set.range p) → ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w

Tactic:
vectorSpan_range_eq_span_range_vsub_right k p i0,

Goal state after:
case mp.inr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
⊢ v ∈ Submodule.span k (Set.range fun i ↦ p i -ᵥ p i0) → ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ x ∈ ⇑p ⁻¹' Metric.closedBall 0 r ↔ x ∈ {x | p x ≤ r}

Tactic:
simp only [mem_ofPred, mem_preimage, mem_closedBall_zero_iff,
    Real.norm_of_nonneg (apply_nonneg p _)]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
h₁₂₄₅ : line[k, p₁, p₂] ∥ line[k, p₄, p₅]
h₂₃₅₆ : line[k, p₅, p₆].direction ≤ line[k, p₂, p₃].direction
h₃₁₆₄ : line[k, p₆, p₄].direction ≤ line[k, p₃, p₁].direction
⊢ ∃ r, r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)

Tactic:
by
  rw [affineSpan_pair_parallel_iff_exists_unit_smul'] at h₁₂₄₅
  rw [direction_affineSpan_pair_le_iff_exists_smul] at h₂₃₅₆ h₃₁₆₄
  obtain ⟨r₁, hr₁⟩ := h₁₂₄₅
  obtain ⟨r₂, hr₂⟩ := h₂₃₅₆
  obtain ⟨r₃, hr₃⟩ := h₃₁₆₄
  rw [Units.smul_def] at hr₁
  by_cases h : (r₁ : k) = r₂
  · refine ⟨r₁, r₁.ne_zero, hr₁.symm, h ▸ hr₂.symm, ?_⟩
    rw [← neg_inj, neg_vsub_eq_vsub_rev, ← smul_neg, neg_vsub_eq_vsub_rev,
      ← vsub_add_vsub_cancel p₆ p₅ p₄, ← vsub_add_vsub_cancel p₃ p₂ p₁, smul_add, hr₁, h, hr₂]
  · exfalso
    have h₁₂ : (r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃} := by
      rw [hr₁, hr₂, add_comm, vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, neg_mem_iff, ← hr₃]
      exact smul_vsub_mem_vectorSpan_pair _ _ _
    have h₁₁ : (r₁ : k) • (p₂ -ᵥ p₁) + (r₁ : k) • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃} := by
      rw [add_comm, ← smul_add, vsub_add_vsub_cancel]
      exact smul_vsub_rev_mem_vectorSpan_pair _ _ _
    have h₂₁ : (r₂ - r₁) • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃} := by
      simpa [sub_smul] using sub_mem h₁₂ h₁₁
    rw [Submodule.smul_mem_iff _ (by rwa [sub_ne_zero, ne_comm]), ← direction_affineSpan,
      vsub_left_mem_direction_iff_mem (right_mem_affineSpan_pair _ _ _)] at h₂₁
    exact h₂ h₂₁

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✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ p (a • x) + p (b • y) = p ((a • 1) • x) + p ((b • 1) • y)

Tactic:
smul_one_smul,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ p (a • x) + p (b • y) = p (a • x) + p ((b • 1) • y)
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
inst✝ : IsTopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (⇑p) 0
⊢ Continuous[inst✝¹, _] ⇑p

Tactic:
let := IsTopologicalAddGroup.rightUniformSpace E
  have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
  exact (Seminorm.uniformContinuous_of_continuousAt_zero hp).continuous

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

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
inst✝ : AffineSpace V P
ι : Type u_4
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
⊢ AffineIndependent k (p ∘ ⇑f)

Tactic:
intro fs w hw hs i0 hi0

Goal state after:
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
ι : Type u_4
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
⊢ w i0 = 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ (normSeminorm 𝕜 E).closedBall = Metric.closedBall

Tactic:
by
  ext x r y
  simp only [Seminorm.mem_closedBall, Metric.mem_closedBall, coe_normSeminorm, dist_eq_norm]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ s.face ⋯ = mkOfPoint k (s.points i)

Tactic:
by
  ext
  simp [Affine.Simplex.mkOfPoint_points, Affine.Simplex.face_points, Finset.orderEmbOfFin_singleton]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
V₂ : Type u_3
V₃ : Type u_4
P : Type u_5
P₂ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V
inst✝⁷ : AddCommGroup V₂
inst✝⁶ : AddCommGroup V₃
inst✝⁵ : Module k V
inst✝⁴ : Module k V₂
inst✝³ : Module k V₃
inst✝² : AffineSpace V P
inst✝¹ : AffineSpace V₂ P₂
inst✝ : AffineSpace V₃ P₃
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
S₁ : AffineSubspace k P
S₂ : AffineSubspace k P₂
hS₁ : affineSpan k (Set.range s.points) ≤ S₁
hfS : AffineSubspace.map f S₁ ≤ S₂
this✝ : Nonempty ↥S₁ := Nonempty.map (⇑(AffineSubspace.inclusion hS₁)) inferInstance
this : Nonempty ↥S₂ := Nonempty.map (⇑(AffineSubspace.inclusion hfS)) inferInstance
⊢ affineSpan k (Set.range (s.map f hf).points) = AffineSubspace.map f (affineSpan k (Set.range s.points))

Tactic:
simp [AffineSubspace.map_span, Set.range_comp]

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

Goal state before:
pp: case neg.hb
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
⊢ ¬∃ x ∈ Simplex.setInterior I s, f x = p

Tactic:
contrapose hp

Goal state after:
case neg.hb
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
I : Set k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective ⇑f
p : P₂
hp : ∃ x ∈ Simplex.setInterior I s, f x = p
⊢ p ∈ affineSpan k (Set.range (s.map f hf).points)
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
S : Set (Set α)
⊢ closure[inst✝¹] (⋃₀ S) = ⋃ s ∈ S, closure[inst✝¹] s

Tactic:
sUnion_eq_biUnion,

Goal state after:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
S : Set (Set α)
⊢ closure[inst✝¹] (⋃ i ∈ S, i) = ⋃ s ∈ S, closure[inst✝¹] s
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
hS : ∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s
a : α
ha : (nhdsKer {a} ∩ ⋃₀ S).Nonempty
⊢ a ∈ ⋃₀ S

Tactic:
sUnion_eq_biUnion,

Goal state after:
α : Type u_3
inst✝ : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
S : Set (Set α)
hS : ∀ s ∈ S, ∀ (a : α), (nhdsKer {a} ∩ s).Nonempty → a ∈ s
a : α
ha : (nhdsKer {a} ∩ ⋃ i ∈ S, i).Nonempty
⊢ a ∈ ⋃₀ S
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : LinearOrder 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst✝¹] s, Ioo x a ⊆ s
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x

Tactic:
rcases eq_empty_or_nonempty (s ∩ Iio a) with hs' | ⟨b, hbs, hba⟩
  · simp [hs']
  have : Ioo b a ⊆ s := h b (subset_closure hbs)
  apply eventually_of_mem (U := Ioo b a) ?_ fun x hx ↦ ?_
  · exact mem_nhdsWithin.2 ⟨Ioi b, isOpen_Ioi, hba, fun _ ⟨h₁, _, h₂⟩ ↦ ⟨h₁, h₂⟩⟩
  · exact mem_nhds_iff.2 ⟨Ioo b a, subset_sdiff_singleton this right_notMem_Ioo, isOpen_Ioo, hx⟩

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

Goal state before:
pp: case refine_3
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
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ (affineCombination R s v) w ∈ (convexHull R) (Set.range v)

Tactic:
exact affineCombination_mem_convexHull hw₀ hw₁

Goal state after:
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f) t
⊢ LocallyConvexSpace 𝕜 E

Tactic:
refine LocallyConvexSpace.ofBases 𝕜 E (fun _ => preimage f)
    (fun x => fun s : Set F => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) (fun x => ?_) fun x s ⟨_, hs⟩ =>
    hs.linear_preimage f

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f) t
x : E
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) (preimage ⇑f)
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι : Type u_6
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ (𝓝 0).HasBasis (fun Si ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun Si ↦ {f | ∀ x ∈ Si.1, f x ∈ b Si.2}

Tactic:
(isEmbedding_coeFn σ F 𝔖).isInducing.nhds_eq_comap

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι : Type u_6
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ (comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (𝓝 ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) 0))).HasBasis
    (fun Si ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun Si ↦ {f | ∀ x ∈ Si.1, f x ∈ b Si.2}
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case pos
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
h' : 0 < I.sup' hI r
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
refine ⟨I.sup' hI r, h', fun x hx => finset_sup_apply_lt h' fun i hi => ?_⟩

Goal state after:
case pos
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ (p i) x < I.sup' hI r
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case mpr
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
⊢ (∃ x, ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i) x_1 ≤ x) → ∃ r > 0, ∀ x ∈ s, (p i) x < r

Tactic:
· rintro ⟨r, _⟩
    use 1 + max r 0
    grind

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
x : E
hx : 0 < ‖x‖
ha : 0 ≤ a
⊢ a ≤ ‖f‖

Tactic:
simpa only [hf, hx, mul_le_mul_iff_left₀] using f.le_opNorm x

Goal state after: