mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp

Goal state before:
pp: ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ π ≤ π * 2 * ξ.im

Tactic:
mul_assoc,

Goal state after:
ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ π ≤ π * (2 * ξ.im)
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: case refine_2
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝ : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
⊢ ContinuousOn g (closure (Metric.closedBall 0 1)ᶜ)

Tactic:
refine continuousOn_id.norm.inv₀ ?_ |>.smul continuousOn_id
    simp only [closure_compl, interior_closedBall (0 : E) one_ne_zero, mem_compl_iff,
      Metric.mem_ball, dist_zero_right, not_lt, id_eq, ne_eq, norm_eq_zero]
    exact fun x hx ↦ norm_pos_iff.mp <| one_pos.trans_le hx

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

Goal state before:
pp: g : GL (Fin 2) ℝ
h : 0 < (↑g).det
z : ℍ
hz : g • z = z
hc : ↑g 1 0 = 0
hgc : ↑g 1 1 = ↑g 0 0 → ¬0 = ↑g 0 1
⊢ False

Tactic:
simp [gl_smul_eq_iff_num_eq, Complex.ext_iff, σ, h, num, denom, hc, mul_comm, z.im_ne_zero]
      at hz

Goal state after:
g : GL (Fin 2) ℝ
h : 0 < (↑g).det
z : ℍ
hc : ↑g 1 0 = 0
hgc : ↑g 1 1 = ↑g 0 0 → ¬0 = ↑g 0 1
hz : z.re * ↑g 0 0 + ↑g 0 1 = z.re * ↑g 1 1 ∧ ↑g 0 0 = ↑g 1 1
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
⊢ m.IsParabolic ↔ m 0 0 = m 1 1 ∧ m 0 1 ≠ 0

Tactic:
by
  rw [IsParabolic]
  have aux : m.discr = 0 ↔ m 0 0 = m 1 1 := by
    suffices m.discr = (m 0 0 - m 1 1) ^ 2 by
      rw [this, pow_eq_zero_iff two_ne_zero, sub_eq_zero]
    grind [discr_fin_two, trace_fin_two, det_fin_two]
  have (h : m 0 0 = m 1 1) : m ∈ Set.range (scalar _) ↔ m 0 1 = 0 := by
    constructor
    · rintro ⟨a, rfl⟩
      simp
    · intro h'
      use m 1 1
      ext i j
      fin_cases i <;> fin_cases j <;> simp [h, h', hm]
  tauto

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

Goal state before:
pp: n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
⊢ (f' (M' k k)).det ∈ nonZeroDivisors R[X]

Tactic:
polyToMatrix_cornerAddX,

Goal state after:
n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
⊢ (-f (M k k)).charmatrix.det ∈ nonZeroDivisors R[X]
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case pos
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := ⋯
⊢ IsIntegral R ((norm K) (gen K x))

Tactic:
← isIntegral_algebraMap_iff (algebraMap K (AlgebraicClosure F)).injective,

Goal state after:
case pos
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ IsIntegral R ((algebraMap K (AlgebraicClosure ↥F)) ((norm K) (gen K x)))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ 1 + 2 * (dist ↑z ↑w ^ 2 / (2 * 2 * (z.im * w.im))) = 1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)

pp: z w : ℍ
⊢ 0 ≤ z.im * w.im

Tactic:
mul_assoc,

Goal state after:
z w : ℍ
⊢ 1 + 2 * (dist ↑z ↑w ^ 2 / (2 * (2 * (z.im * w.im)))) = 1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)

z w : ℍ
⊢ 0 ≤ z.im * w.im
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ 1 + 2 * dist ↑z ↑w ^ 2 / (2 * (2 * (z.im * w.im))) = 1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)

pp: z w : ℍ
⊢ 0 ≤ z.im * w.im

Tactic:
mul_assoc,

Goal state after:
z w : ℍ
⊢ 1 + 2 * dist ↑z ↑w ^ 2 / (2 * (2 * (z.im * w.im))) = 1 + dist ↑z ↑w ^ 2 / (2 * (z.im * w.im))

z w : ℍ
⊢ 0 ≤ z.im * w.im
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 : P
R : ℝ
hR : R ≠ 0
x : P
⊢ inversion c R (inversion c R x) = x

Tactic:
by
  rcases eq_or_ne x c with (rfl | hne)
  · rw [inversion_self, inversion_self]
  · rw [inversion, dist_inversion_center, inversion_vsub_center, smul_smul, ← mul_pow,
      div_mul_div_comm, div_mul_cancel₀ _ (dist_ne_zero.2 hne), ← sq, div_self, one_pow, one_smul,
      vsub_vadd]
    exact pow_ne_zero _ hR

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 : P
R : ℝ
⊢ inversion c R x = c ↔ x = c ∨ R = 0

Tactic:
by
  by_cases hR : R = 0 <;> simp [inversion_eq_center, hR]

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

Goal state before:
pp: ⊢ StrictMono fun x ↦ sinh x - x

Tactic:
by
  refine strictMono_of_odd_strictMonoOn_nonneg (fun x => by simp; abel) ?_
  refine strictMonoOn_of_deriv_pos (convex_Ici _) ?_ fun x hx => ?_
  · exact (continuous_sinh.sub continuous_id).continuousOn
  · rw [interior_Ici, mem_Ioi] at hx
    rw [deriv_fun_sub, deriv_sinh, deriv_id'', sub_pos, one_lt_cosh]
    exacts [hx.ne', differentiableAt_sinh, differentiableAt_id]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T0Space R
⊢ IsClosed[Units.instTopologicalSpaceUnits] (Set.range ⇑toGL)

Tactic:
by simpa [range_toGL] using isClosed_singleton.preimage <| by fun_prop

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

Goal state before:
pp: α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ s ∈ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i)

Tactic:
rw [← le_principal_iff]

Goal state after:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i) ≤ 𝓟 s
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
⊢ Continuous[_, inst✝²] (Ultrafilter.extend f)

Tactic:
let _ : TopologicalSpace α := ⊥

Goal state after:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
h : ∀ (b : Ultrafilter α), ∃ c, Tendsto f (comap pure (𝓝 b)) (𝓝 c)
x✝ : TopologicalSpace α := ⊥
⊢ Continuous[_, inst✝²] (Ultrafilter.extend f)
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✝ : ProperSMul G X
t : Set X
Φ : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
Φ_proper : IsProperMap Φ
α : G × ↑t ≃ₜ ↑(Φ ⁻¹' snd ⁻¹' t) :=
  have this := ⋯;
  (((Homeomorph.Set.univ G).symm.prodCongr (Homeomorph.refl ↑t)).trans (Homeomorph.Set.prod univ t).symm).trans
    (Homeomorph.setCongr this)
⊢ IsProperMap fun gx ↦ (gx.1 • ↑gx.2, gx.2)

Tactic:
let β : X × t ≃ₜ (snd ⁻¹' t) :=
    Homeomorph.Set.univ X |>.symm.prodCongr (.refl t) |>.trans
      ((Homeomorph.Set.prod _ t).symm) |>.trans (Homeomorph.setCongr univ_prod)

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✝ : ProperSMul G X
t : Set X
Φ : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
Φ_proper : IsProperMap Φ
α : G × ↑t ≃ₜ ↑(Φ ⁻¹' snd ⁻¹' t) :=
  have this := ⋯;
  (((Homeomorph.Set.univ G).symm.prodCongr (Homeomorph.refl ↑t)).trans (Homeomorph.Set.prod univ t).symm).trans
    (Homeomorph.setCongr this)
β : X × ↑t ≃ₜ ↑(snd ⁻¹' t) :=
  (((Homeomorph.Set.univ X).symm.prodCongr (Homeomorph.refl ↑t)).trans (Homeomorph.Set.prod univ t).symm).trans
    (Homeomorph.setCongr ⋯)
⊢ IsProperMap fun gx ↦ (gx.1 • ↑gx.2, gx.2)
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)
s : Set ((i : ι) × X i)
h :
  ∀ (K : Type (max u v)) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → (i : ι) × X i),
    Continuous[_, instTopologicalSpaceSigma] f → IsClosed (f ⁻¹' s)
i : ι
K : Type v
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X i
hf : Continuous[x✝², inst✝¹ i] f
⊢ IsClosed[x✝²] (f ⁻¹' Sigma.mk i ⁻¹' s)

Tactic:
let g : ULift.{u} K → (Σ i, X i) := Sigma.mk i ∘ f ∘ ULift.down

Goal state after:
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)
s : Set ((i : ι) × X i)
h :
  ∀ (K : Type (max u v)) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → (i : ι) × X i),
    Continuous[_, instTopologicalSpaceSigma] f → IsClosed (f ⁻¹' s)
i : ι
K : Type v
x✝² : TopologicalSpace K
x✝¹ : CompactSpace K
x✝ : T2Space K
f : K → X i
hf : Continuous[x✝², inst✝¹ i] f
g : ULift.{u, v} K → (i : ι) × X i := Sigma.mk i ∘ f ∘ ULift.down
⊢ IsClosed[x✝²] (f ⁻¹' Sigma.mk i ⁻¹' s)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ σ =ᶠ[𝓝 g] fun x ↦ σ g

Tactic:
suffices {h | 0 < h.det.val} ∈ 𝓝 g by
      filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]
    exact isOpen_Ioi (a := (0 : ℝ)) |>.preimage (by fun_prop) |>.mem_nhds hg

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

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ characteristic f ⊤ - characteristic f⁻¹ ⊤ =
    circleAverage (fun x ↦ log ‖f x‖) 0 - Function.locallyFinsuppWithin.logCounting (divisor f Set.univ)

Tactic:
by
  calc characteristic f ⊤ - characteristic f⁻¹ ⊤
  _ = proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤) := by
    unfold characteristic
    ring
  _ = circleAverage (log ‖f ·‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) := by
    rw [proximity_sub_proximity_inv_eq_circleAverage h]
  _ = circleAverage (log ‖f ·‖) 0 - (logCounting f 0 - logCounting f ⊤) := by
    rw [logCounting_inv]
  _ = circleAverage (log ‖f ·‖) 0 - (divisor f Set.univ).logCounting := by
    rw [← ValueDistribution.log_counting_zero_sub_logCounting_top]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
⊢ 0 ≤ logCounting f r

Tactic:
suffices ∀ z, 0 ≤ toClosedBall r f z * log (r * ‖z‖⁻¹) from
    add_nonneg (finsum_nonneg this) <| mul_nonneg (by simpa using h 0) (log_nonneg hr)

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
⊢ ∀ (z : E), 0 ≤ ↑(((toClosedBall r) f) z) * log (r * ‖z‖⁻¹)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case pos.e_6
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : a = ⊤
⊢ divisor f univ = divisor g univ

Tactic:
exact divisor_congr_codiscreteWithin hfg isOpen_univ

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ logCounting (f₁ * f₂) 0 r ≤ (logCounting f₁ 0 + logCounting f₂ 0) r

Tactic:
simp only [logCounting, WithTop.zero_ne_top, reduceDIte, WithTop.untop₀_zero, sub_zero]

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ locallyFinsuppWithin.logCounting (divisor (fun x ↦ (f₁ * f₂) x) univ)⁺ r ≤
    (locallyFinsuppWithin.logCounting (divisor (fun x ↦ f₁ x) univ)⁺ +
        locallyFinsuppWithin.logCounting (divisor (fun x ↦ f₂ x) univ)⁺)
      r
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (Icc 0 t)
⊢ EqOn φ id (Icc 0 s)

Tactic:
← φst

Goal state after:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
⊢ EqOn φ id (Icc 0 s)
Module: Mathlib.Analysis.Convex.BetweenList

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

Tactic:
wbtw_cons,

Goal state after:
case cons
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]
⊢ (Pairwise (Wbtw R head) tail ∧ List.Wbtw R tail) ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (head :: tail) ↔
    Triplewise (Sbtw R) (head :: tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
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}
⊢ (x, ↑a) ∉ A

Tactic:
by simp [A, hax]

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

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' ι'' : Finset ι
h : ι' ⊆ ι''
f : ↑(hallMatchingsOn t ι'')
⊢ ↑(hallMatchingsOn t ι')

Tactic:
refine ⟨fun i => f.val ⟨i, h i.property⟩, ?_⟩
  obtain ⟨hinj, hc⟩ := f.property
  refine ⟨?_, fun i => hc ⟨i, h i.property⟩⟩
  rintro ⟨i, hi⟩ ⟨j, hj⟩ hh
  simpa only [Subtype.mk_eq_mk] using hinj hh

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

Goal state before:
pp: case mp.refine_1
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
⊢ ι → α

pp: case mp.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
⊢ Injective ?mp.refine_1

pp: case mp.refine_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
⊢ ∀ (x : ι), ?mp.refine_1 x ∈ t x

Tactic:
· -- Build the matching function from the section
        exact fun i =>
          (u (Opposite.op ({i} : Finset ι))).val ⟨i, by simp only [mem_singleton]⟩

Goal state after:
case mp.refine_2
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
⊢ Injective fun i ↦ ↑(u (Opposite.op {i})) ⟨i, ⋯⟩

case mp.refine_3
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
h : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
this✝ : ∀ (ι' : (Finset ι)ᵒᵖ), Nonempty ((hallMatchingsFunctor t).obj ι')
this : ∀ (ι' : (Finset ι)ᵒᵖ), Finite ((hallMatchingsFunctor t).obj ι')
u : (j : (Finset ι)ᵒᵖ) → (hallMatchingsFunctor t).obj j
hu : u ∈ (hallMatchingsFunctor t).sections
⊢ ∀ (x : ι), ↑(u (Opposite.op {x})) ⟨x, ⋯⟩ ∈ t x
Module: Mathlib.CategoryTheory.CofilteredSystem

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

Tactic:
by
  have : ∀ j, Fintype (F.obj j) := fun j => Fintype.ofFinite (F.obj j)
  have : Fintype F.sections := Fintype.ofFinite F.sections
  have card_le : ∀ j, Fintype.card (F.obj j) ≤ Fintype.card F.sections :=
    fun j => Fintype.card_le_of_surjective _ (F.eval_section_surjective_of_surjective Fsur j)
  let fn j := Fintype.card F.sections - Fintype.card (F.obj j)
  refine ⟨fn.argmin,
    fun i f => ((Fintype.bijective_iff_surjective_and_card _).2
      ⟨Fsur f, le_antisymm ?_ (Fintype.card_le_of_surjective _ <| Fsur f)⟩).1⟩
  rw [← Nat.sub_le_sub_iff_left (card_le i)]
  apply fn.argmin_le

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

Goal state before:
pp: case h
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
hd : #{i | M i.1 i.2 ≠ 0} = d
hs : 0 ≤ 0
hM : (∃ x, x ∈ doublyStochastic R n) ∧ M = 0
⊢ (∀ (σ : Equiv.Perm n), 0 ≤ 0 σ) ∧ ∑ σ, 0 σ • Equiv.Perm.permMatrix R σ = M

Tactic:
simp [hM]

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

Goal state before:
pp: case inl
V : Type u_1
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup V
inst✝¹ : Module ℝ V
inst✝ : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
b : ℝ≥0
h : 0 ≤ b
⊢ 0 • ↑K ⊆ b • ↑K

Tactic:
rw [Set.zero_smul_set K.nonempty, Set.zero_subset]

Goal state after:
case inl
V : Type u_1
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup V
inst✝¹ : Module ℝ V
inst✝ : ContinuousSMul ℝ V
K : ConvexBody V
h_zero : 0 ∈ K
b : ℝ≥0
h : 0 ≤ b
⊢ 0 ∈ b • ↑K
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x y z : R
hxz : x ≤ z
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
by
  cases hxz.eq_or_lt with
  | inl hxz =>
    subst hxz
    rw [← le_antisymm_iff, wbtw_self_iff, eq_comm]
  | inr hxz =>
    have hxz' : 0 < z - x := sub_pos.mpr hxz
    let r := (y - x) / (z - x)
    have hy : y = r * (z - x) + x := by simp [r, hxz'.ne']
    simp [hy, wbtw_mul_sub_add_iff, mul_nonneg_iff_of_pos_right hxz', ← le_sub_iff_add_le,
      mul_le_iff_le_one_left hxz', hxz.ne]

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

Goal state before:
pp: case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ (1 - r) • (y -ᵥ x) ≠ 0

Tactic:
smul_ne_zero_iff,

Goal state after:
case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ 1 - r ≠ 0 ∧ y -ᵥ x ≠ 0
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
hne : x ≠ y
r : R
hr : 1 < r
⊢ 1 ≠ r ∧ y ≠ x

Tactic:
exact ⟨hr.ne, hne.symm⟩

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

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K ↑C
x₀ : E
hx₀ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, f a < u
huv : u < v
hv : ∀ b ∈ ↑C, v < f b
⊢ ∃ f, (∀ x ∈ C, 0 ≤ f x) ∧ ∀ x ∈ K, f x < 0

Tactic:
have hv₀ : v < 0 := by simpa using hv 0 C.zero_mem

Goal state after:
case inr
E : Type u_1
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
K : Set E
C : ProperCone ℝ E
hKconv : Convex ℝ K
hKcomp : IsCompact K
hKC : Disjoint K ↑C
x₀ : E
hx₀ : x₀ ∈ K
f : StrongDual ℝ E
u v : ℝ
hu : ∀ a ∈ K, f a < u
huv : u < v
hv : ∀ b ∈ ↑C, v < f b
hv₀ : v < 0
⊢ ∃ f, (∀ x ∈ C, 0 ≤ f x) ∧ ∀ x ∈ K, f x < 0
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: case refine_1
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
C₁ : PointedCone R G
C₂ : PointedCone R H
w : G ⊗[R] H
hw : ∀ φ ∈ dual (Dual.eval R G) ↑C₁, ∀ ψ ∈ dual (Dual.eval R H) ↑C₂, 0 ≤ ((dualDistrib R G H) (φ ⊗ₜ[R] ψ)) w
ψ : Dual R H
hψ : ψ ∈ dual (Dual.eval R H) ↑C₂
φ : Dual R G
hφ : φ ∈ dual (Dual.eval R G) ↑C₁
⊢ 0 ≤ ((dualDistrib R H G) (ψ ⊗ₜ[R] φ)) (↑(TensorProduct.comm R G H) w)

Tactic:
simpa [dualDistrib_apply_comm] using hw φ hφ ψ hψ

Goal state after: