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

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ (a⁻¹ • b) • a • x ∈ s

Tactic:
refine hs.smul_mem ?_ ha
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ hba (norm_nonneg _)

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
S : Type u_7
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 ↑V
⊢ ↑V = univ

Tactic:
rw [eq_univ_iff_forall]

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
S : Type u_7
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 ↑V
⊢ ∀ (x : E), x ∈ ↑V
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddGroup E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : DistribMulAction 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
⊢ IsVonNBounded 𝕜 (s - t)

Tactic:
by
  rw [sub_eq_add_neg]
  exact hs.add ht.neg

Goal state after:
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
⊢ 𝓝[univ] σ 0 = 𝓝 0

Tactic:
nhdsWithin_univ,

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✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : (fun x1 x2 ↦ x1 + x2) v w ≠ (fun x1 x2 ↦ x1 + x2) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • v + a • w + (b • x + b • y) ∈ interior (s + t)

Tactic:
add_add_add_comm

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : (fun x1 x2 ↦ x1 + x2) v w ≠ (fun x1 x2 ↦ x1 + x2) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Field 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : ContinuousConstSMul 𝕝 E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕝
hc : c ≠ 0
⊢ StrictConvex 𝕜 (c • s)

Tactic:
· exact hs.linear_image (LinearMap.lsmul _ _ c) (isOpenMap_smul₀ hc)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + (b • f y + b • g y)

Tactic:
add_add_add_comm

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + a • g x + (b • f y + b • g y) = a • f x + a • g x + (b • f y + b • g y)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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
Q : AffineSubspace k P
p₀ p₁ : P
c : k
h₀ : p₀ ∈ Q
h₁ : p₁ ∈ Q
⊢ (lineMap p₀ p₁) c ∈ Q

Tactic:
rw [AffineMap.lineMap_apply]
  exact Q.smul_vsub_vadd_mem c h₁ h₀ h₀

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + (b • f y + b • g y)

Tactic:
add_add_add_comm

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + a • g x + (b • f y + b • g y) = a • f x + a • g x + (b • f y + b • g y)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y + (a • g x + b • g y) = a • f x + a • g x + (b • f y + b • g y)

Tactic:
add_add_add_comm

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + a • g x + (b • f y + b • g y) = a • f x + a • g x + (b • f y + b • g 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
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
⊢ b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)) = 0

Tactic:
conv_lhs =>
    congr
    · skip
    · congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]

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
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
⊢ b₁ -ᵥ b₂ + ∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0
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
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 : AffineSubspace k P₁
h : ↑(map f s) = ∅
⊢ s = ⊥

Tactic:
coe_map,

Goal state after:
case refine_1
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 : AffineSubspace k P₁
h : ⇑f '' ↑s = ∅
⊢ s = ⊥
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 : AffineSubspace k P
⊢ ⊥ ∥ s ↔ s = ⊥

Tactic:
rw [parallel_comm, parallel_bot_iff_eq_bot]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.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
s₁ s₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₂ = ⊥ → s₁ = ⊥

pp: case refine_3
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
h : s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
⊢ s₁ ∥ s₂

Tactic:
· rintro rfl
    exact parallel_bot_iff_eq_bot.1 h

Goal state after:
case refine_3
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
h : s₁.direction = s₂.direction ∧ (s₁ = ⊥ ↔ s₂ = ⊥)
⊢ s₁ ∥ s₂
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mpr
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
p : ι → P
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ∑ i ∈ s.erase i1, w i • (p i -ᵥ p i1) = 0
i : ι
hi : i ∈ s
f : ι → V := fun i ↦ w i • (p i -ᵥ p i1)
hs2 : ∑ i ∈ Finset.subtype (fun i ↦ i ≠ i1) (s.erase i1), f ↑i = 0
h2 : ∀ (i : { x // x ≠ i1 }), ↑i ∈ s.erase i1 → w ↑i = 0
h2b : ∀ i ∈ s, i ≠ i1 → w i = 0
⊢ w i = 0

Tactic:
exact Finset.eq_zero_of_sum_eq_zero hw h2b i hi

Goal state after:
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✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
i : ι
j : { j // j ≠ i }
⊢ (b.basisOf i) j = b ↑j -ᵥ b i

Tactic:
simp [basisOf]

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
p : ι → P
ha : AffineIndependent k p
⊢ AffineIndependent k fun x ↦ ↑x

Tactic:
let f : Set.range p → ι := fun x => x.property.choose
  have hf : ∀ x, p (f x) = x := fun x => x.property.choose_spec
  let fe : Set.range p ↪ ι := ⟨f, fun x₁ x₂ he => Subtype.ext (hf x₁ ▸ hf x₂ ▸ he ▸ rfl)⟩
  convert! ha.comp_embedding fe
  ext
  simp [fe, hf]

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

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ t.centerMass w z = t'.centerMass w' z'

Tactic:
← centerMass_filter_ne_zero,

Goal state after:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ {i ∈ t | w i ≠ 0}.centerMass w z = t'.centerMass w' z'
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ (∑ i ∈ t with w i ≠ 0, w i)⁻¹ • ∑ i ∈ t with w i ≠ 0, w i • z i = t'.centerMass w' z'

Tactic:
← centerMass_filter_ne_zero,

Goal state after:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ (∑ i ∈ t with w i ≠ 0, w i)⁻¹ • ∑ i ∈ t with w i ≠ 0, w i • z i = {i ∈ t' | w' i ≠ 0}.centerMass w' z'
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
S : Set (Set α)
⊢ interior (⋂₀ S) = ⋂ s ∈ S, interior s

Tactic:
by
  simp_rw [sInter_eq_biInter, interior_iInter]

Goal state after:
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:
rw [sUnion_eq_biUnion, inter_iUnion₂, nonempty_biUnion] at ha

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 : ∃ i ∈ S, (nhdsKer {a} ∩ i).Nonempty
⊢ a ∈ ⋃₀ S
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ IsPathConnected s) id

Tactic:
rw [hasBasis_self]
    intro t ht
    rcases (h x).mem_iff.mp ht with ⟨i, hpi, hi⟩
    exact ⟨s x i, (h x).mem_of_mem hpi, h' x i hpi, hi⟩

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✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := ⟨1, ⋯⟩
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ LinearIndependent k fun i ↦ ![p₁, p₂] ↑i -ᵥ ![p₁, p₂] 0

Tactic:
refine .of_subsingleton default ?_

Goal state after:
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
h : p₁ ≠ p₂
i₁ : { x // x ≠ 0 } := ⟨1, ⋯⟩
he' : ∀ (i : { x // x ≠ 0 }), i = i₁
this : Unique { x // x ≠ 0 }
⊢ ![p₁, p₂] ↑default -ᵥ ![p₁, p₂] 0 ≠ 0
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
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
x : 𝕜
hx : x ∈ Ioo b a
⊢ s \ {a} ∈ 𝓝 x

Tactic:
· 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 mpr
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
h : p ∈ s.closedInterior
⊢ ∃ s_1 w, (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points) w = p

Tactic:
obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype <|
      Set.mem_of_mem_of_subset h s.closedInterior_subset_affineSpan
    rw [affineCombination_mem_closedInterior_iff hw1] at h
    exact ⟨Finset.univ, w, fun i _ ↦ (h i).1, hw1, rfl⟩

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case h.h
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
H✝ : ∀ (i : ι'), ∃ s C, ∀ (x : E), (q i) (f x) ≤ C * (s.sup p) x
i : ι'
s : Finset ι
H : ∃ C, ∀ (x : E), (q i) (f x) ≤ C * (s.sup p) x
⊢ ∃ C, (q i).comp f ≤ C • s.sup p

Tactic:
obtain ⟨C, hC⟩ := H

Goal state after:
case h.h
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
H : ∀ (i : ι'), ∃ s C, ∀ (x : E), (q i) (f x) ≤ C * (s.sup p) x
i : ι'
s : Finset ι
C : ℝ
hC : ∀ (x : E), (q i) (f x) ≤ C * (s.sup p) x
⊢ ∃ C, (q i).comp f ≤ C • s.sup p
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ p.basisSets) id

Tactic:
rw [congr_fun (congr_arg (@nhds E) hp.1) 0]

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ (𝓝 0).HasBasis (fun s ↦ s ∈ p.basisSets) id
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✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
⊢ CompleteSpace (E →SLᵤ[σ, 𝔖] F)

Tactic:
by
  wlog hF : T2Space F generalizing F
  · rw [(isUniformInducing_postcomp σ (SeparationQuotient.mkCLM 𝕜₂ F)
      SeparationQuotient.isUniformInducing_mk _).completeSpace_congr]
    exacts [this _ inferInstance, SeparationQuotient.postcomp_mkCLM_surjective F σ E]
  rw [completeSpace_iff_isComplete_range (isUniformInducing_coeFn _ _ _)]
  apply IsClosed.isComplete
  have H₁ : IsClosed {f : E →ᵤ[𝔖] F | Continuous ((UniformOnFun.toFun 𝔖) f)} :=
    UniformOnFun.isClosed_setOfPred_continuous h𝔖
  convert!
    H₁.inter <|
      (LinearMap.isClosed_range_coe E F σ).preimage
        (UniformOnFun.uniformContinuous_toFun h𝔖U).continuous
  exact ContinuousLinearMap.range_coeFn_eq

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
S : Type u_5
inst✝²² : NormedField 𝕜
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommGroup E
inst✝¹⁹ : Module 𝕜 E
inst✝¹⁸ : TopologicalSpace E
inst✝¹⁷ : IsTopologicalAddGroup E
inst✝¹⁶ : ContinuousConstSMul 𝕜 E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : Module 𝕜 F
inst✝¹³ : TopologicalSpace F
inst✝¹² : IsTopologicalAddGroup F
inst✝¹¹ : ContinuousConstSMul 𝕜 F
inst✝¹⁰ : AddCommGroup G
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalAddGroup G
inst✝⁶ : ContinuousConstSMul 𝕜 G
inst✝⁵ : Module S G
inst✝⁴ : SMulCommClass 𝕜 S G
inst✝³ : ContinuousConstSMul S G
inst✝² : Module S F
inst✝¹ : SMulCommClass 𝕜 S F
inst✝ : ContinuousConstSMul S F
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace] (↑(prodₗ S)).toFun

Tactic:
change Continuous fun x => .id 𝕜 _ ∘L prodₗ S x

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
S : Type u_5
inst✝²² : NormedField 𝕜
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommGroup E
inst✝¹⁹ : Module 𝕜 E
inst✝¹⁸ : TopologicalSpace E
inst✝¹⁷ : IsTopologicalAddGroup E
inst✝¹⁶ : ContinuousConstSMul 𝕜 E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : Module 𝕜 F
inst✝¹³ : TopologicalSpace F
inst✝¹² : IsTopologicalAddGroup F
inst✝¹¹ : ContinuousConstSMul 𝕜 F
inst✝¹⁰ : AddCommGroup G
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalAddGroup G
inst✝⁶ : ContinuousConstSMul 𝕜 G
inst✝⁵ : Module S G
inst✝⁴ : SMulCommClass 𝕜 S G
inst✝³ : ContinuousConstSMul S G
inst✝² : Module S F
inst✝¹ : SMulCommClass 𝕜 S F
inst✝ : ContinuousConstSMul S F
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace] fun x ↦ ContinuousLinearMap.id 𝕜 (F × G) ∘SL (prodₗ S) x
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr : r < ‖f‖
hr₀ : r < 0
⊢ ‖0‖ < 1 ∧ r < ‖f 0‖

Tactic:
by simpa using hr₀

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝³ : TopologicalSpace α
inst✝² : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst✝¹ : TopologicalSpace δ₁
inst✝ : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap ⇑φ₁
h_proper₂ : IsProperMap ⇑φ₂
h_cover : range ⇑φ₁ ∪ range ⇑φ₂ = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K | IsCompact K}
h_image₁ : MapsTo (fun x ↦ ⇑φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ ⇑φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ ⇑φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ ⇑φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover' : ∀ S ∈ 𝔖, S ⊆ range ⇑φ₁ ∪ range ⇑φ₂
⊢ inferInstance =
    UniformSpace.comap (fun x ↦ x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp φ₂) inferInstance

Tactic:
← UniformSpace.comap_comap

Goal state after:
α : Type u₁
β : Type u₂
inst✝³ : TopologicalSpace α
inst✝² : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst✝¹ : TopologicalSpace δ₁
inst✝ : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap ⇑φ₁
h_proper₂ : IsProperMap ⇑φ₂
h_cover : range ⇑φ₁ ∪ range ⇑φ₂ = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K | IsCompact K}
h_image₁ : MapsTo (fun x ↦ ⇑φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ ⇑φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ ⇑φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ ⇑φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover' : ∀ S ∈ 𝔖, S ⊆ range ⇑φ₁ ∪ range ⇑φ₂
⊢ inferInstance =
    UniformSpace.comap (toUniformOnFunIsCompact ∘ fun x ↦ x.comp φ₁) inferInstance ⊓
      UniformSpace.comap (toUniformOnFunIsCompact ∘ fun x ↦ x.comp φ₂) inferInstance