harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Denumerable.lean
theorem exists_succ (x : s) : ∃ n, (x : ℕ) + n + 1 ∈ s

Proof state:
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
⊢ ∃ n, ↑x + n + 1 ∈ s

Tactic:
by_contra h

Result:
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
⊢ False

Proof state:
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
⊢ False

Tactic:
have (a : ℕ) (ha : a ∈ s) : a < x + 1 :=
  lt_of_not_ge fun hax => h ⟨a - (x + 1), by rwa [Nat.add_right_comm, Nat.add_sub_cancel' hax]⟩

Result:
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
this : ∀ a ∈ s, a < ↑x + 1
⊢ False

Proof state:
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
this : ∀ a ∈ s, a < ↑x + 1
⊢ ∀ a ∈ Multiset.filter (fun x => x ∈ s) (Multiset.range (↑x).succ), a ∈ s

Tactic:
simp [-Multiset.range_succ]

Result:
no goals

Proof state:
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
a : ℕ
ha : a ∈ s
hax : a ≥ ↑x + 1
⊢ ↑x + (a - (↑x + 1)) + 1 ∈ s

Tactic:
rwa [Nat.add_right_comm, Nat.add_sub_cancel' hax]

Result:
no goals

Proof state:
s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
this : ∀ a ∈ s, a < ↑x + 1
⊢ ∀ (x_1 : Subtype (Membership.mem s)),
    x_1 ∈ (Multiset.pmap (fun y hy => ⟨y, hy⟩) (Multiset.filter (fun x => x ∈ s) (Multiset.range (↑x).succ)) ⋯).toFinset

Tactic:
simpa [Subtype.ext_iff_val, Multiset.mem_filter, -Multiset.range_succ]

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
protected lemma sq_sub_sq (h : Commute a b) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

Proof state:
R : Type u
inst✝ : Ring R
a b : R
h : Commute a b
⊢ a ^ 2 - b ^ 2 = (a + b) * (a - b)

Tactic:
rw [sq, sq, h.mul_self_sub_mul_self_eq]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_add_left_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.tan (o.oangle (x + y) y) = ‖x‖ / ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (x + y)).tan = ‖x‖ / ‖y‖

Tactic:
rw [add_comm]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (y + x)).tan = ‖x‖ / ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (y + x)).tan = ‖x‖ / ‖y‖

Tactic:
exact (-o).tan_oangle_add_right_of_oangle_eq_pi_div_two h

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x + y) y).tan = ‖x‖ / ‖y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (x + y)).tan = ‖x‖ / ‖y‖
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem isCycle_iff_sameCycle (hx : f x ≠ x) : IsCycle f ↔ ∀ {y}, SameCycle f x y ↔ f y ≠ y :=
  ⟨fun hf y =>
    ⟨fun ⟨i, hi⟩ hy =>
      hx <| by
        rw [← zpow_apply_eq_self_of_apply_eq_self hy i, (f ^ i).injective.eq_iff] at hi
        rw [hi, hy],
      hf.exists_zpow_eq hx⟩,
    fun h => ⟨x, hx, fun _ hy => h.2 hy⟩⟩

Proof state:
α : Type u_2
f : Perm α
x : α
hx : f x ≠ x
hf : f.IsCycle
y : α
x✝ : f.SameCycle x y
hy : f y = y
i : ℤ
hi : x = y
⊢ f x = x

Tactic:
rw [hi, hy]

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
x : α
hx : f x ≠ x
hf : f.IsCycle
y : α
x✝ : f.SameCycle x y
hy : f y = y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x

Tactic:
rw [← zpow_apply_eq_self_of_apply_eq_self hy i, (f ^ i).injective.eq_iff] at hi

Result:
α : Type u_2
f : Perm α
x : α
hx : f x ≠ x
hf : f.IsCycle
y : α
x✝ : f.SameCycle x y
hy : f y = y
i : ℤ
hi : x = y
⊢ f x = x
-- Mathlib/CategoryTheory/Comma/Basic.lean
theorem eqToHom_right (X Y : Comma L R) (H : X = Y) :
    CommaMorphism.right (eqToHom H) = eqToHom (by cases H; rfl)

Proof state:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ X.right = Y.right

Tactic:
cases H

Result:
case refl
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ X.right = X.right

Proof state:
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ (eqToHom H).right = eqToHom ⋯

Tactic:
cases H

Result:
case refl
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ (eqToHom ⋯).right = eqToHom ⋯

Proof state:
case refl
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ (eqToHom ⋯).right = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
case refl
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ X.right = X.right

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_ofList_of_mem [LawfulBEq α]
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} {fallback : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    getD (ofList l) k' fallback = v

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v fallback : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
⊢ getD (ofList l) k' fallback = v

Tactic:
simp_to_raw using Raw₀.Const.getD_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_push {a : Vector α n} {x y : α} : x ∈ a.push y ↔ x ∈ a ∨ x = y

Proof state:
case mk
α : Type u_1
n : Nat
x y : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.push y ↔
    x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∨ x = y

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Vector α n
x y : α
⊢ x ∈ a.push y ↔ x ∈ a ∨ x = y

Tactic:
cases a

Result:
case mk
α : Type u_1
n : Nat
x y : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ }.push y ↔
    x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∨ x = y
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_Ioi_of_hasDerivAt_of_tendsto (hcont : ContinuousWithinAt f (Ici a) a)
    (hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x) (f'int : IntegrableOn f' (Ioi a))
    (hf : Tendsto f atTop (𝓝 m)) : ∫ x in Ioi a, f' x = m - f a

Proof state:
case h
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont✝ : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ ∫ (x : ℝ) in a..id x, f' x = f x - f a

Tactic:
apply
  intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x (hcont.mono Icc_subset_Ici_self)
    fun y hy => hderiv y hy.1

Result:
case h
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont✝ : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntervalIntegrable f' volume a (id x)

Proof state:
case h
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont✝ : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntervalIntegrable f' volume a (id x)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x]

Result:
case h
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont✝ : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntegrableOn f' (Ioc a (id x)) volume
-- Mathlib/Analysis/Normed/Field/Basic.lean
@[simp] lemma enorm_eq (x : ℝ≥0) : ‖(x : ℝ)‖ₑ = x

Proof state:
x : ℝ≥0
⊢ ‖↑x‖ₑ = ↑x

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
/-- The union of two sets is totally bounded
if and only if each of the two sets is totally bounded. -/
@[simp]
lemma totallyBounded_union {s t : Set α} :
    TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t

Proof state:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
⊢ TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t

Tactic:
rw [union_eq_iUnion, totallyBounded_iUnion]

Result:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
⊢ (∀ (i : Bool), TotallyBounded (bif i then s else t)) ↔ TotallyBounded s ∧ TotallyBounded t

Proof state:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
⊢ (∀ (i : Bool), TotallyBounded (bif i then s else t)) ↔ TotallyBounded s ∧ TotallyBounded t

Tactic:
simp [and_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_addXYZ (P Q : Fin 3 → A) : (W'.baseChange B).toJacobian.addXYZ (f ∘ P) (f ∘ Q) =
    f ∘ (W'.baseChange A).toJacobian.addXYZ P Q

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (baseChange W' B).toJacobian.addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (baseChange W' A).toJacobian.addXYZ P Q

Tactic:
rw [← RingHom.coe_coe, ← map_addXYZ, map_baseChange]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem summable_geometric_iff_norm_lt_one : (Summable fun n : ℕ ↦ ξ ^ n) ↔ ‖ξ‖ < 1

Proof state:
case intro
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : dist (ξ ^ k) 0 < 1
⊢ ‖ξ‖ < 1

Tactic:
simp only [norm_pow, dist_zero_right] at hk

Result:
case intro
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1
⊢ ‖ξ‖ < 1

Proof state:
case intro
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1 ^ k
⊢ ‖ξ‖ < 1

Tactic:
exact lt_of_pow_lt_pow_left₀ _ zero_le_one hk

Result:
no goals

Proof state:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n => ξ ^ n
⊢ ‖ξ‖ < 1

Tactic:
obtain ⟨k : ℕ, hk : dist (ξ ^ k) 0 < 1⟩ :=
  (h.tendsto_cofinite_zero.eventually (ball_mem_nhds _ zero_lt_one)).exists

Result:
case intro
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : dist (ξ ^ k) 0 < 1
⊢ ‖ξ‖ < 1

Proof state:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
⊢ (Summable fun n => ξ ^ n) ↔ ‖ξ‖ < 1

Tactic:
refine ⟨fun h ↦ ?_, summable_geometric_of_norm_lt_one⟩

Result:
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n => ξ ^ n
⊢ ‖ξ‖ < 1

Proof state:
case intro
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1
⊢ ‖ξ‖ < 1

Tactic:
rw [← one_pow k] at hk

Result:
case intro
K : Type u_2
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n => ξ ^ n
k : ℕ
hk : ‖ξ‖ ^ k < 1 ^ k
⊢ ‖ξ‖ < 1
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_le_le_iff {a b : α} : pred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = pred a

Proof state:
case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a : α
⊢ pred a ≤ pred a ∧ pred a ≤ a

Tactic:
exact ⟨le_rfl, pred_le a⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
⊢ pred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = pred a

Tactic:
refine
  ⟨fun h =>
    or_iff_not_imp_left.2 fun hba : b ≠ a => (le_pred_of_lt <| h.2.lt_of_ne hba).antisymm h.1, ?_⟩

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
⊢ b = a ∨ b = pred a → pred a ≤ b ∧ b ≤ a

Proof state:
case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
b : α
⊢ pred b ≤ b ∧ b ≤ b

Tactic:
exact ⟨pred_le b, le_rfl⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
⊢ b = a ∨ b = pred a → pred a ≤ b ∧ b ≤ a

Tactic:
rintro (rfl | rfl)

Result:
case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
b : α
⊢ pred b ≤ b ∧ b ≤ b

case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a : α
⊢ pred a ≤ pred a ∧ pred a ≤ a
-- Mathlib/CategoryTheory/Triangulated/Functor.lean
lemma isTriangulated_of_precomp_iso {H : C ⥤ E} (e : F ⋙ G ≅ H) [H.CommShift ℤ]
    [H.IsTriangulated] [F.IsTriangulated] [F.mapArrow.EssSurj] [NatTrans.CommShift e.hom ℤ] :
    G.IsTriangulated

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝²⁴ : Category.{u_4, u_1} C
inst✝²³ : Category.{u_6, u_2} D
inst✝²² : Category.{u_5, u_3} E
inst✝²¹ : HasShift C ℤ
inst✝²⁰ : HasShift D ℤ
inst✝¹⁹ : HasShift E ℤ
F : C ⥤ D
inst✝¹⁸ : F.CommShift ℤ
G : D ⥤ E
inst✝¹⁷ : G.CommShift ℤ
inst✝¹⁶ : HasZeroObject C
inst✝¹⁵ : HasZeroObject D
inst✝¹⁴ : HasZeroObject E
inst✝¹³ : Preadditive C
inst✝¹² : Preadditive D
inst✝¹¹ : Preadditive E
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Pretriangulated D
inst✝⁵ : Pretriangulated E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁴ : H.CommShift ℤ
inst✝³ : H.IsTriangulated
inst✝² : F.IsTriangulated
inst✝¹ : F.mapArrow.EssSurj
inst✝ : NatTrans.CommShift e.hom ℤ
this : (F ⋙ G).IsTriangulated
⊢ G.IsTriangulated

Tactic:
exact isTriangulated_of_precomp F G

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝²⁴ : Category.{u_4, u_1} C
inst✝²³ : Category.{u_6, u_2} D
inst✝²² : Category.{u_5, u_3} E
inst✝²¹ : HasShift C ℤ
inst✝²⁰ : HasShift D ℤ
inst✝¹⁹ : HasShift E ℤ
F : C ⥤ D
inst✝¹⁸ : F.CommShift ℤ
G : D ⥤ E
inst✝¹⁷ : G.CommShift ℤ
inst✝¹⁶ : HasZeroObject C
inst✝¹⁵ : HasZeroObject D
inst✝¹⁴ : HasZeroObject E
inst✝¹³ : Preadditive C
inst✝¹² : Preadditive D
inst✝¹¹ : Preadditive E
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Pretriangulated D
inst✝⁵ : Pretriangulated E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁴ : H.CommShift ℤ
inst✝³ : H.IsTriangulated
inst✝² : F.IsTriangulated
inst✝¹ : F.mapArrow.EssSurj
inst✝ : NatTrans.CommShift e.hom ℤ
⊢ G.IsTriangulated

Tactic:
have := (isTriangulated_iff_of_iso e).2 inferInstance

Result:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝²⁴ : Category.{u_4, u_1} C
inst✝²³ : Category.{u_6, u_2} D
inst✝²² : Category.{u_5, u_3} E
inst✝²¹ : HasShift C ℤ
inst✝²⁰ : HasShift D ℤ
inst✝¹⁹ : HasShift E ℤ
F : C ⥤ D
inst✝¹⁸ : F.CommShift ℤ
G : D ⥤ E
inst✝¹⁷ : G.CommShift ℤ
inst✝¹⁶ : HasZeroObject C
inst✝¹⁵ : HasZeroObject D
inst✝¹⁴ : HasZeroObject E
inst✝¹³ : Preadditive C
inst✝¹² : Preadditive D
inst✝¹¹ : Preadditive E
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Pretriangulated D
inst✝⁵ : Pretriangulated E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁴ : H.CommShift ℤ
inst✝³ : H.IsTriangulated
inst✝² : F.IsTriangulated
inst✝¹ : F.mapArrow.EssSurj
inst✝ : NatTrans.CommShift e.hom ℤ
this : (F ⋙ G).IsTriangulated
⊢ G.IsTriangulated
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
/-- This lemma is useful in non-cancellative monoids, like sets under pointwise operations. -/
@[to_additive
"This lemma is useful in non-cancellative monoids, like sets under pointwise operations."]
lemma pow_le_pow_mul_of_sq_le_mul [MulLeftMono M] {a b : M} (hab : a ^ 2 ≤ b * a) :
    ∀ {n}, n ≠ 0 → a ^ n ≤ b ^ (n - 1) * a
  | 1, _ => by simp
  | n + 2, _ => by
    calc
      a ^ (n + 2) = a ^ (n + 1) * a

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * (b * a) = b ^ (n + 1) * a

Tactic:
rw [← mul_assoc, ← pow_succ]

Result:
no goals

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
x✝ : 1 ≠ 0
⊢ a ^ 1 ≤ b ^ (1 - 1) * a

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ n + 1 ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ (n + 2) = a ^ (n + 1) * a

Tactic:
rw [pow_succ]

Result:
no goals

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ n * a * a = b ^ n * a ^ 2

Tactic:
rw [mul_assoc, sq]

Result:
no goals

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ (n + 2) ≤ b ^ (n + 2 - 1) * a

Tactic:
calc
  a ^ (n + 2) = a ^ (n + 1) * a := by rw [pow_succ]
  _ ≤ b ^ n * a * a := mul_le_mul_right' (pow_le_pow_mul_of_sq_le_mul hab (by omega)) _
  _ = b ^ n * a ^ 2 := by rw [mul_assoc, sq]
  _ ≤ b ^ n * (b * a) := mul_le_mul_left' hab _
  _ = b ^ (n + 1) * a := by rw [← mul_assoc, ← pow_succ]

Result:
no goals
-- Mathlib/Data/Int/Cast/Basic.lean
theorem cast_sub (m n) : ((m - n : ℤ) : R) = m - n

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℤ
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
simp [Int.sub_eq_add_neg, sub_eq_add_neg, Int.cast_neg, Int.cast_add]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma genWeightSpace_chainTopCoeff_add_one_nsmul_add :
    genWeightSpace M ((chainTopCoeff α β + 1) • α + β : L → R) = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ genWeightSpace M (Nat.find ⋯ • α + ⇑β) = ⊥

Tactic:
exact Nat.find_spec (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ genWeightSpace M ((chainTopCoeff α β + 1) • α + ⇑β) = ⊥

Tactic:
rw [chainTopCoeff_add_one _ _ hα]

Result:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ genWeightSpace M (Nat.find ⋯ • α + ⇑β) = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ genWeightSpace M ((chainTopCoeff α β + 1) • α + ⇑β) = ⊥

Tactic:
classical
rw [chainTopCoeff_add_one _ _ hα]
exact Nat.find_spec (eventually_genWeightSpace_smul_add_eq_bot M α β hα).exists

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem map_map (g : β ≃o γ) (f : α ≃o β) : map g (map f s) = map (f.trans g) s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : UpperSet α
g : β ≃o γ
f : α ≃o β
⊢ (map g) ((map f) s) = (map (f.trans g)) s

Tactic:
ext

Result:
case a.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : UpperSet α
g : β ≃o γ
f : α ≃o β
x✝ : γ
⊢ x✝ ∈ ↑((map g) ((map f) s)) ↔ x✝ ∈ ↑((map (f.trans g)) s)

Proof state:
case a.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : UpperSet α
g : β ≃o γ
f : α ≃o β
x✝ : γ
⊢ x✝ ∈ ↑((map g) ((map f) s)) ↔ x✝ ∈ ↑((map (f.trans g)) s)

Tactic:
simp

Result:
no goals