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

Goal state before:
pp: case e'_6
R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : c ∈ Ici 0
hc2 : (algebraMap R A) c = a
d : R
hd1 : d ∈ Ici 0
hd2 : (algebraMap R A) d = b
⊢ b • v = d • v

pp: R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : c ∈ Ici 0
hc2 : (algebraMap R A) c = a
d : R
hd1 : d ∈ Ici 0
hd2 : (algebraMap R A) d = b
⊢ c + d = 1

Tactic:
· rw [← hd2, algebraMap_smul]

Goal state after:
R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : c ∈ Ici 0
hc2 : (algebraMap R A) c = a
d : R
hd1 : d ∈ Ici 0
hd2 : (algebraMap R A) d = b
⊢ c + d = 1
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s → ∃ a, s ⊆ a • Metric.closedBall 0 1

pp: case mpr
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.closedBall 0 1) → Bornology.IsBounded s

Tactic:
· rw [isBounded_iff_subset_smul_ball 𝕜]
    exact Exists.imp fun a ha => ha.trans <| Set.smul_set_mono <| Metric.ball_subset_closedBall

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.closedBall 0 1) → Bornology.IsBounded s
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
hx : x ∈ ⇑f ⁻¹' s
y : E
hy : y ∈ ⇑f ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • y) ∈ interior s

Tactic:
Convex.combo_affine_apply hab

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
hy : y ∈ ⇑f ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y ∈ interior s
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
s : Set P
v : V
⊢ vectorSpan k (v +ᵥ s) = vectorSpan k s

Tactic:
simp [vectorSpan]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : SMul 𝕜 β
f : F → β
s : Set F
hf : ConvexOn 𝕜 s f
g : E →ₗ[𝕜] F
x : E
hx : x ∈ ⇑g ⁻¹' s
y : E
hy : y ∈ ⇑g ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (g (a • x + b • y)) = f (a • g x + b • g y)

Tactic:
by rw [g.map_add, g.map_smul, g.map_smul]

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✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ vectorSpan k s = Submodule.span k ((fun x ↦ p -ᵥ x) '' (s \ {p}))

Tactic:
conv_lhs =>
    rw [vectorSpan_eq_span_vsub_set_left k hp, ← Set.insert_eq_of_mem hp, ←
      Set.insert_sdiff_singleton, Set.image_insert_eq]
  simp [Submodule.span_insert_eq_span]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_5
inst✝⁸ : Field 𝕜
inst✝⁷ : LinearOrder 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : SMul 𝕜 β
f : F → β
g : E →ᵃ[𝕜] F
s : Set F
hf : ConvexOn 𝕜 s f
x : E
hx : x ∈ ⇑g ⁻¹' s
y : E
hy : y ∈ ⇑g ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (g (a • x + b • y)) = f (a • g x + b • g y)

Tactic:
Convex.combo_affine_apply hab

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_5
inst✝⁸ : Field 𝕜
inst✝⁷ : LinearOrder 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : SMul 𝕜 β
f : F → β
g : E →ᵃ[𝕜] F
s : Set F
hf : ConvexOn 𝕜 s f
x : E
hx : x ∈ ⇑g ⁻¹' s
y : E
hy : y ∈ ⇑g ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • g x + b • g y) = f (a • g x + 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
s₁ s₂ : Set P
p : P
hp₁ : p ∈ s₁
hp₂ : p ∈ s₂
⊢ vectorSpan k (s₁ ∪ s₂) = vectorSpan k s₁ ⊔ vectorSpan k s₂

Tactic:
simp_rw [← direction_affineSpan, span_union,
    direction_sup_eq_sup_direction (mem_affineSpan k hp₁) (mem_affineSpan k hp₂)]

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

Goal state before:
pp: case inr.inr.hn
k : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : AffineSpace W Q
s : Set P
t : Set Q
ht : t.Nonempty
x : P
hx : x ∈ s
⊢ (↑(affineSpan k (s ×ˢ t)) ∩ ↑((affineSpan k s).prod (affineSpan k t))).Nonempty

Tactic:
obtain ⟨y, hy⟩ := ht

Goal state after:
case inr.inr.hn
k : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : AffineSpace W Q
s : Set P
t : Set Q
x : P
hx : x ∈ s
y : Q
hy : y ∈ t
⊢ (↑(affineSpan k (s ×ˢ t)) ∩ ↑((affineSpan k s).prod (affineSpan k t))).Nonempty
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
v : V
⊢ map (↑(constVAdd k P v)) s₁ ∥ s₁

Tactic:
refine ⟨-v, ?_⟩

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₁ : AffineSubspace k P
v : V
⊢ s₁ = map (↑(constVAdd k P (-v))) (map (↑(constVAdd k P v)) s₁)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case neg.refine_1
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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ p₂ ∈ map (↑(constVAdd k P (p₂ -ᵥ p₁))) s₁

pp: case neg.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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ s₂.direction = (map (↑(constVAdd k P (p₂ -ᵥ p₁))) s₁).direction

Tactic:
· rw [mem_map]
        refine ⟨p₁, hp₁, ?_⟩
        simp

Goal state after:
case neg.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
hd : s₁.direction = s₂.direction
hb : s₁ = ⊥ ↔ s₂ = ⊥
hs₁ : ¬s₁ = ⊥
hs₂ : s₂ ≠ ⊥
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
⊢ s₂.direction = (map (↑(constVAdd k P (p₂ -ᵥ p₁))) s₁).direction
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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ (if hx : i1 = i1 then -∑ y ∈ s, g y else g ⟨i1, hx⟩) + ∑ x ∈ s, g x = 0

Tactic:
rw [dif_pos rfl]

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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ -∑ y ∈ s, g y + ∑ x ∈ s, g x = 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ (s.sup p).closedBall x r = s.inf fun i ↦ (p i).closedBall x r

Tactic:
rw [Finset.inf_eq_iInf]
  exact closedBall_finset_sup_eq_iInter _ _ _ hr

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

Goal state before:
pp: ι : 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
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : ↑s' → k := fun i ↦ w ↑i
h' : ∑ i ∈ s with i ∈ s', w i = 1
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range fun x ↦ p ↑x)

Tactic:
rw [← Finset.sum_subtype_eq_sum_filter] at h'

Goal state after:
ι : 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
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
s' : Set ι
hs' : ∀ i ∈ s, i ∉ s' → w i = 0
p : ι → P
w' : ↑s' → k := fun i ↦ w ↑i
h' : ∑ x ∈ Finset.subtype (Membership.mem s') s, w ↑x = 1
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range fun x ↦ p ↑x)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case neg
ι : 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
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
hj : j ∉ s
⊢ Function.update w j (1 - (s \ {j}).sum w) j + ∑ x ∈ s, Function.update w j (1 - (s \ {j}).sum w) x = 1

Tactic:
Finset.sum_update_of_notMem hj,

Goal state after:
case neg
ι : 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
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
hj : j ∉ s
⊢ Function.update w j (1 - (s \ {j}).sum w) j + ∑ x ∈ s, w x = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.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
I : Set k
n : ℕ
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
⊢ (affineCombination k univ s.points) w ∈ Simplex.setInterior I s ↔ ∀ (i : Fin (n + 1)), w i ∈ I

Tactic:
refine ⟨fun ⟨w', hw', hw'01, hww'⟩ ↦ ?_, fun h ↦ ⟨w, hw, h, 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
I : Set k
n : ℕ
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
x✝ : (affineCombination k univ s.points) w ∈ Simplex.setInterior I s
w' : Fin (n + 1) → k
hw' : ∑ i, w' i = 1
hw'01 : ∀ (i : Fin (n + 1)), w' i ∈ I
hww' : (affineCombination k univ s.points) w' = (affineCombination k univ s.points) w
⊢ ∀ (i : Fin (n + 1)), w i ∈ I
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
i j : ι
hij : i ≠ j
⊢ 1 ≤ Metric.diam (stdSimplex ℝ ι)

Tactic:
rw [show (1 : ℝ) = dist (Pi.single i 1 : ι → ℝ) (Pi.single j 1) by
    simp [dist_single_single i j (1 : ℝ) 1 hij, Real.dist_eq]]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
i j : ι
hij : i ≠ j
⊢ dist (Pi.single i 1) (Pi.single j 1) ≤ Metric.diam (stdSimplex ℝ ι)
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
⊢ Continuous[inst✝³, inst✝³] fun a ↦ a⁻¹

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance
    conv =>
      enter [1, v]
      equals p /ₛ (v • p) => rw [sdiv_smul_eq_sdiv_div, sdiv_self, one_div]
    fun_prop

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
i : ι
t : Finset ι
z : ι → E
inst✝ : DecidableEq ι
hi : i ∈ t
⊢ (∑ j ∈ t, if i = j then z i else 0) = z i

Tactic:
· rw [sum_ite_eq, if_pos hi]

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

Goal state before:
pp: case hw
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i : ι
t : Finset ι
z : ι → E
inst✝ : DecidableEq ι
hi : i ∈ t
⊢ (∑ i_1 ∈ t, if i = i_1 then 1 else 0) = 1

Tactic:
· rw [sum_ite_eq, if_pos hi]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.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
I : Set k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
⊢ (affineCombination k univ s.points) w ∈ Simplex.setInterior I (s.face h) ↔ (∀ i ∈ fs, w i ∈ I) ∧ ∀ i ∉ fs, w i = 0

Tactic:
by
  refine ⟨fun hi ↦ ?_, fun ⟨hii, hi0⟩ ↦ ?_⟩
  · obtain ⟨w', hw', he⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype
      (Set.mem_of_mem_of_subset hi setInterior_subset_affineSpan)
    rw [he, affineCombination_mem_setInterior_iff hw'] at hi
    have he' := s.independent.indicator_extend_eq_of_affineCombination_comp_embedding_eq_of_fintype
      hw hw' (fs.orderEmbOfFin h).toEmbedding he.symm
    simp_rw [he'.symm]
    refine ⟨fun i hi ↦ ?_, fun i hi ↦ by simp [hi]⟩
    simp only [RelEmbedding.coe_toEmbedding, range_orderEmbOfFin, mem_coe, hi, Set.indicator_of_mem]
    rw [← mem_coe, ← fs.range_orderEmbOfFin h] at hi
    obtain ⟨j, rfl⟩ := hi
    simp [(fs.orderEmbOfFin h).injective.extend_apply, hi]
  · let w' : Fin (m + 1) → k := w ∘ fs.orderEmbOfFin h
    have hw' : ∑ i, w' i = 1 := by
      rw [Fintype.sum_of_injective _ (fs.orderEmbOfFin h).injective w' w
        (fun i hi ↦ hi0 _ (by simpa using hi)) (fun _ ↦ rfl), hw]
    have hw'01 (i) : w' i ∈ I := hii (fs.orderEmbOfFin h i) (by simp)
    rw [← (s.face h).affineCombination_mem_setInterior_iff hw'] at hw'01
    convert! hw'01
    convert! Finset.univ.affineCombination_map (fs.orderEmbOfFin h).toEmbedding w s.points using 1
    simp only [map_orderEmbOfFin_univ, Finset.affineCombination_indicator_subset _ _ fs.subset_univ]
    congr
    grind [Set.indicator_eq_self, mem_support]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.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
inst✝² : PartialOrder k
inst✝¹ : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst✝ : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
x✝ : (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, 0 < w i
hi0 : ∀ i ∉ fs, w i = 0
i : Fin (n + 1)
hi : i ∈ fs
⊢ 1 < #fs

Tactic:
by grind [→ NeZero.ne]

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

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
ι : Type u_4
p : ι → P
h✝ : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
h : ∃ r, r • ((affineCombination k s p) w₁ -ᵥ (affineCombination k s p) w₂) = (s.weightedVSub p) w
⊢ ∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ i)

pp: case refine_2
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
h✝ : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
h : ∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
⊢ ∃ r, r • ((affineCombination k s p) w₁ -ᵥ (affineCombination k s p) w₂) = (s.weightedVSub p) w

Tactic:
· rcases h with ⟨r, hr⟩
    refine ⟨r, fun i hi => ?_⟩
    rw [s.affineCombination_vsub, ← s.weightedVSub_const_smul, ← sub_eq_zero, ← map_sub] at hr
    have hw' : (∑ j ∈ s, (r • (w₁ - w₂) - w) j) = 0 := by
      simp_rw [Pi.sub_apply, Pi.smul_apply, Pi.sub_apply, smul_sub, Finset.sum_sub_distrib, ←
        Finset.smul_sum, hw, hw₁, hw₂, sub_self]
    have hr' := h s _ hw' hr i hi
    rw [eq_comm, ← sub_eq_zero, ← smul_eq_mul]
    exact hr'

Goal state after:
case refine_2
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
h✝ : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
h : ∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ i)
⊢ ∃ r, r • ((affineCombination k s p) w₁ -ᵥ (affineCombination k s p) w₂) = (s.weightedVSub p) w
Module: Mathlib.Topology.Compactness.NhdsKer

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact (nhdsKer s) ↔ IsCompact s

Tactic:
simp only [isCompact_iff_finite_subcover]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ {ι : Type u_1} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → nhdsKer s ⊆ ⋃ i, U i → ∃ t, nhdsKer s ⊆ ⋃ i ∈ t, U i) ↔
    ∀ {ι : Type u_1} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : AlexandrovDiscrete α
inst✝ : AlexandrovDiscrete β
s t : Set α
a : α
⊢ AlexandrovDiscrete (α × β)

Tactic:
simp_rw [alexandrovDiscrete_iff_nhds, Prod.forall, nhds_prod_eq, ← principal_nhdsKer_singleton,
    prod_principal_principal, nhdsKer_pair, forall_true_iff]

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

Goal state before:
pp: case «1»
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, ⋯⟩
hi : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
⊢ ↑↑⟨(fun i ↦ i) ⟨1, ⋯⟩, hi⟩ = ↑↑i₁

Tactic:
· simp [i₁]

Goal state after:
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:
rw [inf_eq_iInf]
  refine .iInf fun b => ?_
  cases b <;> assumption

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

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  (affineCombination k s p) w ∈
    line[k, (affineCombination k s p) (Pi.single i₁ 1),
      (affineCombination k s p) (affineCombinationLineMapWeights i₂ i₃ c)]
⊢ (if i₁ ∈ s then 1 else 0) = 1

Tactic:
if_pos h₁

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 1
i₁ i₂ i₃ : ι
h₁ : i₁ ∈ s
h₂ : i₂ ∈ s
h₃ : i₃ ∈ s
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
c : k
hc0 : 0 < c
hc1 : c < 1
hs :
  (affineCombination k s p) w ∈
    line[k, (affineCombination k s p) (Pi.single i₁ 1),
      (affineCombination k s p) (affineCombinationLineMapWeights i₂ i₃ c)]
⊢ 1 = 1