harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem leftInvSeq_eq_reverse_rightInvSeq_reverse (ω : List B) :
    lis ω = (ris ω.reverse).reverse

Proof state:
case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.leftInvSeq [] = (cs.rightInvSeq [].reverse).reverse

Tactic:
simp

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse

Tactic:
induction' ω with i ω ih

Result:
case nil
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.leftInvSeq [] = (cs.rightInvSeq [].reverse).reverse

case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.leftInvSeq (i :: ω) = (cs.rightInvSeq (i :: ω).reverse).reverse

Proof state:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω.reverse).reverse =
    ((List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω.reverse)).concat (cs.simple i)).reverse

Tactic:
simp [map_reverse]

Result:
no goals

Proof state:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.leftInvSeq (i :: ω) = (cs.rightInvSeq (i :: ω).reverse).reverse

Tactic:
rw [leftInvSeq, reverse_cons, ← concat_eq_append, rightInvSeq_concat, ih]

Result:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω.reverse).reverse =
    ((List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω.reverse)).concat (cs.simple i)).reverse
-- Mathlib/Topology/Connected/LocallyConnected.lean
theorem locallyConnectedSpace_iff_connected_basis :
    LocallyConnectedSpace α ↔
      ∀ x, (𝓝 x).HasBasis (fun s : Set α => s ∈ 𝓝 x ∧ IsPreconnected s) id

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id

Tactic:
rw [locallyConnectedSpace_iff_connected_subsets]

Result:
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) ↔
    ∀ (x : α), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) ↔
    ∀ (x : α), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id

Tactic:
exact forall_congr' fun x => Filter.hasBasis_self.symm

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem exists_lt_mem_ball_of_mem_ball (h : x ∈ ball y ε) : ∃ ε' < ε, x ∈ ball y ε'

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : dist x y < ε
⊢ dist x y < (dist x y + ε) / 2

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : x ∈ ball y ε
⊢ ∃ ε' < ε, x ∈ ball y ε'

Tactic:
simp only [mem_ball] at h ⊢

Result:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : dist x y < ε
⊢ ∃ ε' < ε, dist x y < ε'

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : dist x y < ε
⊢ ∃ ε' < ε, dist x y < ε'

Tactic:
exact ⟨(dist x y + ε) / 2, by linarith, by linarith⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : dist x y < ε
⊢ (dist x y + ε) / 2 < ε

Tactic:
linarith

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem Subtype.beq_iff {α : Type u} [DecidableEq α] {p : α → Prop} {x y : {a : α // p a}} :
    (x == y) = (x.1 == y.1)

Proof state:
case mk
α : Type u
inst✝ : DecidableEq α
p : α → Prop
y : { a // p a }
val✝ : α
property✝ : p val✝
⊢ (⟨val✝, property✝⟩ == y) = (⟨val✝, property✝⟩.val == y.val)

Tactic:
cases y

Result:
case mk.mk
α : Type u
inst✝ : DecidableEq α
p : α → Prop
val✝¹ : α
property✝¹ : p val✝¹
val✝ : α
property✝ : p val✝
⊢ (⟨val✝¹, property✝¹⟩ == ⟨val✝, property✝⟩) = (⟨val✝¹, property✝¹⟩.val == ⟨val✝, property✝⟩.val)

Proof state:
case mk.mk
α : Type u
inst✝ : DecidableEq α
p : α → Prop
val✝¹ : α
property✝¹ : p val✝¹
val✝ : α
property✝ : p val✝
⊢ (⟨val✝¹, property✝¹⟩ == ⟨val✝, property✝⟩) = true ↔ (⟨val✝¹, property✝¹⟩.val == ⟨val✝, property✝⟩.val) = true

Tactic:
simp [beq_iff_eq]

Result:
no goals

Proof state:
case mk.mk
α : Type u
inst✝ : DecidableEq α
p : α → Prop
val✝¹ : α
property✝¹ : p val✝¹
val✝ : α
property✝ : p val✝
⊢ (⟨val✝¹, property✝¹⟩ == ⟨val✝, property✝⟩) = (⟨val✝¹, property✝¹⟩.val == ⟨val✝, property✝⟩.val)

Tactic:
rw [Bool.eq_iff_iff]

Result:
case mk.mk
α : Type u
inst✝ : DecidableEq α
p : α → Prop
val✝¹ : α
property✝¹ : p val✝¹
val✝ : α
property✝ : p val✝
⊢ (⟨val✝¹, property✝¹⟩ == ⟨val✝, property✝⟩) = true ↔ (⟨val✝¹, property✝¹⟩.val == ⟨val✝, property✝⟩.val) = true

Proof state:
α : Type u
inst✝ : DecidableEq α
p : α → Prop
x y : { a // p a }
⊢ (x == y) = (x.val == y.val)

Tactic:
cases x

Result:
case mk
α : Type u
inst✝ : DecidableEq α
p : α → Prop
y : { a // p a }
val✝ : α
property✝ : p val✝
⊢ (⟨val✝, property✝⟩ == y) = (⟨val✝, property✝⟩.val == y.val)
-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_iff_mem_image_Ioo_and_ne [NoZeroSMulDivisors R V] {x y z : P} :
    Sbtw R x y z ↔ y ∈ lineMap x z '' Set.Ioo (0 : R) 1 ∧ x ≠ z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y z : P
h : y ∈ ⇑(lineMap x z) '' Set.Ioo 0 1 ∧ x ≠ z
⊢ Sbtw R x y z

Tactic:
rcases h with ⟨⟨t, ht, rfl⟩, hxz⟩

Result:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ Sbtw R x ((lineMap x z) t) z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y z : P
⊢ Sbtw R x y z ↔ y ∈ ⇑(lineMap x z) '' Set.Ioo 0 1 ∧ x ≠ z

Tactic:
refine ⟨fun h => ⟨h.mem_image_Ioo, h.left_ne_right⟩, fun h => ?_⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y z : P
h : y ∈ ⇑(lineMap x z) '' Set.Ioo 0 1 ∧ x ≠ z
⊢ Sbtw R x y z

Proof state:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ Sbtw R x ((lineMap x z) t) z

Tactic:
refine ⟨⟨t, Set.mem_Icc_of_Ioo ht, rfl⟩, ?_⟩

Result:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ (lineMap x z) t ≠ x ∧ (lineMap x z) t ≠ z

Proof state:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ t • (z -ᵥ x) + 0 ≠ 0 ∧ (t - 1) • (z -ᵥ x) ≠ 0

Tactic:
simp [smul_ne_zero, sub_eq_zero, ht.1.ne.symm, ht.2.ne, hxz.symm]

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ (lineMap x z) t ≠ x ∧ (lineMap x z) t ≠ z

Tactic:
rw [lineMap_apply, ← @vsub_ne_zero V, ← @vsub_ne_zero V _ _ _ _ z, vadd_vsub_assoc, vsub_self,
  vadd_vsub_assoc, ← neg_vsub_eq_vsub_rev z x, ← @neg_one_smul R, ← add_smul, ← sub_eq_add_neg]

Result:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x z : P
hxz : x ≠ z
t : R
ht : t ∈ Set.Ioo 0 1
⊢ t • (z -ᵥ x) + 0 ≠ 0 ∧ (t - 1) • (z -ᵥ x) ≠ 0
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_inj_right (hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a)
    (h₃ : a - b = a - c) : b = c

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ a - b + b = a - b + c

Tactic:
rw [tsub_add_cancel_of_le h₁, h₃, tsub_add_cancel_of_le h₂]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ b = c

Tactic:
rw [← hab.inj]

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ a - b + b = a - b + c
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblZ_smul (P : Fin 3 → R) (u : R) : W'.dblZ (u • P) = u ^ 4 * W'.dblZ P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ u * P z * (u ^ 3 * P y - u ^ 3 * W'.negY P) = u ^ 4 * (P z * (P y - W'.negY P))

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.dblZ (u • P) = u ^ 4 * W'.dblZ P

Tactic:
simp only [dblZ, negY_smul, smul_fin3_ext]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ u * P z * (u ^ 3 * P y - u ^ 3 * W'.negY P) = u ^ 4 * (P z * (P y - W'.negY P))
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem NatTrans.equifibered_of_discrete {ι : Type*} {F G : Discrete ι ⥤ C}
    (α : F ⟶ G) : NatTrans.Equifibered α

Proof state:
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
F G : Discrete ι ⥤ C
α : F ⟶ G
i : ι
⊢ 𝟙 (F.obj { as := i }) ≫ α.app { as := i } = α.app { as := i } ≫ 𝟙 (G.obj { as := i })

Tactic:
rw [Category.id_comp, Category.comp_id]

Result:
no goals

Proof state:
case mk.mk.up.up
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
F G : Discrete ι ⥤ C
α : F ⟶ G
i : ι
⊢ IsPullback (F.map { down := { down := ⋯ } }) (α.app { as := i }) (α.app { as := i }) (G.map { down := { down := ⋯ } })

Tactic:
simp only [Discrete.functor_map_id]

Result:
case mk.mk.up.up
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
F G : Discrete ι ⥤ C
α : F ⟶ G
i : ι
⊢ IsPullback (𝟙 (F.obj { as := i })) (α.app { as := i }) (α.app { as := i }) (𝟙 (G.obj { as := i }))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
F G : Discrete ι ⥤ C
α : F ⟶ G
⊢ Equifibered α

Tactic:
rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩

Result:
case mk.mk.up.up
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
F G : Discrete ι ⥤ C
α : F ⟶ G
i : ι
⊢ IsPullback (F.map { down := { down := ⋯ } }) (α.app { as := i }) (α.app { as := i }) (G.map { down := { down := ⋯ } })

Proof state:
case mk.mk.up.up
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
F G : Discrete ι ⥤ C
α : F ⟶ G
i : ι
⊢ IsPullback (𝟙 (F.obj { as := i })) (α.app { as := i }) (α.app { as := i }) (𝟙 (G.obj { as := i }))

Tactic:
exact IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.comp_id]⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeffs_one : coeffs (1 : R[X]) ⊆ {1}

Proof state:
R : Type u
inst✝ : Semiring R
⊢ ∀ x ∈ support 1, coeff 1 x ∈ {1}

Tactic:
simp_all [coeff_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
⊢ coeffs 1 ⊆ {1}

Tactic:
simp_rw [coeffs, Finset.image_subset_iff]

Result:
R : Type u
inst✝ : Semiring R
⊢ ∀ x ∈ support 1, coeff 1 x ∈ {1}

Proof state:
R : Type u
inst✝ : Semiring R
⊢ coeffs 1 ⊆ {1}

Tactic:
classical
simp_rw [coeffs, Finset.image_subset_iff]
simp_all [coeff_one]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Polynomial.lean
theorem jacobson_bot_polynomial_of_jacobson_bot (h : jacobson (⊥ : Ideal R) = ⊥) :
    jacobson (⊥ : Ideal R[X]) = ⊥

Proof state:
R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | J.IsMaximal})
n : ℕ
⊢ f.coeff n = 0

Tactic:
suffices f.coeff n ∈ Ideal.jacobson ⊥ by rwa [h, Submodule.mem_bot] at this

Result:
R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | J.IsMaximal})
n : ℕ
⊢ f.coeff n ∈ ⊥.jacobson

Proof state:
R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | J.IsMaximal})
n : ℕ
this : f.coeff n ∈ ⊥.jacobson
⊢ f.coeff n = 0

Tactic:
rwa [h, Submodule.mem_bot] at this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
⊢ sInf (map C '' {J | J.IsMaximal}) ≤ ⊥

Tactic:
refine fun f hf => (Submodule.mem_bot R[X]).2 <| Polynomial.ext fun n =>
  Trans.trans (?_ : coeff f n = 0) (coeff_zero n).symm

Result:
R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | J.IsMaximal})
n : ℕ
⊢ f.coeff n = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
⊢ ⊥.jacobson = ⊥

Tactic:
refine eq_bot_iff.2 (le_trans jacobson_bot_polynomial_le_sInf_map_maximal ?_)

Result:
R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
⊢ sInf (map C '' {J | J.IsMaximal}) ≤ ⊥

Proof state:
R : Type u_1
inst✝ : CommRing R
h : ⊥.jacobson = ⊥
f : R[X]
hf : f ∈ sInf (map C '' {J | J.IsMaximal})
n : ℕ
⊢ f.coeff n ∈ ⊥.jacobson

Tactic:
exact mem_sInf.2 fun j hj => (mem_map_C_iff.1 ((mem_sInf.1 hf) ⟨j, ⟨hj.2, rfl⟩⟩)) n

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem liminf_le_of_frequently_le' {α β} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β}
    (h : ∃ᶠ a in f, u a ≤ x) : liminf u f ≤ x

Proof state:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ (∀ᶠ (x_1 : α) in f, ¬b ≤ x) → ∀ᶠ (x_1 : α) in f, ¬u x_1 ≤ x

Tactic:
exact fun h => hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))

Result:
no goals

Proof state:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ (∃ᶠ (a : α) in f, u a ≤ x) → ∃ᶠ (x_1 : α) in f, b ≤ x

Tactic:
rw [← not_imp_not, not_frequently, not_frequently]

Result:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ (∀ᶠ (x_1 : α) in f, ¬b ≤ x) → ∀ᶠ (x_1 : α) in f, ¬u x_1 ≤ x

Proof state:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ sSup {a | ∀ᶠ (n : α) in f, a ≤ u n} ≤ x

Tactic:
refine sSup_le fun b hb => ?_

Result:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ b ≤ x

Proof state:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ liminf u f ≤ x

Tactic:
rw [liminf_eq]

Result:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ sSup {a | ∀ᶠ (n : α) in f, a ≤ u n} ≤ x

Proof state:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ b ≤ x

Tactic:
have hbx : ∃ᶠ _ in f, b ≤ x := by
  revert h
  rw [← not_imp_not, not_frequently, not_frequently]
  exact fun h => hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))

Result:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
hbx : ∃ᶠ (x_1 : α) in f, b ≤ x
⊢ b ≤ x

Proof state:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ ∃ᶠ (x_1 : α) in f, b ≤ x

Tactic:
revert h

Result:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ (∃ᶠ (a : α) in f, u a ≤ x) → ∃ᶠ (x_1 : α) in f, b ≤ x

Proof state:
α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
hbx : ∃ᶠ (x_1 : α) in f, b ≤ x
⊢ b ≤ x

Tactic:
exact hbx.exists.choose_spec

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_pair {a b : α} (h : a ≠ b) : ({a, b} : Set α).ncard = 2

Proof state:
α : Type u_1
a b : α
h : a ≠ b
⊢ {a, b}.ncard = 2

Tactic:
rw [ncard_insert_of_not_mem, ncard_singleton]

Result:
α : Type u_1
a b : α
h : a ≠ b
⊢ a ∉ {b}

Proof state:
α : Type u_1
a b : α
h : a ≠ b
⊢ a ∉ {b}

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/Analytic/Inverse.lean
lemma HasFPowerSeriesAt.eventually_hasSum_of_comp  {f : E → F} {g : F → G}
    {q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
    (hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x) (hf : HasFPowerSeriesAt f p x)
    (hq : 0 < q.radius) :
    ∀ᶠ y in 𝓝 0, HasSum (fun n : ℕ => q n fun _ : Fin n => (f (x + y) - f x)) (g (f (x + y)))

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this✝ : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ EMetric.ball 0 q.radius
y : E
hy : Tendsto (fun a => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ EMetric.ball 0 q.radius
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed u
v : Set G
vu : v ⊆ u
v_open : IsOpen v
hv : g (f (x + y)) ∈ v
a₀ b₀ : ℕ
hab : ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b → q.partialSum a (p.partialSum b y - (p 0) fun x => 0) ∈ v
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
⊢ Tendsto (fun x => (p 0) fun x => 0) atTop (𝓝 (f x))

Tactic:
convert tendsto_const_nhds

Result:
case h.e'_5.h.e'_3
𝕜 : 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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
g : F → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x
hf : HasFPowerSeriesAt f p x
hq : 0 < q.radius
this✝ : ∀ᶠ (y : E) in 𝓝 0, f (x + y) - f x ∈ EMetric.ball 0 q.radius
y : E
hy : Tendsto (fun a => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)) atTop (𝓝 ((g ∘ f) (x + y)))
h'y : Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y)))
h''y : f (x + y) - f x ∈ EMetric.ball 0 q.radius
u : Set G
hu : u ∈ 𝓝 (g (f (x + y)))
u_closed : IsClosed u
v : Set G
vu : v ⊆ u
v_open : IsOpen v
hv : g (f (x + y)) ∈ v
a₀ b₀ : ℕ
hab : ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b → q.partialSum a (p.partialSum b y - (p 0) fun x => 0) ∈ v
a : ℕ
ha : a₀ ≤ a
this : ContinuousAt (q.partialSum a) (f (x + y) - f x)
⊢ f x = (p 0) fun x => 0
-- Mathlib/Topology/Order/MonotoneContinuity.lean
theorem Monotone.continuous_of_denseRange [DenselyOrdered β] {f : α → β} (h_mono : Monotone f)
    (h_dense : DenseRange f) : Continuous f :=
  continuous_iff_continuousAt.mpr fun a =>
    continuousAt_of_monotoneOn_of_closure_image_mem_nhds (fun _ _ _ _ hxy => h_mono hxy)
        univ_mem <|
      by simp only [image_univ, h_dense.closure_eq, univ_mem]

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
h_mono : Monotone f
h_dense : DenseRange f
a : α
⊢ closure (f '' univ) ∈ 𝓝 (f a)

Tactic:
simp only [image_univ, h_dense.closure_eq, univ_mem]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem nhds_ne_subtype_neBot_iff {S : Set X} {x : S} :
    (𝓝[≠] x).NeBot ↔ (𝓝[≠] (x : X) ⊓ 𝓟 S).NeBot

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set X
x : ↑S
⊢ (𝓝[≠] x).NeBot ↔ (𝓝[≠] ↑x ⊓ 𝓟 S).NeBot

Tactic:
rw [neBot_iff, neBot_iff, not_iff_not, nhds_ne_subtype_eq_bot_iff]

Result:
no goals
-- Mathlib/FieldTheory/SplittingField/Construction.lean
theorem irreducible_factor (f : K[X]) : Irreducible (factor f)

Proof state:
case pos
K : Type v
inst✝ : Field K
f : K[X]
H : ∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible (Classical.choose H)

Tactic:
exact (Classical.choose_spec H).1

Result:
no goals

Proof state:
K : Type v
inst✝ : Field K
f : K[X]
⊢ Irreducible f.factor

Tactic:
rw [factor]

Result:
K : Type v
inst✝ : Field K
f : K[X]
⊢ Irreducible (if H : ∃ g, Irreducible g ∧ g ∣ f then Classical.choose H else X)

Proof state:
K : Type v
inst✝ : Field K
f : K[X]
⊢ Irreducible (if H : ∃ g, Irreducible g ∧ g ∣ f then Classical.choose H else X)

Tactic:
split_ifs with H

Result:
case pos
K : Type v
inst✝ : Field K
f : K[X]
H : ∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible (Classical.choose H)

case neg
K : Type v
inst✝ : Field K
f : K[X]
H : ¬∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible X

Proof state:
case neg
K : Type v
inst✝ : Field K
f : K[X]
H : ¬∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible X

Tactic:
exact irreducible_X

Result:
no goals