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

Goal state before:
pp: θ : ℝ
k : ℤ
h : -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π
⊢ (2 * ↑k - 1) * π < θ

Tactic:
by linarith

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

Goal state before:
pp: θ : ℝ
k : ℤ
h : -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π
⊢ θ ≤ (2 * ↑k + 1) * π

Tactic:
by linarith

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

Goal state before:
pp: θ : ℝ
k : ℤ
h : (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
⊢ -π < θ - 2 * ↑k * π

Tactic:
by linarith

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

Goal state before:
pp: θ : ℝ
k : ℤ
h : (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
⊢ θ - 2 * ↑k * π ≤ π

Tactic:
by linarith

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

Goal state before:
pp: θ : Angle
h : π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π
⊢ π / 2 < θ.toReal

Tactic:
by linarith

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

Goal state before:
pp: θ : Angle
h : -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π
⊢ θ.toReal ≤ -π / 2

Tactic:
by linarith

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

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ 0 < -b

Tactic:
by linarith

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

Goal state before:
pp: α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
rpow_pos :
  ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ},
    0 ≤ᶠ[l] f → 0 ≤ᶠ[l] g → f =Θ[l] g → r ≥ 0 → (fun x ↦ f x ^ r) =Θ[l] fun x ↦ g x ^ r
hr : ¬r ≥ 0
⊢ -r ≥ 0

Tactic:
by linarith

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

Goal state before:
pp: case inr.inl
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

pp: case inr.inr
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
· grind [sign_eq_zero_iff, coe_pi_add_coe_pi]

Goal state after:
case inr.inr
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ ↑x ^ (↑y * z) = ↑(x ^ y) ^ z

Tactic:
rw [cpow_mul, ofReal_cpow hx]

Goal state after:
case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ -π < (log ↑x * ↑y).im

case h₂
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ (log ↑x * ↑y).im ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ (↑x ^ ↑y * ↑x ^ ↑n).re = (↑x ^ ↑y).re * x ^ n

Tactic:
Complex.cpow_intCast,

Goal state after:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ (↑x ^ ↑y * ↑x ^ n).re = (↑x ^ ↑y).re * x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
by
  rw [rpow_add' hx h, rpow_one]

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

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

Tactic:
by
  rw [rpow_add' hx h, rpow_one]

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

Goal state before:
pp: a b : ℂ
ha : a ≠ 0
cpow_eq : (fun x ↦ a ^ x) = fun x ↦ cexp (Complex.log a * x)
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
rw [cpow_eq]

Goal state after:
a b : ℂ
ha : a ≠ 0
cpow_eq : (fun x ↦ a ^ x) = fun x ↦ cexp (Complex.log a * x)
⊢ ContinuousAt (fun x ↦ cexp (Complex.log a * x)) b
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:
by
  ext; exact Real.rpow_add_of_nonneg x.2 hy hz

Goal state after:
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, z).1 ^ (0, z).2))

Tactic:
zero_cpow hz₀,

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.Continuity

Goal state before:
pp: z w : ℂ
h₁ : (0 < (z, w).1.re ∨ (z, w).1.im ≠ 0) ∨ (z, w).1 = 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (z, w)

Tactic:
rcases h₁ with (h₁ | (rfl : z = 0))

Goal state after:
case inl
z w : ℂ
h₂ : 0 < (z, w).2.re
h₁ : 0 < (z, w).1.re ∨ (z, w).1.im ≠ 0
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (z, w)

case inr
w : ℂ
h₂ : 0 < (0, w).2.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (0, w)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
n : ℕ
hn : m + 1 ≤ n
⊢ x ^ (↑n)⁻¹ ≤ y

Tactic:
simpa only [NNReal.rpow_inv_le_iff (Nat.cast_pos.2 <| m.succ_pos.trans_le hn),
    NNReal.rpow_natCast] using hm.le.trans (pow_right_mono₀ hy.le (m.le_succ.trans hn))

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

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

Tactic:
nth_rw 2 [← ENNReal.rpow_one x]

Goal state after:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x ^ 1
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case pos
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
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

pp: case neg
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
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

Tactic:
· simpa [hy] using fun h : LinearIndependent R ![x, 0] => h.ne_zero 1 rfl

Goal state after:
case neg
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
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
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
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
f g : P1 →ᵃ[k] P2
h : f = g
inhabited_h : Inhabited P1
⊢ P1

Tactic:
exact default

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

Goal state before:
pp: case refine_2
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
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
f : P1 →ᵃ[k] P2
h : ∃ q, f = const k P1 q
⊢ f.linear = 0

Tactic:
· rcases h with ⟨q, rfl⟩
    exact const_linear k P1 q

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a x b c : E
⊢ a +ᵥ x ∈ [a +ᵥ b -[𝕜] a +ᵥ c] ↔ x ∈ [b -[𝕜] c]

Tactic:
← vadd_segment,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a x b c : E
⊢ a +ᵥ x ∈ a +ᵥ [b -[𝕜] c] ↔ x ∈ [b -[𝕜] c]
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
P : Prop
hs : Convex 𝕜 s
hP : P
⊢ Convex 𝕜 {x | P → x ∈ s}

Tactic:
simp [hP, hs, convex_univ]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
P : Prop
hs : Convex 𝕜 s
hP : ¬P
⊢ Convex 𝕜 {x | P → x ∈ s}

Tactic:
simp [hP, hs, convex_univ]

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
p : P
hp : p ∈ s
v : V
| ∃ x ∈ ↑s, x -ᵥ p = -v

Tactic:
congr
    ext
    rw [← neg_vsub_eq_vsub_rev, neg_inj]

Goal state after:
case p
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
p : P
hp : p ∈ s
v : V
x✝ : P
| x✝ ∈ ↑s ∧ p -ᵥ x✝ = v
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ x ∈ (convexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t

Tactic:
by
  simp_rw [convexHull_eq_iInter, mem_iInter]

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
h₀ : 0 ∈ s
⊢ Absorbs 𝕜 s t ↔ (∀ᶠ (x : 𝕜) in 𝓝[≠] 0, MapsTo (fun x_1 ↦ x • x_1) t s) ∧ MapsTo (fun x ↦ 0 • x) t s

Tactic:
← absorbs_iff_eventually_nhdsNE_zero,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h₀ : 0 ∈ s
⊢ Absorbs 𝕜 s t ↔ Absorbs 𝕜 s t ∧ MapsTo (fun x ↦ 0 • x) t s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case right
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
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ + v₂ + (p₁ -ᵥ p₂) = 0
⊢ False

Tactic:
add_comm v₁,

Goal state after:
case right
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
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₂ + v₁ + (p₁ -ᵥ p₂) = 0
⊢ False
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
y : E
hy : y ∈ balancedCoreAux 𝕜 s
ha : ‖0‖ ≤ 1
⊢ (fun x ↦ 0 • x) y ∈ balancedCoreAux 𝕜 s

pp: case inr
𝕜 : 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 : y ∈ balancedCoreAux 𝕜 s
h : a ≠ 0
⊢ (fun x ↦ a • x) y ∈ balancedCoreAux 𝕜 s

Tactic:
· simp_rw [zero_smul, h0]

Goal state after:
case inr
𝕜 : 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 : y ∈ balancedCoreAux 𝕜 s
h : a ≠ 0
⊢ (fun x ↦ a • x) y ∈ balancedCoreAux 𝕜 s
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
x✝ : Finite ↑I
⊢ IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)

Tactic:
biUnion_eq_iUnion,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
x✝ : Finite ↑I
⊢ IsVonNBounded 𝕜 (⋃ x, s ↑x) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (DFunLike.coe ∘ F) 1
⊢ Continuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))

Tactic:
equicontinuousAt_iff_continuousAt

Goal state after:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
⊢ Continuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : UniformSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsUniformGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (DFunLike.coe ∘ F) 1
⊢ UniformContinuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))

Tactic:
equicontinuousAt_iff_continuousAt

Goal state after:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : UniformSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsUniformGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
⊢ UniformContinuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s → ∃ a, s ⊆ a • Metric.closedBall 0 1

Tactic:
rw [isBounded_iff_subset_smul_ball 𝕜]
    exact Exists.imp fun a ha => ha.trans <| Set.smul_set_mono <| Metric.ball_subset_closedBall

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S : Set (Set E)
hdir : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
hS : ∀ s ∈ S, StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]
  exact (directedOn_iff_directed.1 hdir).strictConvex_iUnion fun s => hS _ s.2

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 ι
V₂ : Type u_6
P₂ : Type u_7
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : s.sum w = 1
f : P →ᵃ[k] P₂
⊢ f ((affineCombination k s p) w) = (affineCombination k s (⇑f ∘ p)) w

Tactic:
by
  have b := Classical.choice (inferInstance : AffineSpace V P).nonempty
  have b₂ := Classical.choice (inferInstance : AffineSpace V₂ P₂).nonempty
  rw [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw b,
    s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w (f ∘ p) hw b₂, ←
    s.weightedVSubOfPoint_vadd_eq_of_sum_eq_one w (f ∘ p) hw (f b) b₂]
  simp only [weightedVSubOfPoint_apply, RingHom.id_apply, AffineMap.map_vadd, map_smulₛₗ,
    AffineMap.linearMap_vsub, map_sum, Function.comp_apply]

Goal state after:
Module: Mathlib.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
v : V
⊢ s₁ = map (AffineMap.id k P) s₁

Tactic:
map_id

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
v : V
⊢ s₁ = s₁
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
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k {0, 1} p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0

Tactic:
convert! centroid_pair k p 0 1

Goal state after:
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
hnz : ∑ i ∈ s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := ⋯
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (Finset.affineCombination k s p) w1 = p i1
⊢ ∑ i ∈ s, (w - w1) i = 0

Tactic:
simp [Pi.sub_apply, h, hw1]

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

Goal state before:
pp: case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
h : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
f : { x // x ≠ ⟨p₁, hp₁⟩ } → ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁})) := fun x ↦ ⟨↑↑x -ᵥ p₁, ⋯⟩
⊢ LinearIndependent k fun i ↦ ↑↑i -ᵥ ↑⟨p₁, hp₁⟩

Tactic:
convert!
      h.comp f fun x1 x2 hx => Subtype.ext (Subtype.ext (vsub_left_cancel (Subtype.ext_iff.1 hx)))

Goal state after:
Module: Mathlib.Analysis.Seminorm

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

Tactic:
rwa [Seminorm.mem_closedBall_zero, map_smul_eq_mul, norm_inv, inv_mul_le_iff₀ hk]

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

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
q : P
⊢ ∑ i, (b.coord i) q = 1

Tactic:
have hq : q ∈ affineSpan k (range b) := by
    rw [b.tot]
    exact AffineSubspace.mem_top k V q

Goal state after:
ι : 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✝ : Fintype ι
q : P
hq : q ∈ affineSpan k (range ⇑b)
⊢ ∑ i, (b.coord i) q = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Basis

Goal state before:
pp: ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Fintype ι
q : P
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) q) = q

Tactic:
have hq : q ∈ affineSpan k (range b) := by
    rw [b.tot]
    exact AffineSubspace.mem_top k V q

Goal state after:
ι : 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✝ : Fintype ι
q : P
hq : q ∈ affineSpan k (range ⇑b)
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i ↦ (b.coord i) q) = q
Module: Mathlib.LinearAlgebra.AffineSpace.Restrict

Goal state before:
pp: case refine_2
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✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ Submodule.map φ.linear E.direction ≤ F.direction

Tactic:
← AffineSubspace.map_direction

Goal state after:
case refine_2
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✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty ↥E
inst✝ : Nonempty ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ (AffineSubspace.map φ E).direction ≤ F.direction
Module: Mathlib.LinearAlgebra.AffineSpace.Restrict

Goal state before:
pp: 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✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ Submodule.map φ.linear E.direction ≤ F.direction

Tactic:
← AffineSubspace.map_direction

Goal state after:
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✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ (AffineSubspace.map φ E).direction ≤ F.direction
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:
← affineIndependent_equiv (Equiv.swap 0 1)

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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ AffineIndependent k (![p₂, p₁, p₃] ∘ ⇑(Equiv.swap 0 1))
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)) w₂ = (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:
← hw₂e,

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 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₁
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
V₂ : Type u_3
V₃ : Type u_4
P : Type u_5
P₂ : Type u_6
P₃ : Type u_7
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V
inst✝⁷ : AddCommGroup V₂
inst✝⁶ : AddCommGroup V₃
inst✝⁵ : Module k V
inst✝⁴ : Module k V₂
inst✝³ : Module k V₃
inst✝² : AffineSpace V P
inst✝¹ : AffineSpace V₂ P₂
inst✝ : AffineSpace V₃ P₃
p : P
⊢ Subsingleton (Fin (1 + 0))

Tactic:
rw [add_zero]; infer_instance

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

Goal state before:
pp: case refine_1
S : Type u_1
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
X : Type u_2
Y : Type u_3
inst✝² : Fintype X
inst✝¹ : Fintype Y
inst✝ : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : ∑ x, s x = 1
y : Y
⊢ 0 ≤ {x | f x = y}.sum s

Tactic:
exact Finset.sum_nonneg (by aesop)

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

Goal state before:
pp: case refine_2
S : Type u_1
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
X : Type u_2
Y : Type u_3
inst✝² : Fintype X
inst✝¹ : Fintype Y
inst✝ : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : ∑ x, s x = 1
⊢ ∑ x, {x_1 | f x_1 = x}.sum s = ∑ x, s x

Tactic:
exact Finset.sum_fiberwise Finset.univ f s

Goal state after: