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

Goal state before:
pp: case inr.refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
y : Y
⊢ ‖g y‖ ≤ ‖f‖ / 3

Tactic:
simpa [abs_le, neg_div] using hgf y

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 = 0
⊢ ↑g 1 1 ≠ 0

Tactic:
intro h₀

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 = 0
h₀ : ↑g 1 1 = 0
⊢ 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
g : GL (Fin 2) R
⊢ (↑g * m * (↑g)⁻¹).IsParabolic ↔ m.IsParabolic

Tactic:
by
  simp_rw [IsParabolic, discr_conj, Set.mem_range, ← Matrix.coe_units_inv,
    Units.eq_mul_inv_iff_mul_eq, scalar_apply, ← smul_eq_diagonal_mul, smul_eq_mul_diagonal,
    Units.mul_right_inj]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ 4 = 2 * 2

Tactic:
norm_num

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

Goal state before:
pp: g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : ↑g 1 0 ≠ 0
hge : 0 ≤ (↑g).discr
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = ↑√(↑g).discr * ↑√(↑g).discr
⊢ False

Tactic:
gl_smul_eq_self_iff_quadratic h,

Goal state after:
g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : ↑(↑g 1 0) * (↑z * ↑z) + (↑(↑g 1 1) - ↑(↑g 0 0)) * ↑z + -↑(↑g 0 1) = 0
hc : ↑g 1 0 ≠ 0
hge : 0 ≤ (↑g).discr
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = ↑√(↑g).discr * ↑√(↑g).discr
⊢ False
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case succ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist ((g n).compContinuous e + (F (f - (g n).compContinuous e)).compContinuous e) f ≤ (2 / 3) ^ (n + 1) * ‖f‖

Tactic:
← dist_sub_right,

Goal state after:
case succ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist ((g n).compContinuous e + (F (f - (g n).compContinuous e)).compContinuous e - ?succ.c) (f - ?succ.c) ≤
    (2 / 3) ^ (n + 1) * ‖f‖

case succ.c
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := ⋯
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ X →ᵇ ℝ
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
this : m.discr = 0 ∨ 4 = 0
⊢ 4 = 2 ^ 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
this : (↑g).trace ^ 2 = 4 * (↑g).det
⊢ 4 = 2 ^ 2

Tactic:
norm_num

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

Goal state before:
pp: z : ℂ
hz : 0 < z.im
x : ℂ
hx : 0 < x.im
⊢ (UpperHalfPlane.coe ∘ ↑ofComplex) x = id x

Tactic:
simp only [Function.comp_apply, ofComplex_apply_of_im_pos hx, id_eq]

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

Goal state before:
pp: g : SL(2, ℝ)
hc : ↑g 1 0 = 0
⊢ ∃ u v, (fun x ↦ g • x) = (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x

Tactic:
obtain ⟨a, b, ha, rfl⟩ := g.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero hc

Goal state after:
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
⊢ ∃ u v, (fun x ↦ ⟨!![a, b; 0, a⁻¹], ⋯⟩ • x) = (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case refine_1
f : ℍ → ℂ
τ : ℍ
hf : MDiffAt f τ
⊢ MDiffAt (f ∘ ↑ofComplex) ↑τ

pp: case refine_2
f : ℍ → ℂ
τ : ℍ
hf : MDiffAt (f ∘ ↑ofComplex) ↑τ
⊢ MDiffAt f τ

Tactic:
· exact (ofComplex_apply τ ▸ hf).comp _ (mdifferentiableAt_ofComplex τ.im_pos)

Goal state after:
case refine_2
f : ℍ → ℂ
τ : ℍ
hf : MDiffAt (f ∘ ↑ofComplex) ↑τ
⊢ MDiffAt f τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ dist ↑z ↑w ^ 2 / (2 ^ 2 * (z.im * w.im)) = sinh (r / 2) ^ 2 ↔ dist ↑z ↑w ^ 2 / (4 * (z.im * w.im)) = sinh (r / 2) ^ 2

Tactic:
norm_num

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

Goal state before:
pp: x : ℝ
⊢ |0| ≤ |x|

Tactic:
by simp only [_root_.abs_zero, _root_.abs_nonneg]

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

Goal state before:
pp: case refine_1
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
⊢ f ≫ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } = 𝟙 X

pp: case refine_2
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
⊢ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } ≫ f = 𝟙 Y

Tactic:
· ext x
    apply E.symm_apply_apply

Goal state after:
case refine_2
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
hE : Continuous ⇑E.symm
⊢ ofHom P { toFun := ⇑E.symm, continuous_toFun := hE } ≫ f = 𝟙 Y
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
b : Ultrafilter α
⊢ Tendsto pure (↑b) (𝓝 b)

Tactic:
Tendsto,

Goal state after:
α : Type u
b : Ultrafilter α
⊢ Filter.map pure ↑b ≤ 𝓝 b
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
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
⊢ IsClosed[instTopologicalSpaceProd] (diagonal (Quotient R))

Tactic:
have : IsOpenQuotientMap (Prod.map π π) :=
    MulAction.isOpenQuotientMap_quotientMk.prodMap MulAction.isOpenQuotientMap_quotientMk

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
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
⊢ IsClosed[instTopologicalSpaceProd] (diagonal (Quotient R))
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
h : a = ⊤
⊢ ℝ → ℝ

Tactic:
exact circleAverage (log⁺ ‖f ·‖) 0

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

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
x : ℂ
hx : x ∈ sphere 0 |r|
⊢ log⁺ ‖∑ c ∈ s, f c x‖ ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card

Tactic:
rw [add_comm]

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
x : ℂ
hx : x ∈ sphere 0 |r|
⊢ log⁺ ‖∑ c ∈ s, f c x‖ ≤ log ↑s.card + ∑ c ∈ s, log⁺ ‖f c x‖
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
ℱ : Filter X
hℱ₁ : ℱ.NeBot
hℱ₂ : ℱ ≤ 𝓟 s
hℱ₃ : ℱ ≤ 𝓝 x
⊢ x ∈ s

Tactic:
rcases exists_compact_mem_nhds x with ⟨K, hK, K_mem⟩

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
K : Set X
hK : IsCompact K
K_mem : K ∈ 𝓝 x
⊢ x ∈ s
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
e : WithTop E
x✝ : ℝ
hr : 1 ≤ x✝
⊢ 0 x✝ ≤ logCounting f e x✝

Tactic:
by simp [logCounting_nonneg hr]

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β
p' : β → β → β → Prop
⊢ Triplewise p' (map f l) ↔ Triplewise (fun a b c ↦ p' (f a) (f b) (f c)) l

Tactic:
induction l with

Goal state after:
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 s)
x✝ x : ℝ
xs : x ∈ Icc 0 s
hx : φ x = 0
this : MapsTo φ (Icc 0 s) (Icc 0 t)
⊢ 0 ∈ Icc 0 s

Tactic:
by rw [mem_Icc]; exact ⟨le_rfl, hs⟩

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
l : List α
p : α → α → α → Prop
⊢ Triplewise p l ↔ ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < l.length), p l[i] l[j] l[k]

Tactic:
induction l with

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
l : List α
p : α → α → α → Prop
⊢ Triplewise p l.reverse ↔ Triplewise (fun a b c ↦ p c b a) l

Tactic:
induction l with

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✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
l : List P
⊢ List.Wbtw R l ∧ Pairwise (fun x1 x2 ↦ x1 ≠ x2) l ↔ Triplewise (Sbtw R) l ∧ ∀ (a : P), l ≠ [a, a]

Tactic:
induction l with

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

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
l : List P
hl : l ≠ []
h : List.Wbtw R l
⊢ ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l

Tactic:
induction l with

Goal state after:
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₁
y : F.obj j₃
hy : y ∈ F.eventualRange j₃
h₃ : (ConcreteCategory.hom (F.map (f₃ ≫ f₂))) y = (ConcreteCategory.hom (F.map f₂)) x
g₂ : j₃ ⟶ i
⊢ y ∈ ⇑(ConcreteCategory.hom (F.map g₂)) ⁻¹' s

Tactic:
obtain ⟨j₄, f₄, h₄⟩ := IsCofilteredOrEmpty.cone_maps g₂ ((f₃ ≫ f₂) ≫ g₁)
      obtain ⟨y, rfl⟩ := F.mem_eventualRange_iff.1 hy f₄
      rw [← comp_apply, ← map_comp] at h₃
      rw [mem_preimage, ← comp_apply, ← map_comp, h₄, ← Category.assoc, map_comp, comp_apply, h₃,
        ← comp_apply, ← map_comp]
      apply mem_iInter.1 hx

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

Goal state before:
pp: case e_y.e_a
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✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
h' : affineSegment R (s.points i) (s.points j) = affineSegment R (s.points (min i j)) (s.points (max i j))
⊢ ({i, j}.orderEmbOfFin ⋯) 1 = max i j

Tactic:
· convert! Finset.orderEmbOfFin_last _ _
    · exact (Finset.max'_pair i j).symm
    · lia

Goal state after:
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))
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
⊢ ∃ a, (fun s ↦ ↑s i) a = x

Tactic:
obtain ⟨sec, h⟩ := nonempty_sections_of_finite_cofiltered_system (F.toPreimages s)

Goal state after:
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))
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
⊢ ∃ a, (fun s ↦ ↑s i) a = x
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f g : α ≃. β
a : α
b : β
hf : a ∈ f.symm b ↔ b ∈ f a
hg : a ∈ g.symm b ↔ b ∈ g a
⊢ (if f.symm b = g.symm b then f.symm b else none) = some a ↔ (if f a = g a then f a else none) = some b

Tactic:
simp only [Option.mem_def] at *

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f g : α ≃. β
a : α
b : β
hf : f.symm b = some a ↔ f a = some b
hg : g.symm b = some a ↔ g a = some b
⊢ (if f.symm b = g.symm b then f.symm b else none) = some a ↔ (if f a = g a then f a else none) = some b
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ τ : Perm n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring R
⊢ ((toPEquiv τ).trans (toPEquiv σ)).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ

Tactic:
PEquiv.toMatrix_trans

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ τ : Perm n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring R
⊢ (toPEquiv τ).toMatrix * (toPEquiv σ).toMatrix = Perm.permMatrix R τ * Perm.permMatrix R σ
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
⊢ ¬f i = g i → ∃ x x_1, ¬(if x_1 ∈ f x then 1 else 0) = if x_1 ∈ g x then 1 else 0

Tactic:
hi

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
f g : m ≃. n
i : m
hi : ¬f i = g i
⊢ ∃ x x_1, ¬(if x_1 ∈ f x then 1 else 0) = if x_1 ∈ g x then 1 else 0
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case e'_11
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✝³ : AffineSpace V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
h' : Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))
⊢ ({i, j}.orderEmbOfFin ⋯) 1 = max i j

Tactic:
· convert! Finset.orderEmbOfFin_last _ _
    · exact (Finset.max'_pair i j).symm
    · lia

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

Goal state before:
pp: V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NormedSpace ℝ V
K L : ConvexBody V
⊢ Metric.hausdorffEDist ↑K ↑L = edist K L

Tactic:
edist_dist

Goal state after:
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NormedSpace ℝ V
K L : ConvexBody V
⊢ Metric.hausdorffEDist ↑K ↑L = ENNReal.ofReal (dist K L)
Module: Mathlib.Geometry.Convex.Cone.TensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module R G
H : Type u_3
inst✝¹ : AddCommGroup H
inst✝ : Module R H
C₁ : PointedCone R G
C₂ : PointedCone R H
⊢ map (↑(TensorProduct.comm R G H)) (C₁.maxTensorProduct C₂) = C₂.maxTensorProduct C₁

Tactic:
ext z

Goal state after:
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
z : H ⊗[R] G
⊢ z ∈ map (↑(TensorProduct.comm R G H)) (C₁.maxTensorProduct C₂) ↔ z ∈ C₂.maxTensorProduct C₁
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
⊢ 2⁻¹ ≤ 1

Tactic:
norm_num

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hc : Convex ℝ s
hne : (interior s).Nonempty
hb : Bornology.IsBounded s
⊢ ∃ h,
    ⇑h '' interior s = ball 0 1 ∧
      ⇑h '' closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s = closedBall 0 1 ∧
        ⇑h '' frontier s = sphere 0 1

Tactic:
simpa [isOpen_ball.interior_eq, closure_ball, frontier_ball]
    using exists_homeomorph_image_eq hc hne (NormedSpace.isVonNBounded_of_isBounded _ hb)
    (convex_ball 0 1) (by simp [isOpen_ball.interior_eq]) (NormedSpace.isVonNBounded_ball _ _ _)

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

Goal state before:
pp: case funProp.discharger
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x₀) f
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun x1 x2 ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
⊢ 1 - 0 ≠ 0

Tactic:
norm_num

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t₁ t₂ : Set E
⊢ convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂

Tactic:
convexJoin_comm s,

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t₁ t₂ : Set E
⊢ convexJoin 𝕜 (t₁ ∪ t₂) s = convexJoin 𝕜 t₁ s ∪ convexJoin 𝕜 t₂ s
Module: Mathlib.Analysis.Convex.Join

Goal state before:
pp: ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
t : ι → Set E
⊢ convexJoin 𝕜 s (⋃ i, t i) = ⋃ i, convexJoin 𝕜 s (t i)

Tactic:
convexJoin_comm s,

Goal state after:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
t : ι → Set E
⊢ convexJoin 𝕜 (⋃ i, t i) s = ⋃ i, convexJoin 𝕜 (t i) s
Module: Mathlib.Analysis.Convex.Join

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

Tactic:
convexJoin_comm s,

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 t u) s ⊆ convexJoin 𝕜 (convexJoin 𝕜 t s) u
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : I → Type u_9
s : StdSimplex R I
f : (i : I) → StdSimplex R (J i)
g : (i : I) → J i → M
⊢ sConvexComb (map (fun i ↦ sConvexComb (map (g i) (f i))) s) =
    sConvexComb (map (Sigma.uncurry g) (sConvexComb (map (fun i ↦ map (fun x ↦ ⟨i, x⟩) (f i)) s)))

Tactic:
rw [← map_map, ← sConvexComb_sConvexComb]

Goal state after:
R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : I → Type u_9
s : StdSimplex R I
f : (i : I) → StdSimplex R (J i)
g : (i : I) → J i → M
⊢ sConvexComb (sConvexComb (map (fun i ↦ map (g i) (f i)) s)) =
    sConvexComb (map (Sigma.uncurry g) (sConvexComb (map (fun i ↦ map (fun x ↦ ⟨i, x⟩) (f i)) s)))
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : I → J → M
⊢ sConvexComb (map (fun i ↦ sConvexComb (map (g i) (f i))) s) =
    sConvexComb (map (Function.uncurry g) (sConvexComb (map (fun i ↦ map (fun x ↦ (i, x)) (f i)) s)))

Tactic:
rw [← map_map, ← sConvexComb_sConvexComb]

Goal state after:
R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : Type u_9
s : StdSimplex R I
f : I → StdSimplex R J
g : I → J → M
⊢ sConvexComb (sConvexComb (map (fun i ↦ map (g i) (f i)) s)) =
    sConvexComb (map (Function.uncurry g) (sConvexComb (map (fun i ↦ map (fun x ↦ (i, x)) (f i)) s)))