harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Cone/Extension.lean
theorem exists_extension_of_le_sublinear (f : E →ₗ.[ℝ] ℝ) (N : E → ℝ)
    (N_hom : ∀ c : ℝ, 0 < c → ∀ x, N (c • x) = c * N x) (N_add : ∀ x y, N (x + y) ≤ N x + N y)
    (hf : ∀ x : f.domain, f x ≤ N x) :
    ∃ g : E →ₗ[ℝ] ℝ, (∀ x : f.domain, g x = f x) ∧ ∀ x, g x ≤ N x

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), ↑x ∈ s → 0 ≤ ↑f' x
⊢ ∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x

Tactic:
have hf'_dense : ∀ y : E × ℝ, ∃ x : f'.domain, ↑x + y ∈ s := by
  rintro ⟨x, y⟩
  refine ⟨⟨(0, N x - y), ⟨f.domain.zero_mem, trivial⟩⟩, ?_⟩
  simp only [s, ConvexCone.mem_mk, mem_setOf_eq, Prod.fst_add, Prod.snd_add, zero_add,
    sub_add_cancel, le_rfl]

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
⊢ ∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x

Proof state:
case intro.intro.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
s : ConvexCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ x ∈ s, 0 ≤ g x
g_eq : ∀ (x : ↥f.domain) (y : ℝ), g (↑x, y) = y - ↑f x
x : E
⊢ (-g ∘ₗ inl ℝ E ℝ) x ≤ N x

Tactic:
calc -g (x, 0) = g (0, N x) - g (x, N x) := by simp [← map_sub, ← map_neg]
  _ = N x - g (x, N x) := by simpa using g_eq 0 (N x)
  _ ≤ N x := by simpa using g_nonneg ⟨x, N x⟩ (le_refl (N x))

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
lemma _root_.IsLUB.isSuccLimit_of_not_mem {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty)
    (ha : a ∉ s) : IsSuccLimit a

Proof state:
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
ha : a ∉ s
⊢ ¬IsMin a

Tactic:
obtain ⟨b, hb⟩ := hs'

Result:
case intro
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ∈ s
⊢ ¬IsMin a

Proof state:
case intro
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ∈ s
⊢ ¬IsMin a

Tactic:
obtain rfl | hb := (hs.1 hb).eq_or_lt

Result:
case intro.inl
α : Type u_1
inst✝ : LinearOrder α
s : Set α
b : α
hb : b ∈ s
hs : IsLUB s b
ha : b ∉ s
⊢ ¬IsMin b

case intro.inr
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb✝ : b ∈ s
hb : b < a
⊢ ¬IsMin a

Proof state:
case intro.inr
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb✝ : b ∈ s
hb : b < a
⊢ ¬IsMin a

Tactic:
exact hb.not_isMin

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
ha : a ∉ s
⊢ IsSuccLimit a

Tactic:
refine ⟨?_, hs.isSuccPrelimit_of_not_mem ha⟩

Result:
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
ha : a ∉ s
⊢ ¬IsMin a

Proof state:
case intro.inl
α : Type u_1
inst✝ : LinearOrder α
s : Set α
b : α
hb : b ∈ s
hs : IsLUB s b
ha : b ∉ s
⊢ ¬IsMin b

Tactic:
contradiction

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem hasMFDerivWithinAt_congr_set' (y : M) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
    HasMFDerivWithinAt I I' f s x f' ↔ HasMFDerivWithinAt I I' f t x f'

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ HasMFDerivWithinAt I I' f s x f' ↔ HasMFDerivWithinAt I I' f t x f'

Tactic:
have : T1Space M := I.t1Space M

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
⊢ HasMFDerivWithinAt I I' f s x f' ↔ HasMFDerivWithinAt I I' f t x f'
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfp_mul_eq_opow_omega0 {a b : Ordinal} (hb : 0 < b) (hba : b ≤ a ^ ω) :
    nfp (a * ·) b = a ^ ω

Proof state:
case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) 1 ≤ nfp (fun x => a * x) b

Tactic:
exact nfp_monotone (isNormal_mul_right ha).monotone (one_le_iff_pos.2 hb)

Result:
no goals

Proof state:
case inl
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ 0
ha : a = 0
⊢ nfp (fun x => 0) 0 = 0

Tactic:
exact nfp_zero_left 0

Result:
no goals

Proof state:
case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ ω ≤ nfp (fun x => a * x) b

Tactic:
rw [← nfp_mul_one ha]

Result:
case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) 1 ≤ nfp (fun x => a * x) b

Proof state:
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
⊢ nfp (fun x => a * x) b = a ^ ω

Tactic:
rcases eq_zero_or_pos a with ha | ha

