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

Goal state before:
pp: case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : ↑a ≠ 0
hb'' : ↑b ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Tactic:
rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha,
    add_mul, exp_add, ← cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']

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

Goal state before:
pp: a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Tactic:
by
  rcases eq_or_ne r 0 with (rfl | hr)
  · simp only [cpow_zero, mul_one]
  rcases eq_or_lt_of_le ha with (rfl | ha')
  · rw [ofReal_zero, zero_mul, zero_cpow hr, zero_mul]
  rcases eq_or_lt_of_le hb with (rfl | hb')
  · rw [ofReal_zero, mul_zero, zero_cpow hr, mul_zero]
  have ha'' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha'.ne'
  have hb'' : (b : ℂ) ≠ 0 := ofReal_ne_zero.mpr hb'.ne'
  rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha,
    add_mul, exp_add, ← cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']

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

Goal state before:
pp: case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : ↑n * (2 * π) - -1 * π = 0
⊢ ↑θ = ↑ψ

Tactic:
← mul_assoc,

Goal state after:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : ↑n * 2 * π - -1 * π = 0
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(x / y).arg = ↑x.arg - ↑y.arg

Tactic:
rw [div_eq_mul_inv, arg_mul_coe_angle hx (inv_ne_zero hy), arg_inv_coe_angle, sub_eq_add_neg]

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

Goal state before:
pp: θ : Angle
⊢ (↑π - θ).sign = θ.sign

Tactic:
by
  simp [sign_antiperiodic.sub_eq']

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case refine_1
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ContinuousWithinAt (fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π) {z | 0 ≤ z.im} z

pp: case refine_2
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ z.arg = Real.arcsin ((-z).im / ‖z‖) + π

Tactic:
· refine
      (Real.continuousAt_arcsin.comp_continuousWithinAt
            ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
              continuous_norm.continuousWithinAt ?_)).add
        tendsto_const_nhds
    lift z to ℝ using him
    simpa using hre.ne

Goal state after:
case refine_2
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ z.arg = Real.arcsin ((-z).im / ‖z‖) + π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
h : x ≠ 0
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
by_cases hs : x ∈ slitPlane
  · exact Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg hs)
  · rw [← Function.comp_id (((↑) : ℝ → Real.Angle) ∘ arg),
      (funext_iff.2 fun _ => (neg_neg _).symm : (id : ℂ → ℂ) = Neg.neg ∘ Neg.neg), ←
      Function.comp_assoc]
    refine ContinuousAt.comp ?_ continuous_neg.continuousAt
    suffices ContinuousAt (Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π) (-x) by
      rwa [continuousAt_update_of_ne (neg_ne_zero.2 h)] at this
    have ha :
      Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π = fun z =>
        (arg z : Real.Angle) + π := by
      rw [Function.update_eq_iff]
      exact ⟨by simp, fun z hz => arg_neg_coe_angle hz⟩
    rw [ha]
    replace hs := mem_slitPlane_iff.mpr.mt hs
    push Not at hs
    refine
      (Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg (Or.inl ?_))).add
        continuousAt_const
    rw [neg_re, neg_pos]
    exact hs.1.lt_of_ne fun h0 => h (Complex.ext_iff.2 ⟨h0, hs.2⟩)

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

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (↑(rexp (log (-x) * y) * cos (y * π)) + ↑(rexp (log (-x) * y)) * (↑(sin (y * π)) * Complex.I)).re =
    rexp (log x * y) * cos (y * π)

Tactic:
← mul_assoc,

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (↑(rexp (log (-x) * y) * cos (y * π)) + ↑(rexp (log (-x) * y)) * ↑(sin (y * π)) * Complex.I).re =
    rexp (log x * y) * cos (y * π)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x ↦ b ^ x) atTop (𝓝 0)

Tactic:
simp_rw [Real.rpow_def_of_pos hb]
    refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
    exact (log_neg_iff hb).mpr hb₁

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

Goal state before:
pp: case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : ∀ x ∈ cons i s hi, 0 ≤ f x
⊢ a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x

Tactic:
rw [forall_mem_cons] at h

Goal state after:
case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
⊢ a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖x ^ (↑n)⁻¹‖ = ‖x‖ ^ (↑n)⁻¹

Tactic:
rw [← norm_cpow_real]; simp

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

Goal state before:
pp: x : ℝ≥0
⊢ sqrt x = x ^ (1 / 2)

Tactic:
refine NNReal.eq ?_

Goal state after:
x : ℝ≥0
⊢ ↑(sqrt x) = ↑(x ^ (1 / 2))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: p : ℝ × ℝ
hp_fst : p.1 < 0
⊢ (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)

Tactic:
by
  suffices ∀ᶠ x : ℝ × ℝ in 𝓝 p, x.1 < 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [rpow_def_of_neg hx]
  exact IsOpen.eventually_mem (isOpen_lt continuous_fst continuous_const) hp_fst

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

Goal state before:
pp: y : ℝ
hp : 0 < y
A : Tendsto (fun p ↦ rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p ↦ p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ Tendsto (fun p ↦ p.1 ^ p.2) (pure 0 ×ˢ 𝓝 y) (pure 0)

Tactic:
tendsto_pure,

Goal state after:
y : ℝ
hp : 0 < y
A : Tendsto (fun p ↦ rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p ↦ p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ∀ᶠ (x : ℝ × ℝ) in pure 0 ×ˢ 𝓝 y, x.1 ^ x.2 = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case coe
x✝ : ℝ≥0
⊢ ↑x✝ ^ 1 = ↑x✝

Tactic:
change ite _ _ _ = _
    simp only [NNReal.rpow_one, ite_eq_right_iff, top_ne_coe, and_imp]
    exact fun _ => zero_le_one.not_gt

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

Goal state before:
pp: case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (x, y)

Tactic:
have : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop
    refine (continuousAt_cpow (Or.inl ?_)).comp this
    rwa [ofReal_re]

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

Goal state before:
pp: case inl.inl
z : ℝ
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hyz : z ≤ 0
h : 0 = 0 → 0 = 0 → z = 0
⊢ 0 ^ 0 ≤ 0 ^ z

Tactic:
h rfl rfl

Goal state after:
case inl.inl
z : ℝ
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hyz : z ≤ 0
h : 0 = 0 → 0 = 0 → z = 0
⊢ 0 ^ 0 ≤ 0 ^ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr
x : ℝ≥0∞
hx : x ≠ ∞
y z : ℝ
hyz : 0 < y + z
hx' : x ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
· rw [ENNReal.rpow_add _ _ hx' hx]

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

Goal state before:
pp: x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
⊢ x ^ n ≤ y ↔ ↑n * log x ≤ log y

Tactic:
by
  rw [← rpow_le_iff_le_log hx hy, rpow_natCast]

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

Goal state before:
pp: x : ℝ≥0∞
y z : ℝ
hx : 1 < x
hx' : x ≠ ∞
hyz : y < z
⊢ x ^ y < x ^ z

Tactic:
lift x to ℝ≥0 using hx'

Goal state after:
y z : ℝ
hyz : y < z
x : ℝ≥0
hx : 1 < ↑x
⊢ ↑x ^ y < ↑x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
⊢ (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, sin_half_eq_sqrt, ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub,
    mul_one, norm_mul_cos_arg]

Goal state after:
case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.arg

case hr
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 ≤ ↑x✝
⊢ 1 ≤ ↑x✝ ^ z

Tactic:
· 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.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V1
inst✝¹⁰ : Module k V1
inst✝⁹ : AffineSpace V1 P1
inst✝⁸ : AddCommGroup V2
inst✝⁷ : Module k V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P1 →ᵃ[k] V2
p : P1
v : V1
⊢ (-⇑f) (v +ᵥ p) = (-f.linear) v +ᵥ (-⇑f) p

Tactic:
simp [add_comm, map_vadd f]

Goal state after:
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
⊢ False

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

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

Tactic:
← coe_eq_bot_iff,

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
ι : Sort u_4
p₁ p₂ : P
inst✝ : Subsingleton P
s : AffineSubspace k P
⊢ ↑s = ∅ ∨ s = ⊤
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: case inr
𝕜 : 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
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ a • insert 0 (interior A) ⊆ insert 0 (interior A)

Tactic:
· rw [← image_smul, image_insert_eq, smul_zero]
    apply insert_subset_insert
    exact ((isOpenMap_smul₀ h).mapsTo_interior <| hA.smul_mem ha).image_subset

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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
v : V
hv : v ∈ vectorSpan k ↑s
⊢ v +ᵥ p₁ ∈ s

Tactic:
exact vadd_mem_of_mem_direction hv hp₁

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

Goal state before:
pp: E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Balanced ℝ s
x✝ : E
hx : x✝ ∈ s
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ ‖a‖ ≤ 1

Tactic:
rwa [Real.norm_of_nonneg ha₀]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Metric.ball 0 r
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
Metric.nhds_basis_ball.isVonNBounded_iff

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Metric.ball 0 r
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Metric.ball 0 i) s
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ⇑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : f x ≠ f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • y) = a • f x + b • f y

Tactic:
map_add,

Goal state after:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : PartialOrder 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ⇑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : f x ≠ f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x) + f (b • y) = a • f x + b • f y
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
inst✝ : Nonempty ↥s
a : ↥s.direction
b : ↥s
⊢ ⟨↑(a +ᵥ b) -ᵥ ↑b, ⋯⟩ = a

Tactic:
by
    ext
    apply AddTorsor.vadd_vsub'

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case empty
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ 0 x = ↑⊥

Tactic:
_root_.bot_eq_zero,

Goal state after:
case empty
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
⊢ 0 x = ↑0
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
V₂ : Type u_4
P₂ : Type u_5
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₂
s : AffineSubspace k P₁
h : map f s = ⊥
⊢ s = ⊥

Tactic:
← coe_eq_bot_iff,

Goal state after:
case refine_1
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✝⁴ : 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₁
h : ↑(map f s) = ∅
⊢ 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₁ w₂ : ι → k
r : k
p : ι → P
⊢ ((1 - r) • (s.weightedVSubOfPoint p (Classical.choice ⋯)) w₁ +
        r • (s.weightedVSubOfPoint p (Classical.choice ⋯)) w₂) +ᵥ
      Classical.choice ⋯ =
    (s.weightedVSubOfPoint p (Classical.choice ⋯)) ((1 - r) • w₁ + r • w₂) +ᵥ Classical.choice ⋯

Tactic:
map_add,

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₁ w₂ : ι → k
r : k
p : ι → P
⊢ ((1 - r) • (s.weightedVSubOfPoint p (Classical.choice ⋯)) w₁ +
        r • (s.weightedVSubOfPoint p (Classical.choice ⋯)) w₂) +ᵥ
      Classical.choice ⋯ =
    ((s.weightedVSubOfPoint p (Classical.choice ⋯)) ((1 - r) • w₁) +
        (s.weightedVSubOfPoint p (Classical.choice ⋯)) (r • w₂)) +ᵥ
      Classical.choice ⋯
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
⊢ BddAbove (range p) ↔ ∀ (x : E), BddAbove (range fun i ↦ (p i) x)

Tactic:
by
  rw [Seminorm.bddAbove_iff, ← range_comp, bddAbove_range_pi]; rfl

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
⊢ ⇑(sSup (range fun i ↦ p i)) = ⨆ i, ⇑(p i)

Tactic:
Seminorm.coe_sSup_eq hp

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
⊢ ⨆ p_1, ⇑↑p_1 = ⨆ i, ⇑(p i)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : AffineSpace W Q
s : Set P
t : Set Q
⊢ vectorSpan k (s ×ˢ t) ≤ (vectorSpan k s).prod (vectorSpan k t)

Tactic:
by
  simpa [vectorSpan_def, Set.prod_vsub_prod_comm] using Submodule.span_prod_le (s -ᵥ s) (t -ᵥ t)

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.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
s : AffineSubspace k P
⊢ ⊥ ∥ s ↔ s = ⊥

Tactic:
parallel_comm,

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
s : AffineSubspace k P
⊢ s ∥ ⊥ ↔ s = ⊥
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.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
p₁ q₁ p₂ q₂ : P
⊢ k ∙ (q₁ -ᵥ p₁) ≤ k ∙ (q₂ -ᵥ p₂) ↔ ∃ z, z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁

Tactic:
Submodule.span_singleton_le_iff_mem,

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
p₁ q₁ p₂ q₂ : P
⊢ q₁ -ᵥ p₁ ∈ k ∙ (q₂ -ᵥ p₂) ↔ ∃ z, z • (q₂ -ᵥ p₂) = q₁ -ᵥ p₁
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬↑r₁ = r₂
h₁₂ : ↑r₁ • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
h₁₁ : ↑r₁ • (p₂ -ᵥ p₁) + ↑r₁ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
h₂₁ : (r₂ - ↑r₁) • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
⊢ r₂ ≠ ↑r₁

Tactic:
ne_comm

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₅ p₆ : P
h₂ : p₂ ∉ line[k, p₁, p₃]
r₁ : kˣ
hr₁ : ↑r₁ • (p₂ -ᵥ p₁) = p₅ -ᵥ p₄
r₂ : k
hr₂ : r₂ • (p₃ -ᵥ p₂) = p₆ -ᵥ p₅
r₃ : k
hr₃ : r₃ • (p₁ -ᵥ p₃) = p₄ -ᵥ p₆
h : ¬↑r₁ = r₂
h₁₂ : ↑r₁ • (p₂ -ᵥ p₁) + r₂ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
h₁₁ : ↑r₁ • (p₂ -ᵥ p₁) + ↑r₁ • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
h₂₁ : (r₂ - ↑r₁) • (p₃ -ᵥ p₂) ∈ vectorSpan k {p₁, p₃}
⊢ ↑r₁ ≠ r₂
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
p₁ : P
p : ι → P
s : Set ι
h : p₁ ∈ affineSpan k (p '' s)
⊢ ∃ fs w, ↑fs ⊆ s ∧ ∑ i ∈ fs, w i = 1 ∧ p₁ = (Finset.affineCombination k fs p) w

Tactic:
classical
  rw [Set.image_eq_range] at h
  obtain ⟨fs', w', hw', rfl⟩ := eq_affineCombination_of_mem_affineSpan h
  refine ⟨fs'.map (Function.Embedding.subtype _), fun i ↦ if hi : i ∈ s then w' ⟨i, hi⟩ else 0,
    (by simp), (by simp [hw']), ?_⟩
  simp only [Finset.affineCombination_map, Function.Embedding.coe_subtype]
  exact fs'.affineCombination_congr (by simp) (by simp)

Goal state after:
Module: Mathlib.Analysis.Seminorm

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

Tactic:
← mul_assoc,

Goal state after:
case inr.refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : p x < ‖k‖ * r
⊢ ‖k‖ * ‖k‖⁻¹ * p x < ‖k‖ * r
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
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✝ j : ι
e : ι ≃ ι'
i : ι
q : P
v : V
⊢ 1 - (b.basisOf i).sumCoords (v + (q -ᵥ b i)) = (-(b.basisOf i).sumCoords) v +ᵥ 1 - (b.basisOf i).sumCoords (q -ᵥ b i)

Tactic:
map_add,

Goal state after:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
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✝ j : ι
e : ι ≃ ι'
i : ι
q : P
v : V
⊢ 1 - ((b.basisOf i).sumCoords v + (b.basisOf i).sumCoords (q -ᵥ b i)) =
    (-(b.basisOf i).sumCoords) v +ᵥ 1 - (b.basisOf i).sumCoords (q -ᵥ b i)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_3
𝕜 : 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‖ * (‖c‖⁻¹ * (‖c‖ ^ n)⁻¹ * p x)

Tactic:
← mul_assoc,

Goal state after:
case refine_3
𝕜 : 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‖ * (‖c‖⁻¹ * (‖c‖ ^ n)⁻¹) * p x
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_3
𝕜 : 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‖ * (‖c‖⁻¹ * (‖c‖ ^ n)⁻¹) * p x

Tactic:
← mul_assoc,

Goal state after:
case refine_3
𝕜 : 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‖ * ‖c‖⁻¹ * (‖c‖ ^ n)⁻¹ * p x
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (Metric.closedBall 0 r)

Tactic:
rw [← closedBall_normSeminorm 𝕜]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 ((normSeminorm 𝕜 E).closedBall 0 r)