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

Goal state before:
pp: g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
⊢ g • z = z ↔ z = fixedPt g hell

Tactic:
rw [gl_smul_eq_self_iff_quadratic hpos, quadratic_eq_zero_iff (mod_cast hell.c_ne_zero)
    (hd.trans (pow_two _))]

Goal state after:
g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
⊢ ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) + Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0)) ∨
      ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0)) ↔
    z = fixedPt g hell
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
e : X → Y
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hg : ‖g‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ }‖
⊢ ∃ g_1,
    ‖g_1‖ = ‖g.compContinuous { toFun := e, continuous_toFun := ⋯ }‖ ∧
      ⇑g_1 ∘ e = ⇑(g.compContinuous { toFun := e, continuous_toFun := ⋯ })

Tactic:
exact ⟨g, hg, rfl⟩

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

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
⊢ 0 ∉ {0}ᶜ ∨ 0 ≤ k

Tactic:
by tauto

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

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ (x -ᵥ c) +ᵥ c = x

pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ dist x c ≠ 0

Tactic:
vsub_vadd

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ x = x

case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ dist x c ≠ 0
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr
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
hne : x ≠ c
⊢ (x -ᵥ c) +ᵥ c = x

pp: case inr
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
hne : x ≠ c
⊢ R ^ 2 ≠ 0

Tactic:
vsub_vadd

Goal state after:
case inr
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
hne : x ≠ c
⊢ x = x

case inr
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
hne : x ≠ c
⊢ R ^ 2 ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a b c : ℍ
⊢ dist ↑a ↑c * dist (↑b) ((starRingEnd ℂ) ↑b) / (2 * √(a.im * c.im)) ≤
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * √(a.im * c.im))

Tactic:
gcongr

Goal state after:
case hab
a b c : ℍ
⊢ dist ↑a ↑c * dist (↑b) ((starRingEnd ℂ) ↑b) ≤
    dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case refine_2
x : ℝ
hx : 0 < x
⊢ 0 < cosh x - (fun x ↦ 1) x

pp: case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

pp: case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x ↦ x) x

Tactic:
sub_pos,

Goal state after:
case refine_2
x : ℝ
hx : 0 < x
⊢ (fun x ↦ 1) x < cosh x

case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x ↦ x) x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ 2 * arsinh (dist { re := 0, im := z.im } { re := 0, im := w.im } / (2 * √(z.im * w.im))) ≤
    2 * arsinh (dist ↑z ↑w / (2 * √(z.im * w.im)))

Tactic:
gcongr

Goal state after:
case hab
z w : ℍ
⊢ dist { re := 0, im := z.im } { re := 0, im := w.im } ≤ dist ↑z ↑w
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ w.im * Real.sinh (dist z w) + w.im * (Real.cosh (dist z w) - 1) = w.im * (rexp (dist z w) - 1)

Tactic:
← mul_add,

Goal state after:
z w : ℍ
⊢ w.im * (Real.sinh (dist z w) + (Real.cosh (dist z w) - 1)) = w.im * (rexp (dist z w) - 1)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ (𝓝 ∞).HasBasis (fun s ↦ IsClosed[inst✝] s ∧ IsCompact s) fun s ↦ some '' sᶜ ∪ {∞}

Tactic:
by
  rw [nhds_infty_eq]
  exact (hasBasis_coclosedCompact.map _).sup_pure _

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

Goal state before:
pp: case coe
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
s : Set (OnePoint X)
inst✝ : T1Space X
x✝ : X
⊢ IsClosed[inst✝¹] {x✝} ∧ IsCompact {x✝}

Tactic:
exact ⟨isClosed_singleton, isCompact_singleton⟩

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

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⋯
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ ∀ᶠ (x : ℕ) in atTop, (ULift.up ∘ OnePoint.some) x ∈ g ⁻¹' s

pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⋯
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ IsClosed (g ⁻¹' s)

Tactic:
· simp only [Function.comp_apply, mem_preimage, eventually_atTop]
    exact ⟨0, fun b _ ↦ hu b⟩

Goal state after:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⋯
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ IsClosed (g ⁻¹' s)
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✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x : OnePoint X
x✝¹ : x ∈ univ
y : OnePoint X
x✝ : y ∈ univ
hxy : x ≠ y
⊢ (fun x y ↦
      ∃ u v,
        IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v)
    x y

Tactic:
cases x with
    | infty =>
      refine ⟨{y}ᶜ, {y}, isOpen_compl_singleton, ?_, hxy, rfl, (compl_union_self _).symm.subset,
        disjoint_compl_left⟩
      rw [OnePoint.isOpen_iff_of_notMem]
      exacts [isOpen_discrete _, hxy]
    | coe val =>
      refine ⟨{some val}, {some val}ᶜ, ?_, isOpen_compl_singleton, rfl, hxy.symm, by simp,
        disjoint_compl_right⟩
      rw [OnePoint.isOpen_iff_of_notMem]
      exacts [isOpen_discrete _, (Option.some_ne_none val).symm]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscrete ℂ] g
hr : r ≠ 0
⊢ sphere 0 |r| ⊆ univ

Tactic:
by tauto

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

Goal state before:
pp: case hf₁
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r

pp: case hf₂
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r

pp: case h
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ ∀ x ∈ sphere 0 |r|, log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖

Tactic:
· simp_rw [← norm_mul]
        apply MeromorphicOn.circleIntegrable_posLog_norm
        apply Meromorphic.meromorphicOn
        fun_prop

Goal state after:
case hf₂
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r

case h
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ ∀ x ∈ sphere 0 |r|, log⁺ (‖f₁ x‖ * ‖f₂ x‖) ≤ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ closedBall 0 |R| ⊆ Set.univ

Tactic:
by tauto

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ proximity (∑ a ∈ s, f a) ⊤ r + logCounting (∑ a ∈ s, f a) ⊤ r ≤
    (∑ a ∈ s, proximity (f a) ⊤) r + log ↑s.card + (∑ a ∈ s, logCounting (f a) ⊤) r

Tactic:
gcongr

Goal state after:
case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ proximity (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, proximity (f a) ⊤) r + log ↑s.card

case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ logCounting (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
hab : a ≤ b
⊢ circleAverage (fun x ↦ logCounting f (↑x) a) 0 1 +
      circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 ≤
    circleAverage (fun x ↦ logCounting f (↑x) b) 0 1 +
      circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

Tactic:
gcongr

Goal state after:
case hf₁
f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
hab : a ≤ b
⊢ CircleIntegrable (fun x ↦ logCounting f (↑x) a) 0 1

case hf₂
f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
hab : a ≤ b
⊢ CircleIntegrable (fun x ↦ logCounting f (↑x) b) 0 1

case h
f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
hab : a ≤ b
x✝ : ℂ
a✝ : x✝ ∈ sphere 0 |1|
⊢ logCounting f (↑x✝) a ≤ logCounting f (↑x✝) b
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
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
⊢ ∑ᶠ (z : E), ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹) + ↑(D 0) * log a ≤
    ∑ᶠ (z : E), ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹) + ↑(D 0) * log b

Tactic:
gcongr

Goal state after:
case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
⊢ ∑ᶠ (z : E), ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹) ≤ ∑ᶠ (z : E), ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)

case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
⊢ 0 ≤ ↑(D 0)
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 (single e 1) ℓ| ≤ a * |logCounting D ℓ|

Tactic:
gcongr

Goal state after:
case ha
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 ≤ ℓ
⊢ 0 ≤ logCounting (single e 1) ℓ

case hab
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 (single e 1) ℓ ≤ logCounting D ℓ
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
z : E
hz : z ∈ hs.toFinset
h₂z : ¬z = 0
this : z ∈ closedBall 0 |b|
h₃z : z ∈ closedBall 0 |a|
⊢ ↑(D z) * log (a * ‖z‖⁻¹) ≤ ↑(D z) * log (b * ‖z‖⁻¹)

Tactic:
gcongr

Goal state after:
case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
s : Set E := ⋯
hs : s.Finite
z : E
hz : z ∈ hs.toFinset
h₂z : ¬z = 0
this : z ∈ closedBall 0 |b|
h₃z : z ∈ closedBall 0 |a|
⊢ 0 ≤ ↑(D z)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : ‖e‖ < a
b : ℝ
hb : ‖e‖ < b
hab : a < b
⊢ ↑1 * (log a - log ‖e‖) < ↑1 * (log b - log ‖e‖)

Tactic:
gcongr

Goal state after:
case hx
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
e : E
hD : single e 1 ≤ D
a : ℝ
ha : ‖e‖ < a
b : ℝ
hb : ‖e‖ < b
hab : a < b
⊢ 0 < a
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp.inl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
ws : w ∈ s
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y

pp: case mp.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
wt : w ∈ t
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y

Tactic:
exacts [Or.inl ⟨ws, zw, hs.2 ws⟩, Or.inr ⟨wt, ht.2 wt, wy⟩]

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

Goal state before:
pp: α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this : DecidableEq ι
⊢ Disjoint s (image (fun z ↦ ↑z) s')

Tactic:
simp only [disjoint_left, not_exists, mem_image, SetCoe.exists, exists_and_right,
      exists_eq_right]

Goal state after:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this : DecidableEq ι
⊢ ∀ ⦃a : ι⦄, a ∈ s → ∀ (x : a ∈ (↑s)ᶜ), ⟨a, ⋯⟩ ∉ s'
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z ↦ ↑z) s')
this : #s' = #(s ∪ image (fun z ↦ ↑z) s') - #s
⊢ #((s ∪ image (fun z ↦ ↑z) s').biUnion t \ s.biUnion t) ≤ #(s'.biUnion fun x' ↦ t ↑x' \ s.biUnion t)

Tactic:
gcongr

Goal state after:
case a
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z ↦ ↑z) s')
this : #s' = #(s ∪ image (fun z ↦ ↑z) s') - #s
⊢ (s ∪ image (fun z ↦ ↑z) s').biUnion t \ s.biUnion t ⊆ s'.biUnion fun x' ↦ t ↑x' \ s.biUnion t
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case neg.refine_2.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
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
a b : R
hab : a ≤ b
⊢ r + (1 - r) * a ≤ r + (1 - r) * b

Tactic:
gcongr

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
s : AffineSubspace R P
x z : P
hx : x ∈ s
hz : z ∈ s
ε : R
⊢ (lineMap x z) ε ∈ s

Tactic:
exact lineMap_mem _ hx hz

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

Goal state before:

Tactic:
_ = sSup ((fun g => g ∘ (Equiv.Set.univ E).symm) '' 𝓕) := by
    congr
    ext f
    refine ⟨fun ⟨hp, l, c, hlc⟩ => ⟨f ∘ Subtype.val, ⟨fun x => hp (Subtype.val x), ⟨l, c, ?_⟩⟩, ?_⟩,
      fun ⟨a, ⟨⟨h, ⟨l, c, hlc⟩⟩, hb⟩⟩ => ⟨fun x => ?_, ⟨l, c, ?_⟩⟩⟩
    · ext x; simpa using! congrFun hlc x
    · ext; simp
    · simpa using! hb ▸ h ⟨x, trivial⟩
    · subst hlc; simpa using! hb.symm
  _ = sSup 𝓕 ∘ (Equiv.Set.univ E).symm := by ext x; rw [sSup_image', sSup_eq_iSup']; simp
  _ = φ ∘ Subtype.val ∘ (Equiv.Set.univ E).symm :=
    congrArg (fun g => g ∘ (Equiv.Set.univ E).symm) this
  _ = φ := by ext; simp

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

Goal state before:
pp: case e'_3
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : 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))
⊢ min i j = {i, j}.min' ⋯

Tactic:
exact (Finset.min'_pair i j).symm

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case inr
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
j : J
ji : j ⟶ i
x : F.obj j
ys : (ConcreteCategory.hom (F.map ji)) x ∈ s
⊢ ∃ x, ∀ (i_1 : j ⟶ i), (ConcreteCategory.hom (F.map i_1)) x ∈ s

Tactic:
exact ⟨x, fun ji' => (F.thin_diagram_of_surjective Fsur ji' ji).symm ▸ ys⟩

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : b ∈ f a
hf : b ∈ g a
⊢ b ∈
    { toFun := fun a ↦ if g a = h a then g a else none,
        invFun := fun b ↦ if g.symm b = h.symm b then g.symm b else none, inv := ⋯ }
      a

Tactic:
have hg := gh a b H

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : b ∈ f a
hf : b ∈ g a
hg : b ∈ h a
⊢ b ∈
    { toFun := fun a ↦ if g a = h a then g a else none,
        invFun := fun b ↦ if g.symm b = h.symm b then g.symm b else none, inv := ⋯ }
      a
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case e'_3
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : 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))
⊢ min i j = {i, j}.min' ⋯

Tactic:
exact (Finset.min'_pair i j).symm

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R✝ : Type u_1
n✝ : Type u_2
inst✝⁹ : Fintype n✝
inst✝⁸ : DecidableEq n✝
inst✝⁷ : Semiring R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : IsOrderedRing R✝
M✝ : Matrix n✝ n✝ R✝
x : n✝ → R✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1}
⊢ M * N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1}

Tactic:
refine ⟨fun i j => sum_nonneg fun i _ => mul_nonneg (hM.1 _ _) (hN.1 _ _), ?_⟩

Goal state after:
R✝ : Type u_1
n✝ : Type u_2
inst✝⁹ : Fintype n✝
inst✝⁸ : DecidableEq n✝
inst✝⁷ : Semiring R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : IsOrderedRing R✝
M✝ : Matrix n✝ n✝ R✝
x : n✝ → R✝
R : Type u_3
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M N : Matrix n n R
hM : M ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1}
hN : N ∈ {M | (∀ (i j : n), 0 ≤ M i j) ∧ M *ᵥ 1 = 1}
⊢ (M * N) *ᵥ 1 = 1
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : M ∈ rowStochastic R n
hx : x ⬝ᵥ 1 = 1
⊢ x ᵥ* M ⬝ᵥ 1 = 1

Tactic:
← dotProduct_mulVec,

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : M ∈ rowStochastic R n
hx : x ⬝ᵥ 1 = 1
⊢ x ⬝ᵥ M *ᵥ 1 = 1