mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
a b : α
f : α → β
hcf : Continuous[inst✝³, inst✝²] f
h : stoneCechUnit a = stoneCechUnit b
⊢ (stoneCechExtend hcf ∘ stoneCechUnit) a = f b

Tactic:
← congrFun (stoneCechExtend_extends hcf)

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
a b : α
f : α → β
hcf : Continuous[inst✝³, inst✝²] f
h : stoneCechUnit a = stoneCechUnit b
⊢ (stoneCechExtend hcf ∘ stoneCechUnit) a = (stoneCechExtend hcf ∘ stoneCechUnit) b
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X ↦ ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X ↦ ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
g : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun y' ↦ { down := ⟨φ y', ⋯⟩ }, continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun x ↦ { down := ⟨0, ⋯⟩ }, continuous_toFun := ⋯ }
⊢ h = g

Tactic:
rw [← cancel_epi f]

Goal state after:
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X ↦ ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X ↦ ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
g : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun y' ↦ { down := ⟨φ y', ⋯⟩ }, continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun x ↦ { down := ⟨0, ⋯⟩ }, continuous_toFun := ⋯ }
⊢ f ≫ h = f ≫ g
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : IsTopologicalGroup G
⊢ IsProperMap fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
by
    let Φ : Gᵐᵒᵖ × G ≃ₜ G × G :=
    { toFun := fun gh ↦ (gh.2 * (unop gh.1), gh.2)
      invFun := fun gh ↦ (op (gh.2⁻¹ * gh.1), gh.2)
      left_inv := fun _ ↦ by simp
      right_inv := fun _ ↦ by simp }
    exact Φ.isProperMap

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ IsOpen[tX] s

Tactic:
rw [eq_compactlyGenerated (X := X), TopologicalSpace.compactlyGenerated, isOpen_coinduced,
    isOpen_sigma_iff]

Goal state after:
X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ ∀ (i : (S : CompHaus) × C(↑S.toTop, X)),
    IsOpen
      (Sigma.mk i ⁻¹'
        (fun x ↦
            match x with
            | ⟨⟨fst, i⟩, s⟩ => i s) ⁻¹'
          s)
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : CompactlyCoherentSpace X
⊢ CompactlyGeneratedSpace X

Tactic:
by
  apply compactlyGeneratedSpace_of_isClosed_of_t2
  intro s hs
  rw [CompactlyCoherentSpace.isClosed_iff]
  intro K hK
  rw [← Subtype.preimage_coe_inter_self]
  exact (hs K hK).preimage_val

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
⊢ (fun r ↦ ∑ᶠ (z : E), ↑(((toClosedBall r) (D₁ + D₂)) z) * log (r * ‖z‖⁻¹) + ↑((D₁ + D₂) 0) * log r) =
    (fun r ↦ ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ↑(D₁ 0) * log r) + fun r ↦
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹) + ↑(D₂ 0) * log r

Tactic:
simp only [map_add, coe_add, Pi.add_apply, Int.cast_add]

Goal state after:
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
⊢ (fun r ↦
      ∑ᶠ (z : E), (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹) +
        (↑(D₁ 0) + ↑(D₂ 0)) * log r) =
    (fun r ↦ ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ↑(D₁ 0) * log r) + fun r ↦
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹) + ↑(D₂ 0) * log r
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : (support D).Finite
⊢ logCounting D =O[atTop] log

Tactic:
rw [← sum_apply_smul_single_eq_self_on_univ h, map_sum]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : (support D).Finite
⊢ (∑ x ∈ h.toFinset, logCounting (single x (D x))) =O[atTop] log
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
⊢ False

Tactic:
obtain ⟨t, htsub, htcard⟩ := hInf.exists_subset_card_eq N

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
⊢ False
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
α : Type u_3
s : Finset α
f : α → 𝕜 → E
r : ℝ
h₁f : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r

Tactic:
classical
  induction s using Finset.induction with
  | empty =>
    simp
  | insert a s ha hs =>
    rw [Finset.sum_insert ha, Finset.sum_insert ha]
    calc logCounting (f a + ∑ x ∈ s, f x) ⊤ r
      _ ≤ (logCounting (f a) ⊤ + logCounting (∑ x ∈ s, f x) ⊤) r :=
        logCounting_add_top_le (h₁f a (Finset.mem_insert_self a s))
          (Meromorphic.sum (fun σ hσ ↦ h₁f σ (Finset.mem_insert_of_mem hσ))) hr
      _ ≤ (logCounting (f a) ⊤ + ∑ x ∈ s, logCounting (f x) ⊤) r :=
        add_le_add (by trivial) (hs (fun a ha ↦ h₁f a (Finset.mem_insert_of_mem ha)))

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) → eVariationOn f s = 0

Tactic:
by_contra! ⟨h, hfs⟩

Goal state after:
case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0
hfs : eVariationOn f s ≠ 0
⊢ False
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
f : P →ᵃ[R] P'
x y : P
⊢ ⇑f '' ⇑(lineMap x y) '' Set.Icc 0 1 = ⇑(lineMap (f x) (f y)) '' Set.Icc 0 1

Tactic:
Set.image_image,

Goal state after:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
f : P →ᵃ[R] P'
x y : P
⊢ (fun x_1 ↦ f ((lineMap x y) x_1)) '' Set.Icc 0 1 = ⇑(lineMap (f x) (f y)) '' Set.Icc 0 1
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : Nontrivial P
l : List P
hl : ¬l = []
h : ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)
hlen : ¬l.length = 1
⊢ l.head hl ≠ l.getLast hl ∧ ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l

Tactic:
simp only [hlen, false_or] at h

Goal state after:
case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : Nontrivial P
l : List P
hl : ¬l = []
hlen : ¬l.length = 1
h : ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ l.head hl ≠ l.getLast hl
⊢ l.head hl ≠ l.getLast hl ∧ ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: case some
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ (∑ j_1, M i j_1 * if j ∈ f j_1 then 1 else 0) = Option.rec 0 (fun val ↦ M i val) (some fj)

Tactic:
Finset.sum_eq_single fj

Goal state after:
case some
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ (M i fj * if j ∈ f fj then 1 else 0) = Option.rec 0 (fun val ↦ M i val) (some fj)

case some.h₀
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ ∀ b ∈ Finset.univ, b ≠ fj → (M i b * if j ∈ f b then 1 else 0) = 0

case some.h₁
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ fj ∉ Finset.univ → (M i fj * if j ∈ f fj then 1 else 0) = 0
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
⊢ M ∈ colStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ ∀ (j : n), ∑ i, M i j = 1

Tactic:
by
  simp [funext_iff, colStochastic, vecMul, dotProduct]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 Subtype.val
x : E
m : ∃ w, (∀ y ∈ t, 0 ≤ w y) ∧ ∑ y ∈ t, w y = 1 ∧ t.centerMass w id = x
⊢ ∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = x

Tactic:
obtain ⟨f, fpos, fsum, rfl⟩ := m

Goal state after:
𝕜 : Type u_1
E : Type u
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 Subtype.val
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : ∑ y ∈ t, f y = 1
⊢ ∃ y w, (∀ y_1 ∈ t.erase ↑y, 0 ≤ w y_1) ∧ ∑ y ∈ t.erase ↑y, w y = 1 ∧ (t.erase ↑y).centerMass w id = t.centerMass f id
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_2.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : r ∈ Set.Ici 1
⊢ Wbtw R x y ((lineMap x y) r)

Tactic:
rw [Set.mem_Ici] at hr

Goal state after:
case refine_2.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
⊢ Wbtw R x y ((lineMap x y) r)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : r ∈ Set.Ici 1
h : Sbtw R x y ((lineMap x y) r)
⊢ (lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioi 1

Tactic:
rw [Set.mem_Ici] at hr

Goal state after:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
r : R
hr : 1 ≤ r
h : Sbtw R x y ((lineMap x y) r)
⊢ (lineMap x y) r ∈ ⇑(lineMap x y) '' Set.Ioi 1
Module: Mathlib.Analysis.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsOrderedRing R
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : ClosedIciTopology R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝² : p.IsContPerfPair
inst✝¹ : IsTopologicalRing R
inst✝ : T1Space N
y : N
hy : y ∈ dual p univ
x : M
⊢ (p.flip.toContPerfPair y) x = 0 x

Tactic:
exact (hy <| mem_univ x).antisymm' <| by simpa using hy <| mem_univ (-x)

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Dual

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
hp : Injective ⇑p.flip
y : N
hy : y ∈ dual p univ
x : M
⊢ (p.flip y) x = 0 x

Tactic:
exact (hy <| mem_univ x).antisymm' <| by simpa using hy <| mem_univ (-x)

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ y +ᵥ ⇑h '' interior (-x +ᵥ s) = interior t

Tactic:
rw [image_gaugeRescaleHomeomorph_interior, interior_vadd, vadd_neg_vadd]

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
s : Set P
t : Set Q
e : ↥(affineSpan 𝕜 (s ×ˢ t)) ≃ₜ ↥(affineSpan 𝕜 s) × ↥(affineSpan 𝕜 t) :=
  (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑(affineSpan 𝕜 s) ↑(affineSpan 𝕜 t))
this : Subtype.val ∘ ⇑e.symm = fun p ↦ (↑p.1, ↑p.2)
h : Subtype.val ⁻¹' s ×ˢ t = ⇑e ⁻¹' (Subtype.val ⁻¹' s) ×ˢ (Subtype.val ⁻¹' t)
⊢ intrinsicInterior 𝕜 (s ×ˢ t) = intrinsicInterior 𝕜 s ×ˢ intrinsicInterior 𝕜 t

Tactic:
intrinsicInterior,

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
s : Set P
t : Set Q
e : ↥(affineSpan 𝕜 (s ×ˢ t)) ≃ₜ ↥(affineSpan 𝕜 s) × ↥(affineSpan 𝕜 t) :=
  (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.prod ↑(affineSpan 𝕜 s) ↑(affineSpan 𝕜 t))
this : Subtype.val ∘ ⇑e.symm = fun p ↦ (↑p.1, ↑p.2)
h : Subtype.val ⁻¹' s ×ˢ t = ⇑e ⁻¹' (Subtype.val ⁻¹' s) ×ˢ (Subtype.val ⁻¹' t)
⊢ Subtype.val '' interior (Subtype.val ⁻¹' s ×ˢ t) =
    (Subtype.val '' interior (Subtype.val ⁻¹' s)) ×ˢ (Subtype.val '' interior (Subtype.val ⁻¹' t))
Module: Mathlib.Analysis.Convex.Measure

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Bornology.IsBounded t → μ (frontier t) = 0
⊢ μ (frontier s) = 0

Tactic:
let B : ℕ → Set E := fun n => ball x (n + 1)

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Bornology.IsBounded t → μ (frontier t) = 0
B : ℕ → Set E := fun n ↦ ball x (↑n + 1)
⊢ μ (frontier s) = 0
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ intrinsicInterior 𝕜 (f '' s) = f '' intrinsicInterior 𝕜 s

Tactic:
intrinsicInterior,

Goal state after:
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
this : Nonempty ↑s
⊢ Subtype.val '' interior (Subtype.val ⁻¹' f '' s) = f '' intrinsicInterior 𝕜 s
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u
inst✝² : PartialOrder R
inst✝¹ : Semiring R
M : Type u_9
inst✝ : Nontrivial R
⊢ ∀ (w : StdSimplex R M), w.weights ≠ 0

Tactic:
rintro ⟨_, -, total⟩ rfl; simp at total

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

Goal state before:
pp: V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ (intrinsicInterior ℝ s).Nonempty

Tactic:
intrinsicInterior,

Goal state after:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ (Subtype.val '' interior (Subtype.val ⁻¹' s)).Nonempty
Module: Mathlib.Geometry.Convex.Star

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
x : X
S : Set (Set X)
hS : ∀ s ∈ S, IsStarConvexSet R x s
⊢ IsStarConvexSet R x (⋂₀ S)

Tactic:
simp +contextual [IsStarConvexSet, hS _ _ _]

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

Goal state before:
pp: R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
x : X
s : Set X
hf : IsAffineMap R f
hs : IsStarConvexSet R x s
⊢ IsStarConvexSet R (f x) (f '' s)

Tactic:
rintro _ ⟨y, hy, rfl⟩ a b ha hb hab

Goal state after:
R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
x : X
s : Set X
hf : IsAffineMap R f
hs : IsStarConvexSet R x s
y : X
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ convexCombPair a b ha hb hab (f x) (f y) ∈ f '' s
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
⊢ convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    convexCombPair (s + t * s') (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃

Tactic:
simp only [add_comm s]

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
⊢ convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
x y : X
s t s' t' : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
hss' : s' ≤ s
this : dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) ≤ |s - s'| * dist x y
⊢ dist (convexCombPair s t hs ht h x y) (convexCombPair s' t' hs' ht' h' x y) = |s - s'| * dist x y

Tactic:
refine this.antisymm ?_
    nth_grw 2 [← abs_dist_sub_le (z := x)]
    have : |t - t'| = |s - s'| := by
      rw [eq_sub_iff_add_eq.mpr h, eq_sub_iff_add_eq.mpr h']; simp [abs_sub_comm t t']
    simp [← sub_mul, this]

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Pow

Goal state before:
pp: p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ⇑f
⊢ ∀ (x : ℝ≥0), f.symm x = x ^ p

Tactic:
simp [f, NNReal.orderIsoRpow_symm_eq]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G.edgeSet s ↔ Disjoint s G.edgeSet

Tactic:
disjoint_comm

Goal state after:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint s G.edgeSet ↔ Disjoint s G.edgeSet
Module: Mathlib.Analysis.Convex.Strict.Extreme

Goal state before:
pp: A : Type u_1
inst✝² : NormedAddCommGroup A
inst✝¹ : NormedSpace ℝ A
inst✝ : StrictConvexSpace ℝ A
a : A
r : ℝ
hr : r ≠ 0
x✝ : A
hx : x✝ ∈ sphere a r
⊢ x✝ ∈ extremePoints ℝ (closedBall a r)

Tactic:
by
  rw [← frontier_closedBall _ hr, frontier, closure_closedBall] at hx
  exact (_root_.strictConvex_closedBall ℝ _ _).sdiff_interior_subset_extremePoints hx

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ insert v (G.neighborSet v) = Set.univ ↔ G.IsUniversal v

Tactic:
simp only [Set.ext_iff, Set.mem_insert_iff, mem_neighborSet, IsUniversal]
  grind

Goal state after: