harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_iff_nat_mul_le_aux (h₀ : (∀ x, 0 ≤ ‖f x‖) ∨ ∀ x, 0 ≤ ‖g x‖) :
    f =o[l] g ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖f x‖ ≤ ‖g x‖

Proof state:
case mpr.intro
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < ↑n
hn₀ : 0 < ↑n
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖

Tactic:
refine ((isBigOWith_inv hn₀).2 (H n)).bound.mono fun x hfg => ?_

Result:
case mpr.intro
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < ↑n
hn₀ : 0 < ↑n
x : α
hfg : ‖f x‖ ≤ (↑n)⁻¹ * ‖g x‖
⊢ ‖f x‖ ≤ ε * ‖g x‖

Proof state:
case mpr.intro
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < ↑n
hn₀ : 0 < ↑n
x : α
hfg : ‖f x‖ ≤ (↑n)⁻¹ * ‖g x‖
hf : ∀ (x : α), 0 ≤ ‖f x‖
⊢ 0 < (↑n)⁻¹

Tactic:
exact inv_pos.2 hn₀

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n

Proof state:
n : Nat
a b : Fin n
⊢ ↑(a - b) = (n - ↑b + ↑a) % n

Tactic:
cases a

Result:
case mk
n : Nat
b : Fin n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ↑(⟨val✝, isLt✝⟩ - b) = (n - ↑b + ↑⟨val✝, isLt✝⟩) % n

Proof state:
case mk
n : Nat
b : Fin n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ↑(⟨val✝, isLt✝⟩ - b) = (n - ↑b + ↑⟨val✝, isLt✝⟩) % n

Tactic:
cases b

Result:
case mk.mk
n val✝¹ : Nat
isLt✝¹ : val✝¹ < n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ↑(⟨val✝¹, isLt✝¹⟩ - ⟨val✝, isLt✝⟩) = (n - ↑⟨val✝, isLt✝⟩ + ↑⟨val✝¹, isLt✝¹⟩) % n

Proof state:
case mk.mk
n val✝¹ : Nat
isLt✝¹ : val✝¹ < n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ↑(⟨val✝¹, isLt✝¹⟩ - ⟨val✝, isLt✝⟩) = (n - ↑⟨val✝, isLt✝⟩ + ↑⟨val✝¹, isLt✝¹⟩) % n

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Sets/Opens.lean
theorem eq_bot_or_top {α} [t : TopologicalSpace α] (h : t = ⊤) (U : Opens α) : U = ⊥ ∨ U = ⊤

Proof state:
α : Type u_5
U : Opens α
this : TopologicalSpace α := ⊤
⊢ IsOpen ↑U

Tactic:
exact U.2

Result:
no goals

Proof state:
α : Type u_5
t : TopologicalSpace α
h : t = ⊤
U : Opens α
⊢ U = ⊥ ∨ U = ⊤

Tactic:
subst h

Result:
α : Type u_5
U : Opens α
⊢ U = ⊥ ∨ U = ⊤

Proof state:
α : Type u_5
U : Opens α
this : TopologicalSpace α := ⊤
⊢ U = ⊥ ∨ U = ⊤

Tactic:
rw [← coe_eq_empty, ← coe_eq_univ, ← isOpen_top_iff]

Result:
α : Type u_5
U : Opens α
this : TopologicalSpace α := ⊤
⊢ IsOpen ↑U

Proof state:
α : Type u_5
U : Opens α
⊢ U = ⊥ ∨ U = ⊤

Tactic:
letI : TopologicalSpace α := ⊤

Result:
α : Type u_5
U : Opens α
this : TopologicalSpace α := ⊤
⊢ U = ⊥ ∨ U = ⊤
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_mkVector : (mkVector n a).map f = mkVector n (f a)

Proof state:
n : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
⊢ map f (mkVector n a) = mkVector n (f a)

Tactic:
rw [← toArray_inj]

Result:
n : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
⊢ (map f (mkVector n a)).toArray = (mkVector n (f a)).toArray

Proof state:
n : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
⊢ (map f (mkVector n a)).toArray = (mkVector n (f a)).toArray

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
lemma nonneg_iff_isSelfAdjoint_and_spectrumRestricts {a : A} :
    0 ≤ a ↔ IsSelfAdjoint a ∧ SpectrumRestricts a ContinuousMap.realToNNReal

Proof state:
A : Type u_1
inst✝⁷ : Ring A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarRing A
inst✝⁴ : StarOrderedRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ 0 ≤ a ↔ IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal

Tactic:
refine ⟨fun ha ↦ ⟨.of_nonneg ha, .nnreal_of_nonneg ha⟩, ?_⟩

Result:
A : Type u_1
inst✝⁷ : Ring A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarRing A
inst✝⁴ : StarOrderedRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal → 0 ≤ a

Proof state:
case intro.intro.intro.intro
A : Type u_1
inst✝⁷ : Ring A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarRing A
inst✝⁴ : StarOrderedRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
x : A
hx : IsSelfAdjoint x
ha₁ : IsSelfAdjoint (x ^ 2)
ha₂ : SpectrumRestricts (x ^ 2) ⇑ContinuousMap.realToNNReal
⊢ 0 ≤ x ^ 2

Tactic:
simpa [sq, hx.star_eq] using star_mul_self_nonneg x

Result:
no goals

Proof state:
case intro
A : Type u_1
inst✝⁷ : Ring A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarRing A
inst✝⁴ : StarOrderedRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ 0 ≤ a

Tactic:
obtain ⟨x, hx, -, rfl⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_spectrumRestricts ha₁ ha₂

Result:
case intro.intro.intro.intro
A : Type u_1
inst✝⁷ : Ring A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarRing A
inst✝⁴ : StarOrderedRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
x : A
hx : IsSelfAdjoint x
ha₁ : IsSelfAdjoint (x ^ 2)
ha₂ : SpectrumRestricts (x ^ 2) ⇑ContinuousMap.realToNNReal
⊢ 0 ≤ x ^ 2

Proof state:
A : Type u_1
inst✝⁷ : Ring A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarRing A
inst✝⁴ : StarOrderedRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal → 0 ≤ a

Tactic:
rintro ⟨ha₁, ha₂⟩

Result:
case intro
A : Type u_1
inst✝⁷ : Ring A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarRing A
inst✝⁴ : StarOrderedRing A
inst✝³ : TopologicalSpace A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha₁ : IsSelfAdjoint a
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ 0 ≤ a
-- Mathlib/Analysis/RCLike/Basic.lean
theorem div_im (z w : K) : im (z / w) = im z * re w / normSq w - re z * im w / normSq w

Proof state:
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ im (z / w) = im z * re w / normSq w - re z * im w / normSq w

Tactic:
simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm, neg_mul, mul_neg, map_neg,
  rclike_simps]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
lemma leftUnshift_v {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n')
    (p q : ℤ) (hpq : p + n = q) (p' : ℤ) (hp' : p' + n' = q) :
    (γ.leftUnshift n hn).v p q hpq = (a * n' + ((a * (a-1))/2)).negOnePow •
      (K.shiftFunctorObjXIso a p' p (by omega)).inv ≫ γ.v p' q (by omega)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p' + n' = q
⊢ p' = p - a

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p' + n' = q
⊢ (γ.leftUnshift n hn).v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p' p ⋯).inv ≫ γ.v p' q ⋯

Tactic:
obtain rfl : p' = p - a := by omega

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
p q : ℤ
hpq : p + n = q
hp' : p - a + n' = q
⊢ (γ.leftUnshift n hn).v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (p - a) p ⋯).inv ≫ γ.v (p - a) q ⋯

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
p q : ℤ
hpq : p + n = q
hp' : p - a + n' = q
⊢ (γ.leftUnshift n hn).v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (p - a) p ⋯).inv ≫ γ.v (p - a) q ⋯

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ : ℤ
γ✝ γ₁ γ₂ : Cochain K L n✝
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p' + n' = q
⊢ p = p' + a

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ : ℤ
γ✝ γ₁ γ₂ : Cochain K L n✝
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p' + n' = q
⊢ p' + n' = q

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem Normal.map {H : Subgroup G} (h : H.Normal) (f : G →* N) (hf : Function.Surjective f) :
    (H.map f).Normal

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ (Subgroup.map f H).Normal

Tactic:
rw [← normalizer_eq_top_iff, ← top_le_iff, ← f.range_eq_top_of_surjective hf, f.range_eq_map,
  ← H.normalizer_eq_top]

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ Subgroup.map f H.normalizer ≤ (Subgroup.map f H).normalizer

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ Subgroup.map f H.normalizer ≤ (Subgroup.map f H).normalizer

Tactic:
exact le_normalizer_map _

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem j_of_isCharThreeJNeZeroNF_of_char_three : W.j = -W.a₂ ^ 3 / W.a₆

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : -W.a₂ ^ 3 * W.a₆ ≠ 0
⊢ (W.a₂ ^ 2) ^ 3 * W.a₆ = -W.a₂ ^ 3 * (-W.a₂ ^ 3 * W.a₆)

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
⊢ W.j = -W.a₂ ^ 3 / W.a₆

Tactic:
have h := W.Δ'.ne_zero

Result:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : ↑W.Δ' ≠ 0
⊢ W.j = -W.a₂ ^ 3 / W.a₆

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : -W.a₂ ^ 3 * W.a₆ ≠ 0
⊢ W.j = -W.a₂ ^ 3 / W.a₆

Tactic:
rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
  c₄_of_isCharThreeJNeZeroNF_of_char_three, Δ_of_isCharThreeJNeZeroNF_of_char_three,
  div_eq_div_iff h (right_ne_zero_of_mul h)]

Result:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : -W.a₂ ^ 3 * W.a₆ ≠ 0
⊢ (W.a₂ ^ 2) ^ 3 * W.a₆ = -W.a₂ ^ 3 * (-W.a₂ ^ 3 * W.a₆)

Proof state:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : ↑W.Δ' ≠ 0
⊢ W.j = -W.a₂ ^ 3 / W.a₆

Tactic:
rw [coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three] at h

Result:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : -W.a₂ ^ 3 * W.a₆ ≠ 0
⊢ W.j = -W.a₂ ^ 3 / W.a₆
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem of_mulOpposite
    (h : UniqueMul (B.map ⟨_, op_injective⟩) (A.map ⟨_, op_injective⟩) (op b0) (op a0)) :
    UniqueMul A B a0 b0 := fun a b aA bB ab ↦ by
  simpa [and_comm] using h (mem_map_of_mem _ bB) (mem_map_of_mem _ aA) (congr_arg op ab)

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul (map { toFun := op, inj' := ⋯ } B) (map { toFun := op, inj' := ⋯ } A) (op b0) (op a0)
a b : G
aA : a ∈ A
bB : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
simpa [and_comm] using h (mem_map_of_mem _ bB) (mem_map_of_mem _ aA) (congr_arg op ab)

Result:
no goals
-- Mathlib/Order/Height.lean
theorem chainHeight_add_le_chainHeight_add (s : Set α) (t : Set β) (n m : ℕ) :
    s.chainHeight + n ≤ t.chainHeight + m ↔
      ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, length l + n ≤ length l' + m

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
k : ℕ
this : (∃ l ∈ t.subchain, l.length = k) ↔ ∃ l ∈ t.subchain, k ≤ l.length
⊢ ∃ l ∈ t.subchain, k ≤ l.length

Tactic:
obtain ⟨l, hs, hl⟩ := h (k + m)

Result:
case pos.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
k : ℕ
this : (∃ l ∈ t.subchain, l.length = k) ↔ ∃ l ∈ t.subchain, k ≤ l.length
l : List α
hs : l ∈ s.subchain
hl : l.length = k + m
⊢ ∃ l ∈ t.subchain, k ≤ l.length

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
⊢ ∀ (n : ℕ), ∃ l ∈ t.subchain, l.length = n

Tactic:
intro k

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
k : ℕ
⊢ ∃ l ∈ t.subchain, l.length = k

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
⊢ s.chainHeight + ↑n ≤ t.chainHeight + ↑m

Tactic:
by_cases h : s.chainHeight = ⊤

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : s.chainHeight = ⊤
⊢ s.chainHeight + ↑n ≤ t.chainHeight + ↑m

case neg
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
s : Set α
t : Set β
n m : ℕ
H : ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
h : ¬s.chainHeight = ⊤
⊢ s.chainHeight + ↑n ≤ t.chainHeight + ↑m
-- Mathlib/Logic/Encodable/Basic.lean
theorem decode_ge_two (n) (h : 2 ≤ n) : (decode n : Option Bool) = none

Proof state:
n : ℕ
h : 2 ≤ n
⊢ decodeSum n = none

Tactic:
have : 1 ≤ n / 2 := by
  rw [Nat.le_div_iff_mul_le]
  exacts [h, by decide]

Result:
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
⊢ decodeSum n = none

Proof state:
n : ℕ
h : 2 ≤ n
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
n : ℕ
h : 2 ≤ n
⊢ 1 * 2 ≤ n

n : ℕ
h : 2 ≤ n
⊢ 0 < 2

Tactic:
exacts [h, by decide]

Result:
no goals

Proof state:
case intro
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ decodeSum n = none

Tactic:
simp only [decodeSum, boddDiv2_eq, div2_val]

Result:
case intro
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ (match (n.bodd, n / 2) with
    | (false, m) => Option.map Sum.inl (decode m)
    | (fst, m) => Option.map Sum.inr (decode m)) =
    none

Proof state:
n : ℕ
h : 2 ≤ n
⊢ 1 ≤ n / 2

Tactic:
rw [Nat.le_div_iff_mul_le]

Result:
n : ℕ
h : 2 ≤ n
⊢ 1 * 2 ≤ n

n : ℕ
h : 2 ≤ n
⊢ 0 < 2

Proof state:
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ (decodeSum n).bind (some ∘ ⇑Equiv.boolEquivPUnitSumPUnit.symm) = none

Tactic:
rw [this]

Result:
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ none.bind (some ∘ ⇑Equiv.boolEquivPUnitSumPUnit.symm) = none

Proof state:
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ decode n = none

Tactic:
change (decodeSum n).bind _ = none

Result:
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ (decodeSum n).bind (some ∘ ⇑Equiv.boolEquivPUnitSumPUnit.symm) = none

Proof state:
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ none.bind (some ∘ ⇑Equiv.boolEquivPUnitSumPUnit.symm) = none

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
h : 2 ≤ n
⊢ decode n = none

Tactic:
suffices decodeSum n = none by
  change (decodeSum n).bind _ = none
  rw [this]
  rfl

Result:
n : ℕ
h : 2 ≤ n
⊢ decodeSum n = none

Proof state:
case intro
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ (match (n.bodd, n / 2) with
    | (false, m) => Option.map Sum.inl (decode m)
    | (fst, m) => Option.map Sum.inr (decode m)) =
    none

Tactic:
cases bodd n <;> simp [e]

Result:
no goals

Proof state:
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
⊢ decodeSum n = none

Tactic:
obtain ⟨m, e⟩ := exists_eq_succ_of_ne_zero (_root_.ne_of_gt this)

Result:
case intro
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ decodeSum n = none
-- Mathlib/RingTheory/UniqueFactorizationDomain/Ideal.lean
/-- The ascending chain condition on principal ideals in a domain is sufficient to prove that
the domain is `WfDvdMonoid`. -/
lemma WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt [CommSemiring α] [IsDomain α]
    (h : {I : Ideal α | I.IsPrincipal}.WellFoundedOn (· > ·)) :
    WfDvdMonoid α

Proof state:
case wf
α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2
this : WellFounded fun x1 x2 => x1 > x2
⊢ WellFounded DvdNotUnit

Tactic:
convert InvImage.wf (fun a => ⟨Ideal.span ({a} : Set α), _, rfl⟩) this

Result:
case h.e'_2
α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2
this : WellFounded fun x1 x2 => x1 > x2
⊢ DvdNotUnit = InvImage (fun x1 x2 => x1 > x2) fun a => ⟨Ideal.span {a}, ⋯⟩

