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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
⊢ StarConvex 𝕜 (f x) (⇑f '' s)

Tactic:
by
  rintro y ⟨y', ⟨hy', hy'f⟩⟩ a b ha hb hab
  refine ⟨a • x + b • y', ⟨hs hy' ha hb hab, ?_⟩⟩
  rw [Convex.combo_affine_apply hab, hy'f]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ ⇑f ⁻¹' s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⇑f ⁻¹' s

Tactic:
rw [mem_preimage, f.map_add, LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ ⇑f ⁻¹' s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ s
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
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
⊢ ↑s.direction = (fun x ↦ p -ᵥ x) '' ↑s

Tactic:
ext v
  rw [SetLike.mem_coe, ← Submodule.neg_mem_iff, ← SetLike.mem_coe,
    coe_direction_eq_vsub_set_right hp, Set.mem_image, Set.mem_image]
  conv_lhs =>
    congr
    ext
    rw [← neg_vsub_eq_vsub_rev, neg_inj]

Goal state after:
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
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
v : V
⊢ v ∈ (s₁ ⊓ s₂).direction ↔ v +ᵥ p ∈ s₁ ∧ v ∈ s₂.direction

Tactic:
← vadd_mem_iff_mem_direction v 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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
v : V
⊢ v ∈ (s₁ ⊓ s₂).direction ↔ v +ᵥ p ∈ s₁ ∧ v +ᵥ p ∈ s₂
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
inst✝ : AffineSpace V P
p : P
ps : Set P
h : p ∈ affineSpan k ps
⊢ affineSpan k (insert p ps) = affineSpan k ps

Tactic:
← mem_coe

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
p : P
ps : Set P
h : p ∈ ↑(affineSpan k ps)
⊢ affineSpan k (insert p ps) = affineSpan k ps
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
this : map (⇑σ) (𝓝 0) = 𝓝 0
hf₀ : Tendsto (⇑f) (𝓝 0) (𝓝 0)
⊢ IsVonNBounded 𝕜₂ (⇑f '' s)

Tactic:
simp only [isVonNBounded_iff_tendsto_smallSets_nhds, ← this, tendsto_map'_iff] at hs ⊢

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
f : E →SL[σ] F
this : map (⇑σ) (𝓝 0) = 𝓝 0
hf₀ : Tendsto (⇑f) (𝓝 0) (𝓝 0)
hs : Tendsto (fun x ↦ x • s) (𝓝 0) (𝓝 0).smallSets
⊢ Tendsto ((fun x ↦ x • ⇑f '' s) ∘ ⇑σ) (𝓝 0) (𝓝 0).smallSets
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case convert_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
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ range Subtype.val ⊆ (fun x ↦ x -ᵥ p) '' ({p} ∪ (fun v ↦ v +ᵥ p) '' s)

Tactic:
rintro v ⟨v', rfl⟩

Goal state after:
case convert_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
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
v' : { x // x ∈ s }
⊢ ↑v' ∈ (fun x ↦ x -ᵥ p) '' ({p} ∪ (fun v ↦ v +ᵥ p) '' s)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ (affineSpan k (↑s₁ ∪ ↑s₂)).direction ≤ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
← mem_coe

Goal state after:
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
s₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
⊢ (affineSpan k (↑s₁ ∪ ↑s₂)).direction ≤ s₁.direction ⊔ s₂.direction ⊔ k ∙ (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✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ s
p₂ p : P
⊢ p ∈ affineSpan k (insert p₂ ↑s) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
← mem_coe

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
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ p ∈ affineSpan k (insert p₂ ↑s) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p) w -ᵥ p i = 0

Tactic:
← hw,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
hw : (s.weightedVSub p) w = 0
i : ι
inst✝ : DecidablePred fun x ↦ x ≠ i
his : i ∈ s
hwi : w i = -1
⊢ (affineCombination k ({x ∈ s | x ≠ i}) p) w -ᵥ p i = (s.weightedVSub p) w
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 E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
⊢ (∀ ⦃x : E⦄,
      x ∈ s →
        ∀ ⦃y : E⦄,
          y ∈ s →
            x ≠ y →
              ∀ ⦃a b : 𝕜⦄,
                0 < a → 0 < b → f ((a / (a + b)) • x + (b / (a + b)) • y) < (a / (a + b)) • f x + (b / (a + b)) • f y) →
    ∀ ⦃x : E⦄,
      x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y

Tactic:
intro h x hx y hy hxy a b ha hb hab
    simpa [hab, zero_lt_one] using h hx hy hxy ha hb

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 • (p ⊓ q) x✝ = (r • p ⊓ r • q) x✝

Tactic:
inf_apply,

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 • ⨅ u, p u + q (x✝ - u) = ⨅ u, (r • p) u + (r • q) (x✝ - u)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
c : k
⊢ affineCombinationLineMapWeights i i c = Pi.single i 1

Tactic:
simp [affineCombinationLineMapWeights]

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

Goal state before:
pp: case h
ι : 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)
⊢ ∃ w, ∑ i ∈ insert i0 l.support, w i = 0 ∧ v = ((insert i0 l.support).weightedVSub p) w

Tactic:
use w

Goal state after:
case h
ι : 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 := ⋯
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
⊢ ∑ i ∈ insert i0 l.support, w i = 0 ∧ v = ((insert i0 l.support).weightedVSub p) w
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case neg
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₂
⊢ False

Tactic:
have h₁₂ : (r₁ : k) • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃} := by
      rw [hr₁, hr₂, add_comm, vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, neg_mem_iff, ← hr₃]
      exact smul_vsub_mem_vectorSpan_pair _ _ _

Goal state after:
case neg
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₃}
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.Pointwise

