harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem mem_memberSubfamily : s ∈ 𝒜.memberSubfamily a ↔ insert a s ∈ 𝒜 ∧ a ∉ s

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
rw [insert_erase hs2]

Result:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ s ∈ 𝒜 ∧ a ∉ s.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ (∃ a_1, (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) → insert a s ∈ 𝒜 ∧ a ∉ s

Tactic:
rintro ⟨s, ⟨hs1, hs2⟩, rfl⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜 ∧ a ∉ s.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ (∃ a_1, (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) ↔ insert a s ∈ 𝒜 ∧ a ∉ s

Tactic:
refine ⟨?_, fun h => ⟨insert a s, ⟨h.1, by simp⟩, erase_insert h.2⟩⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ (∃ a_1, (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) → insert a s ∈ 𝒜 ∧ a ∉ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝒜 ∧ a ∉ s
⊢ a ∈ insert a s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ memberSubfamily a 𝒜 ↔ insert a s ∈ 𝒜 ∧ a ∉ s

Tactic:
simp_rw [memberSubfamily, mem_image, mem_filter]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ (∃ a_1, (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) ↔ insert a s ∈ 𝒜 ∧ a ∉ s

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ s ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
exact ⟨hs1, not_mem_erase _ _⟩

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Instances.lean
theorem one_sub_mem {t : β} (ht : t ∈ Icc (0 : β) 1) : 1 - t ∈ Icc (0 : β) 1

Proof state:
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1

Tactic:
exact ⟨sub_nonneg.2 ht.2, (sub_le_self_iff _).2 ht.1⟩

Result:
no goals

Proof state:
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : t ∈ Icc 0 1
⊢ 1 - t ∈ Icc 0 1

Tactic:
rw [mem_Icc] at *

Result:
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- The function `evenKernel a - L` has exponential decay at `+∞`, where `L = 1` if
`a = 0` and `L = 0` otherwise. -/
lemma isBigO_atTop_evenKernel_sub (a : UnitAddCircle) : ∃ p : ℝ, 0 < p ∧
    (evenKernel a · - (if a = 0 then 1 else 0)) =O[atTop] (rexp <| -p * ·)

Proof state:
case H.intro.intro
b p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
⊢ (fun x => evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =ᶠ[atTop] fun t =>
    HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0

Tactic:
filter_upwards [eventually_gt_atTop 0] with t h

Result:
case h
b p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
t : ℝ
h : 0 < t
⊢ (evenKernel (↑b) t - if ↑b = 0 then 1 else 0) = HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0

Proof state:
case H.intro.intro
b p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
⊢ ∃ p, 0 < p ∧ (fun x => evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =O[atTop] fun x => rexp (-p * x)

Tactic:
refine ⟨p, hp, (EventuallyEq.isBigO ?_).trans hp'⟩

Result:
case H.intro.intro
b p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
⊢ (fun x => evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =ᶠ[atTop] fun t =>
    HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0

Proof state:
case H
b : ℝ
⊢ ∃ p, 0 < p ∧ (fun x => evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =O[atTop] fun x => rexp (-p * x)

Tactic:
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub b

Result:
case H.intro.intro
b p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
⊢ ∃ p, 0 < p ∧ (fun x => evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =O[atTop] fun x => rexp (-p * x)

Proof state:
a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ (fun x => evenKernel a x - if a = 0 then 1 else 0) =O[atTop] fun x => rexp (-p * x)

Tactic:
induction a using QuotientAddGroup.induction_on with | H b =>
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub b
refine ⟨p, hp, (EventuallyEq.isBigO ?_).trans hp'⟩
filter_upwards [eventually_gt_atTop 0] with t h
simp [← (hasSum_int_evenKernel b h).tsum_eq, HurwitzKernelBounds.F_int, HurwitzKernelBounds.f_int]

Result:
no goals

Proof state:
case h
b p : ℝ
hp : 0 < p
hp' : (fun t => HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
t : ℝ
h : 0 < t
⊢ (evenKernel (↑b) t - if ↑b = 0 then 1 else 0) = HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0

Tactic:
simp [← (hasSum_int_evenKernel b h).tsum_eq, HurwitzKernelBounds.F_int, HurwitzKernelBounds.f_int]

Result:
no goals
-- Mathlib/Data/Finset/Sigma.lean
theorem mem_sigmaLift (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β)
    (x : Sigma γ) :
    x ∈ sigmaLift f a b ↔ ∃ (ha : a.1 = x.1) (hb : b.1 = x.1), x.2 ∈ f (ha ▸ a.2) (hb ▸ b.2)

Proof state:
case mk.mk.inl.mpr.intro.refl.intro.refl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx : x.snd ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) (⋯ ▸ ⟨x.1, b⟩.snd)
⊢ x ∈ sigmaLift f ⟨x.1, a⟩ ⟨x.1, b⟩

Tactic:
rw [sigmaLift, dif_pos rfl, mem_map]

Result:
case mk.mk.inl.mpr.intro.refl.intro.refl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx : x.snd ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) (⋯ ▸ ⟨x.1, b⟩.snd)
⊢ ∃ a_1 ∈ f (⋯ ▸ ⟨x.1, a⟩.snd) ⟨x.1, b⟩.snd, (Embedding.sigmaMk ⟨x.1, b⟩.fst) a_1 = x

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
⊢ x ∈ sigmaLift f a b ↔ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)

Tactic:
obtain ⟨⟨i, a⟩, j, b⟩ := a, b

Result:
case mk.mk
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨j, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)

Proof state:
case mk.mk.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ ∅ ↔ ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)

Tactic:
refine iff_of_false (not_mem_empty _) ?_

Result:
case mk.mk.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ ¬∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)
-- Mathlib/NumberTheory/Cyclotomic/Three.lean
/-- We have that `x ^ 3 - 1 = (x - 1) * (x - η) * (x - η ^ 2)`. -/
lemma cube_sub_one_eq_mul : x ^ 3 - 1 = (x - 1) * (x - η) * (x - η ^ 2)

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
⊢ x ^ 3 - x ^ 2 * (↑η ^ 2 + ↑η + 1) + x * (↑η ^ 2 + ↑η + ↑η ^ 3) - ↑η ^ 3 =
    x ^ 3 - x ^ 2 * (↑η ^ 2 + ↑η + 1) + x * (↑η ^ 2 + ↑η + 1) - 1

Tactic:
simp [hζ.toInteger_cube_eq_one]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
⊢ (x - 1) * (x - ↑η) * (x - ↑η ^ 2) = x ^ 3 - x ^ 2 * (↑η ^ 2 + ↑η + 1) + x * (↑η ^ 2 + ↑η + ↑η ^ 3) - ↑η ^ 3

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
⊢ (x - 1) * (x - ↑η) * (x - ↑η ^ 2) = x ^ 3 - 1

Tactic:
calc _ = x ^ 3 - x ^ 2 * (η ^ 2 + η + 1) + x * (η ^ 2 + η + η ^ 3) - η ^ 3 := by ring
_ = x ^ 3 - x ^ 2 * (η ^ 2 + η + 1) + x * (η ^ 2 + η + 1) - 1 := by
  simp [hζ.toInteger_cube_eq_one]
_ = x ^ 3 - 1 := by rw [eta_sq_add_eta_add_one hζ]; ring

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
⊢ x ^ 3 - x ^ 2 * 0 + x * 0 - 1 = x ^ 3 - 1

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
⊢ x ^ 3 - 1 = (x - 1) * (x - ↑η) * (x - ↑η ^ 2)

Tactic:
symm

Result:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
⊢ (x - 1) * (x - ↑η) * (x - ↑η ^ 2) = x ^ 3 - 1

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
⊢ x ^ 3 - x ^ 2 * (↑η ^ 2 + ↑η + 1) + x * (↑η ^ 2 + ↑η + 1) - 1 = x ^ 3 - 1

Tactic:
rw [eta_sq_add_eta_add_one hζ]

Result:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
⊢ x ^ 3 - x ^ 2 * 0 + x * 0 - 1 = x ^ 3 - 1
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSub_apply (w : ι → k) (p : ι → P) :
    s.weightedVSub p w = ∑ i ∈ s, w i • (p i -ᵥ Classical.choice S.nonempty)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
⊢ (s.weightedVSub p) w = ∑ i ∈ s, w i • (p i -ᵥ Classical.choice ⋯)

Tactic:
simp [weightedVSub, LinearMap.sum_apply]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_eq_arg_iff {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
    arg x = arg y ↔ (‖y‖ / ‖x‖ : ℂ) * x = y

Proof state:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x.arg = y.arg ↔ (↑‖y‖ / ↑‖x‖ * x).arg = y.arg

Tactic:
rw [← ofReal_div, arg_real_mul]

Result:
case hr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ 0 < ‖y‖ / ‖x‖

Proof state:
case hr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ 0 < ‖y‖ / ‖x‖

Tactic:
exact div_pos (norm_pos_iff.mpr hy) (norm_pos_iff.mpr hx)

Result:
no goals

Proof state:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x.arg = y.arg ↔ ↑‖y‖ / ↑‖x‖ * x = y

Tactic:
simp only [ext_norm_arg_iff, norm_mul, norm_div, norm_real, norm_norm,
  div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hx), eq_self_iff_true, true_and]

Result:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x.arg = y.arg ↔ (↑‖y‖ / ↑‖x‖ * x).arg = y.arg
-- Mathlib/CategoryTheory/Sites/ConstantSheaf.lean
/-- The counit of `constantSheafAdj` factors through the isomorphism `constantCommuteCompose`. -/
lemma constantSheafAdj_counit_w {T : C} (hT : IsTerminal T) :
    ((constantCommuteCompose J U).hom.app (F.val.obj ⟨T⟩)) ≫
      ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)) =
        ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F))

Proof state:
case h
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
⊢ ((constantCommuteCompose J U).hom.app (F.val.obj (op T)) ≫
        (constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).val =
    ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)).val

Tactic:
rw [instCategorySheaf_comp_val, constantCommuteCompose_hom_app_val, assoc, Iso.inv_comp_eq]

Result:
case h
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
⊢ sheafifyMap J (constComp Cᵒᵖ (F.val.obj (op T)) U).hom ≫
      ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).val =
    (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.val.obj (op T)))).hom ≫
      ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)).val

Proof state:
case h
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
⊢ sheafifyMap J (constComp Cᵒᵖ (F.val.obj (op T)) U).hom ≫
      ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).val =
    (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.val.obj (op T)))).hom ≫
      ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)).val

Tactic:
apply sheafify_hom_ext _ _ _ ((sheafCompose J U).obj F).cond

Result:
case h
C : Type u_1
inst✝⁶ : Category.{u_4, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_6, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{u_5, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
⊢ toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)) ⋙ U) ≫
      sheafifyMap J (constComp Cᵒᵖ (F.val.obj (op T)) U).hom ≫
        ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).val =
    toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T)) ⋙ U) ≫
      (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.val.obj (op T)))).hom ≫
        ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)).val
-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
/-- If the left-most part is not `{0}`, then the part containing `0` has at least two elements:
either because it's the left-most part, and then it's not just `0` by assumption, or because it's
not the left-most part and then, by increasingness of maximal elements in parts, it contains
a positive element. -/
lemma one_lt_partSize_index_zero (c : OrderedFinpartition (n + 1)) (hc : range (c.emb 0) ≠ {0}) :
    1 < c.partSize (c.index 0)

Proof state:
case inl
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb (c.index 0)) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 = 0
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
have : {0} ⊂ range (c.emb (c.index 0)) := by
  apply ssubset_of_subset_of_ne ?_ hc.symm
  simpa only [singleton_subset_iff, mem_range] using ⟨0, emb_zero c⟩

Result:
case inl
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb (c.index 0)) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 = 0
this : {0} ⊂ range (c.emb (c.index 0))
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

Proof state:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
⊢ {c.emb (c.index 0) 0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))

Tactic:
simp [insert_subset]

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
rcases eq_or_ne (c.index 0) 0 with h | h

Result:
case inl
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 = 0
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

Proof state:
case inl
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb (c.index 0)) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 = 0
this : {0} ⊂ range (c.emb (c.index 0))
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
simpa using Set.Finite.card_lt_card (finite_range _) this

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
/-- The universal property of a strongly cartesian morphism.

This lemma is more flexible with respect to non-definitional equalities than the field
`universal_property'` of `IsStronglyCartesian`. -/
lemma universal_property {R' : 𝒮} {a' : 𝒳} (g : R' ⟶ R) (f' : R' ⟶ S) (hf' : f' = g ≫ f)
    (φ' : a' ⟶ b) [IsHomLift p f' φ'] : ∃! χ : a' ⟶ a, IsHomLift p g χ ∧ χ ≫ φ = φ'

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R✝ : 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
a' : 𝒳
φ' : a' ⟶ b✝
R S : 𝒮
a b : 𝒳
g : p.obj a' ⟶ R✝
f : R✝ ⟶ p.obj b✝
inst✝¹ : p.IsStronglyCartesian f φ
hf' : p.map φ' = g ≫ f
inst✝ : p.IsHomLift (p.map φ') φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
clear a b R S

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R : 𝒮
a b : 𝒳
φ : a ⟶ b
a' : 𝒳
φ' : a' ⟶ b
g : p.obj a' ⟶ R
f : R ⟶ p.obj b
inst✝¹ : p.IsStronglyCartesian f φ
hf' : p.map φ' = g ≫ f
inst✝ : p.IsHomLift (p.map φ') φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsStronglyCartesian f φ
R' : 𝒮
a' : 𝒳
g : R' ⟶ R
f' : R' ⟶ S
hf' : f' = g ≫ f
φ' : a' ⟶ b
inst✝ : p.IsHomLift f' φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
subst_hom_lift p f' φ'

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R✝ : 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
a' : 𝒳
φ' : a' ⟶ b✝
R S : 𝒮
a b : 𝒳
g : p.obj a' ⟶ R✝
f : R✝ ⟶ p.obj b✝
inst✝¹ : p.IsStronglyCartesian f φ
hf' : p.map φ' = g ≫ f
inst✝ : p.IsHomLift (p.map φ') φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R : 𝒮
a b : 𝒳
φ : a ⟶ b
a' : 𝒳
φ' : a' ⟶ b
g : p.obj a' ⟶ R
f : R ⟶ p.obj b
inst✝¹ : p.IsStronglyCartesian f φ
hf' : p.map φ' = g ≫ f
inst✝ : p.IsHomLift (p.map φ') φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
have : p.IsHomLift (g ≫ f) φ' := (hf' ▸ inferInstance)

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R : 𝒮
a b : 𝒳
φ : a ⟶ b
a' : 𝒳
φ' : a' ⟶ b
g : p.obj a' ⟶ R
f : R ⟶ p.obj b
inst✝¹ : p.IsStronglyCartesian f φ
hf' : p.map φ' = g ≫ f
inst✝ : p.IsHomLift (p.map φ') φ'
this : p.IsHomLift (g ≫ f) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R : 𝒮
a b : 𝒳
φ : a ⟶ b
a' : 𝒳
φ' : a' ⟶ b
g : p.obj a' ⟶ R
f : R ⟶ p.obj b
inst✝¹ : p.IsStronglyCartesian f φ
hf' : p.map φ' = g ≫ f
inst✝ : p.IsHomLift (p.map φ') φ'
this : p.IsHomLift (g ≫ f) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
apply IsStronglyCartesian.universal_property' f

Result:
no goals
-- Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean
theorem ruzsaSzemerediNumberNat_lower_bound (n : ℕ) :
    (n / 3 - 2 : ℝ) * ↑((n - 3) / 6) * exp (-4 * sqrt (log ↑((n - 3) / 6))) ≤
      ruzsaSzemerediNumberNat n

Proof state:
case inl
n : ℕ
hn : ↑n / 3 - 2 ≤ 0
⊢ (↑n / 3 - 2) * (↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)

Tactic:
exact (mul_nonpos_of_nonpos_of_nonneg hn <| by positivity).trans (Nat.cast_nonneg _)

Result:
no goals

Proof state:
n : ℕ
⊢ (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6))) ≤ ↑(ruzsaSzemerediNumberNat n)

Tactic:
rw [mul_assoc]

Result:
n : ℕ
⊢ (↑n / 3 - 2) * (↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)

Proof state:
n : ℕ
hn : ↑n / 3 - 2 ≤ 0
⊢ 0 ≤ ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
⊢ (↑n / 3 - 2) * (↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)

Tactic:
obtain hn | hn := le_total (n / 3 - 2 : ℝ) 0

Result:
case inl
n : ℕ
hn : ↑n / 3 - 2 ≤ 0
⊢ (↑n / 3 - 2) * (↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)

case inr
n : ℕ
hn : 0 ≤ ↑n / 3 - 2
⊢ (↑n / 3 - 2) * (↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)

Proof state:
case inr
n : ℕ
hn : 0 ≤ ↑n / 3 - 2
⊢ (↑n / 3 - 2) * (↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)

Tactic:
exact
  (mul_le_mul_of_nonneg_left Behrend.roth_lower_bound hn).trans
    (rothNumberNat_le_ruzsaSzemerediNumberNat' _)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem NFBelow.mono {o b₁ b₂} (bb : b₁ ≤ b₂) (h : NFBelow o b₁) : NFBelow o b₂

Proof state:
case zero
o : ONote
b₁ b₂ b✝ : Ordinal.{0}
bb : b✝ ≤ b₂
⊢ NFBelow 0 b₂

Tactic:
exact zero

Result:
no goals

Proof state:
case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ e✝.NFBelow ?oadd'.eb

case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ a✝.NFBelow e✝.repr

case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ e✝.repr < b₂

case oadd'.eb
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ Ordinal.{0}

Tactic:
exacts [h₁, h₂, lt_of_lt_of_le h₃ bb]

Result:
no goals

Proof state:
case oadd'
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ (e✝.oadd n✝ a✝).NFBelow b₂

Tactic:
constructor

Result:
case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ e✝.NFBelow ?oadd'.eb

case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ a✝.NFBelow e✝.repr

case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ e✝.repr < b₂

case oadd'.eb
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ Ordinal.{0}

Proof state:
o : ONote
b₁ b₂ : Ordinal.{0}
bb : b₁ ≤ b₂
h : o.NFBelow b₁
⊢ o.NFBelow b₂

Tactic:
induction h with
| zero => exact zero
| oadd' h₁ h₂ h₃ _ _ => constructor; exacts [h₁, h₂, lt_of_lt_of_le h₃ bb]

Result:
no goals