mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp.g
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
hg11 : ↑g 1 1 = -1
⊢ ∃ x, x ≠ 0 ∧ ↑g = ↑(-upperRightHom x)

Tactic:
refine ⟨-g 0 1, neg_eq_zero.not.mpr hg01, ?_⟩

Goal state after:
case mp.g
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
hg11 : ↑g 1 1 = -1
⊢ ↑g = ↑(-upperRightHom (-↑g 0 1))
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
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det *
      ((((Matrix.comp m m n n R) ((auxMat M k).map ⇑f)).toSquareBlock (fun i ↦ i.1 ≠ k) True).det *
        (((Matrix.comp m m n n R) ((auxMat M k).map ⇑f)).toSquareBlock (fun i ↦ i.1 ≠ k) False).det)

Tactic:
comp_toSquareBlock (b := (· ≠ k)),

Goal state after:
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
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det *
      (((reindex Equiv.prodSubtypeFstEquivSubtypeProd.symm Equiv.prodSubtypeFstEquivSubtypeProd.symm)
            ((Matrix.comp { a // (a ≠ k) = True } { a // (a ≠ k) = True } n n R)
              (((auxMat M k).map ⇑f).toSquareBlock (fun x ↦ x ≠ k) True))).det *
        ((reindex Equiv.prodSubtypeFstEquivSubtypeProd.symm Equiv.prodSubtypeFstEquivSubtypeProd.symm)
            ((Matrix.comp { a // (a ≠ k) = False } { a // (a ≠ k) = False } n n R)
              (((auxMat M k).map ⇑f).toSquareBlock (fun x ↦ x ≠ k) False))).det)
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
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det *
      (((Matrix.comp { a // (a ≠ k) = True } { a // (a ≠ k) = True } n n R)
            (((auxMat M k).map ⇑f).toSquareBlock (fun x ↦ x ≠ k) True)).det *
        ((Matrix.comp { a // (a ≠ k) = False } { a // (a ≠ k) = False } n n R)
            (((auxMat M k).map ⇑f).toSquareBlock (fun x ↦ x ≠ k) False)).det)

Tactic:
map_toSquareBlock,

Goal state after:
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
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det *
      (((Matrix.comp { a // (a ≠ k) = True } { a // (a ≠ k) = True } n n R)
            (((auxMat M k).toSquareBlock (fun x ↦ x ≠ k) True).map ⇑f)).det *
        ((Matrix.comp { a // (a ≠ k) = False } { a // (a ≠ k) = False } n n R)
            (((auxMat M k).toSquareBlock (fun x ↦ x ≠ k) False).map ⇑f)).det)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt✝ : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hlt : g y < b
⊢ (g - dg) y < b

Tactic:
exact ((sub_le_self_iff _).2 (dgmem _).1).trans_lt hlt

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
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp { a // (a = k) = True } { a // (a = k) = True } n n R)
          (((M * auxMat M k).map ⇑f).toSquareBlock (fun x ↦ x = k) True)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).map ⇑f).toSquareBlock (fun x ↦ x = k) False)).det =
    (f (M k k)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det

Tactic:
map_toSquareBlock,

Goal state after:
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
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp { a // (a = k) = True } { a // (a = k) = True } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) True).map ⇑f)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    (f (M k k)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.inr.inl.inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
b : ℝ
hb : IsLUB (range ⇑f) b
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
dg : Y →ᵇ ℝ
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
x : X
ha : IsGLB (range ⇑f) (f x)
hmem : ∀ (x_1 : X), f x_1 ∈ Icc (f x) b
hle : f x ≤ b
hlt : f x < b
c : ℝ := (f x + b) / 2
hac : f x < c
hcb : c < b
hsub : c - f x = b - c
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hc : c < g y
⊢ ∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)

Tactic:
refine ⟨x, xu, ?_, hyxu.le⟩

Goal state after:
case inr.inr.inl.inl
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
b : ℝ
hb : IsLUB (range ⇑f) b
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
dg : Y →ᵇ ℝ
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
x : X
ha : IsGLB (range ⇑f) (f x)
hmem : ∀ (x_1 : X), f x_1 ∈ Icc (f x) b
hle : f x ≤ b
hlt : f x < b
c : ℝ := (f x + b) / 2
hac : f x < c
hcb : c < b
hsub : c - f x = b - c
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hc : c < g y
⊢ f x ≤ (g - dg) y
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case left
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ Tendsto (UpperHalfPlane.coe ∘ ↑ofComplex) (𝓝 z) (𝓝 ↑(↑ofComplex z))

Tactic:
refine Tendsto.congr' (eventuallyEq_coe_comp_ofComplex hz).symm ?_

Goal state after:
case left
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ Tendsto id (𝓝 z) (𝓝 ↑(↑ofComplex z))
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
cases isEmpty_or_nonempty X
  · rcases hne with ⟨c, hc⟩
    exact ⟨const Y c, fun _ => hc, funext fun x => isEmptyElim x⟩
  rcases exists_extension_forall_exists_le_ge_of_isClosedEmbedding f he with ⟨g, hg, hgf⟩
  refine ⟨g, fun y => ?_, hgf⟩
  rcases hg y with ⟨xl, xu, h⟩
  exact hs.out (hf _) (hf _) h

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

Goal state before:
pp: z w : ℍ
⊢ Real.cosh (dist z w) = ((z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2) / (2 * z.im * w.im)

Tactic:
simp [field, cosh_dist, Complex.dist_eq, Complex.sq_norm, normSq_apply]

Goal state after:
z w : ℍ
⊢ z.im * w.im * 2 + ((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2) = (z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
⊢ B = A

Tactic:
rw [← Ultrafilter.coe_le_coe]

Goal state after:
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
⊢ ↑B ≤ ↑A
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
⊢ Tendsto preStoneCechUnit (↑g) (𝓝 (preStoneCechUnit x))

Tactic:
have : (map preStoneCechUnit g : Filter (PreStoneCech α)) ≤ 𝓝 (Quot.mk _ g) :=
      (map_mono this).trans (continuous_quot_mk.tendsto _)

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
this✝ : ↑(Ultrafilter.map pure g) ≤ 𝓝 g
this : map preStoneCechUnit ↑g ≤ 𝓝 (Quot.mk (fun F G ↦ ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) g)
⊢ Tendsto preStoneCechUnit (↑g) (𝓝 (preStoneCechUnit x))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ 2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)) / (‖↑y₁ * ↑y₂‖ / ‖↑y₁ * ↑y₂‖)) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))

Tactic:
div_self h₂,

Goal state after:
z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ 2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)) / 1) = 2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))
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
hc : ContinuousSMul G X
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
hxx : Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
g : G
⊢ g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g) ↔ Tendsto fst (↑𝒰) (𝓝 g)

Tactic:
exact and_iff_right_of_imp fun hg ↦ tendsto_nhds_unique
    (hg.smul ((continuous_snd.tendsto _).comp hxx)) ((continuous_fst.tendsto _).comp hxx)

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case mp
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X ↦ ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X ↦ ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
g : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun y' ↦ { down := ⟨φ y', ⋯⟩ }, continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun x ↦ { down := ⟨0, ⋯⟩ }, continuous_toFun := ⋯ }
⊢ False

Tactic:
have H : h = g := by
      rw [← cancel_epi f]
      ext x : 4
      simp [g, h, Z, hφ0 (Set.mem_range_self x)]

Goal state after:
case mp
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
hCD : Disjoint C D
φ : C((fun X ↦ ↑X.toTop) Y, ℝ)
hφ0 : Set.EqOn (⇑φ) 0 C
hφ1 : Set.EqOn (⇑φ) 1 D
hφ01 : ∀ (x : (fun X ↦ ↑X.toTop) Y), φ x ∈ Set.Icc 0 1
this✝ : CompactSpace (ULift.{u, 0} ↑(Set.Icc 0 1))
this : T2Space (ULift.{u, 0} ↑(Set.Icc 0 1))
Z : CompHaus := of (ULift.{u, 0} ↑(Set.Icc 0 1))
g : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun y' ↦ { down := ⟨φ y', ⋯⟩ }, continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun x ↦ True) { toFun := fun x ↦ { down := ⟨0, ⋯⟩ }, continuous_toFun := ⋯ }
H : h = g
⊢ False
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
⊢ ProperSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}

Tactic:
by
  refine ⟨fun h ↦ ProperSMul.isCompact_setOfPred_inter_nonempty, fun h ↦ ⟨?_⟩⟩
  refine isProperMap_iff_isCompact_preimage.mpr ⟨by fun_prop, fun {K} hK ↦ ?_⟩
  -- First reduce to the case `K = U × V`.
  let U := Prod.fst '' K
  let V := Prod.snd '' K
  have hU : IsCompact U := hK.image continuous_fst
  have hV : IsCompact V := hK.image continuous_snd
  suffices IsCompact ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' (U ×ˢ V)) by
    apply this.of_isClosed_subset (hK.isClosed.preimage <| by fun_prop)
    exact Set.preimage_mono Set.subset_fst_image_prod_snd_image
  apply ((h hV hU).prod hV).of_isClosed_subset
  · exact (hU.prod hV).isClosed.preimage (by fun_prop)
  · exact fun ⟨g, x⟩ ⟨hgx, hgx'⟩ ↦ ⟨⟨g • x, smul_mem_smul_set hgx', hgx⟩, hgx'⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ a * |logCounting D ℓ| < a * |logCounting D (1 + ℓ)|

Tactic:
gcongr 2

Goal state after:
case hbc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := ⋯
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ |logCounting D ℓ| < |logCounting D (1 + ℓ)|
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
⊢ MonotoneOn (logCounting D) (Ioi 0)

Tactic:
by
  intro a ha b hb _
  simp_all only [mem_Ioi, logCounting, AddMonoidHom.coe_mk, ZeroHom.coe_mk]
  gcongr
  · let s := (toClosedBall b D).support
    have hs : s.Finite := (toClosedBall b D).finiteSupport (isCompact_closedBall 0 |b|)
    repeat rw [finsum_eq_sum_of_support_subset (s := hs.toFinset)]
    · gcongr 1 with z hz
      by_cases h₂z : z = 0
      · simp [h₂z]
      · have := (toClosedBall_support_subset_closedBall D (hs.mem_toFinset.1 hz))
        rw [toClosedBall_eval_within _ this]
        by_cases h₃z : z ∈ closedBall 0 |a|
        · rw [toClosedBall_eval_within _ h₃z]
          gcongr
          exact Int.cast_nonneg (hD z)
        · simp only [h₃z, not_false_eq_true, apply_eq_zero_of_notMem, Int.cast_zero, zero_mul,
            ge_iff_le]
          apply mul_nonneg (Int.cast_nonneg (hD z)) (log_nonneg _)
          apply (le_mul_inv_iff₀ (norm_pos_iff.mpr h₂z)).2
          simp_all [abs_of_pos hb]
    · intro z
      aesop
    · intro z
      simp only [support_mul, mem_inter_iff, mem_support, ne_eq, Int.cast_eq_zero, log_eq_zero,
        mul_eq_zero, inv_eq_zero, norm_eq_zero, not_or, Finite.coe_toFinset, and_imp, s]
      intro h₁ _ _ _ _
      have : z ∈ closedBall 0 |a| := mem_of_indicator_ne_zero h₁
      rw [toClosedBall_eval_within _ this] at h₁
      rwa [toClosedBall_eval_within]
      · simp_all only [abs_of_pos ha, mem_closedBall, dist_zero_right, abs_of_pos hb]
        linarith
  · exact Int.cast_nonneg (hD 0)

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

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

Tactic:
pairwise_cons,

Goal state after:
case cons.refine_2
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
x✝ : (Pairwise (Sbtw R head) tail ∧ Triplewise (Sbtw R) tail) ∧ ∀ (a : P), head :: tail ≠ [a, a]
hp : Pairwise (Sbtw R head) tail
ht : Triplewise (Sbtw R) tail
ha : ∀ (a : P), head :: tail ≠ [a, a]
ht' : List.Wbtw R tail
ih : Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail ↔ ∀ (a : P), tail ≠ [a, a]
⊢ (∀ a' ∈ tail, head ≠ a') ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) tail
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 ≠ []
h : List.Wbtw R l
l' : List R
hl' : l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l
⊢ ∃ l', l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l

Tactic:
exact ⟨l', hl'⟩

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y : P
⊢ affineSegment R x y = affineSegment R y x

Tactic:
by
  refine Set.ext fun z => ?_
  constructor <;>
    · rintro ⟨t, ht, hxy⟩
      refine ⟨1 - t, ?_, ?_⟩
      · rwa [Set.sub_mem_Icc_iff_right, sub_self, sub_zero]
      · rwa [lineMap_apply_one_sub]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
h : Wbtw R x y z
f : P →ᵃ[R] P'
⊢ Wbtw R (f x) (f y) (f z)

Tactic:
rw [Wbtw, ← affineSegment_image]

Goal state after:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
h : Wbtw R x y z
f : P →ᵃ[R] P'
⊢ f y ∈ ⇑f '' affineSegment R x z
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 z : V
p : P
⊢ Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z

Tactic:
rw [Sbtw, Sbtw, wbtw_vadd_const_iff, (vadd_right_injective p).ne_iff,
    (vadd_right_injective p).ne_iff]

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
hyxz : Wbtw R ((lineMap x z) ty) x z
⊢ x = (lineMap x z) ty

Tactic:
rcases hyxz with ⟨tx, htx, hx⟩

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 : (lineMap ((lineMap x z) ty) z) tx = x
⊢ x = (lineMap x z) ty
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map g))
x : F.obj k
hx : (ConcreteCategory.hom (F.map (g ≫ f))) x ∈ F.eventualRange i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) = (ConcreteCategory.hom (F.map (g ≫ f))) x

Tactic:
map_comp,

Goal state after:
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range ⇑(ConcreteCategory.hom (F.map g))
x : F.obj k
hx : (ConcreteCategory.hom (F.map (g ≫ f))) x ∈ F.eventualRange i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) = (ConcreteCategory.hom (F.map g ≫ F.map f)) x
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case refine_1
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s
this : (ConcreteCategory.hom (F.map f₂)) x ∈ F.eventualRange j₁
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy : (ConcreteCategory.hom (F.map f₄)) y ∈ F.eventualRange j₃
h₃ : (ConcreteCategory.hom (F.map (f₄ ≫ f₃ ≫ f₂))) y = (ConcreteCategory.hom (F.map f₂)) x
⊢ (ConcreteCategory.hom (F.map ((f₄ ≫ f₃ ≫ f₂) ≫ g₁))) y ∈ s

Tactic:
map_comp,

Goal state after:
case refine_1
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s
this : (ConcreteCategory.hom (F.map f₂)) x ∈ F.eventualRange j₁
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy : (ConcreteCategory.hom (F.map f₄)) y ∈ F.eventualRange j₃
h₃ : (ConcreteCategory.hom (F.map (f₄ ≫ f₃ ≫ f₂))) y = (ConcreteCategory.hom (F.map f₂)) x
⊢ (ConcreteCategory.hom (F.map (f₄ ≫ f₃ ≫ f₂) ≫ F.map g₁)) y ∈ s