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

Goal state before:
pp: case h
Y : Type v
Z : Type w
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y)
g : C(X✝, Z)
hg : ContinuousMap.restrict s g = ι.comp f
x : ↑s
this : r.comp (ContinuousMap.restrict s g) = (ContinuousMap.id Y).comp f
⊢ (ContinuousMap.restrict s (r.comp g)) x = f x

Tactic:
f.id_comp

Goal state after:
case h
Y : Type v
Z : Type w
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y)
g : C(X✝, Z)
hg : ContinuousMap.restrict s g = ι.comp f
x : ↑s
this : r.comp (ContinuousMap.restrict s g) = f
⊢ (ContinuousMap.restrict s (r.comp g)) x = f x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
z : ℂ
hz : 0 < z.im
this : ↑a * z * ↑a + ↑b * ↑a = ↑b * ↑a + ↑a * ↑a * z
⊢ ↑(⟨!![a, b; 0, a⁻¹], ⋯⟩ • { coe := z, coe_im_pos := hz }) =
    ↑(((fun x ↦ b * a +ᵥ x) ∘ fun x ↦ ⟨a * a, ⋯⟩ • x) { coe := z, coe_im_pos := hz })

Tactic:
by simpa [specialLinearGroup_apply, add_mul]

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
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
by
  induction l : Fintype.card m generalizing R S m with
  | zero =>
    rw [Fintype.card_eq_zero_iff] at l
    simp_rw [Matrix.det_isEmpty, map_one, det_one]
  | succ l ih =>
    have ⟨k⟩ := Fintype.card_pos_iff.mp (Nat.lt_of_sub_eq_succ l)
    let f' := f.polyToMatrix
    let M' := cornerAddX M k
    have : (f' M'.det).det = ((M'.map f').comp m m n n R[X]).det := by
      refine sub_eq_zero.mp <| mem_nonZeroDivisors_iff_right.mp
        (pow_mem ?_ _) _ (det_det_aux k fun M ↦ ih _ _ <| by
          grind [Fintype.card_subtype_compl, Fintype.card_unique])
      rw [polyToMatrix_cornerAddX, ← charpoly]
      exact (Matrix.charpoly_monic _).mem_nonZeroDivisors
    rw [← eval_zero_det_det, congr_arg (eval 0) this, eval_zero_comp_det]

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
this : Algebra.IsSeparable K ↥K⟮x⟯
⊢ IsSeparable K (adjoin.powerBasis hx).gen

Tactic:
exact Algebra.IsSeparable.isSeparable K _

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ IsSeparable K (adjoin.powerBasis hx).gen

Tactic:
have := Algebra.isSeparable_tower_bot_of_isSeparable K K⟮x⟯ L
    exact Algebra.IsSeparable.isSeparable K _

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist ((R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c) ((R / dist y c) ^ 2 • (y -ᵥ c) +ᵥ c) =
    R ^ 2 / (dist x c * dist y c) * dist x y

Tactic:
simp_rw [dist_vadd_cancel_right, dist_eq_norm_vsub V _ c]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist ((R / ‖x -ᵥ c‖) ^ 2 • (x -ᵥ c)) ((R / ‖y -ᵥ c‖) ^ 2 • (y -ᵥ c)) = R ^ 2 / (‖x -ᵥ c‖ * ‖y -ᵥ c‖) * dist x y
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : PreStoneCech α → β
h₁ : Continuous[_, inst✝¹] g₁
h₂ : Continuous[_, inst✝¹] g₂
h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit
⊢ EqOn g₁ g₂ (range preStoneCechUnit)

Tactic:
rintro x ⟨x, rfl⟩

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : PreStoneCech α → β
h₁ : Continuous[_, inst✝¹] g₁
h₂ : Continuous[_, inst✝¹] g₂
h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit
x : α
⊢ g₁ (preStoneCechUnit x) = g₂ (preStoneCechUnit x)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
⊢ dist (ModularGroup.S • y₁) (ModularGroup.S • y₂) = dist y₁ y₂

Tactic:
by
        have h₁ : 0 ≤ im y₁ * im y₂ := by positivity
        have h₂ : ‖(y₁ * y₂ : ℂ)‖ ≠ 0 := by simp [y₁.ne_zero, y₂.ne_zero]
        simp_rw [modular_S_smul, inv_neg, dist_eq, dist_neg_neg,
          dist_inv_inv₀ y₁.ne_zero y₂.ne_zero, mk_im, neg_im, inv_im, coe_im, neg_div, neg_neg,
          div_mul_div_comm, ← normSq_mul, Real.sqrt_div h₁, ← norm_def, mul_div (2 : ℝ)]
        rw [div_div_div_comm, ← norm_mul, div_self h₂, div_one]

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

Goal state before:
pp: X : Type u_1
Y✝ : Type u_2
inst✝⁴ : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst✝³ : DiscreteTopology X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
inst✝ : Infinite X
f : C(OnePoint X, Y)
⊢ (fun f ↦
        {
          toFun := fun x ↦
            match x with
            | none => Classical.choose ⋯
            | Option.some x => ↑f x,
          continuous_toFun := ⋯ })
      ((fun f ↦ ⟨fun x ↦ f ↑x, ⋯⟩) f) =
    f

Tactic:
by
    ext x
    refine OnePoint.rec ?_ ?_ x
    · refine tendsto_nhds_unique ?_ (continuous_iff_from_discrete _ |>.mp <| map_continuous f)
      let f' : { f : X → Y // ∃ L, Tendsto (fun x : X ↦ f x) cofinite (𝓝 L) } :=
        ⟨fun x ↦ f x, ⟨f ∞, continuous_iff_from_discrete f |>.mp <| map_continuous f⟩⟩
      exact Classical.choose_spec f'.property
    · simp

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : WeaklyLocallyCompactSpace X
s : Set X
h : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
⊢ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Tactic:
intro x ℱ hℱ₁ hℱ₂ hℱ₃

Goal state after:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : WeaklyLocallyCompactSpace X
s : Set X
h : ∀ (K : Set X), IsCompact K → IsClosed[inst✝³] (s ∩ K)
x : X
ℱ : Filter X
hℱ₁ : ℱ.NeBot
hℱ₂ : ℱ ≤ 𝓟 s
hℱ₃ : ℱ ≤ 𝓝 x
⊢ x ∈ s
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ IntegrableOn (fun x ↦ ∫ (β : ℝ) in 0..2 * π, cartanKernel f R x β) (Ioc 0 (2 * π)) volume

Tactic:
by
  have h_int := Cartan.integrableOn_cartanKernel (R := R) h
  rw [uIoc_of_le two_pi_pos.le, IntegrableOn, Measure.volume_eq_prod, ← Measure.prod_restrict]
    at h_int
  simpa [IntegrableOn, intervalIntegral.integral_of_le two_pi_pos.le, Cartan.cartanKernel]
    using h_int.integral_prod_left

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
x y : P
r : R
⊢ (lineMap x y) r ∈ ↑line[R, x, y]

Tactic:
exact lineMap_mem_affineSpan_pair _ _ _

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

Goal state before:
pp: case neg.refine_3
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
tail : List P
ht2 : ¬tail = []
r : R
hr0 : 0 ≤ r
hr1 : r ≤ 1
hl : head :: (lineMap head (tail.getLast ht2)) r :: tail ≠ []
h :
  ((∀ a' ∈ tail, Wbtw R head ((lineMap head (tail.getLast ht2)) r) a') ∧ Pairwise (Wbtw R head) tail) ∧
    List.Wbtw R ((lineMap head (tail.getLast ht2)) r :: tail)
ht : ¬(lineMap head (tail.getLast ht2)) r :: tail = []
hl'' :
  map (⇑(lineMap ((lineMap head (tail.getLast ht2)) r) (tail.getLast ht2))) l'' =
    (lineMap head (tail.getLast ht2)) r :: tail
⊢ map (⇑(lineMap head (tail.getLast ht2))) (0 :: map (fun x ↦ r + (1 - r) * x) l'') =
    head :: (lineMap head (tail.getLast ht2)) r :: tail

Tactic:
simp only [map_cons, lineMap_apply_zero, map_map, ← hl'', cons.injEq,
                map_inj_left, Function.comp_apply, lineMap_lineMap_left, lineMap_eq_lineMap_iff,
                true_and]
              ring_nf
              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✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
⊢ (lineMap x z) r ∈ line[R, x, z]

Tactic:
exact lineMap_mem_affineSpan_pair _ _ _

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✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
l : List P
hl : l ≠ []
⊢ (∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)) ↔
    List.Sbtw R l

Tactic:
by
  refine ⟨fun ⟨l', hl's, hl'l, hla⟩ ↦
            ⟨(exists_map_eq_of_sorted_nonempty_iff_wbtw hl).1
            ⟨l', (hl's.pairwise.imp LT.lt.le).sortedLE, hl'l⟩, ?_⟩,
          fun h ↦ ?_⟩
  · rw [← hl'l]
    rcases hla with hla | hla
    · grind [List.pairwise_iff_forall_sublist]
    · exact (hl's.pairwise.imp LT.lt.ne).map _ fun _ _ ↦ (lineMap_injective _ hla).ne
  · rw [List.Sbtw, ← exists_map_eq_of_sorted_nonempty_iff_wbtw hl] at h
    rcases h with ⟨⟨l', hl's, hl'l⟩, hp⟩
    refine ⟨l', ?_, hl'l, ?_⟩
    · rw [← hl'l] at hp
      have hp' : l'.Pairwise (· ≠ ·) := hp.of_map _ (by simp)
      exact ((pairwise_and_iff.2 ⟨hl's.pairwise, hp'⟩).imp lt_iff_le_and_ne.2).sortedLT
    · cases l with
      | nil => simp at hl
      | cons head tail =>
        simp only [length_cons, add_eq_right, length_eq_zero_iff, head_cons]
        cases tail with
        | nil => simp
        | cons head2 tail =>
          simp only [reduceCtorEq, false_or]
          rw [pairwise_cons] at hp
          refine hp.1 ((head :: head2 :: tail).getLast hl) ?_
          simp

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

Goal state before:
pp: case mp
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 z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : (tx • (z -ᵥ (ty • (z -ᵥ x) +ᵥ x)) + ty • (z -ᵥ x)) +ᵥ x = x
⊢ x = (lineMap x z) ty

Tactic:
← @vsub_eq_zero_iff_eq V,

Goal state after:
case mp
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 z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : ((tx • (z -ᵥ (ty • (z -ᵥ x) +ᵥ x)) + ty • (z -ᵥ x)) +ᵥ x) -ᵥ x = 0
⊢ x = (lineMap x z) ty
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mp
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 z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : tx • (z -ᵥ (ty • (z -ᵥ x) +ᵥ x)) + ty • (z -ᵥ x) = 0
⊢ x = (lineMap x z) ty

Tactic:
vsub_vadd_eq_vsub_sub,

Goal state after:
case mp
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 z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
hx : tx • (z -ᵥ x - ty • (z -ᵥ x)) + ty • (z -ᵥ x) = 0
⊢ x = (lineMap x z) ty
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mp.inl
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 z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : tx * (1 - ty) + ty = 0
⊢ x = (lineMap x z) ty

Tactic:
add_eq_zero_iff_neg_eq

Goal state after:
case mp.inl
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 z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : -(tx * (1 - ty)) = ty
⊢ x = (lineMap x z) ty
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case refine_3
𝕜 : 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
x : E
⊢ f x ≤ φ x

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:
· simpa using! hb ▸ h ⟨x, trivial⟩

Goal state after:
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
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
i : l
j : n
⊢ (if j ∈ (f i).bind ⇑g then 1 else 0) = Option.rec 0 (fun val ↦ if j ∈ g val then 1 else 0) (f i)

Tactic:
cases f i <;> simp

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✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
s : R
hs : 0 ≤ s
⊢ (∃ M' ∈ doublyStochastic R n, M = s • M') →
    (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s

Tactic:
rintro ⟨M', hM', rfl⟩
    rw [mem_doublyStochastic_iff_sum] at hM'
    simp only [Matrix.smul_apply, smul_eq_mul, ← mul_sum]
    exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩

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
x y : P
hne : x ≠ y
r : R
h : Wbtw R x y ((lineMap x y) r)
⊢ (lineMap x y) r ∈ line[R, x, y]

Tactic:
exact lineMap_mem_affineSpan_pair _ _ _

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

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

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

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

Tactic:
suffices ∀ i j : n, x₁ i j = x₂ i j by
    obtain rfl : x₁ = x₂ := by simpa [← Matrix.ext_iff]
    simp_all

Goal state after:
case refine_2
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
σ : Equiv.Perm n
x₁ : Matrix n n R
hx₁ : x₁ ∈ ↑(doublyStochastic R n)
x₂ : Matrix n n R
hx₂ : x₂ ∈ ↑(doublyStochastic R n)
hσ : Equiv.Perm.permMatrix R σ ∈ openSegment R x₁ x₂
⊢ ∀ (i j : n), x₁ i j = x₂ i j
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
ι : Sort u_4
f : ι → Set M
⊢ dual p (⋃ i, f i) = ⨅ i, dual p (f i)

Tactic:
by
  ext; simp [forall_comm (α := M)]

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
S : Set (Set M)
⊢ dual p (⋃₀ S) = sInf (dual p '' S)

Tactic:
by
  ext; simp [forall_comm (α := M)]

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
x y : P
h : x ≠ y
⊢ x ≠ (pointReflection R x) y

Tactic:
nth_rw 1 [← pointReflection_self R x]

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 : P
h : x ≠ y
⊢ (pointReflection R x) x ≠ (pointReflection R x) y
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
ι : Sort u_4
f : ι → Set M
⊢ dual p (⋃ i, f i) = ⨅ i, dual p (f i)

Tactic:
by
  ext; simp [forall_comm (α := M)]

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
S : Set (Set M)
⊢ dual p (⋃₀ S) = sInf (dual p '' S)

Tactic:
by
  ext; simp [forall_comm (α := M)]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
x : E
hxA : x ∈ A
hx : ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x
⊢ x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x} ∩ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}

Tactic:
refine ⟨⟨hxA, fun y hy => ?_⟩, hxA, fun y hy => ?_⟩

Goal state after:
case refine_2.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
x : E
hxA : x ∈ A
hx : ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x
y : E
hy : y ∈ A
⊢ l₁ y ≤ l₁ x

case refine_2.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
inst✝¹ : IsOrderedRing 𝕜
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
x : E
hxA : x ∈ A
hx : ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x
y : E
hy : y ∈ A
⊢ l₂ y ≤ l₂ x