Result:
case inl
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : a = 0
⊢ nfp (fun x => a * x) b = a ^ ω

case inr
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) b = a ^ ω

Proof state:
case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a * a ^ ω ≤ a ^ ω

Tactic:
rw [← opow_one_add, one_add_omega0]

Result:
no goals

Proof state:
case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) b ≤ a ^ ω

Tactic:
apply nfp_le_fp (isNormal_mul_right ha).monotone hba

Result:
case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a * a ^ ω ≤ a ^ ω

Proof state:
case inl
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ 0
ha : a = 0
⊢ nfp (fun x => 0 * x) b = 0

Tactic:
simp_rw [Ordinal.le_zero.1 hba, zero_mul]

Result:
case inl
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ 0
ha : a = 0
⊢ nfp (fun x => 0) 0 = 0

Proof state:
case inl
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : a = 0
⊢ nfp (fun x => a * x) b = a ^ ω

Tactic:
rw [ha, zero_opow omega0_ne_zero] at hba ⊢

Result:
case inl
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ 0
ha : a = 0
⊢ nfp (fun x => 0 * x) b = 0

Proof state:
case inr
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) b = a ^ ω

Tactic:
apply le_antisymm

Result:
case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x => a * x) b ≤ a ^ ω

case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ ω ≤ nfp (fun x => a * x) b
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_apply {α : Type*} {β : α → Type*} {ι : Sort*} [∀ i, SupSet (β i)] {f : ι → ∀ a, β a}
    {a : α} : (⨆ i, f i) a = ⨆ i, f i a

Proof state:
α : Type u_8
β : α → Type u_9
ι : Sort u_10
inst✝ : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ sSup (range ((fun f => f a) ∘ f)) = sSup (range fun i => f i a)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_8
β : α → Type u_9
ι : Sort u_10
inst✝ : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ (⨆ i, f i) a = ⨆ i, f i a

Tactic:
rw [iSup, sSup_apply, iSup, iSup, ← image_eq_range (fun f : ∀ i, β i => f a) (range f), ←
  range_comp]

Result:
α : Type u_8
β : α → Type u_9
ι : Sort u_10
inst✝ : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ sSup (range ((fun f => f a) ∘ f)) = sSup (range fun i => f i a)
-- Mathlib/MeasureTheory/Measure/AddContent.lean
theorem isSigmaSubadditive_of_addContent_iUnion_eq_tsum (hC : IsSetRing C)
    (m_iUnion : ∀ (f : ℕ → Set α) (_ : ∀ i, f i ∈ C) (_ : (⋃ i, f i) ∈ C)
      (_hf_disj : Pairwise (Disjoint on f)), m (⋃ i, f i) = ∑' i, m (f i)) :
    m.IsSigmaSubadditive

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⨆ i, (partialSups f) i)))

Tactic:
refine tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum hC m_iUnion
  (partialSups_monotone f) (hC.partialSups_mem hf) ?_

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ ⋃ i, (partialSups f) i ∈ C

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)

Tactic:
have h_tendsto : Tendsto (fun n ↦ m (partialSups f n)) atTop (𝓝 (m (⋃ i, f i))) := by
  rw [← iSup_eq_iUnion, ← iSup_partialSups_eq]
  refine tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum hC m_iUnion
    (partialSups_monotone f) (hC.partialSups_mem hf) ?_
  rwa [← iSup_eq_iUnion, iSup_partialSups_eq]

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
h_tendsto : Tendsto (fun n => m ((partialSups f) n)) atTop (𝓝 (m (⋃ i, f i)))
⊢ m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem J_squared : J l R * J l R = -1

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (0 * 0 + -1 * 1) (0 * -1 + -1 * 0) (1 * 0 + 0 * 1) (1 * -1 + 0 * 0) = -1

Tactic:
simp only [Matrix.zero_mul, Matrix.neg_mul, zero_add, neg_zero, Matrix.one_mul, add_zero]

Result:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (-1) 0 0 (-1) = -1

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ J l R * J l R = -1

Tactic:
rw [J, fromBlocks_multiply]

Result:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (0 * 0 + -1 * 1) (0 * -1 + -1 * 0) (1 * 0 + 0 * 1) (1 * -1 + 0 * 0) = -1

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (-1) 0 0 (-1) = -1