Proof state:
case h.e'_2.h.h.a
α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2
this : WellFounded fun x1 x2 => x1 > x2
x✝¹ x✝ : α
⊢ DvdNotUnit x✝¹ x✝ ↔ InvImage (fun x1 x2 => x1 > x2) (fun a => ⟨Ideal.span {a}, ⋯⟩) x✝¹ x✝

Tactic:
exact Ideal.span_singleton_lt_span_singleton.symm

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2
this : WellFounded fun x1 x2 => x1 > x2
⊢ WfDvdMonoid α

Tactic:
constructor

Result:
case wf
α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2
this : WellFounded fun x1 x2 => x1 > x2
⊢ WellFounded DvdNotUnit

Proof state:
case h.e'_2
α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2
this : WellFounded fun x1 x2 => x1 > x2
⊢ DvdNotUnit = InvImage (fun x1 x2 => x1 > x2) fun a => ⟨Ideal.span {a}, ⋯⟩

Tactic:
ext

Result:
case h.e'_2.h.h.a
α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2
this : WellFounded fun x1 x2 => x1 > x2
x✝¹ x✝ : α
⊢ DvdNotUnit x✝¹ x✝ ↔ InvImage (fun x1 x2 => x1 > x2) (fun a => ⟨Ideal.span {a}, ⋯⟩) x✝¹ x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_prefix_take_left (l : List α) {m n : Nat} (h : m ≤ n) : take m l <+: take n l

Proof state:
α : Type u_1
l : List α
m n : Nat
h : m ≤ n
⊢ ∀ (i : Nat) (h : i < (take m l).length), (take n l)[i]? = some (take m l)[i]

Tactic:
intro i w

Result:
α : Type u_1
l : List α
m n : Nat
h : m ≤ n
i : Nat
w : i < (take m l).length
⊢ (take n l)[i]? = some (take m l)[i]

Proof state:
α : Type u_1
l : List α
m n : Nat
h : m ≤ n
i : Nat
w : i < (take m l).length
⊢ (take n l)[i]? = some (take m l)[i]

Tactic:
rw [getElem?_take_of_lt, getElem_take, getElem?_eq_getElem]

Result:
α : Type u_1
l : List α
m n : Nat
h : m ≤ n
i : Nat
w : i < (take m l).length
⊢ i < n

Proof state:
α : Type u_1
l : List α
m n : Nat
h : m ≤ n
⊢ take m l <+: take n l

Tactic:
rw [isPrefix_iff]

Result:
α : Type u_1
l : List α
m n : Nat
h : m ≤ n
⊢ ∀ (i : Nat) (h : i < (take m l).length), (take n l)[i]? = some (take m l)[i]

Proof state:
α : Type u_1
l : List α
m n : Nat
h : m ≤ n
i : Nat
w : i < (take m l).length
⊢ i < n

Tactic:
simp only [length_take] at w

Result:
α : Type u_1
l : List α
m n : Nat
h : m ≤ n
i : Nat
w : i < min m l.length
⊢ i < n

Proof state:
α : Type u_1
l : List α
m n : Nat
h : m ≤ n
i : Nat
w : i < min m l.length
⊢ i < n

Tactic:
exact Nat.lt_of_lt_of_le (Nat.lt_of_lt_of_le w (Nat.min_le_left _ _)) h

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Abs.lean
theorem HasFDerivAt.abs_of_pos (hf : HasFDerivAt f f' x)
    (h₀ : 0 < f x) : HasFDerivAt (fun x ↦ |f x|) f' x

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : 0 < f x
⊢ f' = (ContinuousLinearMap.smulRight 1 1).comp f'

Tactic:
ext y

Result:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : 0 < f x
y : E
⊢ f' y = ((ContinuousLinearMap.smulRight 1 1).comp f') y

Proof state:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : 0 < f x
y : E
⊢ f' y = ((ContinuousLinearMap.smulRight 1 1).comp f') y

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : 0 < f x
⊢ HasFDerivAt (fun x => |f x|) f' x

Tactic:
convert (hasDerivAt_abs_pos h₀).hasFDerivAt.comp x hf using 1

Result:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
h₀ : 0 < f x
⊢ f' = (ContinuousLinearMap.smulRight 1 1).comp f'