harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/AbelRuffini.lean
theorem induction2 {α β γ : solvableByRad F E} (hγ : γ ∈ F⟮α, β⟯) (hα : P α) (hβ : P β) : P γ

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
x : ↥(solvableByRad F E)
hx : x ∈ {α, β}
⊢ IsIntegral F x ∧ Splits (algebraMap F (p * q).SplittingField) (minpoly F x)

Tactic:
simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hx

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
x : ↥(solvableByRad F E)
hx : x = α ∨ x = β
⊢ IsIntegral F x ∧ Splits (algebraMap F (p * q).SplittingField) (minpoly F x)

Proof state:
case inl
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
x : ↥(solvableByRad F E)
hx : x = α
⊢ IsIntegral F α ∧ Splits (algebraMap F (p * q).SplittingField) (minpoly F α)

Tactic:
exact ⟨isIntegral α, hpq.1⟩

Result:
no goals

Proof state:
case a.a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
f : ↥F⟮α, β⟯ →ₐ[F] (p * q).SplittingField := Classical.choice ⋯
⊢ (aeval ↑⟨γ, hγ⟩) (minpoly F γ) = ↑0

Tactic:
simp

Result:
no goals

Proof state:
case inr
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α β γ : ↥(solvableByRad F E)
hγ : γ ∈ F⟮α, β⟯
hα : P α
hβ : P β
p : F[X] := minpoly F α
q : F[X] := minpoly F β
hpq :
  Splits (algebraMap F (p * q).SplittingField) (minpoly F α) ∧
    Splits (algebraMap F (p * q).SplittingField) (minpoly F β)
x : ↥(solvableByRad F E)
hx : x = β
⊢ IsIntegral F β ∧ Splits (algebraMap F (p * q).SplittingField) (minpoly F β)

Tactic:
exact ⟨isIntegral β, hpq.2⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
@[reassoc (attr := simp), elementwise nosimp]
lemma appLE_appIso_inv {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] {U : Y.Opens}
    {V : X.Opens} (e : V ≤ f ⁻¹ᵁ U) :
    f.appLE U V e ≫ (f.appIso V).inv =
        Y.presheaf.map (homOfLE <| (f.image_le_image_of_le e).trans
          (f.image_preimage_eq_opensRange_inter U ▸ inf_le_right)).op

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Y.presheaf.map (homOfLE ⋯).op ≫ Y.presheaf.map (homOfLE ⋯).op = Y.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← Functor.map_comp]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Y.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = Y.presheaf.map (homOfLE ⋯).op

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ appLE f U V e ≫ (appIso f V).inv = Y.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [appLE, Category.assoc, appIso_inv_naturality, Functor.op_obj, Functor.op_map,
  Quiver.Hom.unop_op, opensFunctor_map_homOfLE, app_appIso_inv_assoc, Opens.carrier_eq_coe]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Y.presheaf.map (homOfLE ⋯).op ≫ Y.presheaf.map (homOfLE ⋯).op = Y.presheaf.map (homOfLE ⋯).op

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Y.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = Y.presheaf.map (homOfLE ⋯).op

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem le_nth_of_lt_nth_succ {k a : ℕ} (h : a < nth p (k + 1)) (ha : p a) : a ≤ nth p k

Proof state:
case inl
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (setOf p).Finite
⊢ a ≤ nth p k

Tactic:
rcases exists_lt_card_finite_nth_eq hf ha with ⟨n, hn, rfl⟩

Result:
case inl.intro.intro
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
⊢ nth p n ≤ nth p k

Proof state:
case inr.intro
p : ℕ → Prop
k : ℕ
hf : (setOf p).Infinite
n : ℕ
h : nth p n < nth p (k + 1)
ha : p (nth p n)
⊢ nth p n ≤ nth p k

Tactic:
rwa [nth_lt_nth hf, Nat.lt_succ_iff, ← nth_le_nth hf] at h

Result:
no goals

Proof state:
case inr
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (setOf p).Infinite
⊢ a ≤ nth p k

Tactic:
rcases subset_range_nth ha with ⟨n, rfl⟩

Result:
case inr.intro
p : ℕ → Prop
k : ℕ
hf : (setOf p).Infinite
n : ℕ
h : nth p n < nth p (k + 1)
ha : p (nth p n)
⊢ nth p n ≤ nth p k

Proof state:
case inl.intro.intro.inr
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k

Tactic:
rw [nth_of_card_le _ hk] at h

Result:
case inl.intro.intro.inr
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < 0
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k

Proof state:
case inl.intro.intro
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
⊢ nth p n ≤ nth p k

Tactic:
rcases lt_or_le (k + 1) #hf.toFinset with hk | hk

Result:
case inl.intro.intro.inl
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : k + 1 < #hf.toFinset
⊢ nth p n ≤ nth p k

case inl.intro.intro.inr
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k

Proof state:
case inl.intro.intro.inl
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < nth p (k + 1)
ha : p (nth p n)
hk : k + 1 < #hf.toFinset
⊢ nth p n ≤ nth p k

Tactic:
rwa [(nth_strictMonoOn hf).lt_iff_lt hn hk, Nat.lt_succ_iff,
  ← (nth_strictMonoOn hf).le_iff_le hn (k.lt_succ_self.trans hk)] at h

Result:
no goals

Proof state:
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
⊢ a ≤ nth p k

Tactic:
rcases (setOf p).finite_or_infinite with hf | hf

Result:
case inl
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (setOf p).Finite
⊢ a ≤ nth p k

case inr
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (setOf p).Infinite
⊢ a ≤ nth p k

Proof state:
case inl.intro.intro.inr
p : ℕ → Prop
k : ℕ
hf : (setOf p).Finite
n : ℕ
hn : n < #hf.toFinset
h : nth p n < 0
ha : p (nth p n)
hk : #hf.toFinset ≤ k + 1
⊢ nth p n ≤ nth p k

Tactic:
exact absurd h (zero_le _).not_lt

Result:
no goals
-- Mathlib/Order/Filter/Extr.lean
theorem sup_eq_of_max [Nonempty α] {b : β} (hb : b ∈ Set.range D) (hmem : D.invFun b ∈ s)
    (hmax : ∀ a ∈ s, D a ≤ b) : s.sup D = b

Proof state:
case intro
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
⊢ s.sup D = D a

Tactic:
rw [← Function.apply_invFun_apply (f := D)]

Result:
case intro
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
⊢ s.sup D = D (Function.invFun D (D a))

Proof state:
case intro
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
⊢ s.sup D = D (Function.invFun D (D a))

Tactic:
apply sup_eq_of_isMaxOn hmem

Result:
case intro
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
⊢ IsMaxOn D (↑s) (Function.invFun D (D a))

Proof state:
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
b : β
hb : b ∈ range D
hmem : Function.invFun D b ∈ s
hmax : ∀ a ∈ s, D a ≤ b
⊢ s.sup D = b

Tactic:
obtain ⟨a, rfl⟩ := hb

Result:
case intro
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
⊢ s.sup D = D a

Proof state:
case intro
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
a✝ : α
⊢ a✝ ∈ ↑s → a✝ ∈ {x | (fun x => D x ≤ D (Function.invFun D (D a))) x}

Tactic:
rw [Function.apply_invFun_apply (f := D)]

Result:
case intro
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
a✝ : α
⊢ a✝ ∈ ↑s → a✝ ∈ {x | (fun x => D x ≤ D a) x}

Proof state:
case intro
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
a✝ : α
⊢ a✝ ∈ ↑s → a✝ ∈ {x | (fun x => D x ≤ D a) x}

Tactic:
apply hmax

Result:
no goals

Proof state:
case intro
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
⊢ IsMaxOn D (↑s) (Function.invFun D (D a))

Tactic:
intro

Result:
case intro
α : Type u
β : Type v
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
D : α → β
s : Finset α
inst✝ : Nonempty α
a : α
hmem : Function.invFun D (D a) ∈ s
hmax : ∀ a_1 ∈ s, D a_1 ≤ D a
a✝ : α
⊢ a✝ ∈ ↑s → a✝ ∈ {x | (fun x => D x ≤ D (Function.invFun D (D a))) x}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem contains_replicate [BEq α] {n : Nat} {a b : α} :
    (replicate n b).contains a = (a == b && !n == 0)

Proof state:
case zero
α : Type u_1
inst✝ : BEq α
a b : α
⊢ (replicate 0 b).contains a = (a == b && !0 == 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
ih : (replicate n b).contains a = (a == b && !n == 0)
⊢ (replicate (n + 1) b).contains a = (a == b && !n + 1 == 0)

Tactic:
simp only [replicate_succ, elem_cons]

Result:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
ih : (replicate n b).contains a = (a == b && !n == 0)
⊢ (match a == b with
    | true => true
    | false => elem a (replicate n b)) =
    (a == b && !n + 1 == 0)

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
ih : (replicate n b).contains a = (a == b && !n == 0)
⊢ (match a == b with
    | true => true
    | false => elem a (replicate n b)) =
    (a == b && !n + 1 == 0)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
n : Nat
a b : α
⊢ (replicate n b).contains a = (a == b && !n == 0)

Tactic:
induction n with
| zero => simp
| succ n ih =>
  simp only [replicate_succ, elem_cons]
  split <;> simp_all

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem ack_strict_mono_left' : ∀ {m₁ m₂} (n), m₁ < m₂ → ack m₁ n < ack m₂ n
  | m, 0, _ => fun h => (not_lt_zero m h).elim
  | 0, m + 1, 0 => fun _h => by simpa using one_lt_ack_succ_right m 0
  | 0, m + 1, n + 1 => fun h => by
    rw [ack_zero, ack_succ_succ]
    apply lt_of_le_of_lt (le_trans _ <| add_le_add_left (add_add_one_le_ack _ _) m) (add_lt_ack _ _)
    omega
  | m₁ + 1, m₂ + 1, 0 => fun h => by
    simpa using ack_strict_mono_left' 1 ((add_lt_add_iff_right 1).1 h)
  | m₁ + 1, m₂ + 1, n + 1 => fun h => by
    rw [ack_succ_succ, ack_succ_succ]
    exact
      (ack_strict_mono_left' _ <| (add_lt_add_iff_right 1).1 h).trans
        (ack_strictMono_right _ <| ack_strict_mono_left' n h)

Proof state:
m n : ℕ
h : 0 < m + 1
⊢ ack 0 (n + 1) < ack (m + 1) (n + 1)

Tactic:
rw [ack_zero, ack_succ_succ]

Result:
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 < ack m (ack (m + 1) n)

Proof state:
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack (m₁ + 1) (n + 1) < ack (m₂ + 1) (n + 1)

Tactic:
rw [ack_succ_succ, ack_succ_succ]

Result:
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)

Proof state:
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 < ack m (ack (m + 1) n)

Tactic:
apply lt_of_le_of_lt (le_trans _ <| add_le_add_left (add_add_one_le_ack _ _) m) (add_lt_ack _ _)

Result:
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 ≤ m + (m + 1 + n + 1)

Proof state:
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 ≤ m + (m + 1 + n + 1)

Tactic:
omega

Result:
no goals

Proof state:
m₁ m₂ : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack (m₁ + 1) 0 < ack (m₂ + 1) 0

Tactic:
simpa using ack_strict_mono_left' 1 ((add_lt_add_iff_right 1).1 h)

Result:
no goals

Proof state:
m : ℕ
_h : 0 < m + 1
⊢ ack 0 0 < ack (m + 1) 0

Tactic:
simpa using one_lt_ack_succ_right m 0

Result:
no goals

Proof state:
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)

Tactic:
exact
  (ack_strict_mono_left' _ <| (add_lt_add_iff_right 1).1 h).trans
    (ack_strictMono_right _ <| ack_strict_mono_left' n h)

Result:
no goals
-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean
theorem approximates_deriv_on_open_nhds (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    ∃ s : Set E, a ∈ s ∧ IsOpen s ∧
      ApproximatesLinearOn f (f' : E →L[𝕜] F) s (‖(f'.symm : F →L[𝕜] E)‖₊⁻¹ / 2)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s, a ∈ s ∧ IsOpen s ∧ ApproximatesLinearOn f (↑f') s (‖↑f'.symm‖₊⁻¹ / 2)

Tactic:
simp only [← and_assoc]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s, (a ∈ s ∧ IsOpen s) ∧ ApproximatesLinearOn f (↑f') s (‖↑f'.symm‖₊⁻¹ / 2)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f (↑f') s (‖↑f'.symm‖₊⁻¹ / 2)

Tactic:
exact
  hf.approximates_deriv_on_nhds <|
    f'.subsingleton_or_nnnorm_symm_pos.imp id fun hf' => half_pos <| inv_pos.2 hf'

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s, (a ∈ s ∧ IsOpen s) ∧ ApproximatesLinearOn f (↑f') s (‖↑f'.symm‖₊⁻¹ / 2)

Tactic:
refine ((nhds_basis_opens a).exists_iff fun s t => ApproximatesLinearOn.mono_set).1 ?_

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
a : E
hf : HasStrictFDerivAt f (↑f') a
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f (↑f') s (‖↑f'.symm‖₊⁻¹ / 2)
-- Mathlib/Topology/Compactness/Compact.lean
lemma IsCompact.elim_nhds_subcover_nhdsSet' (hs : IsCompact s) (U : ∀ x ∈ s, Set X)
    (hU : ∀ x hx, U x hx ∈ 𝓝 x) : ∃ t : Finset s, (⋃ x ∈ t, U x.1 x.2) ∈ 𝓝ˢ s

Proof state:
case intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset ↑s
hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)
⊢ ∃ t, ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝ˢ s

Tactic:
refine ⟨t, mem_nhdsSet_iff_forall.2 fun x hx ↦ ?_⟩

Result:
case intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset ↑s
hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)
x : X
hx : x ∈ s
⊢ ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝 x

Proof state:
case intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset ↑s
hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)
x : X
hx : x ∈ s
y : ↑s
hyt : y ∈ t
hy : x ∈ interior (U ↑y ⋯)
⊢ ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝 x

Tactic:
refine mem_of_superset ?_ (subset_biUnion_of_mem hyt)

Result:
case intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset ↑s
hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)
x : X
hx : x ∈ s
y : ↑s
hyt : y ∈ t
hy : x ∈ interior (U ↑y ⋯)
⊢ U ↑y ⋯ ∈ 𝓝 x

Proof state:
case intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset ↑s
hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)
x : X
hx : x ∈ s
y : ↑s
hyt : y ∈ t
hy : x ∈ interior (U ↑y ⋯)
⊢ U ↑y ⋯ ∈ 𝓝 x

Tactic:
exact mem_interior_iff_mem_nhds.1 hy

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
⊢ ∃ t, ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝ˢ s

Tactic:
rcases hs.elim_finite_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior)
  fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩ with ⟨t, hst⟩

Result:
case intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset ↑s
hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)
⊢ ∃ t, ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝ˢ s

Proof state:
case intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset ↑s
hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)
x : X
hx : x ∈ s
⊢ ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝 x

Tactic:
rcases mem_iUnion₂.1 (hst hx) with ⟨y, hyt, hy⟩

Result:
case intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset ↑s
hst : s ⊆ ⋃ i ∈ t, interior (U ↑i ⋯)
x : X
hx : x ∈ s
y : ↑s
hyt : y ∈ t
hy : x ∈ interior (U ↑y ⋯)
⊢ ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝 x
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem vonNBornology_eq : Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology

Tactic:
rw [Bornology.ext_iff_isBounded]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
rw [Bornology.isBounded_iff_isVonNBounded]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
intro s

Result:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s

Tactic:
exact isVonNBounded_iff _

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Triangulated.lean
lemma complete_distinguished_essImageDistTriang_morphism
    (H : ∀ (T₁' T₂' : Triangle C) (_ : T₁' ∈ distTriang C) (_ : T₂' ∈ distTriang C)
      (a : L.obj (T₁'.obj₁) ⟶ L.obj (T₂'.obj₁)) (b : L.obj (T₁'.obj₂) ⟶ L.obj (T₂'.obj₂))
      (_ : L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁),
      ∃ (φ : L.mapTriangle.obj T₁' ⟶ L.mapTriangle.obj T₂'), φ.hom₁ = a ∧ φ.hom₂ = b)
    (T₁ T₂ : Triangle D)
    (hT₁ : T₁ ∈ Functor.essImageDistTriang L) (hT₂ : T₂ ∈ L.essImageDistTriang)
    (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁) :
    ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ a⟦1⟧' = c ≫ T₂.mor₃

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Category.{u_4, u_2} D
L : C ⥤ D
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : HasShift D ℤ
inst✝ : L.CommShift ℤ
H :
  ∀ (T₁' T₂' : Triangle C),
    T₁' ∈ distinguishedTriangles →
      T₂' ∈ distinguishedTriangles →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle C
e₁ : T₁ ≅ L.mapTriangle.obj T₁'
hT₁' : T₁' ∈ distinguishedTriangles
T₂' : Triangle C
e₂ : T₂ ≅ L.mapTriangle.obj T₂'
hT₂' : T₂' ∈ distinguishedTriangles
comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂
comm₃' :
  T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ (L.commShiftIso 1).hom.app T₂'.obj₁
comm₃ :
  L.map T₁'.mor₃ ≫ (L.commShiftIso 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃
φ : L.mapTriangle.obj T₁' ⟶ L.mapTriangle.obj T₂'
hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
h₂ : L.map T₁'.mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ L.map T₂'.mor₂
h₃ :
  L.map T₁'.mor₃ ≫ (L.commShiftIso 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map φ.hom₁ =
    φ.hom₃ ≫ L.map T₂'.mor₃ ≫ (L.commShiftIso 1).hom.app T₂'.obj₁
⊢ T₁.mor₂ ≫ e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂

Tactic:
rw [reassoc_of% comm₂, reassoc_of% h₂, hφ₂, assoc, assoc,
  Iso.hom_inv_id_triangle_hom₂_assoc, ← reassoc_of% comm₂',
  Iso.hom_inv_id_triangle_hom₃, comp_id]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
theorem Nonempty.of_disjSups_left : (s ○ t).Nonempty → s.Nonempty

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (s ○ t).Nonempty → s.Nonempty

Tactic:
simp_rw [Finset.Nonempty, mem_disjSups]

Result:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (∃ x, ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ x, x ∈ s

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (∃ x, ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x) → ∃ x, x ∈ s

Tactic:
exact fun ⟨_, a, ha, _⟩ => ⟨a, ha⟩

Result:
no goals