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

Goal state before:
pp: case inr.inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
ha' : ¬∃ x, f x = a
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Ici c)
dga : EqOn (⇑dg) (Function.const Y (c - a)) (⇑g ⁻¹' {a})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (c - a)
hgf : ∀ (x : X), (g + dg) (e x) = f x
y : Y
hay : a < (g + dg) y
x : X
left✝ : a ≤ f x
hxy : f x < (g + dg) y
hc : c ≤ g y
⊢ (g + dg) y ≤ b

pp: case inr.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
ha' : ¬∃ x, f x = a
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Ici c)
dga : EqOn (⇑dg) (Function.const Y (c - a)) (⇑g ⁻¹' {a})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (c - a)
hgf : ∀ (x : X), (g + dg) (e x) = f x
y : Y
hay : a < (g + dg) y
x : X
left✝ : a ≤ f x
hxy : f x < (g + dg) y
hc : g y ≤ c
⊢ (g + dg) y ≤ b

Tactic:
· simp [dg0 (Or.inr hc), (hg_mem y).2]

Goal state after:
case inr.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
ha' : ¬∃ x, f x = a
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Ici c)
dga : EqOn (⇑dg) (Function.const Y (c - a)) (⇑g ⁻¹' {a})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (c - a)
hgf : ∀ (x : X), (g + dg) (e x) = f x
y : Y
hay : a < (g + dg) y
x : X
left✝ : a ≤ f x
hxy : f x < (g + dg) y
hc : g y ≤ c
⊢ (g + dg) y ≤ b
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
g : Y →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
x : X
hb : IsLUB (range ⇑f) (f x)
hmem : ∀ (x_1 : X), f x_1 ∈ Icc a (f x)
hle : a ≤ f x
hlt : a < f x
c : ℝ := (a + f x) / 2
hac : a < c
hcb : c < f x
hsub : c - a = f x - c
hgb : ∀ (y : Y), g y ≤ f x
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f

Tactic:
exact ⟨g, fun y => ⟨xl y, x, hxl y, hgb y⟩, hgf⟩

Goal state after:
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
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det *
      ∏ k_1, (((Matrix.comp m m n n R) ((auxMat M k).map ⇑f)).toSquareBlock (fun i ↦ i.1 ≠ k) k_1).det

Tactic:
Fintype.prod_Prop,

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
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det *
      ((((Matrix.comp m m n n R) ((auxMat M k).map ⇑f)).toSquareBlock (fun i ↦ i.1 ≠ k) True).det *
        (((Matrix.comp m m n n R) ((auxMat M k).map ⇑f)).toSquareBlock (fun i ↦ i.1 ≠ k) False).det)
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
⊢ ∏ k_1, (((Matrix.comp m m n n R) ((M * auxMat M k).map ⇑f)).toSquareBlock (fun i ↦ i.1 = k) k_1).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

Tactic:
Fintype.prod_Prop,

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
⊢ (((Matrix.comp m m n n R) ((M * auxMat M k).map ⇑f)).toSquareBlock (fun i ↦ i.1 = k) True).det *
      (((Matrix.comp m m n n R) ((M * auxMat M k).map ⇑f)).toSquareBlock (fun i ↦ i.1 = k) False).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
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n fun τ ↦ g • τ

Tactic:
intro τ
  refine contMDiffAt_iff_target.mpr ⟨(continuous_const_smul g).continuousAt, ?_⟩
  simpa [glPos_smul_def hg] using! (contMDiff_num g τ).mul (contMDiff_inv_denom g τ)

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

Goal state before:
pp: case hg'
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ deriv G ↑τ ≠ 0

Tactic:
exact τ.deriv_smul_ne_zero hg

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
⊢ dist d c * dist b d ≤ dist d b * dist c d

Tactic:
dist_comm d,

Goal state after:
case inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
⊢ dist c d * dist b d ≤ dist d b * dist c d
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
⊢ dist c d * dist b d ≤ dist d b * dist c d

Tactic:
dist_comm d,

Goal state after:
case inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
⊢ dist c d * dist b d ≤ dist b d * dist c d
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case mp
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 := ⋯ }
⊢ False

Tactic:
let h : Y ⟶ Z := ofHom _
      ⟨fun _ => ⟨⟨0, Set.left_mem_Icc.mpr zero_le_one⟩⟩, continuous_const⟩

Goal state after:
case mp
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 := ⋯ }
⊢ False
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
⊢ IsCompact ((fun g ↦ g • I) ⁻¹' K)

Tactic:
let : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup

Goal state after:
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
⊢ IsCompact ((fun g ↦ g • I) ⁻¹' K)
Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f₁ f₂ : ℂ → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
h_meromorphic : ∀ a ∈ Finset.univ, Meromorphic (![f₁, f₂] a)
⊢ characteristic (f₁ + f₂) ⊤ r ≤ characteristic f₁ ⊤ r + characteristic f₂ ⊤ r + log 2

Tactic:
simpa using characteristic_sum_top_le Finset.univ ![f₁, f₂] h_meromorphic hr

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ (2 * π)⁻¹ * ∫ (β : ℝ) in 0..2 * π, (2 * π)⁻¹ * ∫ (α : ℝ) in 0..2 * π, F α β =
    (2 * π)⁻¹ * ∫ (β : ℝ) in 0..2 * π, log⁺ ‖f (circleMap 0 R β)‖

Tactic:
congr 1
      apply intervalIntegral.integral_congr
      intro β hβ
      calc (2 * π)⁻¹ * ∫ α in 0..2 * π, F α β
        _ = circleAverage (log ‖f (circleMap 0 R β) - ·‖) 0 1 := by
          simp [F, circleAverage, Cartan.cartanKernel]
        _ = log⁺ ‖f (circleMap 0 R β)‖ := by
          simp [norm_sub_rev]

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

Goal state before:
pp: 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✝ : AddTorsor V P
⊢ List.Sbtw R []

Tactic:
by
  simp [List.Sbtw]

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

Goal state before:
pp: 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✝ : AddTorsor V P
p₁ : P
⊢ List.Sbtw R [p₁]

Tactic:
by
  simp [List.Sbtw]

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

Goal state before:
pp: 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✝ : AddTorsor V P
p₁ p₂ : P
⊢ List.Sbtw R [p₁, p₂] ↔ p₁ ≠ p₂

Tactic:
by
  simp [List.Sbtw]

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✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y z : P
⊢ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x

Tactic:
wbtw_comm,

Goal state after:
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✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y z : P
⊢ Wbtw R z y x ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
Module: Mathlib.Analysis.Convex.BetweenList

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
l : List P
h : List.Wbtw R l
⊢ ∃ p₁ p₂ l', l'.SortedLE ∧ map (⇑(lineMap p₁ p₂)) l' = l

Tactic:
by_cases hl : l = []
    · exact ⟨AddTorsor.nonempty.some, AddTorsor.nonempty.some, [], by
        simp [hl, sortedLE_iff_pairwise]⟩
    · exact ⟨l.head hl, l.getLast hl, (exists_map_eq_of_sorted_nonempty_iff_wbtw hl).2 h⟩

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

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
l : List P
hl : l ≠ []
hp : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
⊢ ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)

Tactic:
refine ⟨l', ?_, hl'l, ?_⟩

Goal state after:
case refine_2.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
l : List P
hl : l ≠ []
hp : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
⊢ l'.SortedLT

case refine_2.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
l : List P
hl : l ≠ []
hp : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
l' : List R
hl's : l'.SortedLE
hl'l : map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
⊢ l.length = 1 ∨ l.head hl ≠ l.getLast hl
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
⊢ Wbtw R 1 x 0 ↔ x ∈ Set.Icc 0 1

Tactic:
wbtw_comm,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
⊢ Wbtw R 0 x 1 ↔ x ∈ Set.Icc 0 1
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: 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✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
w x y z : P
h₁ : Wbtw R w y z
h₂ : Wbtw R w x y
⊢ Wbtw R w x z

Tactic:
rcases h₁ with ⟨t₁, ht₁, rfl⟩

Goal state after:
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✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
w x z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
h₂ : Wbtw R w x ((lineMap w z) t₁)
⊢ Wbtw R w x z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: 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✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x y z : P
⊢ Wbtw R x y z ∧ Wbtw R x z y ↔ y = z

Tactic:
wbtw_comm,

Goal state after:
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✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
x y z : P
⊢ Wbtw R z y x ∧ Wbtw R x z y ↔ y = z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: 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✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
y z x : P
⊢ Wbtw R x y z ∧ Wbtw R z x y ↔ x = y

Tactic:
wbtw_comm,

Goal state after:
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✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
y z x : P
⊢ Wbtw R z y x ∧ Wbtw R z x y ↔ x = y
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
⊢ F.IsMittagLeffler ↔
    ∀ (j : J),
      ∃ i f,
        ∀ ⦃k : J⦄ (g : k ⟶ i), range ⇑(ConcreteCategory.hom (F.map f)) ⊆ range ⇑(ConcreteCategory.hom (F.map (g ≫ f)))

Tactic:
simp_rw [isMittagLeffler_iff_eventualRange, eventualRange_eq_iff]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
h : ofSet s = PEquiv.refl α
x✝ : α
⊢ x✝ ∈ (PEquiv.refl α) x✝

Tactic:
exact rfl

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝³ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
i : J
x : F.obj i
⊢ ∃ a, (fun s ↦ ↑s i) a = x

Tactic:
let s : Set (F.obj i) := {x}
  have := F.toPreimages_nonempty_of_surjective s Fsur (singleton_nonempty x)
  obtain ⟨sec, h⟩ := nonempty_sections_of_finite_cofiltered_system (F.toPreimages s)
  refine ⟨⟨fun j => (sec j).val, fun jk => by simpa [Subtype.ext_iff] using! h jk⟩, ?_⟩
  · have := (sec i).prop
    simp only [mem_iInter, mem_preimage] at this
    have := this (𝟙 i)
    rwa [map_id, id_apply] at this

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

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring α
f : l ≃. m
g : m ≃. n
⊢ (f.trans g).toMatrix = f.toMatrix * g.toMatrix

Tactic:
by
  ext i j
  rw [toMatrix_mul_apply]
  dsimp +instances [toMatrix, PEquiv.trans]
  cases f i <;> simp

Goal state after:
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
⊢ y -ᵥ x - r • (y -ᵥ x) ≠ 0

Tactic:
nth_rw 1 [← one_smul R (y -ᵥ x)]

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 • (y -ᵥ x) - r • (y -ᵥ x) ≠ 0
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
⊢ Wbtw R x y z ↔ z = y ∨ x ∈ ⇑(lineMap z y) '' Set.Ici 1

Tactic:
wbtw_comm,

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 y z : P
⊢ Wbtw R z y x ↔ z = y ∨ x ∈ ⇑(lineMap z y) '' Set.Ici 1
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case 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 : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
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_nonneg_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 x y z : P
h₁ : Wbtw R w y z
h₂ : Wbtw R w x y
⊢ Wbtw R x y z

Tactic:
rcases h₁ with ⟨t₁, ht₁, 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
w x z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
h₂ : Wbtw R w x ((lineMap w z) t₁)
⊢ Wbtw R x ((lineMap w z) t₁) z
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 A C
hBA : B ⊆ A
hCB : C ⊆ B
w : E
hw : w ∈ C
⊢ ∃ l, C = {x | x ∈ B ∧ ∀ y ∈ B, l y ≤ l x}

Tactic:
obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hBA : B ⊆ A
w : E
l : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hCB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ⊆ B
hw : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ ∃ l_1, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ B ∧ ∀ y ∈ B, l_1 y ≤ l_1 x}
Module: Mathlib.Analysis.Convex.Exposed

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 A C
hCB : C ⊆ B
w : E
hw : w ∈ C
⊢ ∃ l, C = {x | x ∈ A ∩ B ∧ ∀ y ∈ A ∩ B, l y ≤ l x}

Tactic:
obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
w : E
l : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hCB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ⊆ B
hw : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ ∃ l_1, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ A ∩ B ∧ ∀ y ∈ A ∩ B, l_1 y ≤ l_1 x}
Module: Mathlib.Analysis.Convex.Independent

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ Injective p

Tactic:
by
  refine fun i j hij => hc {j} i ?_
  rw [hij, Set.image_singleton, convexHull_singleton]
  exact Set.mem_singleton _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
⊢ ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))

Tactic:
refine ⟨fun hc i s h => ?_, fun h s i hi => ?_⟩
  · rw [hc.mem_convexHull_iff] at h
    exact h.2 (Set.mem_singleton _)
  · by_contra H
    refine h i s ?_
    rw [Set.sdiff_singleton_eq_self H]
    exact hi

Goal state after: