harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/LocallyConvex/AbsConvex.lean
theorem totallyBounded_absConvexHull (hs : TotallyBounded s) :
    TotallyBounded (absConvexHull ℝ s)

Proof state:
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded ((convexHull ℝ) (s ∪ -s))

Tactic:
apply totallyBounded_convexHull

Result:
case hs
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded (s ∪ -s)

Proof state:
case hs
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded (s ∪ -s)

Tactic:
rw [totallyBounded_union]

Result:
case hs
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded s ∧ TotallyBounded (-s)

Proof state:
case hs
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded s ∧ TotallyBounded (-s)

Tactic:
exact ⟨hs, totallyBounded_neg hs⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded ((absConvexHull ℝ) s)

Tactic:
rw [← convexHull_union_neg_eq_absConvexHull]

Result:
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded ((convexHull ℝ) (s ∪ -s))
-- Mathlib/GroupTheory/Exponent.lean
theorem exponent_ne_zero : exponent G ≠ 0 ↔ ExponentExists G

Proof state:
case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
⊢ 0 ≠ 0 ↔ ExponentExists G

Tactic:
tauto

Result:
no goals

Proof state:
case pos
G : Type u
inst✝ : Monoid G
h : ExponentExists G
⊢ Nat.find h ≠ 0 ↔ ExponentExists G

Tactic:
simp [h, @not_lt_zero' ℕ]

Result:
no goals

Proof state:
G : Type u
inst✝ : Monoid G
⊢ (if h : ExponentExists G then Nat.find h else 0) ≠ 0 ↔ ExponentExists G

Tactic:
split_ifs with h

Result:
case pos
G : Type u
inst✝ : Monoid G
h : ExponentExists G
⊢ Nat.find h ≠ 0 ↔ ExponentExists G

case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
⊢ 0 ≠ 0 ↔ ExponentExists G

Proof state:
G : Type u
inst✝ : Monoid G
⊢ exponent G ≠ 0 ↔ ExponentExists G

Tactic:
rw [exponent]

Result:
G : Type u
inst✝ : Monoid G
⊢ (if h : ExponentExists G then Nat.find h else 0) ≠ 0 ↔ ExponentExists G
-- Mathlib/Data/Sum/Interval.lean
theorem inl_mem_sumLift₂ {c₁ : γ₁} :
    inl c₁ ∈ sumLift₂ f g a b ↔ ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ ¬∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
rintro ⟨_, _, c₂, _, _, h, _⟩

Result:
case intro.intro.intro.intro.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
w✝¹ : α₂
w✝ : β₂
c₂ : γ₂
left✝¹ : a = inr w✝¹
left✝ : b = inr w✝
h : inl c₁ = inr c₂
right✝ : c₂ ∈ g w✝¹ w✝
⊢ False

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ inl c₁ ∈ sumLift₂ f g a b ↔ ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁

Tactic:
rw [mem_sumLift₂, or_iff_left]

Result:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ (∃ a₁ b₁ c₁_1, a = inl a₁ ∧ b = inl b₁ ∧ inl c₁ = inl c₁_1 ∧ c₁_1 ∈ f a₁ b₁) ↔
    ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁

α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ ¬∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂

Proof state:
case intro.intro.intro.intro.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
w✝¹ : α₂
w✝ : β₂
c₂ : γ₂
left✝¹ : a = inr w✝¹
left✝ : b = inr w✝
h : inl c₁ = inr c₂
right✝ : c₂ ∈ g w✝¹ w✝
⊢ False

Tactic:
exact inl_ne_inr h

Result:
no goals

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ (∃ a₁ b₁ c₁_1, a = inl a₁ ∧ b = inl b₁ ∧ inl c₁ = inl c₁_1 ∧ c₁_1 ∈ f a₁ b₁) ↔
    ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁

Tactic:
simp only [inl.injEq, exists_and_left, exists_eq_left']

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
/-- For a triangularizable Lie module in finite dimensions, the weight spaces span the entire space.

See also `LieModule.iSup_genWeightSpace_eq_top'`. -/
lemma iSup_genWeightSpace_eq_top [IsTriangularizable K L M] :
    ⨆ χ : L → K, genWeightSpace M χ = ⊤

Proof state:
K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
⊢ ∀ (i : L), ⨆ μ, ((toEnd K L M) i).maxGenEigenspace μ = ⊤

Tactic:
apply IsTriangularizable.maxGenEigenspace_eq_top

Result:
no goals

Proof state:
K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
⊢ ⨆ i, ⨅ i_1, ↑(genWeightSpaceOf M (i i_1) i_1) = ⊤

Tactic:
refine Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo (toEnd K L M)
  (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem) ?_

Result:
K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
⊢ ∀ (i : L), ⨆ μ, ((toEnd K L M) i).maxGenEigenspace μ = ⊤

Proof state:
K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
⊢ ⨆ χ, genWeightSpace M χ = ⊤

Tactic:
simp only [← LieSubmodule.toSubmodule_inj, LieSubmodule.iSup_toSubmodule,
  LieSubmodule.iInf_toSubmodule, LieSubmodule.top_toSubmodule, genWeightSpace]

Result:
K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
⊢ ⨆ i, ⨅ i_1, ↑(genWeightSpaceOf M (i i_1) i_1) = ⊤
-- Mathlib/Algebra/CharP/Defs.lean
lemma char_is_prime_of_two_le (p : ℕ) [CharP R p] (hp : 2 ≤ p) : Nat.Prime p :=
  suffices ∀ (d) (_ : d ∣ p), d = 1 ∨ d = p from Nat.prime_def.mpr ⟨hp, this⟩
  fun (d : ℕ) (hdvd : ∃ e, p = d * e) =>
  let ⟨e, hmul⟩ := hdvd
  have : (p : R) = 0 := (cast_eq_zero_iff R p p).mpr (dvd_refl p)
  have : (d : R) * e = 0 := @Nat.cast_mul R _ d e ▸ hmul ▸ this
  Or.elim (eq_zero_or_eq_zero_of_mul_eq_zero this)
    (fun hd : (d : R) = 0 =>
      have : p ∣ d := (cast_eq_zero_iff R p d).mp hd
      show d = 1 ∨ d = p from Or.inr (this.antisymm' ⟨e, hmul⟩))
    fun he : (e : R) = 0 =>
    have : p ∣ e := (cast_eq_zero_iff R p e).mp he
    have : e ∣ p := dvd_of_mul_left_eq d (Eq.symm hmul)
    have : e = p := ‹e ∣ p›.antisymm ‹p ∣ e›
    have h₀ : 0 < p

Proof state:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
p : ℕ
inst✝ : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * p
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = p

Tactic:
exact Eq.symm hmul

Result:
no goals

Proof state:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
p : ℕ
inst✝ : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * e
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
⊢ 0 < p

Tactic:
omega

Result:
no goals

Proof state:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
p : ℕ
inst✝ : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * e
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = 1 * p

Tactic:
rw [‹e = p›] at hmul

Result:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
p : ℕ
inst✝ : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * p
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = 1 * p

Proof state:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
p : ℕ
inst✝ : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * p
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = 1 * p

Tactic:
rw [one_mul]

Result:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
p : ℕ
inst✝ : CharP R p
hp : 2 ≤ p
d : ℕ
hdvd : ∃ e, p = d * e
e : ℕ
hmul : p = d * p
this✝³ : ↑p = 0
this✝² : ↑d * ↑e = 0
he : ↑e = 0
this✝¹ : p ∣ e
this✝ : e ∣ p
this : e = p
h₀ : 0 < p
⊢ d * p = p
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiffAt_of_subsingleton [Subsingleton F] : ContDiffAt 𝕜 n f x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
n : WithTop ℕ∞
inst✝ : Subsingleton F
⊢ ContDiffAt 𝕜 n f x

Tactic:
rw [Subsingleton.elim f fun _ => 0]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
n : WithTop ℕ∞
inst✝ : Subsingleton F
⊢ ContDiffAt 𝕜 n (fun x => 0) x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
n : WithTop ℕ∞
inst✝ : Subsingleton F
⊢ ContDiffAt 𝕜 n (fun x => 0) x

Tactic:
exact contDiffAt_const

Result:
no goals
-- Mathlib/Data/Finsupp/Weight.lean
theorem degree_eq_weight_one {R : Type*} [Semiring R] :
    degree (R := R) (σ := σ) = weight (fun _ ↦ 1)

Proof state:
case h
σ : Type u_1
R : Type u_5
inst✝ : Semiring R
d : σ →₀ R
⊢ d.degree = (weight fun x => 1) d

Tactic:
simp only [degree, weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_5
inst✝ : Semiring R
⊢ degree = ⇑(weight fun x => 1)

Tactic:
ext d

Result:
case h
σ : Type u_1
R : Type u_5
inst✝ : Semiring R
d : σ →₀ R
⊢ d.degree = (weight fun x => 1) d
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem cancel_mono_id (f : X ⟶ Y) [Mono f] {g : X ⟶ X} : g ≫ f = f ↔ g = 𝟙 X

Proof state:
case h.e'_1.h.e'_3.h
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
g : X ⟶ X
⊢ f = 𝟙 X ≫ f

Tactic:
simp

Result:
no goals

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

Tactic:
convert cancel_mono f

Result:
case h.e'_1.h.e'_3.h
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
g : X ⟶ X
⊢ f = 𝟙 X ≫ f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem zero_mod (b : Nat) : 0 % b = 0

Proof state:
b : Nat
h₁ : 0 < b
h₂ : b = 0
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
b : Nat
⊢ 0 % b = 0

Tactic:
rw [mod_eq]

Result:
b : Nat
⊢ ite (0 < b ∧ b ≤ 0) ((0 - b) % b) 0 = 0

Proof state:
b : Nat
this : ¬(0 < b ∧ b = 0)
⊢ ite (0 < b ∧ b ≤ 0) ((0 - b) % b) 0 = 0

Tactic:
simp [this]

Result:
no goals

Proof state:
b : Nat
⊢ ite (0 < b ∧ b ≤ 0) ((0 - b) % b) 0 = 0

Tactic:
have : ¬ (0 < b ∧ b = 0) := by
  intro ⟨h₁, h₂⟩
  simp_all

Result:
b : Nat
this : ¬(0 < b ∧ b = 0)
⊢ ite (0 < b ∧ b ≤ 0) ((0 - b) % b) 0 = 0

Proof state:
b : Nat
⊢ ¬(0 < b ∧ b = 0)

Tactic:
intro ⟨h₁, h₂⟩

Result:
b : Nat
h₁ : 0 < b
h₂ : b = 0
⊢ False
-- Mathlib/CategoryTheory/Localization/Triangulated.lean
lemma isTriangulated [Pretriangulated D] [L.IsTriangulated] [IsTriangulated C] :
    IsTriangulated D

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁶ : Category.{u_4, u_1} C
inst✝¹⁵ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝¹⁴ : HasShift C ℤ
inst✝¹³ : Preadditive C
inst✝¹² : HasZeroObject C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
inst✝⁹ : HasShift D ℤ
inst✝⁸ : L.CommShift ℤ
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : W.HasLeftCalculusOfFractions
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.IsTriangulated
inst✝ : IsTriangulated C
⊢ IsTriangulated D

Tactic:
have := essSurj_mapComposableArrows L W 2

Result:
C : Type u_1
D : Type u_2
inst✝¹⁶ : Category.{u_4, u_1} C
inst✝¹⁵ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝¹⁴ : HasShift C ℤ
inst✝¹³ : Preadditive C
inst✝¹² : HasZeroObject C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
inst✝⁹ : HasShift D ℤ
inst✝⁸ : L.CommShift ℤ
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : W.HasLeftCalculusOfFractions
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.IsTriangulated
inst✝ : IsTriangulated C
this : (L.mapComposableArrows 2).EssSurj
⊢ IsTriangulated D

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁶ : Category.{u_4, u_1} C
inst✝¹⁵ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝¹⁴ : HasShift C ℤ
inst✝¹³ : Preadditive C
inst✝¹² : HasZeroObject C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
inst✝⁹ : HasShift D ℤ
inst✝⁸ : L.CommShift ℤ
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : W.HasLeftCalculusOfFractions
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.IsTriangulated
inst✝ : IsTriangulated C
this : (L.mapComposableArrows 2).EssSurj
⊢ IsTriangulated D

Tactic:
exact isTriangulated_of_essSurj_mapComposableArrows_two L

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem one_opow (a : Ordinal) : (1 : Ordinal) ^ a = 1

Proof state:
case H₃
b : Ordinal.{u_1}
l : b.IsLimit
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ 1 ^ b ≤ c ↔ 1 ≤ c

Tactic:
rw [opow_le_of_limit Ordinal.one_ne_zero l]

Result:
case H₃
b : Ordinal.{u_1}
l : b.IsLimit
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ (∀ b' < b, 1 ^ b' ≤ c) ↔ 1 ≤ c

Proof state:
a : Ordinal.{u_1}
⊢ 1 ^ a = 1

Tactic:
induction a using limitRecOn with
| H₁ => simp only [opow_zero]
| H₂ _ ih =>
  simp only [opow_succ, ih, mul_one]
| H₃ b l IH =>
  refine eq_of_forall_ge_iff fun c => ?_
  rw [opow_le_of_limit Ordinal.one_ne_zero l]
  exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩

Result:
no goals

Proof state:
b : Ordinal.{u_1}
l : b.IsLimit
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
H : ∀ b' < b, 1 ^ b' ≤ c
⊢ 1 ≤ c

Tactic:
simpa only [opow_zero] using H 0 l.pos

Result:
no goals

Proof state:
case H₃
b : Ordinal.{u_1}
l : b.IsLimit
IH : ∀ o' < b, 1 ^ o' = 1
⊢ 1 ^ b = 1

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Result:
case H₃
b : Ordinal.{u_1}
l : b.IsLimit
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ 1 ^ b ≤ c ↔ 1 ≤ c

Proof state:
b : Ordinal.{u_1}
l : b.IsLimit
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
H : 1 ≤ c
b' : Ordinal.{u_1}
h : b' < b
⊢ 1 ^ b' ≤ c

Tactic:
rwa [IH _ h]

Result:
no goals

Proof state:
case H₃
b : Ordinal.{u_1}
l : b.IsLimit
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
⊢ (∀ b' < b, 1 ^ b' ≤ c) ↔ 1 ≤ c

Tactic:
exact ⟨fun H => by simpa only [opow_zero] using H 0 l.pos, fun H b' h => by rwa [IH _ h]⟩

Result:
no goals

Proof state:
case H₁

⊢ 1 ^ 0 = 1

Tactic:
simp only [opow_zero]

Result:
no goals

Proof state:
case H₂
o✝ : Ordinal.{u_1}
ih : 1 ^ o✝ = 1
⊢ 1 ^ succ o✝ = 1

Tactic:
simp only [opow_succ, ih, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_concat (x : BitVec w) (b : Bool) (i : Nat) :
    (concat x b).getLsbD i = if i = 0 then b else x.getLsbD (i - 1)

Proof state:
w : Nat
x : BitVec w
b : Bool
i : Nat
⊢ (x.concat b).getLsbD i = if i = 0 then b else x.getLsbD (i - 1)

Tactic:
simp only [concat, getLsbD, toNat_append, toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq]

Result:
w : Nat
x : BitVec w
b : Bool
i : Nat
⊢ ((x.toNat * 2 ^ 1).testBit i || b.toNat.testBit i) = if i = 0 then b else x.toNat.testBit (i - 1)

Proof state:
w : Nat
x : BitVec w
b : Bool
i : Nat
⊢ ((x.toNat * 2 ^ 1).testBit i || b.toNat.testBit i) = if i = 0 then b else x.toNat.testBit (i - 1)

Tactic:
cases i

Result:
case zero
w : Nat
x : BitVec w
b : Bool
⊢ ((x.toNat * 2 ^ 1).testBit 0 || b.toNat.testBit 0) = if 0 = 0 then b else x.toNat.testBit (0 - 1)

case succ
w : Nat
x : BitVec w
b : Bool
n✝ : Nat
⊢ ((x.toNat * 2 ^ 1).testBit (n✝ + 1) || b.toNat.testBit (n✝ + 1)) =
    if n✝ + 1 = 0 then b else x.toNat.testBit (n✝ + 1 - 1)

Proof state:
case succ
w : Nat
x : BitVec w
b : Bool
n✝ : Nat
⊢ ((x.toNat * 2 ^ 1).testBit (n✝ + 1) || b.toNat.testBit (n✝ + 1)) =
    if n✝ + 1 = 0 then b else x.toNat.testBit (n✝ + 1 - 1)

Tactic:
simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one]

Result:
no goals

Proof state:
case zero
w : Nat
x : BitVec w
b : Bool
⊢ ((x.toNat * 2 ^ 1).testBit 0 || b.toNat.testBit 0) = if 0 = 0 then b else x.toNat.testBit (0 - 1)

Tactic:
simp [Nat.mod_eq_of_lt b.toNat_lt]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivativeFinsupp_X : derivativeFinsupp (X : R[X]) = .single 0 X + .single 1 1

Proof state:
R : Type u
inst✝ : Semiring R
⊢ derivativeFinsupp X = Finsupp.single 0 X + Finsupp.single 1 1

Tactic:
ext i : 1

Result:
case h
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (derivativeFinsupp X) i = (Finsupp.single 0 X + Finsupp.single 1 1) i

Proof state:
R : Type u
inst✝ : Semiring R
i n : ℕ
⊢ (derivativeFinsupp X) (n + 2) = (Finsupp.single 0 X + Finsupp.single 1 1) (n + 2)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (derivativeFinsupp X) 1 = (Finsupp.single 0 X + Finsupp.single 1 1) 1

Tactic:
simp

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (derivativeFinsupp X) i = (Finsupp.single 0 X + Finsupp.single 1 1) i

Tactic:
match i with
| 0 => simp
| 1 => simp
| (n + 2) => simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (derivativeFinsupp X) 0 = (Finsupp.single 0 X + Finsupp.single 1 1) 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/Complete.lean
theorem le_coeff_eq_iff_le_sub_coeff_eq_zero {x y : 𝕎 k} {n : ℕ} :
    (∀ i < n, x.coeff i = y.coeff i) ↔ ∀ i < n, (x - y).coeff i = 0

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
h : (truncate n) x = (truncate n) y
i : ℕ
hi : i < n
⊢ x.coeff i = y.coeff i

Tactic:
rw [← coeff_truncate x ⟨i, hi⟩, ← coeff_truncate y ⟨i, hi⟩, h]

Result:
no goals

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
h : ∀ i < n, x.coeff i = y.coeff i
⊢ (truncate n) x = (truncate n) y

Tactic:
ext i

Result:
case refine_1.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
h : ∀ i < n, x.coeff i = y.coeff i
i : Fin n
⊢ TruncatedWittVector.coeff i ((truncate n) x) = TruncatedWittVector.coeff i ((truncate n) y)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
⊢ (∀ i < n, x.coeff i = y.coeff i) ↔ (truncate n) x = (truncate n) y

Tactic:
refine ⟨fun h => ?_, fun h i hi => ?_⟩

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
h : ∀ i < n, x.coeff i = y.coeff i
⊢ (truncate n) x = (truncate n) y

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
h : (truncate n) x = (truncate n) y
i : ℕ
hi : i < n
⊢ x.coeff i = y.coeff i

Proof state:
case refine_1.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
h : ∀ i < n, x.coeff i = y.coeff i
i : Fin n
⊢ TruncatedWittVector.coeff i ((truncate n) x) = TruncatedWittVector.coeff i ((truncate n) y)

Tactic:
simp [h i]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
⊢ (truncate n) (x - y) = 0 ↔ ∀ i < n, (x - y).coeff i = 0

Tactic:
simp only [← mem_ker_truncate, RingHom.mem_ker]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
⊢ (truncate n) x = (truncate n) y ↔ (truncate n) (x - y) = 0

Tactic:
simp only [map_sub, sub_eq_zero]

Result:
no goals
-- Mathlib/Order/Filter/EventuallyConst.lean
lemma eventuallyConst_atTop_nat {f : ℕ → α} :
    EventuallyConst f atTop ↔ ∃ n, ∀ m, n ≤ m → f (m + 1) = f m

Proof state:
α : Type u_1
f : ℕ → α
⊢ (∃ i, ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m

Tactic:
refine exists_congr fun n ↦ ⟨fun h m hm ↦ ?_, fun h m hm ↦ ?_⟩

Result:
case refine_1
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (j : ℕ), n ≤ j → f j = f n
m : ℕ
hm : n ≤ m
⊢ f (m + 1) = f m

case refine_2
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
⊢ f m = f n

Proof state:
case refine_2.base
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
⊢ f n = f n

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (j : ℕ), n ≤ j → f j = f n
m : ℕ
hm : n ≤ m
⊢ f (m + 1) = f m

Tactic:
exact (h (m + 1) (hm.trans m.le_succ)).trans (h m hm).symm

Result:
no goals

Proof state:
case refine_2.succ
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m✝ m : ℕ
hm : n ≤ m
ihm : f m = f n
⊢ f (m + 1) = f n

Tactic:
exact (h m hm).trans ihm

Result:
no goals

Proof state:
case refine_2
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
⊢ f m = f n

Tactic:
induction m, hm using Nat.le_induction with
| base => rfl
| succ m hm ihm => exact (h m hm).trans ihm

Result:
no goals

Proof state:
α : Type u_1
f : ℕ → α
⊢ EventuallyConst f atTop ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m

Tactic:
rw [eventuallyConst_atTop]

Result:
α : Type u_1
f : ℕ → α
⊢ (∃ i, ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m