mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ |(x ^ 2⁻¹).im| = √((‖x‖ - x.re) / 2)

Tactic:
rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : IsStrictOrderedRing R
M : Type u_2
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
S : Type u_5
inst✝⁶ : CommSemiring S
inst✝⁵ : PartialOrder S
inst✝⁴ : Algebra S R
inst✝³ : Module S M
inst✝² : SMulPosMono S R
inst✝¹ : IsScalarTower S R M
a : S
v : M
h✝ : 0 ≤ a
h : 0 < (algebraMap S R) a
inst✝ : Nontrivial R
⊢ 0 < 1

Tactic:
exact zero_lt_one

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ p₃ : P
⊢ midpoint R p₁ p₂ -ᵥ midpoint R p₁ p₃ = ⅟2 • (p₂ -ᵥ p₃)

Tactic:
rw [midpoint_vsub_midpoint, vsub_self, midpoint_eq_smul_add, zero_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.inl.inr.inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 = 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)

pp: case neg.refine_2.inr.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)

pp: case neg.refine_2.inr.inr.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)

pp: case neg.refine_2.inr.inr.inr.inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
· exfalso
      simp [hm0, hy, hm1.ne.symm] at hm

Goal state after:
case neg.refine_2.inr.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)

case neg.refine_2.inr.inr.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 = 0
⊢ SameRay R x y ∨ SameRay R x (-y)

case neg.refine_2.inr.inr.inr.inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
⊢ [c -[𝕜] x] ∩ [c -[𝕜] y] ⊆ {c}

Tactic:
intro z

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
⊢ z ∈ [c -[𝕜] x] ∩ [c -[𝕜] y] → z ∈ {c}
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝⁴ : (i : ι) → AddCommGroup (φv i)
inst✝³ : (i : ι) → Module k (φv i)
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst✝ : Nonempty ι
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
⊢ f = g

Tactic:
by
  apply pi_ext_zero h
  inhabit ι
  rw [← Pi.single_zero default]
  apply h

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y -[𝕜] z] ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

Tactic:
by
  constructor
  · rintro ⟨a, b, ha, hb, hab, rfl⟩
    use a, b, ha, hb
    simp [*]
  · rintro ⟨a, b, ha, hb, hab, rfl⟩
    refine ⟨a / (a + b), b / (a + b), by positivity, by positivity, ?_, rfl⟩
    rw [← add_div, div_self hab.ne']

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + y) (s + t)

