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

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
ι : Sort u_4
p₁ p₂ : P
inst✝ : Subsingleton P
s : AffineSubspace k P
⊢ s = ⊥ ∨ s = ⊤

Tactic:
rw [← coe_eq_bot_iff, ← coe_eq_univ_iff]
    rcases (s : Set P).eq_empty_or_nonempty with h | h
    · exact .inl h
    · exact .inr h.eq_univ

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✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ (Convex 𝕜 s ∧
      ∀ ⦃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) ↔
    Convex 𝕜 s ∧ s.Pairwise fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
refine
    and_congr_right'
      ⟨fun h x hx y hy _ a b ha hb hab => h hx hy ha hb hab, fun h x hx y hy a b ha hb hab => ?_⟩

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✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
h : s.Pairwise fun 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
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
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
⊢ g (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y

Tactic:
calc
      g (a • x + b • y) ≤ a • g x + b • g y := hg.right hx hy ha hb hab
      _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_right

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✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ ConcaveOn 𝕜 s (-f) ↔ ConvexOn 𝕜 s f

Tactic:
by
  rw [← neg_convexOn_iff, neg_neg f]

Goal state after:
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
a : ℝ
ha : 0 < a
h : ∀ i ∈ s, (p i) x < a
⊢ (s.sup p) x < a

Tactic:
lift a to ℝ≥0 using ha.le

Goal state after:
𝕜 : 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
a : ℝ≥0
ha : 0 < ↑a
h : ∀ i ∈ s, (p i) x < ↑a
⊢ (s.sup p) x < ↑a
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case e'_3.a
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
p₁ p₂ : P
s' : Finset ι
h : ∑ i ∈ s, w i = 1
hp₂ : ∀ i ∈ s ∩ s', p i = p₂
hp₁ : ∀ i ∈ s \ s', p i = p₁
i : ι
hi : i ∈ s ∩ s'
⊢ p₂ = p i

Tactic:
exact (hp₂ i hi).symm

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

Goal state before:
pp: case right
ι : 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 : ι
w' : ι → k := (↑s).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∑ a ∈ s, w' a • (p a -ᵥ p i0) = ∑ i ∈ s, w i • (p i -ᵥ p i0)

pp: case right
ι : 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 : ι
w' : ι → k := (↑s).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∀ (a : ι), 0 • (p a -ᵥ p i0) = 0

Tactic:
· apply Finset.sum_congr rfl
        intro i hi
        simp [w', Set.indicator_apply, if_pos hi]

Goal state after:
case right
ι : 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 : ι
w' : ι → k := (↑s).indicator w
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∀ (a : ι), 0 • (p a -ᵥ p i0) = 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case pos
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₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ↑r₁ = r₂
⊢ ∃ r, r ≠ 0 ∧ p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁) ∧ p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂) ∧ p₄ -ᵥ p₆ = r • (p₁ -ᵥ p₃)

Tactic:
refine ⟨r₁, r₁.ne_zero, hr₁.symm, h ▸ hr₂.symm, ?_⟩

Goal state after:
case pos
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₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ↑r₁ = r₂
⊢ p₄ -ᵥ p₆ = ↑r₁ • (p₁ -ᵥ p₃)
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₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬↑r₁ = r₂
h₁₂ : ↑r₁ • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
h₁₁ : ↑r₁ • (p₂ -ᵥ p₁) + ↑r₁ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
⊢ (r₂ - ↑r₁) • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}

Tactic:
simpa [sub_smul] using sub_mem h₁₂ h₁₁

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
⊢ p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r

Tactic:
rcases eq_or_ne k 0 with (rfl | hk)
  · rw [norm_zero, zero_mul, ball_eq_emptyset _ le_rfl]
    exact empty_subset _
  · intro x
    rw [Set.mem_smul_set, Seminorm.mem_ball_zero]
    refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩
    · rwa [Seminorm.mem_ball_zero, map_smul_eq_mul, norm_inv, ←
        mul_lt_mul_iff_right₀ <| norm_pos_iff.mpr hk, ← mul_assoc, ← div_eq_mul_inv ‖k‖ ‖k‖,
        div_self (ne_of_gt <| norm_pos_iff.mpr hk), one_mul]
    rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self hk, one_smul]

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

Goal state before:
pp: case pos
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
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1 ∪ s2, (↑s1).indicator w1 i = 1
hw2 : ∑ i ∈ s1 ∪ s2, (↑s2).indicator w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0

Tactic:
have hws : (∑ i ∈ s1 ∪ s2, (Set.indicator (↑s1) w1 - Set.indicator (↑s2) w2) i) = 0 := by
          simp [hw1, hw2]

Goal state after:
case pos
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
s1 s2 : Finset ι
w1 w2 : ι → k
hw1 : ∑ i ∈ s1 ∪ s2, (↑s1).indicator w1 i = 1
hw2 : ∑ i ∈ s1 ∪ s2, (↑s2).indicator w2 i = 1
heq : (affineCombination k s1 p) w1 = (affineCombination k s2 p) w2
i : ι
hi : i ∈ s1 ∪ s2
hws : ∑ i ∈ s1 ∪ s2, ((↑s1).indicator w1 - (↑s2).indicator w2) i = 0
⊢ (↑s1).indicator w1 i - (↑s2).indicator w2 i = 0
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 ℝ (p.ball x r)

Tactic:
convert! (p.convexOn.translate_left (-x)).convex_lt r

Goal state after:
𝕜 : 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 : ℝ
⊢ p.ball x r = {x_1 | x_1 ∈ (fun z ↦ -x + z) ⁻¹' univ ∧ (⇑p ∘ fun z ↦ z + -x) x_1 < r}
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
inst✝ : Nontrivial ι
i : ι
⊢ Function.Surjective ⇑(b.coord i)

Tactic:
intro x
    obtain ⟨j, hij⟩ := exists_ne i
    let s : Finset ι := {i, j}
    have hi : i ∈ s := by simp [s]
    let w : ι → k := fun j' => if j' = i then x else 1 - x
    have hw : s.sum w = 1 := by simp [s, w, Finset.sum_ite, Finset.filter_insert, hij,
      Finset.filter_true_of_mem, Finset.filter_false_of_mem]
    use s.affineCombination k b w
    simp [w, b.coord_apply_combination_of_mem hi hw]

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
a b : E
⊢ Continuous fun t ↦ (lineMap a b) ↑t

Tactic:
by dsimp [lineMap]; fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
a b c d : E
x✝ : ↑I
⊢ ((Path.segment a b).add (Path.segment c d)) x✝ = (Path.segment (a + c) (b + d)) x✝

Tactic:
simp [lineMap_apply_module, add_add_add_comm]

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

Goal state before:
pp: case mp
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
inst✝ : Nontrivial k
p : ι → P
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : ↑fs₁ ⊆ s₁
w₁ : ι → k
hw₁ : ∑ i ∈ fs₁, w₁ i = 1
fs₂ : Finset ι
hfs₂ : ↑fs₂ ⊆ s₂
w₂ : ι → k
hw₂ : ∑ i ∈ fs₂, w₂ i = 1
hw₁₂ : (affineCombination k fs₁ p) w₁ = (affineCombination k fs₂ p) w₂
ha : (↑fs₁).indicator w₁ = (↑fs₂).indicator w₂
⊢ ∃ fs, ↑fs ⊆ s₁ ∩ s₂ ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ (affineCombination k fs₁ p) w₁ = (affineCombination k fs p) w

Tactic:
refine ⟨fs₁ ∩ fs₂, by grind, w₁, ?_, ?_⟩

Goal state after:
case mp.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
inst✝ : Nontrivial k
p : ι → P
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : ↑fs₁ ⊆ s₁
w₁ : ι → k
hw₁ : ∑ i ∈ fs₁, w₁ i = 1
fs₂ : Finset ι
hfs₂ : ↑fs₂ ⊆ s₂
w₂ : ι → k
hw₂ : ∑ i ∈ fs₂, w₂ i = 1
hw₁₂ : (affineCombination k fs₁ p) w₁ = (affineCombination k fs₂ p) w₂
ha : (↑fs₁).indicator w₁ = (↑fs₂).indicator w₂
⊢ ∑ i ∈ fs₁ ∩ fs₂, w₁ i = 1

case mp.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
inst✝ : Nontrivial k
p : ι → P
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : ↑fs₁ ⊆ s₁
w₁ : ι → k
hw₁ : ∑ i ∈ fs₁, w₁ i = 1
fs₂ : Finset ι
hfs₂ : ↑fs₂ ⊆ s₂
w₂ : ι → k
hw₂ : ∑ i ∈ fs₂, w₂ i = 1
hw₁₂ : (affineCombination k fs₁ p) w₁ = (affineCombination k fs₂ p) w₂
ha : (↑fs₁).indicator w₁ = (↑fs₂).indicator w₂
⊢ (affineCombination k fs₁ p) w₁ = (affineCombination k (fs₁ ∩ fs₂) p) w₁
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 : AffineSubspace k P
inst✝ : Nonempty ↥S
s : Simplex k (↥S) n
⊢ Set.range (s.map S.subtype ⋯).points ⊆ ↑S

Tactic:
rintro x ⟨y, rfl⟩; exact Subtype.prop _

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

Goal state before:
pp: 𝕜 : Type u_2
ι : Type u_1
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : Fintype ι
inst✝² : ZeroLEOneClass 𝕜
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
⊢ stdSimplex 𝕜 ι = {fun x ↦ 1}

Tactic:
cases nonempty_unique ι

Goal state after:
case intro
𝕜 : Type u_2
ι : Type u_1
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : Fintype ι
inst✝² : ZeroLEOneClass 𝕜
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
val✝ : Unique ι
⊢ stdSimplex 𝕜 ι = {fun x ↦ 1}
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : IsOrderedRing 𝕜
⊢ stdSimplex 𝕜 (Fin 2) ⊆ [Pi.single 0 1 -[𝕜] Pi.single 1 1]

Tactic:
rintro f ⟨hf₀, hf₁⟩

Goal state after:
𝕜 : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : IsOrderedRing 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : ∑ x, f x = 1
⊢ f ∈ [Pi.single 0 1 -[𝕜] Pi.single 1 1]
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: case refine_2
S : Type u_1
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
X : Type u_2
Y : Type u_3
inst✝² : Fintype X
inst✝¹ : Fintype Y
inst✝ : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : ∑ x, s x = 1
⊢ ∑ x, (FunOnFinite.linearMap S S f) s x = 1

Tactic:
simp only [FunOnFinite.linearMap_apply_apply, ← hs₁]

Goal state after:
case refine_2
S : Type u_1
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
X : Type u_2
Y : Type u_3
inst✝² : Fintype X
inst✝¹ : Fintype Y
inst✝ : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : ∑ x, s x = 1
⊢ ∑ x, {x_1 | f x_1 = x}.sum s = ∑ x, s x
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
⊢ Simplex.setInterior I s ⊆ ↑(affineSpan k (Set.range s.points))

Tactic:
by
  rintro p ⟨w, hw, hi, rfl⟩
  exact affineCombination_mem_affineSpan_of_nonempty hw _

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
n : ℕ
s : Simplex k P n
⊢ s.closedInterior ⊆ ↑(affineSpan k (Set.range s.points))

Tactic:
by
  rintro p ⟨w, hw, hi, rfl⟩
  exact affineCombination_mem_affineSpan_of_nonempty hw _

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ nhdsKer (⋃ y ∈ s, {y}) ↔ ∃ y ∈ s, x ⤳ y

Tactic:
by
    simp only [nhdsKer_iUnion, mem_nhdsKer_singleton, mem_iUnion₂, exists_prop]

Goal state after:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
V : Set X
hVy : V ∈ 𝓝 y
hVc : IsPathConnected V
z : X
hz : z ∈ V
hxz : z ∈ pathComponent x
⊢ False

Tactic:
exact hxy <| hxz.trans (hVc.joinedIn _ hz _ (mem_of_mem_nhds hVy)).joined

Goal state after:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
x : X
F : Set X
inst✝ : LocallyPathConnectedSpace X
hF : F ∈ 𝓝 x
u : Set X
huF : u ⊆ F
hu : IsOpen[inst✝¹] u
hxu : x ∈ u
⊢ pathComponentIn F x ∈ 𝓝 x

Tactic:
exact mem_nhds_iff.mpr ⟨pathComponentIn u x, pathComponentIn_mono huF,
    hu.pathComponentIn x, mem_pathComponentIn_self hxu⟩

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

Goal state before:
pp: case refine_2.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
ι : 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
i : ι ⊕ ι'
hi : i ∈ sx.disjSum sy
⊢ 0 ≤ Sum.elim (fun i ↦ a * wx i) (fun j ↦ b * wy j) i

Tactic:
rw [Finset.mem_disjSum] at hi

Goal state after:
case refine_2.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
ι : 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
i : ι ⊕ ι'
hi : (∃ a ∈ sx, Sum.inl a = i) ∨ ∃ b ∈ sy, Sum.inr b = i
⊢ 0 ≤ Sum.elim (fun i ↦ a * wx i) (fun j ↦ b * wy j) i
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case refine_2.refine_3
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
i : ι ⊕ ι'
hi : i ∈ sx.disjSum sy
⊢ Sum.elim zx zy i ∈ s

Tactic:
rw [Finset.mem_disjSum] at hi

Goal state after:
case refine_2.refine_3
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
i : ι ⊕ ι'
hi : (∃ a ∈ sx, Sum.inl a = i) ∨ ∃ b ∈ sy, Sum.inr b = i
⊢ Sum.elim zx zy i ∈ s
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
⊢ x ∈ U

Tactic:
by_cases hr₀ : r = 0

Goal state after:
case pos
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : r = 0
⊢ x ∈ U

case neg
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
⊢ x ∈ U
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
⊢ z ∈ U

Tactic:
apply hU_sub

Goal state after:
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x✝ : F
r : ℝ
hr : 0 ≤ r
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := ⋯
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
⊢ z ∈ sphere 0 r
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case fst
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module R E
inst✝² : Module R F
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i, v i • g i = y
h_sum : ∑ i, w i.1 * v i.2 = 1
⊢ ∑ y, ∑ x, v y • w x • f x = x

Tactic:
← Fintype.sum_smul_sum,

Goal state after:
case fst
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module R E
inst✝² : Module R F
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i, v i • g i = y
h_sum : ∑ i, w i.1 * v i.2 = 1
⊢ (∑ i, v i) • ∑ j, w j • f j = x
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case snd
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module R E
inst✝² : Module R F
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i, v i • g i = y
h_sum : ∑ i, w i.1 * v i.2 = 1
⊢ ∑ x, ∑ x_1, w x • v x_1 • g x_1 = y

Tactic:
← Fintype.sum_smul_sum,

Goal state after:
case snd
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module R E
inst✝² : Module R F
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i, v i • g i = y
h_sum : ∑ i, w i.1 * v i.2 = 1
⊢ (∑ i, w i) • ∑ j, v j • g j = y