mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case inl.inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Fintype ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

pp: case inl.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Infinite ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
swap

Goal state after:
case inl.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Infinite ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

case inl.inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Fintype ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case inl.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Infinite ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
rw [det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bA), map_one,
      det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis (bS.smulTower bA))]

Goal state after:
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
⊢ IsIntegral R ((norm K) x)

pp: case neg
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
⊢ IsIntegral R ((norm K) x)

Tactic:
swap

Goal state after:
case neg
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
⊢ IsIntegral R ((norm K) x)

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
⊢ IsIntegral R ((norm K) x)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case convert_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] ↑τ, (f ∘ ↑ofComplex) z = 0

Tactic:
· contrapose! hτ
    rw [eventually_nhdsWithin_iff, ← isOpenEmbedding_coe.map_nhds_eq, eventually_map] at hτ
    rw [eventually_nhdsWithin_iff]
    filter_upwards [hτ] with a ha
    simpa using ha

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

Goal state before:
pp: case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

pp: case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
swap

Goal state after:
case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: ⊢ arsinh 0 = 0

Tactic:
by simp [arsinh]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ 0 ≤ arsinh x ↔ 0 ≤ x

Tactic:
← sinh_le_sinh,

Goal state after:
x : ℝ
⊢ sinh 0 ≤ sinh (arsinh x) ↔ 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ arsinh x ≤ 0 ↔ x ≤ 0

Tactic:
← sinh_le_sinh,

Goal state after:
x : ℝ
⊢ sinh (arsinh x) ≤ sinh 0 ↔ x ≤ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ (↑↑(if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ∘SL
        ContinuousLinearMap.restrictScalars ℝ
          (ContinuousLinearMap.toSpanSingleton ℂ (↑↑(Matrix.GeneralLinearGroup.det g) / denom g z ^ 2))).det =
    ↑(SignType.sign ↑(Matrix.GeneralLinearGroup.det g)) * ↑(Matrix.GeneralLinearGroup.det g) ^ 2 / ‖denom g z‖ ^ 4

Tactic:
rcases g.det_ne_zero.lt_or_gt with h | h

Goal state after:
case inl
g : GL (Fin 2) ℝ
z : ℂ
h : (↑g).det < 0
⊢ (↑↑(if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ∘SL
        ContinuousLinearMap.restrictScalars ℝ
          (ContinuousLinearMap.toSpanSingleton ℂ (↑↑(Matrix.GeneralLinearGroup.det g) / denom g z ^ 2))).det =
    ↑(SignType.sign ↑(Matrix.GeneralLinearGroup.det g)) * ↑(Matrix.GeneralLinearGroup.det g) ^ 2 / ‖denom g z‖ ^ 4

case inr
g : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g).det
⊢ (↑↑(if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ∘SL
        ContinuousLinearMap.restrictScalars ℝ
          (ContinuousLinearMap.toSpanSingleton ℂ (↑↑(Matrix.GeneralLinearGroup.det g) / denom g z ^ 2))).det =
    ↑(SignType.sign ↑(Matrix.GeneralLinearGroup.det g)) * ↑(Matrix.GeneralLinearGroup.det g) ^ 2 / ‖denom g z‖ ^ 4
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist z w / 2 ≤ r / 2 ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) ≤ sinh (r / 2)

Tactic:
← sinh_le_sinh,

Goal state after:
z w : ℍ
r : ℝ
⊢ sinh (dist z w / 2) ≤ sinh (r / 2) ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) ≤ sinh (r / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ sinh x < 0 ↔ x < 0

Tactic:
by simpa only [sinh_zero] using @sinh_lt_sinh x 0

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

Goal state before:
pp: α : Type u
A : Ultrafilter α
⊢ ∀ x ∈ connectedComponent A, x = A

Tactic:
intro B

Goal state after:
α : Type u
A B : Ultrafilter α
⊢ B ∈ connectedComponent A → B = A
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
⊢ g a = g b

Tactic:
have e := ultrafilter_extend_extends g

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ g a = g b
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
⊢ IsOpen[instTopologicalSpace] s ↔ IsCompact (some ⁻¹' s)ᶜ ∧ IsOpen[inst✝] (some ⁻¹' s)

Tactic:
simp [isOpen_def, h]

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∉ s
⊢ IsOpen[instTopologicalSpace] s ↔ IsOpen[inst✝] (some ⁻¹' s)

Tactic:
simp [isOpen_def, h]

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i : Set (OnePoint X)),
    ∞ ∈ i ∧ IsOpen[instTopologicalSpace] i → ∃ i', (IsClosed[inst✝] i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ i ∩ {∞}ᶜ

Tactic:
rintro s ⟨hs, hso⟩

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
hs : ∞ ∈ s
hso : IsOpen[instTopologicalSpace] s
⊢ ∃ i', (IsClosed[inst✝] i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ s ∩ {∞}ᶜ
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ proximity (f₁ * f₂) 0 ≤ proximity f₁ 0 + proximity f₂ 0

Tactic:
calc proximity (f₁ * f₂) 0
    _ ≤ (proximity f₁⁻¹ ⊤) + (proximity f₂⁻¹ ⊤) := by
      rw [← proximity_inv, mul_inv]
      apply proximity_mul_top_le h₁f₁.inv h₁f₂.inv
    _ = (proximity f₁ 0) + (proximity f₂ 0) := by
      rw [proximity_inv, proximity_inv]

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

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝¹ : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
⊢ IsCompact ((fun g ↦ g • I) ⁻¹' K)

Tactic:
have := Matrix.SpecialLinearGroup.isClosedEmbedding_val.isCompact_preimage this

Goal state after:
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
⊢ IsCompact ((fun g ↦ g • I) ⁻¹' K)
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ ∑ᶠ (z : E), ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹) ≤ ∑ᶠ (z : E), ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)

Tactic:
finsum_eq_sum_of_support_subset (s := hs.toFinset)

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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ ∑ i ∈ hs.toFinset, ↑(((toClosedBall a) D) i) * log (a * ‖i‖⁻¹) ≤
    ∑ᶠ (z : E), ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)

case h₁.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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹)) ⊆ ↑hs.toFinset
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ ∑ i ∈ hs.toFinset, ↑(((toClosedBall a) D) i) * log (a * ‖i‖⁻¹) ≤
    ∑ᶠ (z : E), ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)

pp: case h₁.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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹)) ⊆ ↑hs.toFinset

Tactic:
finsum_eq_sum_of_support_subset (s := hs.toFinset)

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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ ∑ i ∈ hs.toFinset, ↑(((toClosedBall a) D) i) * log (a * ‖i‖⁻¹) ≤
    ∑ i ∈ hs.toFinset, ↑(((toClosedBall b) D) i) * log (b * ‖i‖⁻¹)

case h₁.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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)) ⊆ ↑hs.toFinset

case h₁.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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹)) ⊆ ↑hs.toFinset
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: 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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ ∑ i ∈ hs.toFinset, ↑(((toClosedBall a) D) i) * log (a * ‖i‖⁻¹) ≤
    ∑ i ∈ hs.toFinset, ↑(((toClosedBall b) D) i) * log (b * ‖i‖⁻¹)

pp: case h₁.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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)) ⊆ ↑hs.toFinset

pp: case h₁.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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹)) ⊆ ↑hs.toFinset

Tactic:
finsum_eq_sum_of_support_subset (s := hs.toFinset)

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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ ∑ i ∈ hs.toFinset, ↑(((toClosedBall a) D) i) * log (a * ‖i‖⁻¹) ≤
    ∑ i ∈ hs.toFinset, ↑(((toClosedBall b) D) i) * log (b * ‖i‖⁻¹)

case h₁.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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)) ⊆ ↑hs.toFinset

case h₁.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
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹)) ⊆ ↑hs.toFinset
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case neg
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
tail : List P
ih :
  ∀ (hl : tail ≠ []),
    List.Wbtw R tail →
      ∃ l', (∀ a ∈ l', 0 ≤ a) ∧ l'.SortedLE ∧ map (⇑(lineMap (tail.head hl) (tail.getLast hl))) l' = tail
