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

Goal state before:
pp: case h
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    x_1 x = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)

Tactic:
· intro σ
    simp only [Normal.algHomEquivAut, AlgHom.restrictNormal', Equiv.coe_fn_mk,
      AlgEquiv.coe_ofBijective, AlgHom.restrictNormal_commutes, algebraMap_self, RingHom.id_apply]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n✝ n : ℕ
⊢ Differentiable ℂ (iteratedDeriv (n + 2) sinh)

Tactic:
simp [differentiable_iteratedDeriv_sinh]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n✝ n : ℕ
⊢ Differentiable ℝ (iteratedDeriv (n + 2) sinh)

Tactic:
simp [differentiable_iteratedDeriv_sinh]

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

Goal state before:
pp: z w : ℍ
⊢ w.im * (1 - rexp (-dist z w)) = dist ↑z ↑(w.center (dist z w)) - dist ↑w ↑(w.center (dist z w))

Tactic:
rw [dist_center_dist, dist_self_center, ← Real.cosh_sub_sinh]; ring

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: case refine_1
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s ↦ {u | s ∈ u}) a
ub : u ∈ (fun s ↦ {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s ↦ {u | s ∈ u}) (a ∩ b)
⊢ a ∩ b ⊆ a

Tactic:
simp [inter_subset_right]

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: case refine_2
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s ↦ {u | s ∈ u}) a
ub : u ∈ (fun s ↦ {u | s ∈ u}) b
v : Ultrafilter α
hv : v ∈ (fun s ↦ {u | s ∈ u}) (a ∩ b)
⊢ a ∩ b ⊆ b

Tactic:
simp [inter_subset_right]

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : T2Space 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)) ↔
    ContinuousSMul G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)

Tactic:
refine and_congr_right fun hc ↦ ?_

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
hc : 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)) ↔
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, Tendsto fst (↑𝒰) (𝓝 g)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: X : Type u_2
inst✝⁴ : TopologicalSpace X
G : Type u_3
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
g : G
⊢ g ∈ {g | (g • U ∩ V).Nonempty} ↔ g ∈ fst '' (fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' V ×ˢ U

Tactic:
suffices (∃ v, v ∈ g • U ∧ v ∈ V) ↔ ∃ u, g • u ∈ V ∧ u ∈ U by simpa

Goal state after:
X : Type u_2
inst✝⁴ : TopologicalSpace X
G : Type u_3
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
g : G
⊢ (∃ v ∈ g • U, v ∈ V) ↔ ∃ u, g • u ∈ V ∧ u ∈ U
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case coe
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
val : X
x✝ : ↑val ∈ univ
hxy : ↑val ≠ y
⊢ ∃ u v,
    IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ ↑val ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
refine ⟨{some val}, {some val}ᶜ, ?_, isOpen_compl_singleton, rfl, hxy.symm, by simp,
        disjoint_compl_right⟩
      rw [OnePoint.isOpen_iff_of_notMem]
      exacts [isOpen_discrete _, (Option.some_ne_none val).symm]

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

Goal state before:
pp: X✝ : Type u
Y : Type v
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
ι : Type u
X : ι → Type v
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactlyGeneratedSpace (X i)
⊢ CompactlyGeneratedSpace ((i : ι) × X i)

Tactic:
refine compactlyGeneratedSpace_of_isClosed fun s h ↦ isClosed_sigma_iff.2 fun i ↦
    CompactlyGeneratedSpace.isClosed' fun K _ _ _ f hf ↦ ?_
  let g : ULift.{u} K → (Σ i, X i) := Sigma.mk i ∘ f ∘ ULift.down
  have hg : Continuous g := continuous_sigmaMk.comp <| hf.comp continuous_uliftDown
  exact (h _ g hg).preimage continuous_uliftUp

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

Goal state before:
pp: E : Type u_2
inst✝ : NormedAddCommGroup E
r : ℝ
f : locallyFinsupp E ℤ
⊢ ((toClosedBall r) f).support ⊆ closedBall 0 |r|

Tactic:
by
  simp_all [toClosedBall, restrict_apply]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicTrailingCoeffAt f 0 - a = meromorphicTrailingCoeffAt f 0 - meromorphicTrailingCoeffAt (fun x ↦ a) 0

pp: case h₁
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicOrderAt f 0 = meromorphicOrderAt (fun x ↦ a) 0

pp: case h₂
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicTrailingCoeffAt f 0 - meromorphicTrailingCoeffAt (fun x ↦ a) 0 ≠ 0

Tactic:
meromorphicTrailingCoeffAt_const,

Goal state after:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicTrailingCoeffAt f 0 - a = meromorphicTrailingCoeffAt f 0 - a

case h₁
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicOrderAt f 0 = meromorphicOrderAt (fun x ↦ a) 0

case h₂
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicTrailingCoeffAt f 0 - meromorphicTrailingCoeffAt (fun x ↦ a) 0 ≠ 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: case neg.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
⊢ CircleIntegrable (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

Tactic:
refine (circleIntegrable_congr fun a ha ↦ ?_).2 (circleIntegrable_const
      (log ‖meromorphicTrailingCoeffAt f 0‖) 0 1)
    rw [(MeromorphicAt.const a 0).meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt]
    rw [meromorphicOrderAt_const]
    aesop

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) (single e n)) z) * log (r * ‖z‖⁻¹)) ⊆ ↑⋯.toFinset

Tactic:
simp_all [toClosedBall, restrict_apply, single_apply]

Goal state after:
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:
dsimp [HasConstantSpeedOnWith]

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (0 * (y - x))) ↔
    ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: case cons.refine_1
α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih : Triplewise p tail ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
x✝ :
  (∀ (i j : Nat) (_hi : i < tail.length) (_hj : j < tail.length), i < j → p head tail[i] tail[j]) ∧
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
i j k : Nat
hij : i < j
hjk : j < k
hk : k < tail.length + 1
hh : ∀ (i j : Nat) (_hi : i < tail.length) (_hj : j < tail.length), i < j → p head tail[i] tail[j]
ht : ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
⊢ p (head :: tail)[i] (head :: tail)[j] (head :: tail)[k]

pp: case cons.refine_2
α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih : Triplewise p tail ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
h :
  ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length + 1),
    p (head :: tail)[i] (head :: tail)[j] (head :: tail)[k]
i j : Nat
hi : i < tail.length
hj : j < tail.length
hij : i < j
⊢ p head tail[i] tail[j]

pp: case cons.refine_3
α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih : Triplewise p tail ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
h :
  ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length + 1),
    p (head :: tail)[i] (head :: tail)[j] (head :: tail)[k]
i j k : Nat
hij : i < j
hjk : j < k
hk : k < tail.length
⊢ p tail[i] tail[j] tail[k]

Tactic:
· grind

Goal state after:
case cons.refine_2
α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih : Triplewise p tail ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
h :
  ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length + 1),
    p (head :: tail)[i] (head :: tail)[j] (head :: tail)[k]
i j : Nat
hi : i < tail.length
hj : j < tail.length
hij : i < j
⊢ p head tail[i] tail[j]

case cons.refine_3
α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih : Triplewise p tail ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length), p tail[i] tail[j] tail[k]
h :
  ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length + 1),
    p (head :: tail)[i] (head :: tail)[j] (head :: tail)[k]
i j k : Nat
hij : i < j
hjk : j < k
hk : k < tail.length
⊢ p tail[i] tail[j] tail[k]
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case cons.refine_1.refine_3
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
head : P
tail : List P
ih : List.Wbtw R tail ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ Triplewise (Sbtw R) tail ∧ ∀ (a : P), tail ≠ [a, a]
hpne : Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail)
hp : Pairwise (Wbtw R head) tail
ht : List.Wbtw R tail
⊢ ∀ (a : P), head :: tail ≠ [a, a]

Tactic:
· grind

Goal state after:
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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb : re (L (x, ↑a)) < b ∧ ∀ b_1 ∈ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}, b < re (L b_1)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := (re (L (0, 1)))⁻¹
z : ↑s
hv : ∀ (v : 𝕜), v * L (0, 1) = L (0, v)
w : E
h : w ∈ s
⊢ re (L (x, 0)) + re (L (0, 1)) * a < re (L (w, 0)) + re (L (0, 1)) * φ w

Tactic:
have hw := hLb.1.trans (hLb.2 _ (by simp [A, h] : (w, ofReal (φ w)) ∈ A))

Goal state after:
𝕜 : 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
x : E
a : ℝ
hx : x ∈ s
hax : a < φ x
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
A : Set (E × 𝕜) := {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}
L : StrongDual 𝕜 (E × 𝕜)
b : ℝ
hLb : re (L (x, ↑a)) < b ∧ ∀ b_1 ∈ {p | p.1 ∈ s ∧ φ p.1 ≤ re p.2}, b < re (L b_1)
u : E →L[𝕜] 𝕜 := L ∘SL inl 𝕜 E 𝕜
c : ℝ := (re (L (0, 1)))⁻¹
z : ↑s
hv : ∀ (v : 𝕜), v * L (0, 1) = L (0, v)
w : E
h : w ∈ s
hw : re (L (x, ↑a)) < re (L (w, ↑(φ w)))
⊢ re (L (x, 0)) + re (L (0, 1)) * a < re (L (w, 0)) + re (L (0, 1)) * φ w
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
head : P
tail : List P
hl : head :: tail ≠ []
h : Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail
ht : ¬tail = []
l'' : List R
hl''0 : ∀ a ∈ l'', 0 ≤ a
hl''s : l''.SortedLE
hl'' : map (⇑(lineMap (tail.head ht) (tail.getLast ht))) l'' = tail
⊢ ∃ l',
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧ map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl))) l' = head :: tail

Tactic:
simp only [head_cons, getLast_cons ht]

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

Tactic:
← 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
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
⊢ Fintype.card ↑(↑s)ᶜ < Fintype.card ι
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
⊢ a ∈ (ofSet s) a ↔ a ∈ s

Tactic:
dsimp [ofSet]; split_ifs <;> simp [*]

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✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
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
hd : #{i | M i.1 i.2 ≠ 0} = d
hs'✝ : 0 < s
σ : Equiv.Perm n
hσ : ∀ (i j : n), M i j = 0 → Equiv.Perm.permMatrix R σ i j = 0
i : n
hi : i ∈ univ
hi' : ∀ x' ∈ univ, M i (σ i) ≤ M x' (σ x')
N : Matrix n n R := M - M i (σ i) • Equiv.Perm.permMatrix R σ
hMi' : 0 < M i (σ i)
s' : R := s - M i (σ i)
hs' : 0 ≤ s'
⊢ ∀ (j : n), (∑ x, M x j - ∑ x, if σ x = j then M i (σ i) else 0) = s'

Tactic:
simp [s', ← σ.eq_symm_apply, hM]

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

Goal state before:
pp: case inr
V : Type u_1
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup V
inst✝¹ : Module ℝ V
inst✝ : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
a b : ℝ≥0
h : a ≤ b
ha : 0 < a
y : V
hy : y ∈ ↑K
hx : a • y ∈ a • ↑K
⊢ 1 ≤ a⁻¹ * b

Tactic:
rwa [le_inv_mul_iff₀ ha, mul_one]

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

Goal state before:
pp: case refine_1
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ ⋂ n, (1 + ↑(u n)) • ↑K
⊢ x ∈ ↑K

Tactic:
obtain ⟨C, hC_pos, hC_bdd⟩ := K.isBounded.exists_pos_norm_le

Goal state after:
case refine_1
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ ⋂ n, (1 + ↑(u n)) • ↑K
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
⊢ x ∈ ↑K
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_1.right.h
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_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
⊢ t₁ * t₂ ≤ 1 - t₁ + t₁ * t₂

pp: case hb
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_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
⊢ 0 ≤ 1 - t₁ + t₁ * t₂

Tactic:
· grind

Goal state after:
case hb
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_ne : x ≠ y
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
hx : (lineMap w y) t₁ = x
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
hy : (lineMap x z) t₂ = y
⊢ 0 ≤ 1 - t₁ + t₁ * t₂
Module: Mathlib.Analysis.Convex.Birkhoff

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h✝ : Nonempty n
d : ℕ
ih :
  ∀ m < d,
    ∀ (M : Matrix n n R) (s : R),
      0 ≤ s →
        (∃ M' ∈ doublyStochastic R n, M = s • M') →
          #{i | M i.1 i.2 ≠ 0} = m → ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
M : Matrix n n R
s : R
hs : 0 ≤ s
hM : ∃ M' ∈ doublyStochastic R n, M = s • M'
hd : #{i | M i.1 i.2 ≠ 0} = d
⊢ ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M

Tactic:
rcases eq_or_lt_of_le hs with rfl | hs'
  case inl =>
    use 0
    simp only [zero_smul, exists_and_right] at hM
    simp [hM]
  obtain ⟨σ, hσ⟩ := exists_perm_eq_zero_implies_eq_zero hs' hM
  obtain ⟨i, hi, hi'⟩ := exists_min_image _ (fun i => M i (σ i)) univ_nonempty
  rw [exists_mem_doublyStochastic_eq_smul_iff hs] at hM
  let N : Matrix n n R := M - M i (σ i) • σ.permMatrix R
  have hMi' : 0 < M i (σ i) := (hM.1 _ _).lt_of_ne' fun h => by
    simpa [Equiv.toPEquiv_apply] using hσ _ _ h
  let s' : R := s - M i (σ i)
  have hs' : 0 ≤ s' := by
    simp only [s', sub_nonneg, ← hM.2.1 i]
    exact single_le_sum (fun j _ => hM.1 i j) (by simp)
  have : ∃ M' ∈ doublyStochastic R n, N = s' • M' := by
    rw [exists_mem_doublyStochastic_eq_smul_iff hs']
    simp only [Matrix.sub_apply, Matrix.smul_apply, PEquiv.toMatrix_apply, Equiv.toPEquiv_apply,
      Option.mem_def, Option.some.injEq, smul_eq_mul, mul_ite, mul_one, mul_zero, sub_nonneg,
      sum_sub_distrib, sum_ite_eq, mem_univ, ↓reduceIte, N]
    refine ⟨fun i' j => ?_, by simp [s', hM.2.1], by simp [s', ← σ.eq_symm_apply, hM]⟩
    split
    case isTrue h => exact (hi' i' (by simp)).trans_eq (by rw [h])
    case isFalse h => exact hM.1 _ _
  have hd' : #{i : n × n | N i.1 i.2 ≠ 0} < d := by
    rw [← hd]
    gcongr
    rw [ssubset_iff_of_subset (monotone_filter_right _ _)]
    · simp_rw [mem_filter_univ, not_not, Prod.exists]
      exact ⟨i, σ i, hMi'.ne', by simp [N, Equiv.toPEquiv_apply]⟩
    · rintro ⟨i', j'⟩ _ hN' hM'
      have hσ' : σ i' ≠ j' := by
        simpa [Equiv.toPEquiv_apply] using hσ i' j' hM'
      exact hN' <| by simp [N, hM', hσ', Equiv.toPEquiv_apply]
  obtain ⟨w, hw, hw'⟩ := ih _ hd' _ s' hs' this rfl
  refine ⟨w + fun σ' => if σ' = σ then M i (σ i) else 0, ?_⟩
  simp only [Pi.add_apply, add_smul, sum_add_distrib, hw', ite_smul, zero_smul,
    sum_ite_eq', mem_univ, ↓reduceIte, N, sub_add_cancel, and_true]
  intro σ'
  split <;> simp [add_nonneg, hw, hM.1]

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj : b ∉ map f K
⊢ ∃ y, (ContinuousLinearMap.adjoint f) y ∈ innerDual ↑K ∧ ⟪b, y⟫_ℝ < 0

Tactic:
by
  contrapose! disj; rwa [K.relative_hyperplane_separation]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : IsOrderedRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ClosedIciTopology R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
p : M →ₗ[R] N →ₗ[R] R
inst✝ : p.IsContPerfPair
x : M
s : Set M
⊢ dual p (insert x s) = dual p {x} ⊓ dual p s

Tactic:
rw [insert_eq, dual_union]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
x : M
s : Set M
⊢ dual p (insert x s) = dual p {x} ⊓ dual p s

Tactic:
rw [insert_eq, dual_union]

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

Goal state before:
pp: case inr
β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
⊢ f a ≤ f c

Tactic:
have H₁ : ∀ᶠ y in 𝓝[>] a, f a ≤ f y :=
    h_local_min.filter_mono (nhdsWithin_mono _ Ioi_subset_Ici_self)

Goal state after:
case inr
β : Type u_2
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module ℝ β
inst✝¹ : IsOrderedModule ℝ β
inst✝ : PosSMulReflectLE ℝ β
f : ℝ → β
a b : ℝ
a_lt_b : a < b
h_local_min : IsMinFilter f (𝓝[≥] a) a
h_conv : ConvexOn ℝ (Icc a b) f
c : ℝ
hc : c ∈ Icc a b
a_lt_c : a < c
H₁ : ∀ᶠ (y : ℝ) in 𝓝[>] a, f a ≤ f y
⊢ f a ≤ f c