mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2) + ↑(π / 2) - ↑θ - ↑ψ = 0
⊢ ↑θ + ↑ψ = ↑π

Tactic:
← coe_add,

Goal state after:
case mp.inr
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 + π / 2) - ↑θ - ↑ψ = 0
⊢ ↑θ + ↑ψ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case hle
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ ↑n * x.arg ≤ π

Tactic:
← le_div_iff₀' (Nat.cast_pos.2 h₀.bot_lt)

Goal state after:
case hle
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ x.arg ≤ π / ↑n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x n : ℂ
⊢ x⁻¹ ^ n = if x.arg = π then (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else (x ^ n)⁻¹

Tactic:
Complex.cpow_def,

Goal state after:
x n : ℂ
⊢ (if x⁻¹ = 0 then if n = 0 then 1 else 0 else cexp (log x⁻¹ * n)) =
    if x.arg = π then
      (starRingEnd ℂ) (if x = 0 then if (starRingEnd ℂ) n = 0 then 1 else 0 else cexp (log x * (starRingEnd ℂ) n))⁻¹
    else (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (θ - ↑(π / 2)).cos = θ.sin

Tactic:
by
  induction θ using Real.Angle.induction_on
  exact Real.cos_sub_pi_div_two _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
x✝ : ℝ
⊢ (↑x✝ + ↑π).tan = (↑x✝).tan

Tactic:
← coe_add,

Goal state after:
case h
x✝ : ℝ
⊢ (↑(x✝ + π)).tan = (↑x✝).tan
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
h : 2 • (↑x✝¹ + ↑x✝) = ↑π
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
← coe_add,

Goal state after:
case h.h
x✝¹ x✝ : ℝ
h : 2 • ↑(x✝¹ + x✝) = ↑π
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
⊢ (↑x ^ ↑y).re = rexp (log x * y) * cos (y * π)

Tactic:
Complex.cpow_def,

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
⊢ (if ↑x = 0 then if ↑y = 0 then 1 else 0 else Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y) * cos (y * π)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x y : ℝ
hx : 0 ≤ x
⊢ |x ^ y| ≤ |x| ^ y

pp: case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
· rw [abs_rpow_of_nonneg hx]

Goal state after:
case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
by
  suffices ((θ.toReal + ψ.toReal : ℝ) : Angle).toReal = θ.toReal + ψ.toReal by simpa using this
  rw [toReal_coe_eq_self_iff]
  grind [toReal_mem_Ioc, toReal_neg_iff_sign_neg, toReal_mem_Ioo_iff_sign_pos]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ y ^ z ≤ x ^ z

Tactic:
rw [← inv_le_inv₀, ← rpow_neg, ← rpow_neg]

Goal state after:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ x ^ (-z) ≤ y ^ (-z)

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ y

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

case ha
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < x ^ z

case hb
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inl
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) p

Tactic:
rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
    refine ContinuousAt.mul ?_ (by fun_prop)
    · refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
      exact (continuousAt_log hp.ne).comp continuous_fst.continuousAt

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z

Tactic:
rify at *

Goal state after:
x : ℝ≥0
y z : ℝ
hx₀ : 0 < ↑x
hx₁ : ↑x ≠ 1
⊢ ↑x ^ y = ↑x ^ z ↔ y = z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inl.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inl.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y < 0
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Goal state after:
case top.inr.inl.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z < 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inl.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inl.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : y = 0
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z < 0
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Goal state after:
case top.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z < 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z = 0
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Goal state after:
case top.inr.inr.inr.inl
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : z = 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inr.inr.inr
y z : ℝ
hyz : y ≤ z
hx : 1 ≤ ∞
Hy : 0 < y
Hz : 0 < z
⊢ ∞ ^ y ≤ ∞ ^ z

Tactic:
simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : 0 < z
⊢ 1 ≤ x ^ z

Tactic:
by
  cases x
  · simp [top_rpow_of_pos hz]
  · simp only [one_le_coe_iff] at hx
    simp [← coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.one_le_rpow hx (le_of_lt hz)]

Goal state after:
Module: Mathlib.Algebra.Order.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : Semiring β
inst✝³ : PartialOrder β
inst✝² : Algebra α β
inst✝¹ : ZeroLEOneClass β
inst✝ : SMulPosMono α β
⊢ Monotone ⇑(algebraMap α β)

Tactic:
simpa [Algebra.smul_def] using smul_one_mono (α := α) β

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
x y : 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
h : SameRay R x y
ha : 0 ≤ a
hy : y = 0
⊢ a • y = 0

Tactic:
hy,

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
x y : 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
h : SameRay R x y
ha : 0 ≤ a
hy : y = 0
⊢ a • 0 = 0
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
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hy : y = 0
⊢ f y = 0

Tactic:
hy,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x y : M
f : M →ₗ[R] N
h : SameRay R x y
hy : y = 0
⊢ f 0 = 0
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
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)

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

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

Goal state before:
pp: R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : AffineSpace V1 P1
inst✝⁹ : AddCommGroup V2
inst✝⁸ : AffineSpace V2 P2
inst✝⁷ : AddCommGroup V3
inst✝⁶ : AffineSpace V3 P3
inst✝⁵ : Module k V1
inst✝⁴ : Module k V2
inst✝³ : Module k V3
inst✝² : Semiring R
inst✝¹ : Module R V2
inst✝ : SMulCommClass k R V2
v : V2
f : V1 →ₗ[k] V2
⊢ (fun f ↦ (f 0, f.linear)) ((fun p ↦ p.2.toAffineMap + const k V1 p.1) (v, f)) = (v, f)

Tactic:
ext <;> simp [const_linear]

Goal state after:
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✝² : IsOrderedCancelAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
⊢ openSegment 𝕜 x y ⊆ Ioo x y

Tactic:
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.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
h : (↑s).Nonempty
⊢ 0 ∈ ↑s -ᵥ ↑s

Tactic:
obtain ⟨p, hp⟩ := h
    exact vsub_self p ▸ vsub_mem_vsub hp hp

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

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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
⊢ p ∈ s₂ → p ∈ s₁

Tactic:
· intro hp
    rw [← vsub_vadd p hn.some]
    refine vadd_mem_of_mem_direction ?_ hq1
    rw [hd]
    exact vsub_mem_direction hp hq2

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

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
x₁ x₂ : E
y : F
⊢ (fun x ↦ (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y)

Tactic:
openSegment_eq_image₂,

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
x₁ x₂ : E
y : F
⊢ (fun x ↦ (x, y)) '' (fun p ↦ p.1 • x₁ + p.2 • x₂) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    openSegment 𝕜 (x₁, y) (x₂, y)
Module: Mathlib.Analysis.Convex.Segment

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
x₁ x₂ : E
y : F
⊢ (fun x ↦ (x, y)) '' (fun p ↦ p.1 • x₁ + p.2 • x₂) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    openSegment 𝕜 (x₁, y) (x₂, y)

Tactic:
openSegment_eq_image₂,

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
x₁ x₂ : E
y : F
⊢ (fun x ↦ (x, y)) '' (fun p ↦ p.1 • x₁ + p.2 • x₂) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
Module: Mathlib.Analysis.Convex.Segment

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
x : E
y₁ y₂ : F
⊢ (fun y ↦ (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)

Tactic:
openSegment_eq_image₂,

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
x : E
y₁ y₂ : F
⊢ (fun y ↦ (x, y)) '' (fun p ↦ p.1 • y₁ + p.2 • y₂) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    openSegment 𝕜 (x, y₁) (x, y₂)
Module: Mathlib.Analysis.Convex.Segment

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
x : E
y₁ y₂ : F
⊢ (fun y ↦ (x, y)) '' (fun p ↦ p.1 • y₁ + p.2 • y₂) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    openSegment 𝕜 (x, y₁) (x, y₂)

Tactic:
openSegment_eq_image₂,

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
x : E
y₁ y₂ : F
⊢ (fun y ↦ (x, y)) '' (fun p ↦ p.1 • y₁ + p.2 • y₂) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module 𝕜 (M i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
⊢ update y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (update y i x₁) (update y i x₂)

Tactic:
openSegment_eq_image₂,

Goal state after:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module 𝕜 (M i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
⊢ update y i '' (fun p ↦ p.1 • x₁ + p.2 • x₂) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    openSegment 𝕜 (update y i x₁) (update y i x₂)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module 𝕜 (M i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
⊢ update y i '' (fun p ↦ p.1 • x₁ + p.2 • x₂) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    openSegment 𝕜 (update y i x₁) (update y i x₂)

Tactic:
openSegment_eq_image₂,

Goal state after:
𝕜 : Type u_1
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module 𝕜 (M i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : M i
y : (i : ι) → M i
⊢ update y i '' (fun p ↦ p.1 • x₁ + p.2 • x₂) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • update y i x₁ + p.2 • update y i x₂) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ Balanced 𝕜 (balancedHull 𝕜 s)

Tactic:
by
  intro a ha
  simp_rw [balancedHull, smul_set_iUnion₂, subset_def, mem_iUnion₂]
  rintro x ⟨r, hr, hx⟩
  rw [← smul_assoc] at hx
  exact ⟨a • r, (norm_mul_le _ _).trans (mul_le_one₀ ha (norm_nonneg r) hr), hx⟩

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

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : NormedDivisionRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
s : Set E
inst✝⁴ : NormedRing 𝕝
inst✝³ : Module 𝕜 𝕝
inst✝² : NormSMulClass 𝕜 𝕝
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ ‖b⁻¹ • a‖ ≤ 1

Tactic:
norm_smul,

Goal state after:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : NormedDivisionRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
s : Set E
inst✝⁴ : NormedRing 𝕝
inst✝³ : Module 𝕜 𝕝
inst✝² : NormSMulClass 𝕜 𝕝
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ ‖b⁻¹‖ * ‖a‖ ≤ 1
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ ‖a⁻¹ • b‖ ≤ 1

Tactic:
norm_smul,

Goal state after:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ ‖a⁻¹‖ * ‖b‖ ≤ 1
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ 1 ≤ ‖a⁻¹ • r‖

Tactic:
norm_smul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ 1 ≤ ‖a⁻¹‖ * ‖r‖
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
ha : ‖0‖ ≤ 1
⊢ 0 • insert 0 (interior A) ⊆ insert 0 (interior A)

Tactic:
rw [zero_smul_set]
    exacts [subset_union_left, ⟨0, Or.inl rfl⟩]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : AddGroup E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : DistribMulAction 𝕜 E
s : Set E
hs : IsVonNBounded 𝕜 s
U : Set E
hU : U ∈ 𝓝 0
⊢ Absorbs 𝕜 (- -U) (-s)

Tactic:
exact (hs <| neg_mem_nhds_zero _ hU).neg_neg

Goal state after:
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 : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p₁ -ᵥ p - (p₂ -ᵥ p) = v
⊢ ∀ (p_1 : Submodule k V), (fun x ↦ x -ᵥ p) '' s ⊆ ↑p_1 → p₁ -ᵥ p - (p₂ -ᵥ p) ∈ p_1

Tactic:
exact fun m hm => Submodule.sub_mem _ (hm ⟨p₁, hp₁, rfl⟩) (hm ⟨p₂, hp₂, rfl⟩)

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr
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
p q : Seminorm 𝕜 E
a : 𝕜
x : E
ha : a ≠ 0
⊢ ⨅ u, p u + q (a • x - u) = ⨅ i, p (a • i) + q (a • x - a • i)

Tactic:
refine
          Function.Surjective.iInf_congr ((a⁻¹ • ·) : E → E)
            (fun u => ⟨a • u, inv_smul_smul₀ ha u⟩) fun u => ?_

Goal state after:
case inr
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
p q : Seminorm 𝕜 E
a : 𝕜
x : E
ha : a ≠ 0
u : E
⊢ p (a • a⁻¹ • u) + q (a • x - a • a⁻¹ • u) = p u + q (a • x - u)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case inr
ι : 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 : ι
⊢ (s.weightedVSub p) w ∈ vectorSpan k (Set.range p)

Tactic:
rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ,
        Finsupp.mem_span_image_iff_linearCombination,
        Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p h (p i0),
        Finset.weightedVSubOfPoint_apply]

Goal state after:
case inr
ι : 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 : ι
⊢ ∃ l ∈ Finsupp.supported k k Set.univ,
    (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = ∑ i ∈ s, w i • (p i -ᵥ p i0)
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)

Tactic:
apply Finset.sum_congr rfl

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 := ⋯
hwx : ∀ (i : ι), w' i ≠ 0 → i ∈ s
⊢ ∀ x ∈ s, w' x • (p x -ᵥ p i0) = w x • (p x -ᵥ p i0)
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
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSubOfPoint p (p i1)) w = 0
i : ι
hi : i ∈ s
⊢ w i = 0

Tactic:
←
        s.weightedVSubOfPoint_erase w p i1,

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
i1 : ι
h : ∀ (s : Finset { x // x ≠ i1 }) (g : { x // x ≠ i1 } → k), ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : ((s.erase i1).weightedVSubOfPoint p (p i1)) w = 0
i : ι
hi : i ∈ s
⊢ w i = 0