harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Indization/FilteredColimits.lean
theorem exists_nonempty_limit_obj_of_isColimit [IsFiltered K] {c : Cocone H} (hc : IsColimit c)
    (T : Over (colimit F)) (hT : c.pt ≅ T)
    (h : Nonempty <| limit <| 𝒢 ⋙ yoneda.obj T) :
    ∃ k, Nonempty <| limit <| 𝒢 ⋙ yoneda.obj (H.obj k)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
c : Cocone H
hc : IsColimit c
T : Over (colimit F)
hT : c.pt ≅ T
h : Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj T))
⊢ T ≅ colimit H

Tactic:
refine hT.symm ≪≫ IsColimit.coconePointUniqueUpToIso hc (colimit.isColimit _)

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
c : Cocone H
hc : IsColimit c
T : Over (colimit F)
hT : c.pt ≅ T
h : Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj T))
⊢ Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H)))

Tactic:
suffices T ≅ colimit H from Nonempty.map (lim.map (whiskerLeft 𝒢 (yoneda.map this.hom))) h

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
c : Cocone H
hc : IsColimit c
T : Over (colimit F)
hT : c.pt ≅ T
h : Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj T))
⊢ T ≅ colimit H

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
c : Cocone H
hc : IsColimit c
T : Over (colimit F)
hT : c.pt ≅ T
h : Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj T))
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))

Tactic:
refine exists_nonempty_limit_obj_of_colimit F G H ?_

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
c : Cocone H
hc : IsColimit c
T : Over (colimit F)
hT : c.pt ≅ T
h : Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj T))
⊢ Nonempty (limit ((G.op ⋙ (toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H)))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem Sublist.findIdx?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
    (l₁.findIdx? p).isSome → (l₂.findIdx? p).isSome

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ (∃ x, x ∈ l₁ ∧ p x = true) → ∃ x, x ∈ l₂ ∧ p x = true

Tactic:
rintro ⟨w, m, q⟩

Result:
case intro.intro
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <+ l₂
w : α
m : w ∈ l₁
q : p w = true
⊢ ∃ x, x ∈ l₂ ∧ p x = true

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ (findIdx? p l₁).isSome = true → (findIdx? p l₂).isSome = true

Tactic:
simp only [List.findIdx?_isSome, any_eq_true]

Result:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ (∃ x, x ∈ l₁ ∧ p x = true) → ∃ x, x ∈ l₂ ∧ p x = true

Proof state:
case intro.intro
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <+ l₂
w : α
m : w ∈ l₁
q : p w = true
⊢ ∃ x, x ∈ l₂ ∧ p x = true

Tactic:
exact ⟨w, h.mem m, q⟩

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma rnDeriv_pos [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) :
    ∀ᵐ x ∂μ, 0 < μ.rnDeriv ν x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂μ, 0 < μ.rnDeriv ν x

Tactic:
rw [← Measure.withDensity_rnDeriv_eq _ _  hμν,
  ae_withDensity_iff (Measure.measurable_rnDeriv _ _), Measure.withDensity_rnDeriv_eq _ _  hμν]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0 → 0 < μ.rnDeriv ν x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ 0 → 0 < μ.rnDeriv ν x

Tactic:
exact ae_of_all _ (fun x hx ↦ lt_of_le_of_ne (zero_le _) hx.symm)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {h'} :
    m.getKey? a = some (m.getKey a h')

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
h' : m.contains a = true
⊢ m.getKey? a = some (m.getKey a h')

Tactic:
simp_to_model using List.getKey?_eq_some_getKey

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Measure.lean
theorem measurableSet_coe : MeasurableSet (I : Set (ι → ℝ))

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Countable ι
⊢ MeasurableSet (univ.pi fun i => Ioc (I.lower i) (I.upper i))

Tactic:
exact MeasurableSet.univ_pi fun i => measurableSet_Ioc

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Countable ι
⊢ MeasurableSet ↑I

Tactic:
rw [coe_eq_pi]

Result:
ι : Type u_1
I : Box ι
inst✝ : Countable ι
⊢ MeasurableSet (univ.pi fun i => Ioc (I.lower i) (I.upper i))
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem Submodule.rank_le (s : Submodule R M) : Module.rank R s ≤ Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R M

Tactic:
rw [← rank_top R M]

Result:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R ↥⊤

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R ↥⊤

Tactic:
exact rank_mono le_top

Result:
no goals
-- Mathlib/Data/Real/Cardinality.lean
theorem increasing_cantorFunction (h1 : 0 < c) (h2 : c < 1 / 2) {n : ℕ} {f g : ℕ → Bool}
    (hn : ∀ k < n, f k = g k) (fn : f n = false) (gn : g n = true) :
    cantorFunction c f < cantorFunction c g

Proof state:
case h.e'_3
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ ((bif f_max 0 then 1 else 0) + c * cantorFunction c fun n => f_max (n + 1)) = c * ∑' (n : ℕ), c ^ n

Tactic:
apply zero_add

Result:
no goals

Proof state:
case succ
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n✝ : ℕ
hn : f (n✝ + 1) = true
⊢ f_max (n✝ + 1) = true

Tactic:
apply rfl

Result:
no goals

Proof state:
case h.e'_4.refine_1.succ
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ cantorFunctionAux c g_min (n✝ + 1) = 0

Tactic:
rfl

Result:
no goals

Proof state:
case zero
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
⊢ cantorFunction c f < cantorFunction c g

Tactic:
let g_min : ℕ → Bool := fun n => Nat.rec true (fun _ _ => false) n

Result:
case zero
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
⊢ cantorFunction c f < cantorFunction c g

Proof state:
case h.e'_4.refine_1.zero
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
hn : 0 ≠ 0
⊢ cantorFunctionAux c g_min 0 = 0

Tactic:
contradiction

Result:
no goals
-- Mathlib/RingTheory/Localization/Away/Basic.lean
lemma awayLift_mk {A : Type*} [CommRing A] (f : R →+* A) (r : R)
    (a : R) (v : A) (hv : f r * v = 1) (j : ℕ) :
    Localization.awayLift f r (isUnit_iff_exists_inv.mpr ⟨v, hv⟩)
      (Localization.mk a ⟨r ^ j, j, rfl⟩) = f a * v ^ j

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_4
inst✝ : CommRing A
f : R →+* A
r a : R
v : A
hv : f r * v = 1
j : ℕ
⊢ f a = f a * v ^ j * ↑((IsUnit.liftRight ((↑f).restrict (Submonoid.powers r)) ⋯) ⟨r ^ j, ⋯⟩)

Tactic:
simp [IsUnit.liftRight, mul_assoc, ← mul_pow, (mul_comm _ _).trans hv]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_4
inst✝ : CommRing A
f : R →+* A
r a : R
v : A
hv : f r * v = 1
j : ℕ
⊢ (awayLift f r ⋯) (mk a ⟨r ^ j, ⋯⟩) = f a * v ^ j

Tactic:
rw [Localization.mk_eq_mk']

Result:
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_4
inst✝ : CommRing A
f : R →+* A
r a : R
v : A
hv : f r * v = 1
j : ℕ
⊢ (awayLift f r ⋯) (mk' (Localization (Submonoid.powers r)) a ⟨r ^ j, ⋯⟩) = f a * v ^ j

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_4
inst✝ : CommRing A
f : R →+* A
r a : R
v : A
hv : f r * v = 1
j : ℕ
⊢ (awayLift f r ⋯) (mk' (Localization (Submonoid.powers r)) a ⟨r ^ j, ⋯⟩) = f a * v ^ j

Tactic:
erw [IsLocalization.lift_mk']

Result:
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_4
inst✝ : CommRing A
f : R →+* A
r a : R
v : A
hv : f r * v = 1
j : ℕ
⊢ f a * ↑((IsUnit.liftRight ((↑f).restrict (Submonoid.powers r)) ⋯) ⟨r ^ j, ⋯⟩)⁻¹ = f a * v ^ j

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_4
inst✝ : CommRing A
f : R →+* A
r a : R
v : A
hv : f r * v = 1
j : ℕ
⊢ f a * ↑((IsUnit.liftRight ((↑f).restrict (Submonoid.powers r)) ⋯) ⟨r ^ j, ⋯⟩)⁻¹ = f a * v ^ j

Tactic:
rw [Units.mul_inv_eq_iff_eq_mul]

Result:
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_4
inst✝ : CommRing A
f : R →+* A
r a : R
v : A
hv : f r * v = 1
j : ℕ
⊢ f a = f a * v ^ j * ↑((IsUnit.liftRight ((↑f).restrict (Submonoid.powers r)) ⋯) ⟨r ^ j, ⋯⟩)
-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_eventually_measure_zero_of_singular (hρ : ρ ⟂ₘ μ) :
    ∀ᵐ x ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 0)

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ρ o = 0
μo : μ oᶜ = 0
⊢ μ (s ∩ o) + μ oᶜ = μ (s ∩ o)

Tactic:
rw [μo, add_zero]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
z : ℝ≥0∞
hz : z > 0
⊢ ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < z

Tactic:
obtain ⟨w, w_pos, w_lt⟩ : ∃ w : ℝ≥0, (0 : ℝ≥0∞) < w ∧ (w : ℝ≥0∞) < z :=
  ENNReal.lt_iff_exists_nnreal_btwn.1 hz

Result:
case h.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
x : α
hx : ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
h'x : ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < ↑w
w_lt : ↑w < z
⊢ ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < z
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndependent_fin2 {f : Fin 2 → V} :
    LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ a : K, a • f 1 ≠ f 0

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : Fin 2 → V
⊢ Fin.tail f default = f 1

Tactic:
rw [← Fin.succ_zero_eq_one]

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : Fin 2 → V
⊢ Fin.tail f default = f (Fin.succ 0)

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : Fin 2 → V
⊢ Fin.tail f default = f (Fin.succ 0)

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : Fin 2 → V
⊢ LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0

Tactic:
rw [linearIndependent_fin_succ, linearIndependent_unique_iff, range_unique, mem_span_singleton,
  not_exists, show Fin.tail f default = f 1 by rw [← Fin.succ_zero_eq_one]; rfl]

Result:
no goals
-- Mathlib/Order/BooleanGenerators.lean
lemma sSup_inter (hS : BooleanGenerators S) {T₁ T₂ : Set α} (hT₁ : T₁ ⊆ S) (hT₂ : T₂ ⊆ S) :
    sSup (T₁ ∩ T₂) = (sSup T₁) ⊓ (sSup T₂)

Proof state:
case a.intro.intro.a.a.left
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ∈ T₁

Tactic:
apply (hS.mono hT₁).mem_of_isAtom_of_le_sSup_atoms _ _ _

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ IsAtom I

α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ≤ sSup T₁
-- Mathlib/RingTheory/Regular/RegularSequence.lean
lemma _root_.AddEquiv.isRegular_congr {e : M ≃+ M₂} {as bs}
    (h : List.Forall₂ (fun (r : R) (s : S) => ∀ x, e (r • x) = s • e x) as bs) :
    IsRegular M as ↔ IsRegular M₂ bs

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs
⊢ IsRegular M as ↔ IsRegular M₂ bs

Tactic:
conv => congr <;> rw [isRegular_iff, ne_eq, eq_comm,
  ← subsingleton_quotient_iff_eq_top]

Result:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs
⊢ IsWeaklyRegular M as ∧ ¬Subsingleton (M ⧸ Ideal.ofList as • ⊤) ↔
    IsWeaklyRegular M₂ bs ∧ ¬Subsingleton (M₂ ⧸ Ideal.ofList bs • ⊤)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs
⊢ IsWeaklyRegular M as ∧ ¬Subsingleton (M ⧸ Ideal.ofList as • ⊤) ↔
    IsWeaklyRegular M₂ bs ∧ ¬Subsingleton (M₂ ⧸ Ideal.ofList bs • ⊤)

Tactic:
let e' := QuotientAddGroup.congr _ _ e <|
  AddHom.map_smul_top_toAddSubgroup_of_surjective e.surjective h

Result:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs
e' : M ⧸ (Ideal.ofList as • ⊤).toAddSubgroup ≃+ M₂ ⧸ (Ideal.ofList bs • ⊤).toAddSubgroup :=
  QuotientAddGroup.congr (Ideal.ofList as • ⊤).toAddSubgroup (Ideal.ofList bs • ⊤).toAddSubgroup e ⋯
⊢ IsWeaklyRegular M as ∧ ¬Subsingleton (M ⧸ Ideal.ofList as • ⊤) ↔
    IsWeaklyRegular M₂ bs ∧ ¬Subsingleton (M₂ ⧸ Ideal.ofList bs • ⊤)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs
e' : M ⧸ (Ideal.ofList as • ⊤).toAddSubgroup ≃+ M₂ ⧸ (Ideal.ofList bs • ⊤).toAddSubgroup :=
  QuotientAddGroup.congr (Ideal.ofList as • ⊤).toAddSubgroup (Ideal.ofList bs • ⊤).toAddSubgroup e ⋯
⊢ IsWeaklyRegular M as ∧ ¬Subsingleton (M ⧸ Ideal.ofList as • ⊤) ↔
    IsWeaklyRegular M₂ bs ∧ ¬Subsingleton (M₂ ⧸ Ideal.ofList bs • ⊤)

Tactic:
exact and_congr (e.isWeaklyRegular_congr h) e'.subsingleton_congr.not

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc (attr := simp)]
lemma rightHomologyι_comp_fromOpcycles :
    S.rightHomologyι ≫ S.fromOpcycles = 0 :=
  S.rightHomologyι_descOpcycles_π_eq_zero_of_boundary S.g (𝟙 _) (by rw [comp_id])

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.g = S.g ≫ 𝟙 S.X₃

Tactic:
rw [comp_id]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
theorem Convex.taylor_approx_two_segment {v w : E} (hv : x + v ∈ interior s)
    (hw : x + v + w ∈ interior s) :
    (fun h : ℝ => f (x + h • v + h • w)
        - f (x + h • v) - h • f' x w - h ^ 2 • f'' v w - (h ^ 2 / 2) • f'' w w) =o[𝓝[>] 0]
      fun h => h ^ 2

Proof state:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 => ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
⊢ ‖f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w - (h ^ 2 / 2) • (f'' w) w‖ ≤
    ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖

Tactic:
have xt_mem : ∀ t ∈ Icc (0 : ℝ) 1, x + h • v + (t * h) • w ∈ interior s := by
  intro t ht
  have : x + h • v ∈ interior s := s_conv.add_smul_mem_interior xs hv ⟨hpos, h_lt_1.le⟩
  rw [← smul_smul]
  apply s_conv.interior.add_smul_mem this _ ht
  rw [add_assoc] at hw
  convert s_conv.add_smul_mem_interior xs hw ⟨hpos, h_lt_1.le⟩ using 1
  module

Result:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 => ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
xt_mem : ∀ t ∈ Icc 0 1, x + h • v + (t * h) • w ∈ interior s
⊢ ‖f (x + h • v + h • w) - f (x + h • v) - h • (f' x) w - h ^ 2 • (f'' v) w - (h ^ 2 / 2) • (f'' w) w‖ ≤
    ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * h ^ 2‖
-- Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
/-- The length of a hamiltonian cycle is the number of vertices. -/
lemma IsHamiltonianCycle.length_eq [Fintype α] (hp : p.IsHamiltonianCycle) :
    p.length = Fintype.card α

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst✝ : Fintype α
hp : p.IsHamiltonianCycle
⊢ p.length = Fintype.card α

Tactic:
rw [← length_tail_add_one hp.not_nil, hp.isHamiltonian_tail.length_eq, Nat.sub_add_cancel]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst✝ : Fintype α
hp : p.IsHamiltonianCycle
⊢ 1 ≤ Fintype.card α

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst✝ : Fintype α
hp : p.IsHamiltonianCycle
⊢ Nonempty α

Tactic:
exact ⟨a⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst✝ : Fintype α
hp : p.IsHamiltonianCycle
⊢ 1 ≤ Fintype.card α

Tactic:
rw [Nat.succ_le, Fintype.card_pos_iff]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a : α
p : G.Walk a a
inst✝ : Fintype α
hp : p.IsHamiltonianCycle
⊢ Nonempty α