Goal state before:
pp: 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₁
⊢ map f (v +ᵥ s) = f.linear v +ᵥ map f s

Tactic:
rw [pointwise_vadd_eq_map, pointwise_vadd_eq_map, map_map, map_map]

Goal state after:
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₁
⊢ map (f.comp ↑(AffineEquiv.constVAdd k P₁ v)) s = map ((↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f) s
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' : ∑ x ∈ Finset.subtype (Membership.mem s') s, w ↑x = 1
i : ι
hi : i ∈ s
⊢ w i = (↑({x ∈ s | x ∈ s'})).indicator w i

Tactic:
simp_all [Set.indicator_apply]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
⊢ ∀ (p : (ι → P) × P) (v : (ι → V) × V),
    (s.weightedVSubOfPoint (v +ᵥ p).1 (v +ᵥ p).2) w =
      (∑ i ∈ s, w i • (LinearMap.proj i ∘ₗ LinearMap.fst k (ι → V) V - LinearMap.snd k (ι → V) V)) v +ᵥ
        (s.weightedVSubOfPoint p.1 p.2) w

Tactic:
by
    rintro ⟨p, b⟩ ⟨v, b'⟩
    simp [LinearMap.sum_apply, Finset.weightedVSubOfPoint, vsub_vadd_eq_vsub_sub,
     vadd_vsub_assoc, ← sub_add_eq_add_sub, smul_add, Finset.sum_add_distrib]

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst✝⁵ : AddCommGroup V
inst✝⁴ : Ring k
inst✝³ : Module k V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
⊢ (a • b).coord i = (b.coord i).comp (↑(DistribMulAction.toLinearEquiv k V a).symm).toAffineMap

Tactic:
ext v; simp [map_sub, coord]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case a
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
ι : Sort u_12
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓝 0 ≤ 𝓝 0

Tactic:
rw [← @comap_norm_nhds_zero E p.toAddGroupSeminorm.toSeminormedAddGroup, ← tendsto_iff_comap]
    suffices Continuous p from this.tendsto' 0 _ (map_zero p)
    rcases h₁ with ⟨r, hr⟩
    exact p.continuous' hr

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : ι → k := fun i ↦ if h : ∃ i2, f i2 = i then w h.choose else 0
hw' : ∀ (i2 : ι2), w' (f i2) = w i2
⊢ ∑ i ∈ fs', w' i = 0

Tactic:
← hw,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
fs : Finset ι2
w : ι2 → k
hw : ∑ i ∈ fs, w i = 0
hs : (fs.weightedVSub (p ∘ ⇑f)) w = 0
i0 : ι2
hi0 : i0 ∈ fs
fs' : Finset ι := map f fs
w' : ι → k := fun i ↦ if h : ∃ i2, f i2 = i then w h.choose else 0
hw' : ∀ (i2 : ι2), w' (f i2) = w i2
⊢ ∑ i ∈ fs', w' i = ∑ i ∈ fs, w i
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
⊢ w i < 1

Tactic:
← hw,

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
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
⊢ w i < ∑ i, w i
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 : ℕ
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
⊢ w i ≤ 1

Tactic:
← hw,

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
inst✝¹ : PartialOrder k
inst✝ : IsOrderedAddMonoid 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
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
⊢ w i ≤ ∑ i, w i
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case h₁
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✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
h : (affineCombination k univ s.points) w ∉ s.interior
⊢ (affineCombination k univ s.points) w ∈ ⋃ i, (s.faceOpposite i).closedInterior

Tactic:
affineCombination_mem_interior_iff hw1,

Goal state after:
case h₁
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✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
h : ¬∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1
⊢ (affineCombination k univ s.points) w ∈ ⋃ i, (s.faceOpposite i).closedInterior
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case inr
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✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
i : Fin (n + 1)
hi : 1 ≤ w i
⊢ ∃ j, w j = 0

Tactic:
have hi1 : w i = 1 := le_antisymm (hp i).2 hi
        rw [← hi1, ← Finset.sum_erase_add _ _ (show i ∈ Finset.univ by simp), add_eq_right,
          Finset.sum_eq_zero_iff_of_nonneg (fun j _ ↦ (hp j).1)] at hw1
        exact ⟨i + 1, hw1 _ (by simp)⟩

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

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

Tactic:
by
  simp_rw [sUnion_eq_biUnion, closure_iUnion]

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: α : Type u_3
inst✝ : TopologicalSpace α
hα : ∀ (a : α), 𝓝 a = 𝓟 (nhdsKer {a})
⊢ AlexandrovDiscrete α

Tactic:
simp only [alexandrovDiscrete_iff_isClosed, isClosed_iff_clusterPt, ClusterPt, funext hα,
      inf_principal, principal_neBot_iff]

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

Goal state before:
pp: case 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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : ∑ y ∈ t₁, w₁ y = 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : ∑ y ∈ t₂, w₂ y = 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : E → R := fun x ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : ∑ i ∈ s, w i = 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ x ∈ t₁, x ∉ t₂ → w₁ x = 0
⊢ ∀ y ∈ t₁ ∩ t₂, 0 ≤ w₁ y

Tactic:
simp only [and_imp, Finset.mem_inter]
    exact fun y hy₁ _ ↦ h₁w₁ y hy₁

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

Goal state before:
pp: case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ U

Tactic:
rcases comp_open_symm_mem_uniformity_sets hU with ⟨V, hV, hVo, hVsymm, hVU⟩

Goal state after:
case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a ↦ (F i) a) n y) ∈ U
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup F
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NontriviallyNormedField 𝕜₃
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
C : ℝ
h : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖
x : E
⊢ max (C * ‖x‖) 0 = max C 0 * ‖x‖

Tactic:
rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]

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