hl : head :: tail ≠ []
h : List.Wbtw R (head :: tail)
ht : ¬tail = []
⊢ ∃ l',
    (∀ a ∈ l', 0 ≤ a) ∧
      l'.SortedLE ∧ map (⇑(lineMap ((head :: tail).head hl) ((head :: tail).getLast hl))) l' = head :: tail

Tactic:
rw [wbtw_cons] at h
        replace ih := ih ht h.2
        rcases ih with ⟨l'', hl''0, hl''s, hl''⟩
        simp only [head_cons, getLast_cons ht]
        cases tail with
        | nil => simp at ht
        | cons head2 tail =>
          by_cases ht2 : tail = []
          · exact ⟨[0, 1], by simp [ht2, sortedLE_iff_pairwise]⟩
          · simp only [head_cons, getLast_cons ht2] at hl'' ⊢
            rw [pairwise_cons] at h
            have hw := h.1.1 _ (getLast_mem ht2)
            rcases hw with ⟨r, ⟨hr0, hr1⟩, rfl⟩
            refine ⟨0 :: l''.map fun x ↦ r + (1 - r) * x, ?_, ?_, ?_⟩
            · simp only [mem_cons, mem_map, forall_eq_or_imp, le_refl, forall_exists_index,
                and_imp, forall_apply_eq_imp_iff₂, true_and]
              intro a ha
              have := hl''0 a ha
              nlinarith
            · simp only [sortedLE_iff_pairwise, pairwise_cons, mem_map,
                forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
              refine ⟨?_, ?_⟩
              · intro a ha
                have := hl''0 a ha
                nlinarith
              · refine hl''s.pairwise.map _ fun a b hab ↦ ?_
                gcongr
            · simp only [map_cons, lineMap_apply_zero, map_map, ← hl'', cons.injEq,
                map_inj_left, Function.comp_apply, lineMap_lineMap_left, lineMap_eq_lineMap_iff,
                true_and]
              ring_nf
              simp

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

Goal state before:
pp: case pos
𝕜 : 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
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s.Nonempty
𝓕 : Set (↑s → ℝ) := {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c}
hl : IsLUB 𝓕 (s.domRestrict φ)
⊢ ∃ 𝓕',
    𝓕'.Countable ∧
      sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c

Tactic:
have hr (f) (hf : f ∈ 𝓕) : LowerSemicontinuous f := by
      obtain ⟨l, c, hlc⟩ := hf.2
      exact Continuous.lowerSemicontinuous (hlc ▸ by fun_prop)

Goal state after:
case pos
𝕜 : 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
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s.Nonempty
𝓕 : Set (↑s → ℝ) := {f | f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c}
hl : IsLUB 𝓕 (s.domRestrict φ)
hr : ∀ f ∈ 𝓕, LowerSemicontinuous f
⊢ ∃ 𝓕',
    𝓕'.Countable ∧
      sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : ∀ (j : J), T2Space ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
this : partialSections F H = ⋂ f ∈ H, {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}
f : FiniteDiagramArrow G
a✝ : f ∈ ↑H
⊢ IsClosed {u | (ConcreteCategory.hom (F.map f.snd.snd.snd.snd)) (u f.fst) = u f.snd.fst}

Tactic:
apply isClosed_eq <;> fun_prop

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

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : ↑(hallMatchingsOn t ι')
i : ↥ι'
⊢ ↥(ι'.biUnion t)

Tactic:
refine ⟨f.val i, ?_⟩

Goal state after:
ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
f : ↑(hallMatchingsOn t ι')
i : ↥ι'
⊢ ↑f i ∈ ι'.biUnion t
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) := {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c}
hl : IsLUB 𝓕 φ
⊢ ∃ 𝓕', 𝓕'.Countable ∧ sSup 𝓕' = φ ∧ ∀ f ∈ 𝓕', f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c

Tactic:
have hr (f) (hf : f ∈ 𝓕) : LowerSemicontinuous f := by
    obtain ⟨l, c, hlc⟩ := hf.2
    exact Continuous.lowerSemicontinuous (by rw [hlc]; fun_prop)

Goal state after:
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
𝓕 : Set (E → ℝ) := {f | f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c}
hl : IsLUB 𝓕 φ
hr : ∀ f ∈ 𝓕, LowerSemicontinuous f
⊢ ∃ 𝓕', 𝓕'.Countable ∧ sSup 𝓕' = φ ∧ ∀ f ∈ 𝓕', f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
i j : J
f : i ⟶ j
x✝ : (fun X ↦ X) (F.toEventualRanges.obj j)
y : F.obj i
hy : y ∈ F.eventualRange i
hx : (ConcreteCategory.hom (F.map f)) y ∈ F.eventualRange j
⊢ ∃ a, (ConcreteCategory.hom (F.toEventualRanges.map f)) a = ⟨(ConcreteCategory.hom (F.map f)) y, hx⟩

Tactic:
exact ⟨⟨y, hy⟩, rfl⟩

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✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : p ∈ line[R, t.points i₁, p₁]
h₂' : p ∈ line[R, t.points i₂, p₂]
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Sbtw R (t.points i₁) p p₁

Tactic:
have h3 : ∀ i : Fin 3, i = i₁ ∨ i = i₂ ∨ i = i₃ := by lia

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
p₁ p₂ p : P
h₁ : Sbtw R (t.points i₂) p₁ (t.points i₃)
h₂ : Sbtw R (t.points i₁) p₂ (t.points i₃)
h₁' : p ∈ line[R, t.points i₁, p₁]
h₂' : p ∈ line[R, t.points i₂, p₂]
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ Sbtw R (t.points i₁) p p₁
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
hM : M ∈ colStochastic R n
i j : n
⊢ M j i ≤ 1

Tactic:
by
  rw [← sum_col_of_mem_colStochastic hM i]
  exact single_le_sum (fun k _ => hM.1 k _) (mem_univ j)

Goal state after: