mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ HasConstantSpeedOnWith f s 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

Tactic:
by
  dsimp [HasConstantSpeedOnWith]
  simp only [zero_mul, ENNReal.ofReal_zero, ← eVariationOn.eq_zero_iff]
  constructor
  · by_contra! ⟨h, hfs⟩
    simp_rw [ne_eq, eVariationOn.eq_zero_iff] at hfs h
    push Not at hfs
    obtain ⟨x, xs, y, ys, hxy⟩ := hfs
    rcases le_total x y with (xy | yx)
    · exact hxy (h xs ys x ⟨xs, le_rfl, xy⟩ y ⟨ys, xy, le_rfl⟩)
    · rw [edist_comm] at hxy
      exact hxy (h ys xs y ⟨ys, le_rfl, yx⟩ x ⟨xs, yx, le_rfl⟩)
  · rintro h x _ y _
    simpa [h] using eVariationOn.mono (s := s) f inter_subset_left

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

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ IsClosed A

Tactic:
exact (lowerSemicontinuousOn_iff_isClosed_epigraph hsc).1
      (continuous_coe_real_ereal.comp_lowerSemicontinuousOn hφ_cont (EReal.coe_strictMono.monotone))

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

Goal state before:
pp: case refine_2.cons
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
head : P
tail : List P
ih :
  ∀ (hl : tail ≠ []),
    List.Wbtw R tail →
      ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (tail.head hl) (tail.getLast hl))) l' = tail
hl : head :: tail ≠ []
h : List.Wbtw R (head :: tail)
⊢ ∃ l',
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧ map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl))) l' = head :: tail

Tactic:
by_cases ht : tail = []

Goal state after:
case pos
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
head : P
tail : List P
ih :
  ∀ (hl : tail ≠ []),
    List.Wbtw R tail →
      ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (tail.head hl) (tail.getLast hl))) l' = tail
hl : head :: tail ≠ []
h : List.Wbtw R (head :: tail)
ht : tail = []
⊢ ∃ l',
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧ map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl))) l' = head :: tail

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
head : P
tail : List P
ih :
  ∀ (hl : tail ≠ []),
    List.Wbtw R tail →
      ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (tail.head hl) (tail.getLast hl))) l' = tail
hl : head :: tail ≠ []
h : List.Wbtw R (head :: tail)
ht : ¬tail = []
⊢ ∃ l',
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧ map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl))) l' = head :: tail
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case pos
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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : Pairwise (Wbtw R head) (head2 :: tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
hl'' : map (⇑(lineMap ((head2 :: tail).head ht) ((head2 :: tail).getLast ht))) l'' = head2 :: tail
ht2 : tail = []
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head ((head2 :: tail).getLast ht))) l' = head :: head2 :: tail

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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : Pairwise (Wbtw R head) (head2 :: tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
hl'' : map (⇑(lineMap ((head2 :: tail).head ht) ((head2 :: tail).getLast ht))) l'' = head2 :: tail
ht2 : ¬tail = []
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head ((head2 :: tail).getLast ht))) l' = head :: head2 :: tail

Tactic:
· exact ⟨[0, 1], by simp [ht2, sortedLE_iff_pairwise]⟩

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
head : P
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
head2 : P
tail : List P
hl : head :: head2 :: tail ≠ []
h : Pairwise (Wbtw R head) (head2 :: tail) ∧ List.Wbtw R (head2 :: tail)
ht : ¬head2 :: tail = []
hl'' : map (⇑(lineMap ((head2 :: tail).head ht) ((head2 :: tail).getLast ht))) l'' = head2 :: tail
ht2 : ¬tail = []
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap head ((head2 :: tail).getLast ht))) l' = head :: head2 :: tail
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
s : AffineSubspace R P
x y z : P
hxyz : Wbtw R x y z
hx : x ∈ s
hz : z ∈ s
⊢ y ∈ s

Tactic:
by obtain ⟨ε, -, rfl⟩ := hxyz; exact lineMap_mem _ hx hz

Goal state after:
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x

Tactic:
have card_ι'_le : Fintype.card s ≤ n := by
    apply Nat.le_of_lt_succ
    calc
      Fintype.card s = #s := Fintype.card_coe _
      _ < Fintype.card ι := (card_lt_iff_ne_univ _).mpr hns
      _ = n.succ := hn

Goal state after:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s.Nonempty
𝓕 : Set (↑s → ℝ) := {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c}
⊢ IsLUB 𝓕 (s.domRestrict φ)

Tactic:
refine (hφcv.sSup_affine_eq (𝕜 := 𝕜) hsc hφc) ▸ isLUB_csSup ?_ ?_

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s.Nonempty
𝓕 : Set (↑s → ℝ) := {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c}
⊢ 𝓕.Nonempty

case refine_2
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s.Nonempty
𝓕 : Set (↑s → ℝ) := {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c}
⊢ BddAbove 𝓕
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
h : Wbtw R x y z
hne : y ≠ x
⊢ x ≠ z

Tactic:
rintro rfl
  rw [wbtw_self_iff] at h
  exact hne 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✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y z : P
h : Wbtw R x y z
hne : y ≠ z
⊢ x ≠ z

Tactic:
rintro rfl
  rw [wbtw_self_iff] at h
  exact hne h

Goal state after:
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case refine_2
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
card_ι''_le : Fintype.card ↑ι'' ≤ n
f'' : ↑ι'' → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' ⟨x'', hx''⟩ ∉ s.biUnion t
im_disj : ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s), f' ⟨x', hx'⟩ ≠ f'' ⟨x'', hx''⟩
x : ι
⊢ (if h : x ∈ s then f' ⟨x, h⟩ else f'' ⟨x, h⟩) ∈ t x

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
card_ι''_le : Fintype.card ↑ι'' ≤ n
f'' : ↑ι'' → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' ⟨x'', hx''⟩ ∉ s.biUnion t
im_disj : ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s), f' ⟨x', hx'⟩ ≠ f'' ⟨x'', hx''⟩
x : ι
h : x ∈ s
⊢ f' ⟨x, h⟩ ∈ t x

case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n.succ
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
s : Finset ι
hs : s.Nonempty
hns : s ≠ univ
hus : #s = #(s.biUnion t)
this : DecidableEq ι
card_ι'_le : Fintype.card ↥s ≤ n
t' : ↥s → Finset α := fun x' ↦ t ↑x'
f' : ↥s → α
hf' : Function.Injective f'
hsf' : ∀ (x : ↥s), f' x ∈ t' x
ι'' : Set ι := (↑s)ᶜ
t'' : ↑ι'' → Finset α := fun a'' ↦ t ↑a'' \ s.biUnion t
card_ι''_le : Fintype.card ↑ι'' ≤ n
f'' : ↑ι'' → α
hf'' : Function.Injective f''
hsf'' : ∀ (x : ↑ι''), f'' x ∈ t'' x
f''_notMem_biUnion : ∀ (x'' : ι) (hx'' : x'' ∉ s), f'' ⟨x'', hx''⟩ ∉ s.biUnion t
im_disj : ∀ (x' x'' : ι) (hx' : x' ∈ s) (hx'' : x'' ∉ s), f' ⟨x', hx'⟩ ≠ f'' ⟨x'', hx''⟩
x : ι
h : x ∉ s
⊢ f'' ⟨x, h⟩ ∈ t x
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
f : Y✝ ⟶ i
⊢ x ∈ (fun x ↦ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x)) ⁻¹' s

Tactic:
mem_preimage

Goal state after:
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
f : Y✝ ⟶ i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) ∈ s
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_4
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁸ : RCLike 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set ({ x // x ∈ univ } → ℝ) := {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c}
this : sSup {f | f ≤ φ ∘ Subtype.val ∧ ∃ l c, f = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c} = φ ∘ Subtype.val
f : E → ℝ
x✝ : ∃ a ∈ 𝓕, (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) a = f
a : ↑univ → ℝ
h : a ≤ φ ∘ Subtype.val
l : E →L[𝕜] 𝕜
c : ℝ
hlc : a = (⇑re ∘ ⇑l) ∘ Subtype.val + const (↑univ) c
hb : (fun g ↦ g ∘ ⇑(Equiv.Set.univ E).symm) a = f
⊢ f = ⇑re ∘ ⇑l + const E c

Tactic:
subst hlc; simpa using! hb.symm

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ f.trans f.symm = ofSet {a | (f a).isSome = true}

Tactic:
ext
  dsimp [PEquiv.trans]
  simp only [eq_some_iff f, Option.isSome_iff_exists, bind_eq_some_iff,
    ofSet_eq_some_iff]
  constructor
  · rintro ⟨b, hb₁, hb₂⟩
    exact ⟨PEquiv.inj _ hb₂ hb₁, b, hb₂⟩
  · simp +contextual

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
inst✝ : CommRing R
⊢ (Perm.permMatrix R σ).det = ↑↑(Perm.sign σ)

Tactic:
← Matrix.mul_one (σ.permMatrix R),

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
inst✝ : CommRing R
⊢ (Perm.permMatrix R σ * 1).det = ↑↑(Perm.sign σ)
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
hM : M ∈ colStochastic R n
i j : n
⊢ M j i ≤ 1

Tactic:
rw [← sum_col_of_mem_colStochastic hM i]
  exact single_le_sum (fun k _ => hM.1 k _) (mem_univ j)

Goal state after:
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✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
⊢ 1 ᵥ* N = 1

Tactic:
hN.2.2

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✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
⊢ 1 = 1
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₃ : Fin 3
h₁₃ : i₁ ≠ i₃
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)
w : Fin (2 + 1) → R
hw : ∑ i, w i = 1
hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)
h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)
i : Fin 3
h₁₂ : i₁ ≠ i
h₂₃ : i ≠ i₃
h3 : ∀ (i_1 : Fin 3), i_1 = i₁ ∨ i_1 = i ∨ i_1 = i₃
hu : Finset.univ = {i₁, i, i₃}
h₁ : Sbtw R (t.points i) ((lineMap (t.points i) (t.points i₃)) r₁) (t.points i₃)
h₁' :
  (Finset.affineCombination R Finset.univ t.points) w ∈
    line[R, (Finset.affineCombination R Finset.univ t.points) (Pi.single i₁ 1),
      (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i i₃ r₁)]
h₂' :
  (Finset.affineCombination R Finset.univ t.points) w ∈ line[R, t.points i, (lineMap (t.points i₁) (t.points i₃)) r₂]
h₁s : SignType.sign (w i) = SignType.sign (w i₃)
⊢ SignType.sign (w i) = SignType.sign (w i₃)

Tactic:
exact h₁s

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

Goal state before:
pp: case e'_10
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₂ ≤ r₁
⊢ r₁ • v +ᵥ x = -r₁ • -v +ᵥ x

Tactic:
neg_smul_neg

Goal state after:
case e'_10
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₂ ≤ r₁
⊢ r₁ • v +ᵥ x = r₁ • v +ᵥ x
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case e'_11
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₂ ≤ r₁
⊢ r₂ • v +ᵥ x = -r₂ • -v +ᵥ x

Tactic:
neg_smul_neg

Goal state after:
case e'_11
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₂ ≤ r₁
⊢ r₂ • v +ᵥ x = r₂ • v +ᵥ x
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case inr.inr.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 z : P
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x)
this : ∀ {y z : P} (r₁ r₂ : R), 0 < r₁ → 0 < r₂ → r₁ • (y -ᵥ x) = r₂ • (z -ᵥ x) → r₂ ≤ r₁ → Wbtw R x y z ∨ Wbtw R x z y
hr : ¬r₂ ≤ r₁
⊢ Wbtw R x z y ∨ Wbtw R x y z

Tactic:
apply this r₂ r₁ hr₂ hr₁ h.symm (Std.le_of_not_ge hr)

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
⊢ (TensorProduct.lid ℝ F) ((LinearMap.rTensor F (b.coord i)) z) ∈
    ↑(ProperCone.dual (topDualPairing ℝ F) ↑(ProperCone.dual (topDualPairing ℝ F).flip ↑C₂))

Tactic:
intro f (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.Independent

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t) → ConvexIndependent 𝕜 Subtype.val

Tactic:
intro hc

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hc : ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t
⊢ ConvexIndependent 𝕜 Subtype.val
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
oneside : ∀ {x y : E}, x ∈ ball x₀ (r - ε) → y ∈ ball x₀ (r - ε) → f x - f y ≤ K * ‖x - y‖
⊢ LipschitzOnWith K.toNNReal f (ball x₀ (r - ε))

Tactic:
refine .of_dist_le' fun x hx y hy ↦ ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
oneside : ∀ {x y : E}, x ∈ ball x₀ (r - ε) → y ∈ ball x₀ (r - ε) → f x - f y ≤ K * ‖x - y‖
x : E
hx : x ∈ ball x₀ (r - ε)
y : E
hy : y ∈ ball x₀ (r - ε)
⊢ dist (f x) (f y) ≤ K * dist x y