Goal state before:
pp: case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
hf : 0 < ‖f‖
x : E
⊢ ‖c x‖ ≤ ‖smulRight c f‖ * ‖x‖ / ‖f‖

Tactic:
le_div_iff₀ hf

Goal state after:
case refine_2.inr
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
hf : 0 < ‖f‖
x : E
⊢ ‖c x‖ * ‖f‖ ≤ ‖smulRight c f‖ * ‖x‖
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
c : StrongDual 𝕜 E
f : Fₗ
⊢ ‖c‖ * ‖f‖ ≤ ‖smulRight c f‖

Tactic:
obtain hf | hf := (norm_nonneg f).eq_or_lt'
    · simp [hf]
    · rw [← le_div_iff₀ hf]
      refine opNorm_le_bound _ (by positivity) fun x => ?_
      rw [div_mul_eq_mul_div, le_div_iff₀ hf]
      calc
        ‖c x‖ * ‖f‖ = ‖c x • f‖ := (norm_smul _ _).symm
        _ = ‖smulRight c f x‖ := rfl
        _ ≤ ‖smulRight c f‖ * ‖x‖ := le_opNorm _ _

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ[t | s] * μ s + μ[t | sᶜ] * μ sᶜ = μ t

Tactic:
by
  rw [cond_mul_eq_inter hms, cond_mul_eq_inter hms.compl, Set.inter_comm _ t,
    Set.inter_comm _ t]
  exact measure_inter_add_sdiff t hms

Goal state after: