harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem bowtie {j₁ j₂ k₁ k₂ : C} (f₁ : j₁ ⟶ k₁) (g₁ : j₁ ⟶ k₂) (f₂ : j₂ ⟶ k₁) (g₂ : j₂ ⟶ k₂) :
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β

Tactic:
obtain ⟨t, k₁t, k₂t, ht⟩ := span f₁ g₁

Result:
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β

Proof state:
case intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β

Tactic:
obtain ⟨s, ts, hs⟩ := IsFilteredOrEmpty.cocone_maps (f₂ ≫ k₁t) (g₂ ≫ k₂t)

Result:
case intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
s : C
ts : t ⟶ s
hs : (f₂ ≫ k₁t) ≫ ts = (g₂ ≫ k₂t) ≫ ts
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β

Proof state:
case intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
s : C
ts : t ⟶ s
hs : f₂ ≫ k₁t ≫ ts = g₂ ≫ k₂t ≫ ts
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β

Tactic:
exact ⟨s, k₁t ≫ ts, k₂t ≫ ts, by simp only [← Category.assoc, ht], hs⟩

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
s : C
ts : t ⟶ s
hs : f₂ ≫ k₁t ≫ ts = g₂ ≫ k₂t ≫ ts
⊢ f₁ ≫ k₁t ≫ ts = g₁ ≫ k₂t ≫ ts

Tactic:
simp only [← Category.assoc, ht]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
s : C
ts : t ⟶ s
hs : (f₂ ≫ k₁t) ≫ ts = (g₂ ≫ k₂t) ≫ ts
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β

Tactic:
simp_rw [Category.assoc] at hs

Result:
case intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
s : C
ts : t ⟶ s
hs : f₂ ≫ k₁t ≫ ts = g₂ ≫ k₂t ≫ ts
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean
theorem bddBelow_projectiveSemiNormAux (x : ⨂[𝕜] i, E i) :
    BddBelow (Set.range (fun (p : lifts x) ↦ projectiveSeminormAux p.1))

Proof state:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ 0 ∈ lowerBounds (Set.range fun p => projectiveSeminormAux ↑p)

Tactic:
rw [mem_lowerBounds]

Result:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ ∀ x_1 ∈ Set.range fun p => projectiveSeminormAux ↑p, 0 ≤ x_1

Proof state:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ ∀ a ∈ x.lifts, 0 ≤ projectiveSeminormAux a

Tactic:
exact fun p _ ↦ projectiveSeminormAux_nonneg p

Result:
no goals

Proof state:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ ∀ x_1 ∈ Set.range fun p => projectiveSeminormAux ↑p, 0 ≤ x_1

Tactic:
simp only [Set.mem_range, Subtype.exists, exists_prop, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂]

Result:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ ∀ a ∈ x.lifts, 0 ≤ projectiveSeminormAux a

Proof state:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ BddBelow (Set.range fun p => projectiveSeminormAux ↑p)

Tactic:
existsi 0

Result:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
⊢ 0 ∈ lowerBounds (Set.range fun p => projectiveSeminormAux ↑p)
-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem lintegral_Lp_add_le {p : ℝ} {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
    (hp1 : 1 ≤ p) :
    (∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≤
      (∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p)

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_top : ¬∫⁻ (a : α), g a ^ p ∂μ = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
have hpq := Real.IsConjExponent.conjExponent hp1_lt

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ⊤
hg_top : ¬∫⁻ (a : α), g a ^ p ∂μ = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : p.IsConjExponent p.conjExponent
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : p.IsConjExponent p.conjExponent
h0 : ¬∫⁻ (a : α), (f + g) a ^ p ∂μ = 0
⊢ ∫⁻ (a : α), (f + g) a ^ p ∂μ < ⊤

Tactic:
exact lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top hf hf_top hg_top hp1

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
have hp_pos : 0 < p := lt_of_lt_of_le zero_lt_one hp1

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
-- Mathlib/Data/ZMod/Basic.lean
theorem val_cast_eq_val_of_lt {m n : ℕ} [nzm : NeZero m] {a : ZMod m}
    (h : a.val < n) : (a.cast : ZMod n).val = a.val

Proof state:
case succ.zero
m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
nzn : NeZero 0
h : a.val < 0
⊢ a.cast.val = a.val

Tactic:
cases nzn

Result:
case succ.zero.mk
m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
h : a.val < 0
out✝ : 0 ≠ 0
⊢ a.cast.val = a.val

Proof state:
m n : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < n
⊢ a.cast.val = a.val

Tactic:
have nzn : NeZero n := by constructor; rintro rfl; simp at h

Result:
m n : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < n
nzn : NeZero n
⊢ a.cast.val = a.val

Proof state:
case succ.zero.mk
m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
h : a.val < 0
out✝ : 0 ≠ 0
⊢ a.cast.val = a.val

Tactic:
simp_all

Result:
no goals

Proof state:
case succ.succ
m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
nzn : NeZero (n + 1)
h : a.val < n + 1
⊢ a.cast.val = a.val

Tactic:
exact Fin.val_cast_of_lt h

Result:
no goals

Proof state:
case out
m n : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < n
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
case out
m : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < 0
⊢ False

Proof state:
m n : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < n
nzn : NeZero n
⊢ a.cast.val = a.val

Tactic:
cases m with
| zero => cases nzm; simp_all
| succ m =>
  cases n with
  | zero => cases nzn; simp_all
  | succ n => exact Fin.val_cast_of_lt h

Result:
no goals

Proof state:
case zero
n : ℕ
nzn : NeZero n
nzm : NeZero 0
a : ZMod 0
h : a.val < n
⊢ a.cast.val = a.val

Tactic:
cases nzm

Result:
case zero.mk
n : ℕ
nzn : NeZero n
a : ZMod 0
h : a.val < n
out✝ : 0 ≠ 0
⊢ a.cast.val = a.val

Proof state:
case succ
n : ℕ
nzn : NeZero n
m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
h : a.val < n
⊢ a.cast.val = a.val

Tactic:
cases n with
| zero => cases nzn; simp_all
| succ n => exact Fin.val_cast_of_lt h

Result:
no goals

Proof state:
case zero.mk
n : ℕ
nzn : NeZero n
a : ZMod 0
h : a.val < n
out✝ : 0 ≠ 0
⊢ a.cast.val = a.val

Tactic:
simp_all

Result:
no goals

Proof state:
case out
m : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < 0
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
m n : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < n
⊢ NeZero n

Tactic:
constructor

Result:
case out
m n : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < n
⊢ n ≠ 0
-- Mathlib/Data/Nat/Init.lean
protected lemma eq_mul_of_div_eq_left (H1 : b ∣ a) (H2 : a / b = c) : a = c * b

Proof state:
a b c : ℕ
H1 : b ∣ a
H2 : a / b = c
⊢ a = c * b

Tactic:
rw [Nat.mul_comm, Nat.eq_mul_of_div_eq_right H1 H2]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
@[simp] lemma limsup_top_eq_iSup (u : β → α) : limsup u ⊤ = ⨆ i, u i

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ limsup u ⊤ = ⨆ i, u i

Tactic:
rw [limsup, map_top, limsSup_principal_eq_sSup, sSup_range]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem ContinuousMultilinearMap.norm_map_snoc_le (f : ContinuousMultilinearMap 𝕜 Ei G)
    (m : ∀ i : Fin n, Ei <| castSucc i) (x : Ei (last n)) :
    ‖f (snoc m x)‖ ≤ (‖f‖ * ∏ i, ‖m i‖) * ‖x‖ :=
  calc
    ‖f (snoc m x)‖ ≤ ‖f‖ * ∏ i, ‖snoc m x i‖ := f.le_opNorm _
    _ = (‖f‖ * ∏ i, ‖m i‖) * ‖x‖

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n) → Ei i.castSucc
x : Ei (last n)
⊢ ‖f‖ * ∏ i : Fin (n + 1), ‖snoc m x i‖ = (‖f‖ * ∏ i : Fin n, ‖m i‖) * ‖x‖

Tactic:
rw [prod_univ_castSucc]

Result:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n) → Ei i.castSucc
x : Ei (last n)
⊢ ‖f‖ * ((∏ i : Fin n, ‖snoc m x i.castSucc‖) * ‖snoc m x (last n)‖) = (‖f‖ * ∏ i : Fin n, ‖m i‖) * ‖x‖

Proof state:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n) → Ei i.castSucc
x : Ei (last n)
⊢ ‖f‖ * ((∏ i : Fin n, ‖snoc m x i.castSucc‖) * ‖snoc m x (last n)‖) = (‖f‖ * ∏ i : Fin n, ‖m i‖) * ‖x‖

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem slt_eq_not_carry (x y : BitVec w) :
    x.slt y = (x.msb == y.msb).xor (carry w x (~~~y) true)

Proof state:
w : Nat
x y : BitVec w
⊢ (!(!x.msb == y.msb) == !carry w x (~~~y) true) = !(x.msb == y.msb) == carry w x (~~~y) true

Tactic:
cases x.msb == y.msb <;> simp

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x.slt y = (x.msb == y.msb ^^ carry w x (~~~y) true)

Tactic:
simp only [slt_eq_ult, bne, ult_eq_not_carry]

Result:
w : Nat
x y : BitVec w
⊢ (!(!x.msb == y.msb) == !carry w x (~~~y) true) = !(x.msb == y.msb) == carry w x (~~~y) true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem getElem_unattach
    {p : α → Prop} {l : Vector { x // p x } n} (i : Nat) (h : i < n) :
    l.unattach[i] = (l[i]'(by simpa using h)).1

Proof state:
α : Type ?u.77632
n : Nat
p : α → Prop
l : Vector { x // p x } n
i : Nat
h : i < n
⊢ i < n

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Prop
l : Vector { x // p x } n
i : Nat
h : i < n
⊢ l.unattach[i] = l[i].val

Tactic:
simp [unattach]

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Final.lean
theorem IsCofiltered.of_exists_of_isCofiltered_of_fullyFaithful [IsCofiltered D] [F.Full]
    [F.Faithful] (h : ∀ d, ∃ c, Nonempty (F.obj c ⟶ d)) : IsCofiltered C :=
  { IsCofilteredOrEmpty.of_exists_of_isCofiltered_of_fullyFaithful F h with
    nonempty

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ Nonempty C

Tactic:
have : Nonempty D := IsCofiltered.nonempty

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
this : Nonempty D
⊢ Nonempty C

Proof state:
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
this : Nonempty D
c : C
⊢ Nonempty C

Tactic:
exact ⟨c⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
this : Nonempty D
⊢ Nonempty C

Tactic:
obtain ⟨c, -⟩ := h (Classical.arbitrary D)

Result:
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
this : Nonempty D
c : C
⊢ Nonempty C
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem FaithfulSMul.ker_algebraMap_eq_bot (R A : Type*) [CommSemiring R] [Semiring A]
    [Algebra R A] [FaithfulSMul R A] : RingHom.ker (algebraMap R A) = ⊥

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : R
⊢ x✝ ∈ RingHom.ker (algebraMap R A) ↔ x✝ ∈ ⊥

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ RingHom.ker (algebraMap R A) = ⊥

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : R
⊢ x✝ ∈ RingHom.ker (algebraMap R A) ↔ x✝ ∈ ⊥
-- Mathlib/Combinatorics/Additive/Corner/Roth.lean
theorem roth_3ap_theorem_nat (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound (ε / 3) ≤ n)
    (A : Finset ℕ) (hAn : A ⊆ range n) (hAε : ε * n ≤ #A) : ¬ ThreeAPFree (A : Set ℕ)

Proof state:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' (Nat.cast '' ↑A))
this✝¹ : ↑A = Fin.val '' (Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x => ↑x) A)
⊢ False

Tactic:
refine roth_3ap_theorem (ε / 3) (by positivity) (by simp; omega) _ ?_ this

Result:
n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' (Nat.cast '' ↑A))
this✝¹ : ↑A = Fin.val '' (Nat.cast '' ↑A)
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x => ↑x) A)
⊢ ε / 3 * ↑(Fintype.card (Fin (2 * n + 1))) ≤ ↑(#(image (fun x => ↑x) A))
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem induction_on_adjoin_finset (S : Finset E) (P : IntermediateField F E → Prop) (base : P ⊥)
    (ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (K⟮x⟯.restrictScalars F)) :
    P (adjoin F S)

Proof state:
case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)
a✝ : E
s✝ : Finset E
ha : a✝ ∈ S
x✝¹ : s✝ ⊆ S
x✝ : a✝ ∉ s✝
h : P (adjoin F ↑s✝)
⊢ P (adjoin F ↑(insert a✝ s✝))

Tactic:
rw [Finset.coe_insert, Set.insert_eq, Set.union_comm, ← adjoin_adjoin_left]

Result:
case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)
a✝ : E
s✝ : Finset E
ha : a✝ ∈ S
x✝¹ : s✝ ⊆ S
x✝ : a✝ ∉ s✝
h : P (adjoin F ↑s✝)
⊢ P (restrictScalars F (↥(adjoin F ↑s✝))⟮a✝⟯)

Proof state:
case refine_1
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)
⊢ P (adjoin F ↑∅)

Tactic:
simp [base]

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)
⊢ P (adjoin F ↑S)

Tactic:
refine Finset.induction_on' S ?_ (fun ha _ _ h => ?_)

Result:
case refine_1
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)
⊢ P (adjoin F ↑∅)

case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)
a✝ : E
s✝ : Finset E
ha : a✝ ∈ S
x✝¹ : s✝ ⊆ S
x✝ : a✝ ∉ s✝
h : P (adjoin F ↑s✝)
⊢ P (adjoin F ↑(insert a✝ s✝))

Proof state:
case refine_2
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Finset E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)
a✝ : E
s✝ : Finset E
ha : a✝ ∈ S
x✝¹ : s✝ ⊆ S
x✝ : a✝ ∉ s✝
h : P (adjoin F ↑s✝)
⊢ P (restrictScalars F (↥(adjoin F ↑s✝))⟮a✝⟯)

Tactic:
exact ih (adjoin F _) _ ha h

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem a_add_one_le_four_pow_parts_card : a + 1 ≤ 4 ^ #P.parts

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ Fintype.card α / #P.parts - Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts + 1 ≤ 4 ^ #P.parts

Tactic:
conv_rhs => rw [← Nat.sub_add_cancel h]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ Fintype.card α / #P.parts - Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts + 1 ≤ 4 ^ #P.parts - 1 + 1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
⊢ a + 1 ≤ 4 ^ #P.parts

Tactic:
have h : 1 ≤ 4 ^ #P.parts := one_le_pow₀ (by norm_num)

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ a + 1 ≤ 4 ^ #P.parts

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ a + 1 ≤ 4 ^ #P.parts

Tactic:
rw [stepBound, ← Nat.div_div_eq_div_mul]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ Fintype.card α / #P.parts - Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts + 1 ≤ 4 ^ #P.parts

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
⊢ 1 ≤ 4

Tactic:
norm_num

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ Fintype.card α / #P.parts - Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts + 1 ≤ 4 ^ #P.parts - 1 + 1

Tactic:
rw [add_le_add_iff_right, tsub_le_iff_left, ← Nat.add_sub_assoc h]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ Fintype.card α / #P.parts ≤ Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts + 4 ^ #P.parts - 1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
h : 1 ≤ 4 ^ #P.parts
⊢ Fintype.card α / #P.parts ≤ Fintype.card α / #P.parts / 4 ^ #P.parts * 4 ^ #P.parts + 4 ^ #P.parts - 1

Tactic:
exact Nat.le_sub_one_of_lt (Nat.lt_div_mul_add h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem min?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) :
    (replicate n a).min? = if n = 0 then none else some a

Proof state:
case succ
α : Type u_1
inst✝ : Min α
a : α
w : min a a = a
n : Nat
ih : (replicate n a).min? = if n = 0 then none else some a
⊢ (replicate (n + 1) a).min? = if n + 1 = 0 then none else some a

Tactic:
cases n <;> simp_all [replicate_succ, min?_cons']

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : Min α
a : α
w : min a a = a
⊢ (replicate 0 a).min? = if 0 = 0 then none else some a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Min α
n : Nat
a : α
w : min a a = a
⊢ (replicate n a).min? = if n = 0 then none else some a

Tactic:
induction n with
| zero => rfl
| succ n ih => cases n <;> simp_all [replicate_succ, min?_cons']

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/CompareExp.lean
theorem isLittleO_cpow_exp (hl : IsExpCmpFilter l) (a : ℂ) {b : ℝ} (hb : 0 < b) :
    (fun z => z ^ a) =o[l] fun z => exp (b * z) :=
  calc
    (fun z => z ^ a) =Θ[l] fun z => Real.exp (re a * Real.log ‖z‖) :=
      hl.isTheta_cpow_exp_re_mul_log a
    _ =o[l] fun z => exp (b * z) :=
      IsLittleO.of_norm_right <| by
        simp only [norm_exp, re_ofReal_mul, Real.isLittleO_exp_comp_exp_comp]
        refine (IsEquivalent.refl.sub_isLittleO ?_).symm.tendsto_atTop
          (hl.tendsto_re.const_mul_atTop hb)
        exact (hl.isLittleO_log_norm_re.const_mul_left _).const_mul_right hb.ne'

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ (fun z => Real.exp (a.re * Real.log ‖z‖)) =o[l] fun x => ‖cexp (↑b * x)‖

Tactic:
simp only [norm_exp, re_ofReal_mul, Real.isLittleO_exp_comp_exp_comp]

Result:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ Tendsto (fun x => b * x.re - a.re * Real.log ‖x‖) l atTop

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ Tendsto (fun x => b * x.re - a.re * Real.log ‖x‖) l atTop

Tactic:
refine (IsEquivalent.refl.sub_isLittleO ?_).symm.tendsto_atTop
  (hl.tendsto_re.const_mul_atTop hb)

Result:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ (fun x => a.re * Real.log ‖x‖) =o[l] fun x => b * x.re

Proof state:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ (fun x => a.re * Real.log ‖x‖) =o[l] fun x => b * x.re

Tactic:
exact (hl.isLittleO_log_norm_re.const_mul_left _).const_mul_right hb.ne'

Result:
no goals