Tactic:
rw [← neg_zero, ← Matrix.fromBlocks_neg, ← fromBlocks_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
lemma one_mem_posTangentConeAt_iff_frequently :
    1 ∈ posTangentConeAt s a ↔ ∃ᶠ x in 𝓝[>] a, x ∈ s

Proof state:
s : Set ℝ
a : ℝ
⊢ (∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∩ Ioi a) ↔ ∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∧ x ∈ Ioi a

Tactic:
simp_rw [mem_inter_iff]

Result:
no goals

Proof state:
s : Set ℝ
a : ℝ
⊢ 1 ∈ posTangentConeAt s a ↔ ∃ᶠ (x : ℝ) in 𝓝[>] a, x ∈ s

Tactic:
rw [one_mem_posTangentConeAt_iff_mem_closure, mem_closure_iff_frequently,
  frequently_nhdsWithin_iff, inter_comm]

Result:
s : Set ℝ
a : ℝ
⊢ (∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∩ Ioi a) ↔ ∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∧ x ∈ Ioi a
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem mul_edist_le (h : LipschitzWith K f) (x y : α) :
    (K⁻¹ : ℝ≥0∞) * edist (f x) (f y) ≤ edist x y

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ edist (f x) (f y) / ↑K ≤ edist x y

Tactic:
exact ENNReal.div_le_of_le_mul' (h x y)

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ (↑K)⁻¹ * edist (f x) (f y) ≤ edist x y

Tactic:
rw [mul_comm, ← div_eq_mul_inv]

Result:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ edist (f x) (f y) / ↑K ≤ edist x y
-- Mathlib/Analysis/Calculus/Darboux.lean
theorem hasDerivWithinAt_forall_lt_or_forall_gt_of_forall_ne {s : Set ℝ} (hs : Convex ℝ s)
    (hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) {m : ℝ} (hf' : ∀ x ∈ s, f' x ≠ m) :
    (∀ x ∈ s, f' x < m) ∨ ∀ x ∈ s, m < f' x

Proof state:
case intro.intro.intro.intro.intro
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m b : ℝ
hb : b ∈ s
hmb : m ≤ f' b
a : ℝ
ha : a ∈ s
hma : f' a ≤ m
⊢ ∃ x ∈ s, f' x = m

Tactic:
exact (hs.ordConnected.image_hasDerivWithinAt hf).out (mem_image_of_mem f' ha)
  (mem_image_of_mem f' hb) ⟨hma, hmb⟩

Result:
no goals

Proof state:
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m : ℝ
hf' : ∀ x ∈ s, f' x ≠ m
⊢ (∀ x ∈ s, f' x < m) ∨ ∀ x ∈ s, m < f' x

Tactic:
contrapose! hf'

Result:
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m : ℝ
hf' : (∃ x ∈ s, m ≤ f' x) ∧ ∃ x ∈ s, f' x ≤ m
⊢ ∃ x ∈ s, f' x = m

Proof state:
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m : ℝ
hf' : (∃ x ∈ s, m ≤ f' x) ∧ ∃ x ∈ s, f' x ≤ m
⊢ ∃ x ∈ s, f' x = m

Tactic:
rcases hf' with ⟨⟨b, hb, hmb⟩, ⟨a, ha, hma⟩⟩

Result:
case intro.intro.intro.intro.intro
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m b : ℝ
hb : b ∈ s
hmb : m ≤ f' b
a : ℝ
ha : a ∈ s
hma : f' a ≤ m
⊢ ∃ x ∈ s, f' x = m
-- Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
theorem mapMono_comp (i' : Δ'' ⟶ Δ') (i : Δ' ⟶ Δ) [Mono i'] [Mono i] :
    mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Proof state:
case pos
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0

Tactic:
rw [mapMono_δ₀' K i h₃, mapMono_δ₀' K i' h₄, HomologicalComplex.d_comp_d]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_add_index [DecidableEq α] [AddZeroClass M] [CommMonoid N] {f g : α →₀ M}
    {h : α → M → N} (h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1)
    (h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂), h a (b₁ + b₂) = h a b₁ * h a b₂) :
    (f + g).prod h = f.prod h * g.prod h

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = f.prod h * g.prod h

Tactic:
rw [Finsupp.prod_of_support_subset f subset_union_left h h_zero,
  Finsupp.prod_of_support_subset g subset_union_right h h_zero, ←
  Finset.prod_mul_distrib, Finsupp.prod_of_support_subset (f + g) Finsupp.support_add h h_zero]

Result:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ ∏ x ∈ f.support ∪ g.support, h x ((f + g) x) = ∏ x ∈ f.support ∪ g.support, h x (f x) * h x (g x)

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
x : α
hx : x ∈ f.support ∪ g.support
⊢ h x ((f + g) x) = h x (f x) * h x (g x)

Tactic:
apply h_add x hx

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ ∏ x ∈ f.support ∪ g.support, h x ((f + g) x) = ∏ x ∈ f.support ∪ g.support, h x (f x) * h x (g x)

Tactic:
exact Finset.prod_congr rfl fun x hx => by apply h_add x hx

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem smul [Regular μ] {x : ℝ≥0∞} (hx : x ≠ ∞) : (x • μ).Regular

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
x : ℝ≥0∞
hx : x ≠ ⊤
⊢ (x • μ).Regular

Tactic:
haveI := OuterRegular.smul μ hx

Result:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
x : ℝ≥0∞
hx : x ≠ ⊤
this : (x • μ).OuterRegular
⊢ (x • μ).Regular

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
x : ℝ≥0∞
hx : x ≠ ⊤
this✝ : (x • μ).OuterRegular
this : IsFiniteMeasureOnCompacts (x • μ)
⊢ (x • μ).Regular

Tactic:
exact ⟨Regular.innerRegular.smul x⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
x : ℝ≥0∞
hx : x ≠ ⊤
this : (x • μ).OuterRegular
⊢ (x • μ).Regular

Tactic:
haveI := IsFiniteMeasureOnCompacts.smul μ hx

Result:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
x : ℝ≥0∞
hx : x ≠ ⊤
this✝ : (x • μ).OuterRegular
this : IsFiniteMeasureOnCompacts (x • μ)
⊢ (x • μ).Regular
-- Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean
theorem _root_.AlgHomClass.unitization_injective {F R S A : Type*} [Field R] [Ring A]
    [Algebra R A] [SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A]
    (s : S) (h1 : 1 ∉ s) [FunLike F (Unitization R s) A] [AlgHomClass F R (Unitization R s) A]
    (f : F) (hf : ∀ x : s, f x = x) : Function.Injective f

Proof state:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : Field R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
⊢ Function.Injective ⇑f

Tactic:
refine AlgHomClass.unitization_injective' s (fun r hr hr' ↦ ?_) f hf

Result:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : Field R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
hr : r ≠ 0
hr' : (algebraMap R A) r ∈ s
⊢ False

Proof state:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : Field R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
hr : r ≠ 0
hr' : (algebraMap R A) r ∈ s
⊢ False

Tactic:
rw [Algebra.algebraMap_eq_smul_one] at hr'

Result:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : Field R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
hr : r ≠ 0
hr' : r • 1 ∈ s
⊢ False

Proof state:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : Field R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
hr : r ≠ 0
hr' : r • 1 ∈ s
⊢ False

Tactic:
exact h1 <| inv_smul_smul₀ hr (1 : A) ▸ SMulMemClass.smul_mem r⁻¹ hr'

Result:
no goals
-- Mathlib/Data/Int/ConditionallyCompleteOrder.lean
theorem csSup_eq_greatest_of_bdd {s : Set ℤ} [DecidablePred (· ∈ s)] (b : ℤ) (Hb : ∀ z ∈ s, z ≤ b)
    (Hinh : ∃ z : ℤ, z ∈ s) : sSup s = greatestOfBdd b Hb Hinh

Proof state:
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ z, z ∈ s
this : s.Nonempty ∧ BddAbove s
⊢ ↑((Classical.choose ⋯).greatestOfBdd ⋯ ⋯) = ↑(b.greatestOfBdd Hb Hinh)

Tactic:
convert (coe_greatestOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddAbove s)) Hinh).symm

