harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/EpiMono.lean
theorem IsIso.of_mono_retraction' {X Y : C} {f : X ⟶ Y} (hf : SplitMono f) [Mono <| hf.retraction] :
    IsIso f :=
  ⟨⟨hf.retraction, ⟨by simp, (cancel_mono_id <| hf.retraction).mp (by simp)⟩⟩⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitMono f
inst✝ : Mono hf.retraction
⊢ (hf.retraction ≫ f) ≫ hf.retraction = hf.retraction

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitMono f
inst✝ : Mono hf.retraction
⊢ f ≫ hf.retraction = 𝟙 X

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :
    (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
cs : Array β
⊢ List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ List.foldl (fun bs a => bs ++ f a) cs as

Tactic:
induction as generalizing cs <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
this :
  ∀ (cs : Array β), List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ List.foldl (fun bs a => bs ++ f a) cs as
⊢ List.foldl (fun bs a => bs ++ f a) (#[] ++ f a) as = f a ++ List.foldl (fun bs a => bs ++ f a) #[] as

Tactic:
erw [empty_append]

Result:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
this :
  ∀ (cs : Array β), List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ List.foldl (fun bs a => bs ++ f a) cs as
⊢ List.foldl (fun bs a => bs ++ f a) (f a) as = f a ++ List.foldl (fun bs a => bs ++ f a) #[] as

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
⊢ ∀ (cs : Array β), List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ List.foldl (fun bs a => bs ++ f a) cs as

Tactic:
intro cs

Result:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
cs : Array β
⊢ List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ List.foldl (fun bs a => bs ++ f a) cs as

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
this :
  ∀ (cs : Array β), List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ List.foldl (fun bs a => bs ++ f a) cs as
⊢ List.foldl (fun bs a => bs ++ f a) (f a) as = f a ++ List.foldl (fun bs a => bs ++ f a) #[] as

Tactic:
simpa using this #[]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
⊢ List.foldl (fun bs a => bs ++ f a) (#[] ++ f a) as = f a ++ List.foldl (fun bs a => bs ++ f a) #[] as

Tactic:
suffices ∀ cs, List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as =
    f a ++ List.foldl (fun bs a => bs ++ f a) cs as by
  erw [empty_append] simpa using this #[]

Result:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
⊢ ∀ (cs : Array β), List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as = f a ++ List.foldl (fun bs a => bs ++ f a) cs as

Proof state:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
⊢ flatMap f (a :: as).toArray = f a ++ flatMap f as.toArray

Tactic:
simp [flatMap]

Result:
α : Type u_1
β : Type u_2
f : α → Array β
a : α
as : List α
⊢ List.foldl (fun bs a => bs ++ f a) (#[] ++ f a) as = f a ++ List.foldl (fun bs a => bs ++ f a) #[] as
-- Mathlib/Algebra/Order/Floor.lean
lemma ceil_eq_self_iff_mem (a : α) : ⌈a⌉ = a ↔ a ∈ Set.range Int.cast

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ↑⌈a⌉ = a ↔ a ∈ range Int.cast

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Finsupp.lean
theorem exists_of_mem_closure_range [Fintype ι] (hx : x ∈ closure (Set.range f)) :
    ∃ a : ι → ℤ, x = ∏ i, f i ^ a i

Proof state:
M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
hx : x ∈ closure (Set.range f)
⊢ ∃ a, x = ∏ i : ι, f i ^ a i

Tactic:
obtain ⟨a, rfl⟩ := exists_finsupp_of_mem_closure_range f x hx

Result:
case intro
M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
inst✝ : Fintype ι
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
⊢ ∃ a_1, (a.prod fun x1 x2 => f x1 ^ x2) = ∏ i : ι, f i ^ a_1 i

Proof state:
case intro
M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
inst✝ : Fintype ι
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
⊢ ∃ a_1, (a.prod fun x1 x2 => f x1 ^ x2) = ∏ i : ι, f i ^ a_1 i

Tactic:
exact ⟨a, by simp⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
inst✝ : Fintype ι
a : ι →₀ ℤ
hx : (a.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
⊢ (a.prod fun x1 x2 => f x1 ^ x2) = ∏ i : ι, f i ^ a i

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Submonoid/Inverses.lean
theorem leftInv_leftInv_eq (hS : S ≤ IsUnit.submonoid M) : S.leftInv.leftInv = S

Proof state:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x = ↑(IsUnit.unit ⋯)⁻¹⁻¹

Tactic:
rw [inv_inv (hS hx).unit]

Result:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x = ↑(IsUnit.unit ⋯)

Proof state:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = ↑(IsUnit.unit ⋯)⁻¹⁻¹
⊢ ↑(IsUnit.unit ⋯)⁻¹⁻¹ ∈ S.leftInv.leftInv

Tactic:
exact S.leftInv.unit_mem_leftInv _ (S.unit_mem_leftInv _ hx)

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = ↑(IsUnit.unit ⋯)⁻¹⁻¹
⊢ x ∈ S.leftInv.leftInv

Tactic:
rw [this]

Result:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = ↑(IsUnit.unit ⋯)⁻¹⁻¹
⊢ ↑(IsUnit.unit ⋯)⁻¹⁻¹ ∈ S.leftInv.leftInv

Proof state:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ S ≤ S.leftInv.leftInv

Tactic:
intro x hx

Result:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x ∈ S.leftInv.leftInv

Proof state:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x ∈ S.leftInv.leftInv

Tactic:
have : x = ((hS hx).unit⁻¹⁻¹ : Mˣ) := by
  rw [inv_inv (hS hx).unit]
  rfl

Result:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
this : x = ↑(IsUnit.unit ⋯)⁻¹⁻¹
⊢ x ∈ S.leftInv.leftInv

Proof state:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : M
hx : x ∈ S
⊢ x = ↑(IsUnit.unit ⋯)

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ S.leftInv.leftInv = S

Tactic:
refine le_antisymm S.leftInv_leftInv_le ?_

Result:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ S ≤ S.leftInv.leftInv
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_infty : ContDiff 𝕜 ∞ f ↔ ∀ n : ℕ, ContDiff 𝕜 n f

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ ContDiff 𝕜 ∞ f ↔ ∀ (n : ℕ), ContDiff 𝕜 (↑n) f

Tactic:
simp [contDiffOn_univ.symm, contDiffOn_infty]

Result:
no goals
-- Mathlib/FieldTheory/CardinalEmb.lean
theorem equivSucc_coherence (i f) : (equivSucc i f).1 = embFunctor F E (le_succ i) f

Proof state:
case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
f : ↥(filtration (⊤⁺)) →ₐ[F] Ē
⊢ ((equivSucc ⊤) f).1 = embFunctor F E ⋯ f

case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
a✝ : (Module.rank F E).ord.toType
f : ↥(filtration (↑a✝⁺)) →ₐ[F] Ē
⊢ ((equivSucc ↑a✝) f).1 = embFunctor F E ⋯ f

Tactic:
exacts [rfl, succEquiv_coherence _ f]

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.toType
f : ↥(filtration (i⁺)) →ₐ[F] Ē
⊢ ((equivSucc i) f).1 = embFunctor F E ⋯ f

Tactic:
cases i

Result:
case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
f : ↥(filtration (⊤⁺)) →ₐ[F] Ē
⊢ ((equivSucc ⊤) f).1 = embFunctor F E ⋯ f

case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
a✝ : (Module.rank F E).ord.toType
f : ↥(filtration (↑a✝⁺)) →ₐ[F] Ē
⊢ ((equivSucc ↑a✝) f).1 = embFunctor F E ⋯ f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWith_foldr_eq_zip_foldr {f : α → β → γ} (i : δ):
    (zipWith f l₁ l₂).foldr g i = (zip l₁ l₂).foldr (fun p r => g (f p.1 p.2) r) i

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l₁ : List α
l₂ : List β
g : γ → δ → δ
f : α → β → γ
i : δ
⊢ foldr g i (zipWith f l₁ l₂) = foldr (fun p r => g (f p.fst p.snd) r) i (l₁.zip l₂)

Tactic:
induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem bind {n f g} (hf : @Partrec' n f) (hg : @Partrec' (n + 1) g) :
    @Partrec' n fun v => (f v).bind fun a => g (a ::ᵥ v) :=
  (@comp n (n + 1) g (fun i => Fin.cases f (fun i v => some (v.get i)) i) hg fun i => by
      refine Fin.cases ?_ (fun i => ?_) i <;> simp [*]
      exact prim (Nat.Primrec'.get _)).of_eq
    fun v => by simp [mOfFn, Part.bind_assoc, pure]

Proof state:
n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
v : List.Vector ℕ n
⊢ (mOfFn fun i => Fin.cases f (fun i v => ↑(some (v.get i))) i v) >>= g = (f v).bind fun a => g (a ::ᵥ v)

Tactic:
simp [mOfFn, Part.bind_assoc, pure]

Result:
no goals

Proof state:
n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i : Fin (n + 1)
⊢ Partrec' ((fun i => Fin.cases f (fun i v => ↑(some (v.get i))) i) i)

Tactic:
refine Fin.cases ?_ (fun i => ?_) i <;> simp [*]

Result:
case refine_2
n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i✝ : Fin (n + 1)
i : Fin n
⊢ Partrec' fun v => Part.some (v.get i)

Proof state:
case refine_2
n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i✝ : Fin (n + 1)
i : Fin n
⊢ Partrec' fun v => Part.some (v.get i)

Tactic:
exact prim (Nat.Primrec'.get _)

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Basic.lean
theorem isNilpotent_sub (h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) :
    IsNilpotent (x - y)

Proof state:
R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x - y)

Tactic:
rw [sub_eq_add_neg]

Result:
R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x + -y)

Proof state:
R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x - y)

Tactic:
rw [← isNilpotent_neg_iff] at hy

Result:
R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x - y)

Proof state:
R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x - y)

Tactic:
rw [← neg_right_iff] at h_comm

Result:
R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x - y)

Proof state:
R : Type u_1
x y : R
inst✝ : Ring R
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x + -y)

Tactic:
exact h_comm.isNilpotent_add hx hy

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem isClosed_frontier : IsClosed (frontier s)

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ IsClosed (closure s ∩ closure sᶜ)

Tactic:
exact IsClosed.inter isClosed_closure isClosed_closure

Result:
no goals

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ IsClosed (frontier s)

Tactic:
rw [frontier_eq_closure_inter_closure]

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ IsClosed (closure s ∩ closure sᶜ)
-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_floor_atTop : Tendsto (floor : α → ℤ) atTop atTop :=
  floor_mono.tendsto_atTop_atTop fun b =>
    ⟨(b + 1 : ℤ), by rw [floor_intCast]; exact (lt_add_one _).le⟩

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b ≤ ⌊↑(b + 1)⌋

Tactic:
rw [floor_intCast]

Result:
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b ≤ b + 1

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
b : ℤ
⊢ b ≤ b + 1

Tactic:
exact (lt_add_one _).le

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorRightHomEquiv_tensor {X X' Y Y' Z Z' : C} [ExactPairing Y Y'] (f : X ⟶ Z ⊗ Y')
    (g : X' ⟶ Z') :
    (tensorRightHomEquiv (X' ⊗ X) Y Y' (Z' ⊗ Z)).symm ((g ⊗ f) ≫ (α_ _ _ _).inv) =
      (α_ _ _ _).hom ≫ (g ⊗ (tensorRightHomEquiv X Y Y' Z).symm f)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y Y' Z Z' : C
inst✝ : ExactPairing Y Y'
f : X ⟶ Z ⊗ Y'
g : X' ⟶ Z'
⊢ (tensorRightHomEquiv (X' ⊗ X) Y Y' (Z' ⊗ Z)).symm ((g ⊗ f) ≫ (α_ Z' Z Y').inv) =
    (α_ X' X Y).hom ≫ (g ⊗ (tensorRightHomEquiv X Y Y' Z).symm f)

Tactic:
simp [tensorRightHomEquiv, tensorHom_def]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem DifferentiableAt.hasFDerivAt (h : DifferentiableAt 𝕜 f x) :
    HasFDerivAt f (fderiv 𝕜 f x) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : DifferentiableAt 𝕜 f x
⊢ HasFDerivAt f (fderiv 𝕜 f x) x

Tactic:
rw [fderiv, ← hasFDerivWithinAt_univ]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : DifferentiableAt 𝕜 f x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f univ x) univ x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : DifferentiableWithinAt 𝕜 f univ x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f univ x) univ x

Tactic:
exact h.hasFDerivWithinAt

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : DifferentiableAt 𝕜 f x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f univ x) univ x

Tactic:
rw [← differentiableWithinAt_univ] at h

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : DifferentiableWithinAt 𝕜 f univ x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f univ x) univ x
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_add_of_principal_mul (ho : Principal (· * ·) o) (ho₂ : o ≠ 2) :
    Principal (· + ·) o

Proof state:
case inr
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ a + b ≤ a ⊔ b + a ⊔ b

Tactic:
exact add_le_add (le_max_left a b) (le_max_right a b)

Result:
no goals

Proof state:
case inl
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂ : o ≠ 2
ho₁ : o < succ 1
⊢ Principal (fun x1 x2 => x1 + x2) o

Tactic:
rw [lt_succ_iff] at ho₁

Result:
case inl
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂ : o ≠ 2
ho₁ : o ≤ 1
⊢ Principal (fun x1 x2 => x1 + x2) o

Proof state:
case inr
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
⊢ Principal (fun x1 x2 => x1 + x2) o

Tactic:
refine fun a b hao hbo => lt_of_le_of_lt ?_ (ho (max_lt hao hbo) ho₂)

Result:
case inr
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 => x1 + x2) a b ≤ (fun x1 x2 => x1 * x2) (a ⊔ b) 2

Proof state:
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂ : o ≠ 2
⊢ Principal (fun x1 x2 => x1 + x2) o

Tactic:
rcases lt_or_gt_of_ne ho₂ with ho₁ | ho₂

Result:
case inl
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂ : o ≠ 2
ho₁ : o < 2
⊢ Principal (fun x1 x2 => x1 + x2) o

case inr
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
⊢ Principal (fun x1 x2 => x1 + x2) o

Proof state:
case inl
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂ : o ≠ 2
ho₁ : o ≤ 1
⊢ Principal (fun x1 x2 => x1 + x2) o

Tactic:
exact principal_add_of_le_one ho₁

Result:
no goals

Proof state:
case inr
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ a + b ≤ (a ⊔ b) * 2

Tactic:
rw [← one_add_one_eq_two, mul_add, mul_one]

Result:
case inr
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ a + b ≤ a ⊔ b + a ⊔ b

Proof state:
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂ : o ≠ 2
ho₁ : o < 2
⊢ o < succ 1

Tactic:
rwa [succ_one]

Result:
no goals

Proof state:
case inl
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂ : o ≠ 2
ho₁ : o < 2
⊢ Principal (fun x1 x2 => x1 + x2) o

Tactic:
replace ho₁ : o < succ 1 := by rwa [succ_one]

Result:
case inl
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂ : o ≠ 2
ho₁ : o < succ 1
⊢ Principal (fun x1 x2 => x1 + x2) o

Proof state:
case inr
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 => x1 + x2) a b ≤ (fun x1 x2 => x1 * x2) (a ⊔ b) 2

Tactic:
dsimp only

Result:
case inr
o : Ordinal.{u}
ho : Principal (fun x1 x2 => x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : o > 2
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ a + b ≤ (a ⊔ b) * 2
-- Mathlib/SetTheory/Nimber/Basic.lean
theorem add_cancel_left (a b : Nimber) : a + (a + b) = b

Proof state:
a b : Nimber
⊢ a + (a + b) = b

Tactic:
rw [← add_assoc, add_self, zero_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem addEquality_sat (w : c + Coeffs.dot x y = 0) :
    Constraint.sat' { lowerBound := some (-c), upperBound := some (-c) } x y

Proof state:
c : Int
x y : Coeffs
w : c + x.dot y = 0
⊢ -c ≤ x.dot y ∧ x.dot y ≤ -c

Tactic:
rw [Int.eq_iff_le_and_ge] at w

Result:
c : Int
x y : Coeffs
w : c + x.dot y ≤ 0 ∧ 0 ≤ c + x.dot y
⊢ -c ≤ x.dot y ∧ x.dot y ≤ -c

Proof state:
c : Int
x y : Coeffs
w : c + x.dot y ≤ 0 ∧ 0 ≤ c + x.dot y
⊢ -c ≤ x.dot y ∧ x.dot y ≤ -c

Tactic:
rwa [Int.add_le_zero_iff_le_neg', Int.add_nonnneg_iff_neg_le', and_comm] at w

Result:
no goals

Proof state:
c : Int
x y : Coeffs
w : c + x.dot y = 0
⊢ { lowerBound := some (-c), upperBound := some (-c) }.sat' x y = true

Tactic:
simp [Constraint.sat', Constraint.sat]

Result:
c : Int
x y : Coeffs
w : c + x.dot y = 0
⊢ -c ≤ x.dot y ∧ x.dot y ≤ -c
-- Mathlib/Data/List/Basic.lean
theorem getLast?_append_of_ne_nil (l₁ : List α) :
    ∀ {l₂ : List α} (_ : l₂ ≠ []), getLast? (l₁ ++ l₂) = getLast? l₂
  | [], hl₂ => by contradiction
  | b :: l₂, _ => getLast?_append_cons l₁ b l₂

Proof state:
α : Type u
l₁ : List α
hl₂ : [] ≠ []
⊢ (l₁ ++ []).getLast? = [].getLast?

Tactic:
contradiction

Result:
no goals
-- Mathlib/Topology/Gluing.lean
theorem MkCore.t_inv (h : MkCore) (i j : h.J) (x : h.V j i) : h.t i j ((h.t j i) x) = x

Proof state:
case refine_2
h : MkCore
i j : h.J
x : ↥(h.V j i)
this : ↑((ConcreteCategory.hom (h.t i j)) ⟨↑((ConcreteCategory.hom (h.t j i)) x), ⋯⟩) = ↑(id ⟨↑x, ?refine_1⟩)
⊢ (ConcreteCategory.hom (h.t i j)) ((ConcreteCategory.hom (h.t j i)) x) = x

Tactic:
convert Subtype.eq this

Result:
no goals

Proof state:
case refine_1
h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ ↑x ∈ h.V j j

Tactic:
rw [h.V_id]

Result:
case refine_1
h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ ↑x ∈ ⊤

Proof state:
case refine_2
h : MkCore
i j : h.J
x : ↥(h.V j i)
this :
  ↑((ConcreteCategory.hom (h.t i j)) ⟨↑((ConcreteCategory.hom (h.t j i)) x), ⋯⟩) =
    ↑((ConcreteCategory.hom (h.t j j)) ⟨↑x, ?refine_1⟩)
⊢ (ConcreteCategory.hom (h.t i j)) ((ConcreteCategory.hom (h.t j i)) x) = x

Tactic:
rw [h.t_id] at this

Result:
case refine_2
h : MkCore
i j : h.J
x : ↥(h.V j i)
this : ↑((ConcreteCategory.hom (h.t i j)) ⟨↑((ConcreteCategory.hom (h.t j i)) x), ⋯⟩) = ↑(id ⟨↑x, ?refine_1⟩)
⊢ (ConcreteCategory.hom (h.t i j)) ((ConcreteCategory.hom (h.t j i)) x) = x

Proof state:
case refine_1
h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ ↑x ∈ ⊤

Tactic:
trivial

Result:
no goals

Proof state:
h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ (ConcreteCategory.hom (h.t i j)) ((ConcreteCategory.hom (h.t j i)) x) = x

Tactic:
have := h.cocycle j i j x ?_

Result:
case refine_2
h : MkCore
i j : h.J
x : ↥(h.V j i)
this :
  ↑((ConcreteCategory.hom (h.t i j)) ⟨↑((ConcreteCategory.hom (h.t j i)) x), ⋯⟩) =
    ↑((ConcreteCategory.hom (h.t j j)) ⟨↑x, ?refine_1⟩)
⊢ (ConcreteCategory.hom (h.t i j)) ((ConcreteCategory.hom (h.t j i)) x) = x

case refine_1
h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ ↑x ∈ h.V j j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem reverse_replicate {n : Nat} {x : BitVec w} :
    (x.replicate n).reverse = (x.reverse).replicate n

Proof state:
case succ
w : Nat
x : BitVec w
n : Nat
ih : (replicate n x).reverse = replicate n x.reverse
⊢ (BitVec.cast ⋯ (replicate n x ++ x)).reverse = replicate (n + 1) x.reverse

Tactic:
simp [reverse_append, ih]

Result:
no goals

Proof state:
case zero
w : Nat
x : BitVec w
⊢ (replicate 0 x).reverse = replicate 0 x.reverse

Tactic:
rfl

Result:
no goals

Proof state:
w n : Nat
x : BitVec w
⊢ (replicate n x).reverse = replicate n x.reverse

Tactic:
induction n with
| zero => rfl
| succ n ih =>
  conv => lhs; simp only [replicate_succ']
  simp [reverse_append, ih]

Result:
no goals

Proof state:
case succ
w : Nat
x : BitVec w
n : Nat
ih : (replicate n x).reverse = replicate n x.reverse
⊢ (replicate (n + 1) x).reverse = replicate (n + 1) x.reverse

Tactic:
conv => lhs; simp only [replicate_succ']

Result:
case succ
w : Nat
x : BitVec w
n : Nat
ih : (replicate n x).reverse = replicate n x.reverse
⊢ (BitVec.cast ⋯ (replicate n x ++ x)).reverse = replicate (n + 1) x.reverse