Tactic:
rw [← add_image_prod]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + y) ((fun x ↦ x.1 + x.2) '' s ×ˢ t)
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (z + x) s
y : E
hy : y ∈ (fun x ↦ z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ (fun x ↦ z + x) ⁻¹' s

Tactic:
have h := hs hy ha hb hab

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (z + x) s
y : E
hy : y ∈ (fun x ↦ z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : a • (z + x) + b • (fun x ↦ z + x) y ∈ s
⊢ a • x + b • y ∈ (fun x ↦ z + x) ⁻¹' s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x y : E
h : x ≤ y
⊢ [x -[𝕜] y] ⊆ Icc x y

Tactic:
by
  rintro z ⟨a, b, ha, hb, hab, rfl⟩
  constructor
  · calc
      x = a • x + b • x := (Convex.combo_self hab _).symm
      _ ≤ a • x + b • y := by gcongr
  · calc
      a • x + b • y ≤ a • y + b • y := by gcongr
      _ = y := Convex.combo_self hab _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s + t)

Tactic:
rw [← add_image_prod]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 ((fun x ↦ x.1 + x.2) '' s ×ˢ t)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
h : ↑s.direction = s
⊢ 0 ∈ s

Tactic:
← h

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
h : ↑s.direction = s
⊢ 0 ∈ ↑s.direction
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ s

Tactic:
exact hs hx hy (sub_nonneg_of_le ht.2) ht.1 (sub_add_cancel _ _)

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

Goal state before:
pp: case a
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
⊢ (affineSpan k s).direction ≤ vectorSpan k s

pp: case a
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
⊢ vectorSpan k s ≤ (affineSpan k s).direction

Tactic:
· refine Submodule.span_le.2 ?_
    rintro v ⟨p₁, ⟨p₂, hp₂, v₁, hv₁, hp₁⟩, p₃, ⟨p₄, hp₄, v₂, hv₂, hp₃⟩, rfl⟩
    simp only [SetLike.mem_coe]
    rw [hp₁, hp₃, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc]
    exact
      (vectorSpan k s).sub_mem ((vectorSpan k s).add_mem hv₁ (vsub_mem_vectorSpan k hp₂ hp₄)) hv₂

Goal state after:
case a
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
⊢ vectorSpan k s ≤ (affineSpan k s).direction
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : (convexHull 𝕜) s = ∅
⊢ s ⊆ ∅

Tactic:
← h

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : (convexHull 𝕜) s = ∅
⊢ s ⊆ (convexHull 𝕜) 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
⊢ affineSpan k (insert p ↑(affineSpan k ps)) = affineSpan k (insert p ps)

Tactic:
rw [Set.insert_eq, Set.insert_eq, span_union, span_union, affineSpan_coe]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h✝ }
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i ↦ (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i ↦ i.1 ×ˢ i.2
⊢ Absorbs 𝕜 U s

Tactic:
rcases h.basis_left h' U hU with ⟨x, hx, h''⟩

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h✝ }
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' : (𝓝 (0, 0)).HasBasis (fun i ↦ (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2) fun i ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx : (x.1 ∈ 𝓝 0 ∧ Balanced 𝕜 x.1) ∧ x.2 ∈ 𝓝 0 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun x ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
⊢ Absorbs 𝕜 U s
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : IsDomain 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module.IsTorsionFree 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 ((fun z ↦ 0) ⁻¹' s)

Tactic:
preimage_const

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : IsDomain 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module.IsTorsionFree 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (if 0 ∈ s then univ else ∅)
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) = ⊤
⊢ ⊤ ≤ Submodule.span k ((fun x ↦ x -ᵥ p) '' ({p} ∪ (fun v ↦ v +ᵥ p) '' s))

Tactic:
← h

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) = ⊤
⊢ Submodule.span k (range Subtype.val) ≤ Submodule.span k ((fun x ↦ x -ᵥ p) '' ({p} ∪ (fun v ↦ v +ᵥ p) '' s))
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
⊢ (s.weightedVSub p) w = ∑ i ∈ s, w i • (p i -ᵥ Classical.choice ⋯)

Tactic:
simp [weightedVSub]

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

Goal state before:
pp: case h
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
⊢ t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s

Tactic:
exact s.smul_vsub_vadd_mem t h₁ h₂ h₃

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ x' ≠ y'

Tactic:
← f.injective.ne_iff,

Goal state after:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ 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
p0 : P
s : Set ι
p : ι → P
⊢ (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs p) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = 1 ∧ p0 = (affineCombination k fs fun i ↦ p ↑i) w

Tactic:
by
  simp_rw [affineCombination_apply, eq_vadd_iff_vsub_eq]
  exact eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ x' ≠ y'

Tactic:
← f.injective.ne_iff,

Goal state after:
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
⊢ 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 ι
V₂ : Type u_6
P₂ : Type u_7
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : s.sum w = 1
f : P →ᵃ[k] P₂
b : P
b₂ : P₂
⊢ f ((s.weightedVSubOfPoint p b) w +ᵥ b) = (s.weightedVSubOfPoint (⇑f ∘ p) (f b)) w +ᵥ f b

Tactic:
simp only [weightedVSubOfPoint_apply, RingHom.id_apply, AffineMap.map_vadd, map_smulₛₗ,
    AffineMap.linearMap_vsub, map_sum, Function.comp_apply]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr.refine_1
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q✝ : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
i : ↑s
⊢ ∀ x_1 ∈ range fun i ↦ (↑i).toFun x, x_1 ≤ q x

Tactic:
forall_mem_range

Goal state after:
case inr.refine_1
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q✝ : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
i : ↑s
⊢ ∀ (i : { x // x ∈ s }), (↑i).toFun x ≤ q x
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr.refine_2
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q✝ : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
i : ↑s
⊢ ∀ x ∈ range fun i ↦ (↑i).toFun y, x ≤ q y

Tactic:
forall_mem_range

Goal state after:
case inr.refine_2
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q✝ : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
i : ↑s
⊢ ∀ (i : { x // x ∈ s }), (↑i).toFun y ≤ q y
Module: Mathlib.LinearAlgebra.AffineSpace.Centroid

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
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Invertible 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ centroid k {i₁, i₂} p = 2⁻¹ • (p i₂ -ᵥ p i₁) +ᵥ p i₁

Tactic:
· have hc : (#{i₁, i₂} : k) ≠ 0 := by
      rw [card_insert_of_notMem (notMem_singleton.2 h), card_singleton]
      simpa using Invertible.ne_zero _
    rw [centroid_def,
      affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _
        (sum_centroidWeights_eq_one_of_cast_card_ne_zero _ hc) (p i₁)]
    simp [h, one_add_one_eq_two]

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

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∉ s
w : ι → k
hw : s.sum w = 1
⊢ (b.coord i) ((Finset.affineCombination k s ⇑b) w) = 0

Tactic:
classical simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_false,
      mul_boole, hw, Function.comp_apply, smul_eq_mul, s.sum_ite_eq,
      s.map_affineCombination b w hw]

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

Goal state before:
pp: case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i ∈ s, w2 i = 1
hw2s : (affineCombination k s p) w2 = p i0
ha : (↑s).indicator w2 = (↑s).indicator w1
⊢ w i0 = 0

Tactic:
have hws : w2 i0 - w1 i0 = 0 := by
        rw [← Finset.mem_coe] at hi0
        rw [← Set.indicator_of_mem hi0 w2, ← Set.indicator_of_mem hi0 w1, ha, sub_self]

Goal state after:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
i0 : ι
hi0 : i0 ∈ s
w1 : ι → k := update (const ι 0) i0 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (affineCombination k s p) w1 = p i0
w2 : ι → k := w + w1
hw2 : ∑ i ∈ s, w2 i = 1
hw2s : (affineCombination k s p) w2 = p i0
ha : (↑s).indicator w2 = (↑s).indicator w1
hws : w2 i0 - w1 i0 = 0
⊢ w i0 = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case e'_2.e'_6
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 : ι
hi : i ∈ fs₁ \ fs₂
⊢ w₁ i = 0

Tactic:
← Set.indicator_of_mem (s := ↑fs₁) (by grind) w₁,

Goal state after:
case e'_2.e'_6
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 : ι
hi : i ∈ fs₁ \ fs₂
⊢ (↑fs₁).indicator w₁ i = 0
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: 𝕜 : Type u_2
ι : Type u_1
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ι
inst✝ : IsOrderedAddMonoid 𝕜
f : ι → 𝕜
h : f ∈ stdSimplex 𝕜 ι
⊢ f ∈ Icc 0 1

Tactic:
rw [← pi_univ_Icc, univ_pi_eq_iInter, mem_iInter]

Goal state after:
𝕜 : Type u_2
ι : Type u_1
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Fintype ι
inst✝ : IsOrderedAddMonoid 𝕜
f : ι → 𝕜
h : f ∈ stdSimplex 𝕜 ι
⊢ ∀ (i : ι), f ∈ Function.eval i ⁻¹' Icc (0 i) (1 i)
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: case refine_1
R : Type u_1
ι : Type u_2
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ (fun i j ↦ if i = j then 1 else 0) i ∈ stdSimplex R ι

Tactic:
exact ite_eq_mem_stdSimplex R i

Goal state after: