mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • max (f x) (f y) + b • max (f x) (f y)

Tactic:
gcongr

Goal state after:
case hb
𝕜 : 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 : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f x ≤ max (f x) (f y)

case hb
𝕜 : 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 : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f y ≤ max (f x) (f 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✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
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 • max (f x) (f y) + b • max (f x) (f y)

Tactic:
gcongr

Goal state after:
case hb
𝕜 : 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 : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f x ≤ max (f x) (f y)

case hb
𝕜 : 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 : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f y ≤ max (f x) (f y)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : P
h : ∑ i ∈ s, w i = 1
⊢ (p -ᵥ Classical.choice ⋯) +ᵥ Classical.choice ⋯ = p

Tactic:
vsub_vadd

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
⊢ p = p
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
r : k
p₃ : P
hp₃ : p₃ ∈ s
⊢ ∃ y ∈ k ∙ (p₂ -ᵥ p₁), ∃ z ∈ s.direction, y + z = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁

Tactic:
use r • (p₂ -ᵥ p₁), Submodule.mem_span_singleton.2 ⟨r, rfl⟩, p₃ -ᵥ p₁,
      vsub_mem_direction hp₃ hp₁

Goal state after:
case right
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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
r : k
p₃ : P
hp₃ : p₃ ∈ s
⊢ r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁) = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁
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
V₃ : Type u_6
P₃ : Type u_7
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₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
s : AffineSubspace k P₁
t : k
p₁ : P₁
h₁ : p₁ ∈ ↑s
p₂ : P₁
h₂ : p₂ ∈ ↑s
p₃ : P₁
h₃ : p₃ ∈ ↑s
this : t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ ↑s ∧ f (t • (p₁ -ᵥ p₂) +ᵥ p₃) = t • (f p₁ -ᵥ f p₂) +ᵥ f p₃

Tactic:
{ simp only [SetLike.mem_coe, true_and, this]
      rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub] }

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ (r • 1) • ⨅ u, p u + q (x✝ - u) = ⨅ u, (r • 1) • p u + (r • 1) • q (x✝ - u)

Tactic:
NNReal.smul_def,

Goal state after:
R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ ↑(r • 1) • ⨅ u, p u + q (x✝ - u) = ⨅ u, ↑(r • 1) • p u + ↑(r • 1) • q (x✝ - u)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : IsOrderedAddMonoid β
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := 2⁻¹ • x + 2⁻¹ • y
hz : z ∈ s
⊢ 2⁻¹ • f x + 2⁻¹ • f y ≤ 2⁻¹ • f z + 2⁻¹ • f z

Tactic:
gcongr

Goal state after:
case hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : IsOrderedAddMonoid β
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := ⋯
hz : z ∈ s
⊢ f x ≤ f z

case hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : IsOrderedAddMonoid β
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
f : E → β
s : Set E
x y : E
hf : StrictConvexOn 𝕜 s f
hfx : IsMinOn f s x
hfy : IsMinOn f s y
hx : x ∈ s
hy : y ∈ s
hxy : ¬x = y
z : E := ⋯
hz : z ∈ s
⊢ f y ≤ f z
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case 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
h : s₁ ∥ s₂
⊢ s₁ = ⊥ → s₂ = ⊥

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 bot_parallel_iff_eq_bot.1 h

Goal state after:
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₁ = ⊥

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.Analysis.Seminorm

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

Tactic:
NNReal.smul_def,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x✝ : E
⊢ ↑c • p (x✝ - x) < r ↔ p (x✝ - x) < r / ↑c
Module: Mathlib.Analysis.Seminorm

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

Tactic:
NNReal.smul_def,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
c : ℝ≥0
hc : 0 < c
r : ℝ
x x✝ : E
⊢ ↑c • p (x✝ - x) ≤ r ↔ p (x✝ - x) ≤ r / ↑c
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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
⊢ ∑ i ∈ insert i0 l.support, (⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)) i = 0

Tactic:
simp_rw [Pi.sub_apply, Finset.sum_sub_distrib,
            Finset.sum_update_of_mem (Finset.mem_insert_self _ _),
            Finset.sum_insert_of_eq_zero_if_notMem Finsupp.notMem_support_iff.1]

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
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
⊢ ∑ x ∈ l.support, l x - (∑ i ∈ l.support, l i + ∑ x ∈ insert i0 l.support \ {i0}, Function.const ι 0 x) = 0
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
hp₁ : p₁ ∈ line[k, p₃, p₄]
hp₂ : p₂ ∈ line[k, p₃, p₄]
hp₁₂ : p₁ ≠ p₂
⊢ line[k, p₃, p₄] ≤ line[k, p₁, p₂]

Tactic:
← vsub_vadd p₁ p₃,

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₃ p₄ : P
hp₁ : (p₁ -ᵥ p₃) +ᵥ p₃ ∈ line[k, p₃, p₄]
hp₂ : p₂ ∈ line[k, p₃, p₄]
hp₁₂ : p₁ ≠ p₂
⊢ line[k, p₃, p₄] ≤ line[k, p₁, p₂]
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
x : E
r : ℝ
hr : r ≤ 0
x✝ : E
⊢ p (x✝ - x) < r ↔ x✝ ∈ ∅

Tactic:
Set.mem_empty_iff_false,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x✝ : E
⊢ p (x✝ - x) < r ↔ False
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
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ p (x✝ - x) ≤ r ↔ x✝ ∈ ∅

Tactic:
Set.mem_empty_iff_false,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ p (x✝ - x) ≤ r ↔ False
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₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : p b ≤ r₂
⊢ p b * ‖a‖ < r₁ * r₂

Tactic:
mul_comm r₁

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : p b ≤ r₂
⊢ p b * ‖a‖ < r₂ * r₁
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case refine_2
ι : 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
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
hs : p1 -ᵥ p i0 = (s.weightedVSub p) w
s' : Finset ι := insert i0 s
w' : ι → k := (↑s).indicator w
h' : ∑ i ∈ s', w' i = 0
hs' : (s'.weightedVSub p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
hw0 : ∑ i ∈ s', w0 i = 1
hw0s : (Finset.affineCombination k s' p) w0 = p i0
⊢ p1 = (p1 -ᵥ p i0) +ᵥ p i0

Tactic:
vsub_vadd

Goal state after:
case refine_2
ι : 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
p1 : P
p : ι → P
h✝ : p1 ∈ affineSpan k (Set.range p)
i0 : ι
h0 : p i0 ∈ affineSpan k (Set.range p)
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
hs : p1 -ᵥ p i0 = (s.weightedVSub p) w
s' : Finset ι := insert i0 s
w' : ι → k := (↑s).indicator w
h' : ∑ i ∈ s', w' i = 0
hs' : (s'.weightedVSub p) w' = p1 -ᵥ p i0
w0 : ι → k := Function.update (Function.const ι 0) i0 1
hw0 : ∑ i ∈ s', w0 i = 1
hw0s : (Finset.affineCombination k s' p) w0 = p i0
⊢ p1 = p1
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₁ r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : p b ≤ r₂
⊢ ‖a‖ * p b ≤ r₁ * r₂

Tactic:
gcongr

Goal state after:
case b0
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
a : 𝕜
ha : ‖a‖ ≤ r₁
b : E
hb : p b ≤ r₂
⊢ 0 ≤ r₁
Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise

Goal state before:
pp: case e_f
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
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₂
v : V₁
s : AffineSubspace k P₁
p✝ : P₁
⊢ (f.comp ↑(AffineEquiv.constVAdd k P₁ v)) p✝ = ((↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f) p✝

Tactic:
exact f.map_vadd _ _

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 : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun x ↦ k • x) y = x
⊢ x ∈ p.closedBall 0 (‖k‖ * r)

Tactic:
Seminorm.mem_closedBall_zero,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
x y : E
hy : y ∈ p.closedBall 0 r
h : (fun x ↦ k • x) y = x
⊢ p x ≤ ‖k‖ * r
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 : ℝ
x y : E
hy : p y ≤ r
h : (fun x ↦ k • x) y = x
⊢ ‖k‖ * p y ≤ ‖k‖ * r

Tactic:
gcongr

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ k⁻¹ • x ∈ p.closedBall 0 r

Tactic:
Seminorm.mem_closedBall_zero,

Goal state after:
case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ p (k⁻¹ • x) ≤ r
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
⊢ 1 - (s \ {j}).sum w + ∑ x ∈ s, w x = 1

Tactic:
← Finset.erase_eq,

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
⊢ 1 - ∑ x ∈ s.erase j, w x + ∑ x ∈ s, w x = 1
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
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : p x < r₂
⊢ r * r₁ ≤ ‖a‖ * r₁

Tactic:
gcongr

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

Goal state before:
pp: case refine_2
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✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ ↥E.direction →ₗ[k] ↥F.direction

Tactic:
refine φ.linear.restrict (?_ : E.direction ≤ F.direction.comap φ.linear)
    rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]
    exact AffineSubspace.direction_le hEF

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
w₁ w₂ : ι → k
s : Finset ι
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
h : (affineCombination k s p) w₁ = (affineCombination k s p) w₂
⊢ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
have hi := ha.indicator_eq_of_affineCombination_eq _ _ _ _ hw₁ hw₂ h

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
ha : AffineIndependent k p
w₁ w₂ : ι → k
s : Finset ι
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
h : (affineCombination k s p) w₁ = (affineCombination k s p) w₂
hi : (↑s).indicator w₁ = (↑s).indicator w₂
⊢ ∀ i ∈ s, w₁ i = w₂ i
Module: Mathlib.Analysis.Seminorm

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

Tactic:
show c ^ (-(n + 1)) ≠ 0

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

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

Tactic:
gcongr

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

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x
x : E
j : ι
hj : j ∈ s
hjx : (p j) x ≠ 0
this : (s.sup p) x ≠ 0
⊢ q x ≤ (C • s.sup p) x

Tactic:
refine (s.sup p).bound_of_shell_smul q ε_pos hc (fun y hle hlt ↦ ?_) this

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x
x : E
j : ι
hj : j ∈ s
hjx : (p j) x ≠ 0
this : (s.sup p) x ≠ 0
y : E
hle : ε / ‖c‖ ≤ (s.sup p) y
hlt : (s.sup p) y < ε
⊢ q y ≤ (C • s.sup p) y
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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
this : Nonempty ↥S := ⋯
i : Fin (m + 1)
⊢ ↑(((s.restrict S hS).face h).points i) = ↑(((s.face h).restrict S ⋯).points i)

Tactic:
rw [restrict_points_coe]

Goal state after:
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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
this : Nonempty ↥S := Nonempty.map (⇑(AffineSubspace.inclusion hS)) inferInstance
i : Fin (m + 1)
⊢ ↑(((s.restrict S hS).face h).points i) = (s.face h).points i
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
ha : AffineIndependent k p
s₁ s₂ : Set ι
⊢ vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂) → s₁ = s₂ ∨ s₁.Subsingleton ∧ s₂.Subsingleton

Tactic:
intro h
    by_cases he : s₁ = s₂
    · simp [he]
    simp only [he, false_or]
    by_cases h₁ : s₁.Subsingleton
    · rw [vectorSpan_of_subsingleton _ (h₁.image _), eq_comm, vectorSpan_eq_bot_iff_subsingleton]
        at h
      exact ⟨h₁, Set.subsingleton_of_image ha.injective s₂ h⟩
    by_cases h₂ : s₂.Subsingleton
    · rw [vectorSpan_of_subsingleton _ (h₂.image _), vectorSpan_eq_bot_iff_subsingleton]
        at h
      exact ⟨Set.subsingleton_of_image ha.injective s₁ h, h₂⟩
    simp only [h₁, h₂, false_and]
    have hi : (∃ i ∈ s₁, i ∉ s₂) ∨ ∃ i ∈ s₂, i ∉ s₁ := by grind
    rcases hi with ⟨i, his₁, his₂⟩ | ⟨i, his₂, his₁⟩
    · exact ha.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton his₁ his₂ h₁ h
    · exact ha.vectorSpan_image_ne_of_mem_of_notMem_of_not_subsingleton his₂ his₁ h₂ h.symm

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✝ : ZeroLEOneClass k
s : Simplex k P 0
⊢ 1 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ 1 i ∧ 1 i ≤ 1) ∧ (affineCombination k {0} s.points) 1 = s.points 0

Tactic:
by simp [affineCombination_apply]

Goal state after: