mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f (M k k) * f ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0

Tactic:
det_mul,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S),
    (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det
⊢ (f (M k k)).det * (f ((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).det).det -
      (f (M k k)).det *
        ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
            (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    0
Module: Mathlib.Topology.TietzeExtension

Goal state before:

Tactic:
f x = c - (b - c) := by rw [← hsub, sub_sub_cancel]
        _ ≤ g y - dg y := sub_le_sub hc.le (dgmem _).2

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h✝ : IsEmpty X
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h✝ : Nonempty X
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
· rcases hne with ⟨c, hc⟩
    exact ⟨const Y c, fun _ => hc, funext fun x => isEmptyElim x⟩

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h✝ : Nonempty X
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ deriv (fun z ↦ ↑(g • ↑ofComplex z)) ↑τ ≠ 0

Tactic:
rw [deriv_smul hg]

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ ↑(↑g).det / denom g ↑τ ^ 2 ≠ 0
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
inst✝ : CompactSpace β
⊢ stoneCechExtend hg ∘ stoneCechUnit = g

Tactic:
ext x
  rw [stoneCechExtend, Function.comp_apply, stoneCechUnit, T2Quotient.lift_mk]
  apply congrFun (preStoneCechExtend_extends hg)

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: case refine_2
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
x✝ :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
⊢ ProperSMul G X

Tactic:
· rw [properSMul_iff, isProperMap_iff_ultrafilter]
    refine ⟨by fun_prop, fun 𝒰 (x₁, x₂) hxx ↦ ?_⟩
    rcases h 𝒰 x₁ x₂ hxx with ⟨g, hg1, hg2⟩
    refine ⟨(g, x₂), by simp_rw [hg1], ?_⟩
    rw [nhds_prod_eq, 𝒰.le_prod]
    exact ⟨hg2, (continuous_snd.tendsto _).comp hxx⟩

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : Infinite X
inst✝ : DiscreteTopology X
⊢ ¬Continuous[_, instTopologicalSpace] ⇑CofiniteTopology.of.symm

Tactic:
inhabit X
  simp only [continuous_iff_continuousAt, ContinuousAt, not_forall]
  use CofiniteTopology.of ↑(default : X)
  simpa [nhds_coe_eq, nhds_discrete, CofiniteTopology.nhds_eq, Equiv.symm_apply_eq,
    Set.compl_def, Set.mem_singleton_iff] using (finite_singleton _).infinite_compl

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: 𝒢 : Subgroup SL(2, ℝ)
inst✝ : DiscreteTopology ↥𝒢
⊢ ProperlyDiscontinuousSMul ↥𝒢 ℍ

Tactic:
have : IsClosed (𝒢 : Set SL(2, ℝ)) := Subgroup.isClosed_of_discrete
  rw [properlyDiscontinuousSMul_iff_properSMul]
  infer_instance

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E)ᶜ
⊢ (convexHull ℝ) (connectedComponentIn (↑E)ᶜ x) = univ

Tactic:
rw [E.connectedComponentIn_eq_self_of_one_lt_codim hcodim hx, eq_univ_iff_forall]
  intro y
  by_cases h : y ∈ E
  · obtain ⟨z, hz⟩ : ∃ z, z ∉ E := by
      rw [← not_forall, ← Submodule.eq_top_iff']
      rintro rfl
      simp at hcodim
    refine segment_subset_convexHull ?_ ?_ (mem_segment_sub_add y z) <;>
      simpa [sub_eq_add_neg, Submodule.add_mem_iff_right _ h]
  · exact subset_convexHull ℝ (Eᶜ : Set F) h

Goal state after:
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
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
hle : D' ≤ D
R₀ : ℝ
hR₀ : ∀ z ∈ t, ‖z‖ ≤ R₀
K : ℝ := ∑ z ∈ t, log ‖z‖
hK : K = ∑ z ∈ t, log ‖z‖
r : ℝ
hr : R₀ ≤ r
⊢ ∑ z ∈ t, (log r - log ‖z‖) = ↑N * log r - K

Tactic:
by simp [Finset.sum_sub_distrib, hK, htcard]

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

Goal state before:
pp: R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
⊢ (logCounting f 0 - logCounting f ⊤) R = circleAverage (fun x ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
rw [← locallyFinsuppWithin.logCounting_divisor]

Goal state after:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
⊢ locallyFinsuppWithin.logCounting (divisor f univ) R =
    circleAverage (fun x ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝¹ : RCLike 𝕜
inst✝ : TopologicalSpace E
hsc : IsClosed s
hφ_cont : LowerSemicontinuousOn φ s
A : Set (E × EReal) := {p | p.1 ∈ s ∧ ↑(φ p.1) ≤ p.2}
hC : {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2} = Prod.map id (Real.toEReal ∘ ⇑re) ⁻¹' A
⊢ Continuous (Prod.map id (Real.toEReal ∘ ⇑re))

Tactic:
exact continuous_id.prodMap <| continuous_coe_real_ereal.comp reCLM.cont

Goal state after:
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 '' affineSegment R x y = affineSegment R (f x) (f y)

Tactic:
by
  rw [affineSegment, affineSegment, Set.image_image, ← comp_lineMap]
  rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : PartialOrder R
x : R
⊢ Sbtw R 0 x 1 ↔ x ∈ Set.Ioo 0 1

Tactic:
rw [Sbtw, wbtw_zero_one_iff, Set.mem_Icc, Set.mem_Ioo]

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : PartialOrder R
x : R
⊢ (0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ 0 < x ∧ x < 1
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite (F.obj j)
hne : ∀ (j : J), Nonempty (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
this✝¹ : ∀ (j : J), DiscreteTopology ↑(F'.obj j)
this✝ : ∀ (j : J), Finite ↑(F'.obj j)
this : ∀ (j : J), Nonempty ↑(F'.obj j)
u : (j : J) → ↑(F'.obj j)
hu : u ∈ {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F'.map f)) (u i) = u j}
⊢ F.sections.Nonempty

Tactic:
exact ⟨u, hu⟩

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

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
⊢ (Finset.affineCombination R Finset.univ s.points) (Finset.affineCombinationLineMapWeights 0 1 r) ∈ s.interior

Tactic:
affineCombination_mem_interior_iff
        (Finset.sum_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _) _)

Goal state after:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
⊢ ∀ (i : Fin (1 + 1)), Finset.affineCombinationLineMapWeights 0 1 r i ∈ Set.Ioo 0 1
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
⊢ (lineMap (s.points 0) (s.points 1)) r ∈ s.interior

Tactic:
rw [← Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _), affineCombination_mem_interior_iff
        (Finset.sum_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _) _)]

Goal state after:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
r : R
h0 : 0 < r
h1 : r < 1
⊢ ∀ (i : Fin (1 + 1)), Finset.affineCombinationLineMapWeights 0 1 r i ∈ Set.Ioo 0 1
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
p : P
⊢ p ∈ ⇑(lineMap (s.points 0) (s.points 1)) '' Set.Ioo 0 1 → p ∈ s.interior

Tactic:
rintro ⟨r, ⟨h0, h1⟩, rfl⟩
    rw [← Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
      (Finset.mem_univ _), affineCombination_mem_interior_iff
        (Finset.sum_affineCombinationLineMapWeights _ (Finset.mem_univ _) (Finset.mem_univ _) _)]
    intro i
    fin_cases i <;> simp [h0, h1]

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
j : n
⊢ f.toPEquiv.toMatrixᵀ j = Pi.single (f.symm j) 1

Tactic:
ext
  simp [toMatrix_apply, Pi.single_apply, eq_comm, Equiv.eq_symm_apply]

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: case h.none.some
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬f i = g i
hf : f i = none
gi : n
hg : g i = some gi
⊢ ∃ x, ¬(if x ∈ none then 1 else 0) = if x ∈ some gi then 1 else 0

Tactic:
use gi
      simp

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁵ : Fintype n
inst✝⁴ : Fintype k
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : Semiring α
a : m
b : n
c : k
M : Matrix k l α
⊢ (single a b).toMatrix * (single b c).toMatrix * M = (single a c).toMatrix * M

Tactic:
single_mul_single

Goal state after:
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁵ : Fintype n
inst✝⁴ : Fintype k
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : Semiring α
a : m
b : n
c : k
M : Matrix k l α
⊢ (single a c).toMatrix * M = (single a c).toMatrix * M
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

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
hM : M ∈ doublyStochastic R n
i j : n
⊢ M i j ≤ 1

Tactic:
← sum_row_of_mem_doublyStochastic hM i

Goal state after:
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
hM : M ∈ doublyStochastic R n
i j : n
⊢ M i j ≤ ∑ j, M i j
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_2
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
hne : x ≠ y
r : R
hr : 1 < r
⊢ 1 • (y -ᵥ x) - r • (y -ᵥ x) ≠ 0

Tactic:
rw [← sub_smul, smul_ne_zero_iff, vsub_ne_zero, sub_ne_zero]

Goal state after:
case refine_2
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
hne : x ≠ y
r : R
hr : 1 < r
⊢ 1 ≠ r ∧ y ≠ x
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: 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 : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)

Tactic:
refine ⟨r₁ / r₂, ⟨div_nonneg hr₁ (hr₁.trans hr₂), div_le_one_of_le₀ hr₂ (hr₁.trans hr₂)⟩, ?_⟩
  by_cases h : r₁ = 0; · simp [h]
  simp [lineMap_apply, smul_smul, ((hr₁.lt_of_ne' h).trans_le hr₂).ne.symm]

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

Goal state before:
pp: case inl
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 : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ 0
h : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x)

Tactic:
exact Or.inr (wbtw_smul_vadd_smul_vadd_of_nonpos_of_le x v hr₂ h)

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

Goal state before:
pp: 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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : t₂ * t₁ = 1
this : t₁ = 1
⊢ ((t₁ - 1) * ((1 - 1) / (1 - 1)) + 1) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
by simp [this]

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

Goal state before:
pp: case refine_2
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
σ : Equiv.Perm n
⊢ Equiv.Perm.permMatrix R σ ∈ Set.extremePoints R ↑(doublyStochastic R n)

Tactic:
refine ⟨permMatrix_mem_doublyStochastic, fun x₁ hx₁ x₂ hx₂ hσ ↦ ?_⟩

Goal state after:
case refine_2
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
⊢ x₁ = Equiv.Perm.permMatrix R σ
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: 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 z : P
v : V
h : ∀ (p : P), p = x ∨ p = y ∨ p = z → ∃ r, p = r • v +ᵥ x
hy : ∃ r, y = r • v +ᵥ x
hz : ∃ r, z = r • v +ᵥ x
⊢ Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y

Tactic:
rcases hy with ⟨ty, rfl⟩

Goal state after:
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 z : P
v : V
hz : ∃ r, z = r • v +ᵥ x
ty : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = z → ∃ r, p = r • v +ᵥ x
⊢ Wbtw R x (ty • v +ᵥ x) z ∨ Wbtw R (ty • v +ᵥ x) z x ∨ Wbtw R z x (ty • v +ᵥ x)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: 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
h : x ≠ y
⊢ Sbtw R y x ((pointReflection R x) y)

Tactic:
by
  refine ⟨wbtw_pointReflection _ _ _, h, ?_⟩
  nth_rw 1 [← pointReflection_self R x]
  exact (pointReflection_involutive R x).injective.ne h

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.TensorProduct

Goal state before:
pp: case refine_2
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
i : ↑s
x✝ : i ∈ Finset.univ
f : F →L[ℝ] ℝ
⊢ f ∈ ↑(ProperCone.dual (topDualPairing ℝ F).flip ↑C₂) →
    0 ≤ ((topDualPairing ℝ F) f) ((TensorProduct.lid ℝ F) ((LinearMap.rTensor F (b.coord i)) z))

Tactic:
(hf : (f : F →ₗ[ℝ] ℝ) ∈ dual (Dual.eval ℝ F) (C₂ : Set F))

Goal state after:
case refine_2
E : Type u_1
F : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module ℝ F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : T2Space F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : ContinuousSMul ℝ F
inst✝ : LocallyConvexSpace ℝ F
C₁ : PointedCone ℝ E
C₂ : ProperCone ℝ F
h₁_gen : Submodule.span ℝ ↑C₁ = ⊤
s : Set E
hs_fin : s.Finite
hs_lin : LinearIndepOn ℝ id s
hs_span : hull ℝ s = C₁
this : Fintype ↑s
hull_sub_span : ↑(hull ℝ s) ⊆ ↑(Submodule.span ℝ s)
b : Basis ↑s ℝ E := Basis.mk hs_lin ⋯
h_coord_dual : ∀ (i : ↑s), b.coord i ∈ dual (Dual.eval ℝ E) ↑C₁
z : E ⊗[ℝ] F
hz : z ∈ C₁.maxTensorProduct ↑C₂
i : ↑s
x✝ : i ∈ Finset.univ
f : F →L[ℝ] ℝ
hf : ↑f ∈ dual (Dual.eval ℝ F) ↑C₂
⊢ 0 ≤ ((topDualPairing ℝ F) f) ((TensorProduct.lid ℝ F) ((LinearMap.rTensor F (b.coord i)) z))
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
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb).symm '' closure[inst✝³] t ⊆ closure[inst✝³] s

Tactic:
exact (mapsTo_gaugeRescale_closure htc ht₀ hsc
    (mem_of_mem_nhds hs₀) (absorbent_nhds_zero hs₀)).image_subset

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Convex

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i} ⊆ interior ((convexHull ℝ) (range ⇑b) + (convexHull ℝ) ↑u)

Tactic:
← subset_interior_add_left,

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
U : Set E
hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU₂ : s ⊆ U
hU₃ : U ⊆ t
V : Set E
hV₁ : V ∈ 𝓝 0
hV₂ : V + s ⊆ U
b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E
hb₁ : 0 ∈ interior ((convexHull ℝ) (range ⇑b))
hb₂ : (convexHull ℝ) (range ⇑b) ⊆ V
u : Finset E
hu₁ : ↑u ⊆ s
hu₃ : s ⊆ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i}
⊢ ⋃ i ∈ ↑u, interior ((convexHull ℝ) (range ⇑b)) + {i} ⊆ interior ((convexHull ℝ) (range ⇑b)) + (convexHull ℝ) ↑u
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 +ᵥ -y +ᵥ interior t = interior t

Tactic:
vadd_neg_vadd

Goal state after:
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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ interior t = interior t
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 +ᵥ -y +ᵥ closure[inst✝³] t = closure[inst✝³] t

Tactic:
vadd_neg_vadd

Goal state after:
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) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ closure[inst✝³] t = closure[inst✝³] t