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

Goal state before:
pp: case neg.hr
x : ℂ
hx : ¬x = 0
⊢ 0 < normSq x

Tactic:
Complex.normSq_pos

Goal state after:
case neg.hr
x : ℂ
hx : ¬x = 0
⊢ x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support fun i ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a)
h' : ¬HasFiniteMulSupport f
⊢ log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset h, f i else 1) =
    if h : HasFiniteSupport fun i ↦ log (f i) then ∑ i ∈ Finite.toFinset h, log (f i) else 0

Tactic:
· simp [h', mt H'.mpr h']

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: n : ℕ
⊢ log ↑n = n.factorization.sum fun p t ↦ ↑t * log ↑p

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)
  · simp -- relies on junk values of `log` and `Nat.factorization`
  · simp only [← log_pow, ← Nat.cast_pow]
    rw [← Finsupp.log_prod, ← Nat.cast_finsuppProd, Nat.prod_factorization_pow_eq_self hn]
    intro p hp
    rw [eq_zero_of_pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsNat e n
⊢ 0 ≤ Real.log ↑n

Tactic:
exact Real.log_natCast_nonneg _

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

Goal state before:
pp: θ : Angle
⊢ θ.sin = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
nth_rw 1 [← sin_zero]

Goal state after:
θ : Angle
⊢ θ.sin = sin 0 ↔ θ = 0 ∨ θ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ -π < θ.toReal

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

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

Goal state before:
pp: case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(-x).arg = ↑x.arg + ↑π

pp: case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑(-x).arg = ↑x.arg + ↑π

Tactic:
· rw [(ext rfl hi : x = x.re)]
    rcases lt_trichotomy x.re 0 with (hr | hr | hr)
    · rw [arg_ofReal_of_neg hr, ← ofReal_neg, arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le, ←
        Real.Angle.coe_add, ← two_mul, Real.Angle.coe_two_pi, Real.Angle.coe_zero]
    · exact False.elim (hx (ext hr hi))
    · rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr),
        Real.Angle.coe_zero, zero_add]

Goal state after:
case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑(-x).arg = ↑x.arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ContinuousWithinAt arg {z | 0 ≤ z.im} z

Tactic:
have : arg =ᶠ[𝓝[{ z : ℂ | 0 ≤ z.im }] z] fun x => Real.arcsin ((-x).im / ‖x‖) + π := by
    have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)
    filter_upwards [self_mem_nhdsWithin (s := { z : ℂ | 0 ≤ z.im }),
      mem_nhdsWithin_of_mem_nhds this] with _ him hre
    rw [arg, if_neg hre.not_ge, if_pos him]

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

Goal state before:
pp: case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
rw [Complex.zero_cpow (Complex.ofReal_ne_zero.mpr h)] at hyp
      exact Or.inl ⟨h, hyp.symm⟩

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

Goal state before:
pp: θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
⊢ -π < θ.toReal + ψ.toReal ∧ θ.toReal + ψ.toReal ≤ π

Tactic:
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 : ℝ
hx : 0 ≤ x
y z : ℝ
h : y - z ≠ 0
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
simp only [sub_eq_add_neg] at h ⊢
  simp only [rpow_add' hx h, rpow_neg hx, div_eq_mul_inv]

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
⊢ x ^ (-z) < y ^ (-z)

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

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

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

pp: case hb
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < y ^ z

Tactic:
on_goal 1 => refine rpow_lt_rpow ?_ hxy (neg_pos.2 hz)

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

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)]

Goal state after:
case inl
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)) p
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x ↦ x.1 ^ x.2) (𝓝 (0, z)) (𝓝 0)

Tactic:
tendsto_zero_iff_norm_tendsto_zero

Goal state after:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x ↦ ‖x.1 ^ x.2‖) (𝓝 (0, z)) (𝓝 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.Real

Goal state before:
pp: x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < 1

Tactic:
by
  rw [← one_rpow z]
  exact rpow_lt_rpow hx1 hx2 hz

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

Goal state before:
pp: x : ℝ≥0∞
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
induction x using recTopCoe
  · rcases hy.eq_or_lt with rfl | hy
    · rw [rpow_zero, one_mul, zero_add]
    rcases hz.eq_or_lt with rfl | hz
    · rw [rpow_zero, mul_one, add_zero]
    simp [top_rpow_of_pos, hy, hz, add_pos hy hz]
  simp [← coe_rpow_of_nonneg, hy, hz, add_nonneg hy hz, NNReal.rpow_add_of_nonneg _ hy hz]

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

Goal state before:
pp: x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (x, y)

Tactic:
by
  have :
    (fun p : ℝ≥0 × ℝ => p.1 ^ p.2) =
      Real.toNNReal ∘ (fun p : ℝ × ℝ => p.1 ^ p.2) ∘ fun p : ℝ≥0 × ℝ => (p.1.1, p.2) := by
    ext p
    simp only [coe_rpow, val_eq_coe, Function.comp_apply, coe_toNNReal', left_eq_sup]
    positivity
  rw [this]
  refine continuous_real_toNNReal.continuousAt.comp (ContinuousAt.comp ?_ ?_)
  · apply Real.continuousAt_rpow
    simpa using h
  · fun_prop

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

Goal state before:
pp: case pos
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : y = ∞
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y

pp: case neg
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : ¬y = ∞
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y

Tactic:
· exact Eventually.of_forall fun n => h.symm ▸ le_top

Goal state after:
case neg
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : ¬y = ∞
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y
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:
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.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = (x ^ (1 / 2)) ^ r

Tactic:
← rpow_mul hx

Goal state after:
x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = x ^ (1 / 2 * r)
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 z : M
hx : SameRay R x z
hy : SameRay R y z
⊢ SameRay R (x + y) z

Tactic:
by
  rcases eq_or_ne x 0 with (rfl | hx₀); · rwa [zero_add]
  rcases eq_or_ne y 0 with (rfl | hy₀); · rwa [add_zero]
  rcases eq_or_ne z 0 with (rfl | hz₀); · apply zero_right
  rcases hx.exists_pos hx₀ hz₀ with ⟨rx, rz₁, hrx, hrz₁, Hx⟩
  rcases hy.exists_pos hy₀ hz₀ with ⟨ry, rz₂, hry, hrz₂, Hy⟩
  refine Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, ?_, ?_⟩)
  · positivity
  · convert! congr(ry • $Hx + rx • $Hy) using 1 <;> module

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

Goal state before:
pp: k : Type u_10
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b x : k
⊢ f x = x • f.linear (1 -ᵥ 0) +ᵥ f 0

Tactic:
← f.linear.map_smul,

Goal state after:
k : Type u_10
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b x : k
⊢ f x = f.linear (x • (1 -ᵥ 0)) +ᵥ f 0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : 2 • x = 2 • y
⊢ x = y

Tactic:
rwa [two_nsmul, two_nsmul, ← two_smul k x, ← two_smul k y,
      (isUnit_of_invertible (2 : k)).smul_left_cancel] at h

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✝ : SMul 𝕜 E
x : E
S : Set (Set E)
hS : ∀ s ∈ S, StarConvex 𝕜 x s
⊢ StarConvex 𝕜 x (⋃ i, ↑i)

Tactic:
exact starConvex_iUnion fun s => hS _ s.2

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ Ioo x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
simp only [← openSegment_eq_Ioo h, openSegment, smul_eq_mul, exists_and_left, mem_ofPred_eq]

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

Goal state before:

Tactic:
y = a • y + b • y := (Convex.combo_self hab _).symm
        _ ≤ a • x + b • y := by gcongr

Goal state after:
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 : Submodule k V
⊢ (↑s).direction = s

Tactic:
by
  ext x; simp [← s.toAffineSubspace.vadd_mem_iff_mem_direction _ s.zero_mem]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ s₁ ≤ s₂ ∧ ¬s₂ ≤ s₁ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁

Tactic:
not_le_iff_exists

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ (s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁) ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝⁶ : Monoid N
inst✝⁵ : SMul M N
inst✝⁴ : SMul M α
inst✝³ : MulAction N α
inst✝² : IsScalarTower M N α
inst✝¹ : Bornology M
inst✝ : Bornology N
s t : Set α
h : Absorbs N s t
hbdd : Tendsto (fun x ↦ x • 1) (cobounded M) (cobounded N)
x : M
hx : t ⊆ (x • 1) • s
⊢ t ⊆ x • s

Tactic:
by rwa [smul_one_smul N x s] at hx

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

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

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
⊢ (insert 0 (interior A)).Nonempty
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
p : P
d₁ d₂ : Submodule k V
h : ∀ ⦃x : P⦄, x -ᵥ p ∈ d₁ → x -ᵥ p ∈ d₂
x : V
hx : x ∈ d₁
⊢ x ∈ d₂

Tactic:
simpa using h (show (x +ᵥ p) -ᵥ p ∈ d₁ by simpa using hx)

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
hU : IsClosed[inst✝¹] U
⊢ IsClosed[inst✝¹] (balancedCore 𝕜 U)

Tactic:
by_cases h : (0 : E) ∈ U
  · rw [balancedCore_eq_iInter h]
    refine isClosed_iInter fun a => ?_
    refine isClosed_iInter fun ha => ?_
    have ha' := lt_of_lt_of_le zero_lt_one ha
    rw [norm_pos_iff] at ha'
    exact isClosedMap_smul_of_ne_zero ha' U hU
  · have : balancedCore 𝕜 U = ∅ := by
      contrapose! h
      exact balancedCore_nonempty_iff.mp h
    rw [this]
    exact isClosed_empty

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✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : IsVonNBounded 𝕜 s
x : E
⊢ IsVonNBounded 𝕜 (x +ᵥ s)

Tactic:
by
  rw [← singleton_vadd]
  -- TODO: dot notation timeouts in the next line
  exact IsVonNBounded.add (isVonNBounded_singleton x) hs

Goal state after:
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
⊢ 0 +ᵥ a = a

Tactic:
ext
    exact zero_vadd _ _

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

Goal state before:
pp: case refine_1.inl
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₂
p₃ : P
hp₃ : p₃ ∈ ↑s₁
⊢ (fun x ↦ x -ᵥ p₁) p₃ ∈ ↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁))

Tactic:
rw [sup_assoc, sup_comm, SetLike.mem_coe, Submodule.mem_sup]

Goal state after:
case refine_1.inl
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₂
p₃ : P
hp₃ : p₃ ∈ ↑s₁
⊢ ∃ y ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁), ∃ z ∈ s₁.direction, y + z = (fun x ↦ x -ᵥ p₁) p₃
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
⊢ 0 ∈ lowerBounds (range fun u ↦ p u + q (x - u))

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ x : E
⊢ 0 ≤ (fun u ↦ p u + q (x✝ - u)) x
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case right.e_f
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hw : ∑ i ∈ insert i0 l.support, w i = 0
hz : (fun i ↦ w i • (p i -ᵥ p i0)) i0 = 0
i : ι
⊢ l i • (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)

Tactic:
by_cases h : i = i0

Goal state after:
case pos
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hw : ∑ i ∈ insert i0 l.support, w i = 0
hz : (fun i ↦ w i • (p i -ᵥ p i0)) i0 = 0
i : ι
h : i = i0
⊢ l i • (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)

case neg
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hw : ∑ i ∈ insert i0 l.support, w i = 0
hz : (fun i ↦ w i • (p i -ᵥ p i0)) i0 = 0
i : ι
h : ¬i = i0
⊢ l i • (p i -ᵥ p i0) = w i • (p i -ᵥ p i0)
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
v : V
p : ι → P
⊢ v ∈ vectorSpan k (Set.range p) → ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w

Tactic:
rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)
      swap
      · rw [vectorSpan_range_eq_span_range_vsub_right k p i0, ← Set.image_univ,
          Finsupp.mem_span_image_iff_linearCombination]
        rintro ⟨l, _, hv⟩
        use insert i0 l.support
        set w :=
          (l : ι → k) - Function.update (Function.const ι 0 : ι → k) i0 (∑ i ∈ l.support, l i) with
          hwdef
        use w
        have hw : ∑ i ∈ insert i0 l.support, w i = 0 := by
          rw [hwdef]
          simp_rw [Pi.sub_apply, Finset.sum_sub_distrib,
            Finset.sum_update_of_mem (Finset.mem_insert_self _ _),
            Finset.sum_insert_of_eq_zero_if_notMem Finsupp.notMem_support_iff.1]
          simp only [Function.const_apply, Finset.sum_const_zero, add_zero, sub_self]
        use hw
        have hz : w i0 • (p i0 -ᵥ p i0 : V) = 0 := (vsub_self (p i0)).symm ▸ smul_zero _
        change (fun i => w i • (p i -ᵥ p i0 : V)) i0 = 0 at hz
        rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w p hw (p i0),
          Finset.weightedVSubOfPoint_apply, ← hv, Finsupp.linearCombination_apply,
          @Finset.sum_insert_zero _ _ l.support i0 _ _ _ hz]
        change (∑ i ∈ l.support, l i • _) = _
        congr with i
        by_cases h : i = i0
        · simp [h]
        · simp [hwdef, h]
      · rw [Set.range_eq_empty, vectorSpan_empty, Submodule.mem_bot]
        rintro rfl
        use ∅
        simp

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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ AffineIndependent k ![p₃, p₂, p₁]

Tactic:
by
  rw [← affineIndependent_equiv (Equiv.swap 0 2)]
  convert! h using 1
  ext x
  fin_cases x <;> rfl

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
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : ∑ i ∈ s₁, w₁ i = 1
hw₂ : ∑ i ∈ s₂, w₂ i = 1
e : ι₂ ↪ ι
h : (affineCombination k s₂ (p ∘ ⇑e)) (extend (⇑e) w₂ 0 ∘ ⇑e) = (affineCombination k s₁ p) w₁
hw₂e : extend (⇑e) w₂ 0 ∘ ⇑e = w₂
⊢ (↑(map e s₂)).indicator (extend (⇑e) w₂ 0) = (↑s₁).indicator w₁

Tactic:
← affineCombination_map

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : ∑ i ∈ s₁, w₁ i = 1
hw₂ : ∑ i ∈ s₂, w₂ i = 1
e : ι₂ ↪ ι
h : (affineCombination k (map e s₂) p) (extend (⇑e) w₂ 0) = (affineCombination k s₁ p) w₁
hw₂e : extend (⇑e) w₂ 0 ∘ ⇑e = w₂
⊢ (↑(map e s₂)).indicator (extend (⇑e) w₂ 0) = (↑s₁).indicator w₁
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ s.points i ∈ s.closedInterior

Tactic:
by
  rw [← Finset.univ.affineCombination_piSingle k s.points (Finset.mem_univ i),
    affineCombination_mem_closedInterior_iff (Fintype.sum_pi_single' _ _)]
  intro j
  obtain rfl | hj := eq_or_ne j i <;> simp_all

Goal state after:
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹² : AddCommGroup V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : AddTorsor V P
inst✝⁹ : TopologicalSpace P
inst✝⁸ : IsTopologicalAddTorsor P
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : AddTorsor W Q
inst✝⁴ : TopologicalSpace Q
inst✝³ : IsTopologicalAddTorsor Q
inst✝² : Ring R
inst✝¹ : Module R V
inst✝ : Module R W
f : P →ᵃ[R] Q
⊢ IsOpenMap ⇑f.linear ↔ IsOpenMap ⇑f

Tactic:
inhabit P
  have :
    (f.linear : V → W) =
      (Homeomorph.vaddConst <| f default).symm ∘ f ∘ (Homeomorph.vaddConst default) := by
    ext v
    simp
  rw [this]
  simp only [Homeomorph.comp_isOpenMap_iff, Homeomorph.comp_isOpenMap_iff']

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

Goal state before:
pp: R : Type u_1
ι : Type u_5
α : Type u_7
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : Module R α
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid α
inst✝ : PosSMulMono R α
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : 0 < ∑ i ∈ s, w i
⊢ s.centerMass w f ≤ s.sup' ⋯ f

Tactic:
by
  rw [centerMass, inv_smul_le_iff_of_pos hw₁, sum_smul]
  exact sum_le_sum fun i hi => smul_le_smul_of_nonneg_left (le_sup' _ hi) <| hw₀ i hi

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : PartialOrder k
inst✝ : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
⊢ (affineCombination k univ s.points) w ∈ (s.face h).closedInterior ↔ (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0

Tactic:
by
  rw [s.affineCombination_mem_closedInterior_face_iff_mem_Icc h hw]
  refine ⟨by grind, fun ⟨hii, hi0⟩ ↦ ⟨fun i hi ↦ ⟨hii i hi, ?_⟩, hi0⟩⟩
  rw [← hw, ← Finset.sum_subset (Finset.subset_univ fs) fun j _ ↦ hi0 j]
  exact Finset.single_le_sum (fun t ht ↦ (hii t ht)) hi

Goal state after: