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

Goal state before:
pp: case top
⊢ (match ∞, 0 with
    | some x, y => if x = 0 ∧ y < 0 then ∞ else ↑(x.rpow y)
    | none, y => if 0 < y then ∞ else if y = 0 then 1 else 0) =
    1

Tactic:
simp [← none_eq_top]

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

Goal state before:
pp: case coe
x✝ : ℝ≥0
⊢ (if x✝ = 0 ∧ 0 < 0 then ∞ else ↑(x✝.rpow 0)) = 1

Tactic:
simp [← none_eq_top]

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

Goal state before:
pp: b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti fun x ↦ b ^ x

Tactic:
by
  simp_rw [Real.rpow_def_of_pos hb₀]
  exact exp_strictMono.comp_strictAnti <| StrictMono.const_mul_of_neg strictMono_id
      <| Real.log_neg hb₀ hb₁

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

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

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ by rw [H]⟩
  rcases hx₁.lt_or_gt with h | h
  · exact (strictAnti_rpow_of_base_lt_one hx₀ h).injective H
  · exact (strictMono_rpow_of_base_gt_one h).injective H

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

Goal state before:
pp: case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p

Tactic:
exact rpow_lt_rpow hx_pos hp_pos

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

Goal state before:
pp: case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_nonpos : p ≤ 0
⊢ 0 < x ^ p

Tactic:
← neg_neg p,

Goal state after:
case inr
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hx_ne_top : x ≠ ∞
hp_nonpos : p ≤ 0
⊢ 0 < x ^ (- -p)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: a b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ b = a ^ (-(↑n / ↑d))

Tactic:
hb.neg_to_eq rfl rfl

Goal state after:
a b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ (-(↑n / ↑d)) = a ^ (-(↑n / ↑d))
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: a : ℝ≥0
b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ b = a ^ (-(↑n / ↑d))

Tactic:
hb.neg_to_eq rfl rfl

Goal state after:
a : ℝ≥0
b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ (-(↑n / ↑d)) = a ^ (-(↑n / ↑d))
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
S : Type u_5
inst✝⁵ : CommSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : SMulPosMono S R
inst✝ : IsScalarTower S R M
a : S
v : M
h : 0 ≤ a
⊢ SameRay R v (a • v)

Tactic:
obtain h | h := (algebraMap_nonneg R h).eq_or_lt'
  · rw [← algebraMap_smul R a v, h, zero_smul]
    exact zero_right _
  · refine Or.inr <| Or.inr ⟨algebraMap S R a, 1, h, by nontriviality R; exact zero_lt_one, ?_⟩
    module

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
⊢ SameRay R (x + y) z

Tactic:
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.Ray

Goal state before:
pp: case 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
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ = 0
⊢ SameRay R (c₁ • v) (c₂ • v)

Tactic:
rw [hc₁, zero_smul]; exact SameRay.zero_left _

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case 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
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ = 0
⊢ SameRay R (c₁ • v) (c₂ • v)

pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ ≠ 0
⊢ SameRay R (c₁ • v) (c₂ • v)

Tactic:
· rw [hc₁, zero_smul]; exact SameRay.zero_left _

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ ≠ 0
⊢ SameRay R (c₁ • v) (c₂ • v)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
⊢ [x -[𝕜] y] ⊆ insert x (insert y (openSegment 𝕜 x y))

Tactic:
rintro z ⟨a, b, ha, hb, hab, rfl⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ insert x (insert y (openSegment 𝕜 x y))
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 : (fun x ↦ 2 • x) x = (fun x ↦ 2 • x) y
⊢ x = y

Tactic:
by
    dsimp at h
    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: case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 x t
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∪ t

Tactic:
exact Or.inl (hs hy ha hb hab)

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
⊢ x ∈ openSegment 𝕜 x y → x = y

Tactic:
rintro ⟨a, b, _, hb, hab, hx⟩

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
a b : 𝕜
left✝ : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
⊢ x = y
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x y : E
h : x ≤ y
⊢ [x -[𝕜] y] ⊆ Icc x y

Tactic:
rintro z ⟨a, b, ha, hb, hab, rfl⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x y : E
h : x ≤ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ Icc x y
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedCancelAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
⊢ openSegment 𝕜 x y ⊆ Ioo x y

Tactic:
rintro z ⟨a, b, ha, hb, hab, rfl⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedCancelAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ Ioo x y
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : y ≤ x
⊢ Icc y x = Icc (min x y) x

Tactic:
min_eq_right h

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : y ≤ x
⊢ Icc y x = Icc y x
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : IsStrictOrderedModule 𝕜 E
inst✝ : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
hz : z ∈ (Iic x)ᶜ
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • y + b • z ∈ (Iic x)ᶜ

Tactic:
rw [mem_compl_iff, mem_Iic] at hz ⊢

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : IsStrictOrderedModule 𝕜 E
inst✝ : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
hz : ¬z ≤ x
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ¬a • y + b • z ≤ x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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 : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
hp₂ : p₂ ∈ ↑s
⊢ (fun x ↦ x -ᵥ p) p₂ ∈ ↑s -ᵥ ↑s

Tactic:
exact ⟨p₂, hp₂, p, hp, rfl⟩

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
p : P
direction : Submodule k V
⊢ (mk' p direction).direction = direction

Tactic:
by
  ext v
  rw [mem_direction_iff_eq_vsub (mk'_nonempty _ _)]
  constructor
  · rintro ⟨p₁, hp₁, p₂, hp₂, rfl⟩
    simpa using direction.sub_mem hp₁ hp₂
  · exact fun hv => ⟨v +ᵥ p, vadd_mem_mk' _ hv, p, self_mem_mk' _ _, (vadd_vsub _ _).symm⟩

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
s₁ : AffineSubspace k P
h : s ⊆ ↑s₁
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ ↑s₁
hs : ∀ ⦃x : V⦄, x ∈ vectorSpan k s → x ∈ s₁.direction
⊢ v ∈ ↑s₁.direction

Tactic:
exact Set.mem_of_mem_of_subset hv hs

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

Goal state before:
pp: case inl
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 : Set P
inst✝ : Nontrivial P
hs : s = ∅
⊢ affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤

Tactic:
simp [hs, subsingleton_iff_bot_eq_top, AddTorsor.subsingleton_iff V P, not_subsingleton]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
x : E
⊢ (∃ t ∈ {t | Balanced 𝕜 t ∧ t ⊆ s}, x ∈ t) ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t

Tactic:
mem_ofPred_eq,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
x : E
⊢ (∃ t, (Balanced 𝕜 t ∧ t ⊆ s) ∧ x ∈ t) ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
Module: Mathlib.Analysis.LocallyConvex.Basic

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

Tactic:
norm_le_zero_iff

Goal state after:
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : NormedDivisionRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
s : Set E
inst✝⁴ : NormedRing 𝕝
inst✝³ : Module 𝕜 𝕝
inst✝² : NormSMulClass 𝕜 𝕝
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
hs : Balanced 𝕝 s
a : 𝕝
h : a = 0
⊢ a • s ⊆ 0 • s
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 t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
⊢ StrictConvex 𝕜 (s ∩ t)

Tactic:
intro x hx y hy hxy a b ha hb hab
  rw [interior_inter]
  exact ⟨hs hx.1 hy.1 hxy ha hb hab, ht hx.2 hy.2 hxy ha hb hab⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
s : Set E
x y : E
inst✝² : IsOrderedRing 𝕜
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
⊢ x = y

Tactic:
by
  obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
  classical
    by_contra hxy
    exact
      (h ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, rfl⟩).2
        (hs hx hy hxy ha₀ (sub_pos_of_lt ha₁) <| add_sub_cancel _ _)

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst✝⁹ : Semiring 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : SMul 𝕜 E
inst✝¹ : SMul 𝕜 α
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : StrictConvexOn 𝕜 (f '' s) g
hf : ConvexOn 𝕜 s f
hg' : MonotoneOn g (f '' s)
hf' : InjOn f s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (g ∘ f) (a • x + b • y) ≤ g (a • f x + b • f y)

Tactic:
· refine hg' ?_ ?_ <| hf.right hx hy ha.le hb.le hab
    · exact mem_image_of_mem f <| hf.left hx hy ha.le hb.le hab
    · exact hg.left (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab

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
p₁ p₂ : P
⊢ vectorSpan k {p₁, p₂} = k ∙ (p₂ -ᵥ p₁)

Tactic:
rw [pair_comm, vectorSpan_pair]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝¹⁴ : SeminormedRing 𝕜
inst✝¹³ : SeminormedRing 𝕜₂
inst✝¹² : SeminormedRing 𝕜₃
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁰ : RingHomIsometric σ₂₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝⁹ : RingHomIsometric σ₁₃
inst✝⁸ : AddCommGroup E
inst✝⁷ : AddCommGroup E₂
inst✝⁶ : AddCommGroup E₃
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ E₂
inst✝³ : Module 𝕜₃ E₃
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x✝¹ : 𝕜
x✝ : E
⊢ p (f (x✝¹ • x✝)) = ‖x✝¹‖ * p (f x✝)

Tactic:
simp only [map_smulₛₗ _, map_smul_eq_mul, RingHomIsometric.norm_map]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
⊢ s.sup p ≤ ∑ i ∈ s, p i

Tactic:
refine Finset.sup_le_iff.mpr ?_

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
⊢ ∀ b ∈ s, p b ≤ ∑ i ∈ s, p i
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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✝⁴ : 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₁
⊢ (map f s).direction = Submodule.map f.linear s.direction

Tactic:
simp [direction_eq_vectorSpan, AffineMap.map_vectorSpan]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
x : E
⊢ p x + q (x - x) ≤ p x

Tactic:
simp only [sub_self, map_zero, add_zero]

Goal state after:
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
x : E
⊢ p x ≤ p x
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ ∑ t ∈ s, affineCombinationLineMapWeights i j c t = 1

Tactic:
simp_rw [affineCombinationLineMapWeights, Pi.add_apply, sum_add_distrib]
  simp [hi, hj, ← mul_sum]

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
x✝ : E
⊢ (sSup ∅) x✝ = ⊥ x✝

Tactic:
Seminorm.sSup_apply bddAbove_empty,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x✝ : E
⊢ ⨆ p, ↑p x✝ = ⊥ x✝
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₁ p₂ : P
⊢ line[k, p₁, p₂] = line[k, p₂, p₁]

Tactic:
rw [Set.pair_comm]

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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι ∈ s2, f ι = 0
f2 : ι → V := fun x ↦ f x • (p x -ᵥ p i1)
hf2def : f2 = fun x ↦ f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x ↦ g x • (p ↑x -ᵥ p i1)
hg : s.sum g2 = 0
hf2g2 : ∀ (x : { x // x ≠ i1 }), f2 ↑x = g2 x
⊢ ∑ i ∈ map (Embedding.subtype fun x ↦ x ≠ i1) s, f i • (p i -ᵥ p i1) = 0

Tactic:
Finset.sum_subtype_map_embedding fun x _ => hf2g2 x

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
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι ∈ s2, f ι = 0
f2 : ι → V := fun x ↦ f x • (p x -ᵥ p i1)
hf2def : f2 = fun x ↦ f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x ↦ g x • (p ↑x -ᵥ p i1)
hg : s.sum g2 = 0
hf2g2 : ∀ (x : { x // x ≠ i1 }), f2 ↑x = g2 x
⊢ ∑ x ∈ s, g2 x = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
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
p : ι → P
j : ι
q : P
⊢ (∃ s w, q = (s.weightedVSubOfPoint p (p j)) w +ᵥ p j) → q ∈ affineSpan k (Set.range p)

Tactic:
rintro ⟨s, w, rfl⟩

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
p : ι → P
j : ι
s : Finset ι
w : ι → k
⊢ (s.weightedVSubOfPoint p (p j)) w +ᵥ p j ∈ affineSpan k (Set.range p)
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
i j : ι
h : i ≠ j
⊢ (b.coord i) (b j) = 0

Tactic:
coord,

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
i j : ι
h : i ≠ j
⊢ { toFun := fun q ↦ 1 - (b.basisOf i).sumCoords (q -ᵥ b i), linear := -(b.basisOf i).sumCoords, map_vadd' := ⋯ }
      (b j) =
    0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : p.closedBall 0 r ∈ 𝓝 0
⊢ ContinuousAt (⇑p) 0

Tactic:
by
  refine continuousAt_zero_of_forall' fun ε hε ↦ ?_
  obtain ⟨k, hk₀, hk⟩ : ∃ k : 𝕜, 0 < ‖k‖ ∧ ‖k‖ * r < ε := by
    rcases le_or_gt r 0 with hr | hr
    · use 1; simpa using hr.trans_lt hε
    · simpa [lt_div_iff₀ hr] using exists_norm_lt 𝕜 (div_pos hε hr)
  grw [← hk]
  rwa [← set_smul_mem_nhds_zero_iff (norm_pos_iff.1 hk₀), smul_closedBall_zero hk₀] at hp

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 1 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
p : ι → P
ha : AffineIndependent k p
fs : Finset ι
w : ι → k
hw : ∑ i ∈ fs, w i = 1
s : Set ι
hm : (affineCombination k fs p) w ∈ affineSpan k (p '' s)
i : ι
hifs : i ∈ fs
his : i ∉ s
fs' : Finset ι
w' : ι → k
hfs's : ↑fs' ⊆ s
hw' : ∑ i ∈ fs', w' i = 1
he : (affineCombination k fs p) w = (affineCombination k fs' p) w'
⊢ w i = 0

Tactic:
have hi' : (fs : Set ι).indicator w i = 0 := by
    rw [ha.indicator_eq_of_affineCombination_eq fs fs' w w' hw hw' he]
    exact Set.indicator_of_notMem (Set.notMem_subset hfs's his) w'

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
p : ι → P
ha : AffineIndependent k p
fs : Finset ι
w : ι → k
hw : ∑ i ∈ fs, w i = 1
s : Set ι
hm : (affineCombination k fs p) w ∈ affineSpan k (p '' s)
i : ι
hifs : i ∈ fs
his : i ∉ s
fs' : Finset ι
w' : ι → k
hfs's : ↑fs' ⊆ s
hw' : ∑ i ∈ fs', w' i = 1
he : (affineCombination k fs p) w = (affineCombination k fs' p) w'
hi' : (↑fs).indicator w i = 0
⊢ w i = 0
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 (Set.range (s.faceOpposite i).points)

Tactic:
· rw [range_faceOpposite_points]
    rcases subsingleton_or_nontrivial k with hk | hk
    · have : Subsingleton V := Module.subsingleton k _
      have : Subsingleton P := (AddTorsor.subsingleton_iff V P).1 inferInstance
      rw [(affineSpan_eq_top_iff_nonempty_of_subsingleton k).2 (by simp)]
      simp
    · exact affineCombination_mem_affineSpan_image hw (by simpa using h) s.points

Goal state after: