mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.CofilteredSystem

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

Tactic:
apply range_comp_subset_range

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

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
⊢ (fun i ↦ ↑f ⟨↑i, ⋯⟩) ∈ hallMatchingsOn t ι'

Tactic:
obtain ⟨hinj, hc⟩ := f.property

Goal state after:
ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
hinj : Injective ↑f
hc : ∀ (x : ↥ι''), ↑f x ∈ t ↑x
⊢ (fun i ↦ ↑f ⟨↑i, ⋯⟩) ∈ hallMatchingsOn t ι'
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case pos
α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
h✝ : a ∈ s
⊢ a ∈ some a ↔ a ∈ s

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case neg
α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
h✝ : ¬a ∈ s
⊢ a ∈ none ↔ a ∈ s

Tactic:
simp [*]

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 α
⊢ s = Set.univ

Tactic:
by
    rw [Set.eq_univ_iff_forall]
    intro
    rw [← mem_ofSet_self_iff, h]
    exact rfl

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : y = b
h2 : x = a
⊢ some a = some x ↔ some b = some y

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
h✝ : x✝³ x✝¹ = x✝² x✝¹
⊢ x✝³ x✝¹ = some x✝ → x✝³ x✝¹ = some x✝

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
h✝ : ¬x✝³ x✝¹ = x✝² x✝¹
⊢ False → x✝³ x✝¹ = some x✝

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
h✝ : x✝³ x✝¹ = x✝² x✝¹
⊢ x✝³ x✝¹ = some x✝ → x✝² x✝¹ = some x✝

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
h✝ : ¬x✝³ x✝¹ = x✝² x✝¹
⊢ False → x✝² x✝¹ = some x✝

Tactic:
simp [*]

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

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
i✝ j✝ : n
⊢ (PEquiv.refl n).toMatrix i✝ j✝ = 1 i✝ j✝

Tactic:
simp [toMatrix_apply, one_apply]

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 ᵥ* M ᵥ* N = 1

Tactic:
hM.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 ᵥ* N = 1
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

Goal state before:
pp: case mpr.inr
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs✝ : 0 ≤ s
hs : 0 < s
hM₁ : ∀ (i j : n), 0 ≤ M i j
hM₂ : ∀ (i : n), ∑ j, M i j = s
hM₃ : ∀ (j : n), ∑ i, M i j = s
⊢ ∃ M' ∈ doublyStochastic R n, M = s • M'

Tactic:
exact ⟨s⁻¹ • M, by simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', *]⟩

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 < s
hM : (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s
f : n → Finset n := fun i ↦ {j | M i j ≠ 0}
A : Finset n
this : ∀ (i : n), ∑ j ∈ f i, M i j = s
h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = ↑(#A) * s
h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = ↑(#(A.biUnion f)) * s
i : n
hi : i ∈ A
⊢ ∀ i_1 ∈ A.biUnion f, i_1 ∉ f i → 0 ≤ M i i_1

Tactic:
simp [*]

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✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
s : AffineSubspace R P
hx : x ∈ s
ε : R
hy : (lineMap x z) ε ∈ s
hxy : x ≠ (lineMap x z) ε
hε : ε ≠ 0
⊢ z ∈ s

Tactic:
simpa [hε] using lineMap_mem ε⁻¹ hx hy

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
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)

Tactic:
by_cases h : 1 - t₂ * t₁ = 0

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

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
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
h : ¬1 - t₂ * t₁ = 0
⊢ ((t₁ - t₂ * t₁) * ((1 - t₂ * t₁) / (1 - t₂ * t₁)) + t₂ * t₁) • (z -ᵥ w) = t₁ • (z -ᵥ w)
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
x : G
y : H
C₁ : PointedCone R G
C₂ : PointedCone R H
hx : x ∈ C₁
hy : y ∈ C₂
⊢ x ⊗ₜ[R] y ∈ C₁.maxTensorProduct C₂

Tactic:
simp only [mem_maxTensorProduct, dualDistrib_apply]
  exact fun φ hφ ψ hψ => mul_nonneg (hφ hx) (hψ hy)

Goal state after:
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 𝕜 B C
hCA : C ⊆ A
⊢ IsExposed 𝕜 (A ∩ B) C

Tactic:
inter_comm

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 C : Set E
hC : IsExposed 𝕜 B C
hCA : C ⊆ A
⊢ IsExposed 𝕜 (B ∩ A) C
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t : Set E
⊢ ⋃ i' ∈ t, ⋃ i ∈ s, segment 𝕜 i i' = convexJoin 𝕜 t s

Tactic:
simp_rw [convexJoin, segment_symm]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u v : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v)

Tactic:
simp_rw [← convexJoin_assoc, convexJoin_right_comm]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ (convexHull 𝕜) ((convexHull 𝕜) s ∪ (convexHull 𝕜) t) = convexJoin 𝕜 ((convexHull 𝕜) s) ((convexHull 𝕜) t)

Tactic:
exact (convex_convexHull 𝕜 s).convexHull_union (convex_convexHull 𝕜 t) hs.convexHull ht.convexHull

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

Goal state before:
pp: f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ioc y z) f
hf_cont : ContinuousWithinAt f (Iic z) z
⊢ ContinuousOn f (Ioc y z)

Tactic:
intro x hx
  rcases eq_or_lt_of_le (α := ℝ) hx.2 with rfl | hxz
  · rw [continuousWithinAt_Ioc_iff_Iic hx.1]
    exact hf_cont
  · have h := hf_cvx.continuousOn_interior x
    simp only [interior_Ioc, mem_Ioo, hx.1, hxz, and_self, forall_const] at h
    rw [continuousWithinAt_iff_continuousAt (Ioo_mem_nhds hx.1 hxz)] at h
    exact h.continuousWithinAt

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: I : Type u_6
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
w : StdSimplex K I
s : Set I
hs : ∃ x ∈ s, w.weights x ≠ 0
hs' : ∃ x ∈ sᶜ, w.weights x ≠ 0
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (convexCombPair ((filter (fun x ↦ x ∈ s) w.weights).sum fun _x k ↦ k)
        ((filter (fun x ↦ x ∉ s) w.weights).sum fun _x k ↦ k) ⋯ ⋯ ⋯ (w.restrict s hs) (w.restrict sᶜ hs')).weights =
    w.weights

Tactic:
simp only [Set.mem_compl_iff] at hs'

Goal state after:
I : Type u_6
K : Type u_8
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
w : StdSimplex K I
s : Set I
hs : ∃ x ∈ s, w.weights x ≠ 0
hs'✝ : ∃ x ∈ sᶜ, w.weights x ≠ 0
inst✝ : DecidablePred fun x ↦ x ∈ s
hs' : ∃ x ∉ s, w.weights x ≠ 0
⊢ (convexCombPair ((filter (fun x ↦ x ∈ s) w.weights).sum fun _x k ↦ k)
        ((filter (fun x ↦ x ∉ s) w.weights).sum fun _x k ↦ k) ⋯ ⋯ ⋯ (w.restrict s hs) (w.restrict sᶜ hs'✝)).weights =
    w.weights
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 : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ convexCombPair s t hs ht h (convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ =
    convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)

Tactic:
rw [convexCombPair_convexCombPair_left_eq_sConvexComb,
    convexCombPair_convexCombPair_right_eq_sConvexComb]

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 : t * s'' = s * t' * t''
m₁ m₂ m₃ : M
⊢ sConvexComb (convexCombPair s t hs ht h (duple m₁ m₂ hs' ht' h') (StdSimplex.single m₃)) =
    sConvexComb (convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ (StdSimplex.single m₁) (duple m₂ m₃ hs'' ht'' h''))
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
⊢ ∀ (a : X), (if a ∈ u then w.weights (f a) else 0) ≠ 0 → a ∈ u

Tactic:
by simp +contextual

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

Goal state before:
pp: E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_5
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconcaveOn ℝ s f
⊢ IsPreconnected (f ⁻¹' Ici t ∩ s)

Tactic:
inter_comm

Goal state after:
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_5
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconcaveOn ℝ s f
⊢ IsPreconnected (s ∩ f ⁻¹' Ici t)
Module: Mathlib.Analysis.Convex.Quasiconvex

Goal state before:
pp: case refine_1
𝕜 : Type u_1
β : Type u_3
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
a✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ a ∈ {x | x ∈ s ∧ min (f a) (f b) ≤ f x}

Tactic:
simp [*]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
β : Type u_3
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
a✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ b ∈ {x | x ∈ s ∧ min (f a) (f b) ≤ f x}

Tactic:
simp [*]

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

Goal state before:
pp: case refine_3
𝕜 : Type u_1
β : Type u_3
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
a✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ a ∈ {x | x ∈ s ∧ f x ≤ max (f a) (f b)}

Tactic:
simp [*]

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

Goal state before:
pp: case refine_4
𝕜 : Type u_1
β : Type u_3
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → β
inst✝ : LinearOrder β
hf : QuasilinearOn 𝕜 s f
a : 𝕜
ha : a ∈ s
b : 𝕜
hb : b ∈ s
c : 𝕜
a✝ : c ∈ s
h : c ∈ segment 𝕜 a b
⊢ b ∈ {x | x ∈ s ∧ f x ≤ max (f a) (f b)}

Tactic:
simp [*]

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

Goal state before:
pp: case «0»
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
⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ (Finsupp.equivFunOnFinite.symm ![s', s - s', t]) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [*]

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

Goal state before:
pp: case «1»
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
⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ (Finsupp.equivFunOnFinite.symm ![s', s - s', t]) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [*]

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

Goal state before:
pp: case «2»
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
⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ (Finsupp.equivFunOnFinite.symm ![s', s - s', t]) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [*]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
i : ↥s
⊢ (⋂ j ∈ s.erase ↑i, F j).Nonempty

Tactic:
by
    apply hk (s := s.erase i)
    · exact fun i hi ↦ h_convex i (mem_of_mem_erase hi)
    · intro J hJ_ss hJ_card
      exact h_inter J (subset_trans hJ_ss (erase_subset i.val s)) hJ_card
    · simp only [coe_mem, card_erase_of_mem]; lia

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

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 0
r : ℝ
hr : 0 < r
⊢ 0 < r / D / 3

Tactic:
simp [*]

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

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 0
r : ℝ
hr : 0 < r
⊢ t ∈ f ⁻¹' {1}ᶜ

Tactic:
simp [*]

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

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
⊢ 0 < r / D / 3

Tactic:
simp [*]

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

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
⊢ t ∈ f ⁻¹' {0}ᶜ

Tactic:
simp [*]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ a ≠ b

Tactic:
by
  rintro rfl
  exact G.irrefl h

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

Goal state before:
pp: ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Fintype ↑(G₁ \ G₂).edgeSet

Tactic:
by
  rw [edgeSet_sdiff]
  exact Set.fintypeDiff _ _

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ fromEdgeSet s ≤ G ↔ s \ Sym2.diagSet ⊆ G.edgeSet

Tactic:
simp [← edgeSet_subset_edgeSet]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ (∃ u, G.Adj v u) ↔ ¬G.IsIsolated v

Tactic:
simp [IsIsolated]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G = ⊥ ↔ ∀ (v : V), G.IsIsolated v

Tactic:
by
  simp [eq_bot_iff_forall_not_adj, ← neighborSet_eq_empty, Set.eq_empty_iff_forall_notMem]

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

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
s : AffineSubspace R P
x y z : P
hy : y ∉ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hxy : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
p₃ : P
hp₃ : p₃ ∈ s
hyz : SameRay R (p₂ -ᵥ y) (z -ᵥ p₃)
h : p₂ = y
⊢ False

Tactic:
exact hy (h ▸ hp₂)

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

Goal state before:

Tactic:
(1 - w i) / w i = 0 + (1 - w i) / w i + 0 := by simp
          _ ≤ (1 - ε) / ε + (1 - w i) / w i + 1 := by gcongr <;> positivity

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

Goal state before:
pp: case neg
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x p : P
hp : p ∈ ↑s
this : Nonempty ↥s
hx : x ∉ s
⊢ IsConnected {y | s.WOppSide x y}

Tactic:
rw [setOfPred_wOppSide_eq_image2 hx hp, ← Set.image_prod]
    refine (isConnected_Iic.prod (isConnected_iff_connectedSpace.2 ?_)).image _
      ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
    convert! AddTorsor.connectedSpace s.direction s

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
t : ℝ
ht : 0 ≤ t
⊢ IntervalIntegrable g volume 0 t

Tactic:
rcases eq_or_lt_of_le ht with h | h

Goal state after:
case inl
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
t : ℝ
ht : 0 ≤ t
h : 0 = t
⊢ IntervalIntegrable g volume 0 t

case inr
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
t : ℝ
ht : 0 ≤ t
h : 0 < t
⊢ IntervalIntegrable g volume 0 t