Result:
no goals

Proof state:
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ z, z ∈ s
this : s.Nonempty ∧ BddAbove s
⊢ sSup s = ↑(b.greatestOfBdd Hb Hinh)

Tactic:
simp only [sSup, this, and_self, dite_true]

Result:
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ z, z ∈ s
this : s.Nonempty ∧ BddAbove s
⊢ ↑((Classical.choose ⋯).greatestOfBdd ⋯ ⋯) = ↑(b.greatestOfBdd Hb Hinh)

Proof state:
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ z, z ∈ s
⊢ sSup s = ↑(b.greatestOfBdd Hb Hinh)

Tactic:
have : s.Nonempty ∧ BddAbove s := ⟨Hinh, b, Hb⟩

Result:
s : Set ℤ
inst✝ : DecidablePred fun x => x ∈ s
b : ℤ
Hb : ∀ z ∈ s, z ≤ b
Hinh : ∃ z, z ∈ s
this : s.Nonempty ∧ BddAbove s
⊢ sSup s = ↑(b.greatestOfBdd Hb Hinh)
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem ne₁₂_of_not_collinear {p₁ p₂ p₃ : P} (h : ¬Collinear k ({p₁, p₂, p₃} : Set P)) :
    p₁ ≠ p₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₃ : P
h : ¬Collinear k {p₁, p₁, p₃}
⊢ False

Tactic:
simp [collinear_pair] at h

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
h : ¬Collinear k {p₁, p₂, p₃}
⊢ p₁ ≠ p₂

Tactic:
rintro rfl

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₃ : P
h : ¬Collinear k {p₁, p₁, p₃}
⊢ False