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

Goal state before:
pp: s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ rexp (b * x) / x ^ s) atTop atTop

Tactic:
by
  refine ((tendsto_rpow_atTop hb).comp (tendsto_exp_div_rpow_atTop (s / b))).congr' ?_
  filter_upwards [eventually_ge_atTop (0 : ℝ)] with x hx₀
  simp [Real.div_rpow, (exp_pos x).le, rpow_nonneg, ← Real.rpow_mul, ← exp_mul,
    mul_comm x, hb.ne', *]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
y z : ℝ
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
by
  simp only [sub_eq_add_neg, rpow_add hx, rpow_neg (le_of_lt hx), div_eq_mul_inv]

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t ↦ t ^ a
hg : g =O[atTop] fun t ↦ t ^ b
h : a + b ≤ c
⊢ (f * g) =O[atTop] fun t ↦ t ^ c

Tactic:
refine (hf.mul hg).trans (Eventually.isBigO ?_)
  filter_upwards [eventually_ge_atTop 1] with t ht
  rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg
    (zero_le_one.trans ht) (a + b))]
  exact Real.rpow_le_rpow_of_exponent_le ht h

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

Goal state before:
pp: ⊢ Tendsto (fun x ↦ log x * x) (𝓝[<] 0) (𝓝 0)

Tactic:
by
  have h := tendsto_log_mul_rpow_nhdsGT_zero zero_lt_one
  simp only [Real.rpow_one] at h
  have h_eq : ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ (fun x ↦ |x|)) x = log x * x := by
    simp only [Set.mem_Iio, Pi.neg_apply, Function.comp_apply, log_abs]
    intro x hx
    simp only [abs_of_nonpos hx.le, mul_neg, neg_neg]
  refine tendsto_nhdsWithin_congr h_eq ?_
  nth_rewrite 3 [← neg_zero]
  refine (h.comp (tendsto_abs_nhdsNE_zero.mono_left ?_)).neg
  refine nhdsWithin_mono 0 (fun x hx ↦ ?_)
  push _ ∈ _ at hx
  simp only [Set.mem_compl_iff, Set.mem_singleton_iff, hx.ne, not_false_eq_true]

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
simpa using rpow_add_natCast hx y 1

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
rw [← rpow_neg_eq_inv_rpow, rpow_neg hx]

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

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
simpa using rpow_add_natCast hx y 1

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

Goal state before:
pp: x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x ^ z = (y ^ (1 / z)) ^ z ↔ x ^ z = y

Tactic:
rpow_self_rpow_inv hz

Goal state after:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x ^ z = y ↔ x ^ z = y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ (x ^ (1 / z)) ^ z = y ^ z ↔ x = y ^ z

Tactic:
rpow_self_rpow_inv hz

Goal state after:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x = y ^ z ↔ x = y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: M : ℝ≥0
P : ℝ
hP : 0 ≤ P
⊢ ↑M ^ P = ↑(M ^ P)

Tactic:
ENNReal.coe_rpow_of_nonneg _ hP,

Goal state after:
M : ℝ≥0
P : ℝ
hP : 0 ≤ P
⊢ ↑M ^ P = ↑M ^ P
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
h₁ : 0 ≤ x
h₂ : x ≤ 1
h₃ : y ≤ 1
⊢ x ≤ x ^ y

Tactic:
simpa only [rpow_one]
    using rpow_le_rpow_of_exponent_ge_of_imp h₁ h₂ h₃ fun _ ↦ (absurd · one_ne_zero)

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

Goal state before:
pp: case inl
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : 0 ≤ y
⊢ (0 * y) ^ z = if (0 = 0 ∧ y = ∞ ∨ 0 = ∞ ∧ y = 0) ∧ z < 0 then ∞ else 0 ^ z * y ^ z

Tactic:
induction y

Goal state after:
case inl.top
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : 0 ≤ ∞
⊢ (0 * ∞) ^ z = if (0 = 0 ∧ ∞ = ∞ ∨ 0 = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else 0 ^ z * ∞ ^ z

case inl.coe
z : ℝ
hz : z < 0 ∨ 0 < z
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ∞ ∨ 0 = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else 0 ^ z * ↑x✝ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.coe
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
x✝ : ℝ≥0
hxy : ↑x✝ ≤ y
hx0 : ↑x✝ ≠ 0
⊢ (↑x✝ * y) ^ z = if (↑x✝ = 0 ∧ y = ∞ ∨ ↑x✝ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * y ^ z

Tactic:
induction y

Goal state after:
case inr.inr.coe.top
z : ℝ
hz : z < 0 ∨ 0 < z
x✝ : ℝ≥0
hx0 : ↑x✝ ≠ 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z

case inr.inr.coe.coe
z : ℝ
hz : z < 0 ∨ 0 < z
x✝¹ : ℝ≥0
hx0 : ↑x✝¹ ≠ 0
x✝ : ℝ≥0
hy0 : ↑x✝ ≠ 0
hxy : ↑x✝¹ ≤ ↑x✝
⊢ (↑x✝¹ * ↑x✝) ^ z = if (↑x✝¹ = 0 ∧ ↑x✝ = ∞ ∨ ↑x✝¹ = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else ↑x✝¹ ^ z * ↑x✝ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.coe.coe
z : ℝ
x✝¹ x✝ : ℝ≥0
hz : z < 0 ∨ 0 < z
hx0 : ¬x✝¹ = 0
hy0 : ¬x✝ = 0
hxy : x✝¹ ≤ x✝
⊢ ↑(x✝¹ * x✝) ^ z = if (False ∧ ↑x✝ = ∞ ∨ ↑x✝¹ = ∞ ∧ False) ∧ z < 0 then ∞ else ↑x✝¹ ^ z * ↑x✝ ^ z

Tactic:
← coe_rpow_of_ne_zero (mul_ne_zero hx0 hy0),

Goal state after:
case inr.inr.coe.coe
z : ℝ
x✝¹ x✝ : ℝ≥0
hz : z < 0 ∨ 0 < z
hx0 : ¬x✝¹ = 0
hy0 : ¬x✝ = 0
hxy : x✝¹ ≤ x✝
⊢ ↑((x✝¹ * x✝) ^ z) = if (False ∧ ↑x✝ = ∞ ∨ ↑x✝¹ = ∞ ∧ False) ∧ z < 0 then ∞ else ↑x✝¹ ^ z * ↑x✝ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ x ^ y ≤ 1 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y

Tactic:
rw [rpow_def_of_pos hx, exp_le_one_iff, mul_nonpos_iff, log_nonneg_iff hx, log_nonpos_iff hx.le]

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

Goal state before:
pp: x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ |log x * x ^ t| < 1 / t

Tactic:
by
  rw [lt_div_iff₀ ht]
  have := abs_log_mul_self_lt (x ^ t) (rpow_pos_of_pos h1 t) (rpow_le_one h1.le h2 ht.le)
  rwa [log_rpow h1, mul_assoc, abs_mul, abs_of_pos ht, mul_comm] at this

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 : Set P
h : vectorSpan k s = ⊥
hns : ¬s.Subsingleton
⊢ False

Tactic:
rw [Set.not_subsingleton_iff] at hns

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 : Set P
h : vectorSpan k s = ⊥
hns : s.Nontrivial
⊢ False
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
y : F
y' : E
hy' : y' ∈ s
hy'f : f y' = y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y') = a • f x + b • y

Tactic:
rw [Convex.combo_affine_apply hab, hy'f]

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
s : ι → AffineSubspace k P
⊢ ⨅ s_1 ∈ range s, s_1.direction = ⨅ i, (s i).direction

Tactic:
rw [iInf_range]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, MapsTo (fun x ↦ c • x) t s

Tactic:
by
  rw [absorbs_iff_eventually_cobounded_mapsTo, ← Filter.inv_cobounded₀]; rfl

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
⊢ balancedCore 𝕜 U ∈ 𝓝 0

Tactic:
obtain ⟨r, V, hr, hV, hrVU⟩ : ∃ (r : ℝ) (V : Set E),
      0 < r ∧ V ∈ 𝓝 (0 : E) ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U := by
    have h : Filter.Tendsto (fun x : 𝕜 × E => x.fst • x.snd) (𝓝 (0, 0)) (𝓝 0) :=
      continuous_smul.tendsto' (0, 0) _ (smul_zero _)
    simpa only [← Prod.exists', ← Prod.forall', ← and_imp, ← and_assoc, exists_prop] using!
      h.basis_left (NormedAddGroup.nhds_zero_basis_norm_lt.prod_nhds (𝓝 _).basis_sets) U hU

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
⊢ balancedCore 𝕜 U ∈ 𝓝 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_2
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₂
⊢ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction

Tactic:
refine sup_le (sup_direction_le _ _) ?_
    rw [direction_eq_vectorSpan, vectorSpan_def]
    exact
      sInf_le_sInf fun p hp =>
        Set.Subset.trans
          (Set.singleton_subset_iff.2
            (vsub_mem_vsub (mem_affineSpan k (Set.mem_union_right _ hp₂))
              (mem_affineSpan k (Set.mem_union_left _ hp₁))))
          hp

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✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : P
h : ∑ i ∈ s, w i = 1
⊢ (s.weightedVSubOfPoint (fun x ↦ p) (Classical.choice ⋯)) w +ᵥ Classical.choice ⋯ = p

Tactic:
s.weightedVSubOfPoint_apply_const,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : P
h : ∑ i ∈ s, w i = 1
⊢ (∑ i ∈ s, w i) • (p -ᵥ Classical.choice ⋯) +ᵥ Classical.choice ⋯ = p
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
p : ι → P
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)

Tactic:
classical
    have hnz : ∑ i ∈ s, w i ≠ 0 := h.symm ▸ one_ne_zero
    have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
    obtain ⟨i1, hi1⟩ := hn
    let w1 : ι → k := Function.update (Function.const ι 0) i1 1
    have hw1 : ∑ i ∈ s, w1 i = 1 := by
      simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
          Finset.sum_const_zero, add_zero]
    have hw1s : s.affineCombination k p w1 = p i1 :=
      s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_self ..) fun _ _ hne =>
        Function.update_of_ne hne ..
    have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction := by
      rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
      apply weightedVSub_mem_vectorSpan
      simp [Pi.sub_apply, h, hw1]
    rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
    exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k (Set.mem_range_self _))

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

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
ι : Type u_4
s : Finset ι
inst✝ : CharZero k
p : ι → P
p₀ : P
hs : s.Nonempty
⊢ centroid k s p -ᵥ p₀ = centroid k s fun i ↦ p i -ᵥ p₀

Tactic:
have h := s.sum_centroidWeights_eq_one_of_nonempty k hs
  simp only [centroid_def]
  grind [sum_smul_vsub_const_eq_affineCombination_vsub, affineCombination_eq_linear_combination]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ p.closedBall 0 r = ⇑p ⁻¹' Metric.closedBall 0 r

Tactic:
rw [closedBall_zero_eq, preimage_metric_closedBall]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x✝ : E
⊢ r ≤ p (x✝ - x)

Tactic:
exact hr.trans (apply_nonneg p _)

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

Goal state before:
pp: 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
s : AffineSubspace k P
⊢ (v +ᵥ s).direction = s.direction

Tactic:
pointwise_vadd_eq_map,

Goal state after:
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
s : AffineSubspace k P
⊢ (map (↑(AffineEquiv.constVAdd k P v)) s).direction = s.direction
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:
pointwise_vadd_eq_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 (map (↑(AffineEquiv.constVAdd k P₁ v)) s) = f.linear v +ᵥ map f s
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 (map (↑(AffineEquiv.constVAdd k P₁ v)) s) = f.linear v +ᵥ map f s

Tactic:
pointwise_vadd_eq_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 (map (↑(AffineEquiv.constVAdd k P₁ v)) s) = map (↑(AffineEquiv.constVAdd k P₂ (f.linear v))) (map 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
⊢ (Finset.affineCombination k s p) w = (Finset.affineCombination k ({x ∈ s | x ∈ s'}) p) w

Tactic:
Finset.affineCombination_indicator_subset w p
    (Finset.filter_subset _ _)

Goal state after:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
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
⊢ (Finset.affineCombination k s p) w = (Finset.affineCombination k s p) ((↑({x ∈ s | x ∈ s'})).indicator w)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case mp
ι : 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
p1 : P
p : ι → P
⊢ p1 ∈ affineSpan k (Set.range p) → ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w

pp: case mpr
ι : 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
p1 : P
p : ι → P
⊢ (∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w) → p1 ∈ affineSpan k (Set.range p)

Tactic:
· exact eq_affineCombination_of_mem_affineSpan

Goal state after:
case mpr
ι : 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
p1 : P
p : ι → P
⊢ (∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w) → p1 ∈ affineSpan k (Set.range p)
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: case intro
ι : 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
inst✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂
val✝ : Fintype ι
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) q₁) =
    (Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) q₂

Tactic:
simp only [h]

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

Goal state before:
pp: case refine_2
k : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
i : Fin (n + 1)
h : w i = 0
⊢ (affineCombination k univ s.points) w ∈ affineSpan k (s.points '' {i}ᶜ)

Tactic:
rcases subsingleton_or_nontrivial k with hk | hk

Goal state after:
case refine_2.inl
k : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
i : Fin (n + 1)
h : w i = 0
hk : Subsingleton k
⊢ (affineCombination k univ s.points) w ∈ affineSpan k (s.points '' {i}ᶜ)

case refine_2.inr
k : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
i : Fin (n + 1)
h : w i = 0
hk : Nontrivial k
⊢ (affineCombination k univ s.points) w ∈ affineSpan k (s.points '' {i}ᶜ)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case mp.refine_2
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₂
⊢ (affineCombination k fs₁ p) w₁ = (affineCombination k (fs₁ ∩ fs₂) p) w₁

Tactic:
affineCombination_indicator_subset w₁ p Finset.inter_subset_left

Goal state after:
case mp.refine_2
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₂
⊢ (affineCombination k fs₁ p) w₁ = (affineCombination k fs₁ p) ((↑(fs₁ ∩ fs₂)).indicator w₁)
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
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₁
⊢ i ∈ ↑fs₁

Tactic:
simpa using hi

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
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₁
hi₂ : i ∉ fs₂
⊢ i ∈ ↑fs₁

Tactic:
simpa using hi

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

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (insert i t).centerMass w z =
    (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z

Tactic:
simp only [centerMass, sum_insert ha, smul_add, (mul_smul _ _ _).symm, ← div_eq_inv_mul]

Goal state after:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (w i / (w i + ∑ i ∈ t, w i)) • z i + (w i + ∑ i ∈ t, w i)⁻¹ • ∑ i ∈ t, w i • z i =
    (w i / (w i + ∑ i ∈ t, w i)) • z i + ((∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹) • ∑ i ∈ t, w i • z 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
I : Set 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, w i ∈ I) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, w i ∈ I
hi0 : ∀ i ∉ fs, w i = 0
w' : Fin (m + 1) → k := w ∘ ⇑(fs.orderEmbOfFin h)
i : Fin (n + 1)
hi : i ∉ Set.range ⇑(fs.orderEmbOfFin h)
⊢ i ∉ fs

Tactic:
simpa using hi

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

Goal state before:
pp: case refine_2
k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : PartialOrder k
inst✝¹ : Nontrivial k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
hfs : j ∈ fs
⊢ s.points j ∈ (s.face h).closedInterior

Tactic:
· obtain ⟨i, rfl⟩ : ∃ i, fs.orderEmbOfFin h i = j := range_orderEmbOfFin fs h |>.ge hfs
    exact point_mem_closedInterior _ _

Goal state after:
Module: Mathlib.Topology.AlexandrovDiscrete

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

Tactic:
hS

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