harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem simple_determines_coxeterSystem :
    Injective (simple : CoxeterSystem M W → B → W)

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
⊢ Injective simple

Tactic:
intro cs1 cs2 h

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
⊢ cs1 = cs2

Proof state:
case mulEquiv
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
⊢ cs1.mulEquiv = cs2.mulEquiv

Tactic:
apply MulEquiv.toMonoidHom_injective

Result:
case mulEquiv.a
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
⊢ cs1.mulEquiv.toMonoidHom = cs2.mulEquiv.toMonoidHom

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
⊢ cs1 = cs2

Tactic:
apply CoxeterSystem.ext

Result:
case mulEquiv
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
⊢ cs1.mulEquiv = cs2.mulEquiv

Proof state:
case mulEquiv.a
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
⊢ ∀ (i : B), cs1.mulEquiv.toMonoidHom (cs1.simple i) = cs2.mulEquiv.toMonoidHom (cs1.simple i)

Tactic:
intro i

Result:
case mulEquiv.a
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
i : B
⊢ cs1.mulEquiv.toMonoidHom (cs1.simple i) = cs2.mulEquiv.toMonoidHom (cs1.simple i)

Proof state:
case mulEquiv.a
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
i : B
⊢ cs1.mulEquiv.toMonoidHom (cs1.simple i) = cs2.mulEquiv.toMonoidHom (cs2.simple i)

Tactic:
simp [simple]

Result:
no goals

Proof state:
case mulEquiv.a
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
⊢ cs1.mulEquiv.toMonoidHom = cs2.mulEquiv.toMonoidHom

Tactic:
apply cs1.ext_simple

Result:
case mulEquiv.a
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
⊢ ∀ (i : B), cs1.mulEquiv.toMonoidHom (cs1.simple i) = cs2.mulEquiv.toMonoidHom (cs1.simple i)

Proof state:
case mulEquiv.a
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
i : B
⊢ cs1.mulEquiv.toMonoidHom (cs1.simple i) = cs2.mulEquiv.toMonoidHom (cs1.simple i)

Tactic:
nth_rw 2 [h]

Result:
case mulEquiv.a
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs1 cs2 : CoxeterSystem M W
h : cs1.simple = cs2.simple
i : B
⊢ cs1.mulEquiv.toMonoidHom (cs1.simple i) = cs2.mulEquiv.toMonoidHom (cs2.simple i)
-- Mathlib/Data/Finset/Basic.lean
theorem range_filter_eq {n m : ℕ} : (range n).filter (· = m) = if m < n then {m} else ∅

Proof state:
case h.e'_3.h₁.a
n m : ℕ
⊢ m < n ↔ m ∈ range n

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.h.e'_2
n m : ℕ
⊢ (fun x => x = m) = Eq m

Tactic:
ext

Result:
case h.e'_2.h.e'_2.h.a
n m x✝ : ℕ
⊢ x✝ = m ↔ m = x✝

Proof state:
n m : ℕ
⊢ filter (fun x => x = m) (range n) = if m < n then {m} else ∅

Tactic:
convert filter_eq (range n) m using 2

Result:
case h.e'_2.h.e'_2
n m : ℕ
⊢ (fun x => x = m) = Eq m

case h.e'_3.h₁.a
n m : ℕ
⊢ m < n ↔ m ∈ range n

Proof state:
case h.e'_2.h.e'_2.h.a
n m x✝ : ℕ
⊢ x✝ = m ↔ m = x✝

Tactic:
rw [eq_comm]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/SheafedSpace.lean
lemma mono_of_base_injective_of_stalk_epi {X Y : SheafedSpace C} (f : X ⟶ Y)
    (h₁ : Function.Injective f.base)
    (h₂ : ∀ x, Epi (f.stalkMap x)) : Mono f

Proof state:
case right_cancellation
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f x)
Z : SheafedSpace C
g : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
gc hc : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
e : { base := g, c := gc } ≫ f = { base := g, c := hc } ≫ f
⊢ { base := g, c := gc } = { base := g, c := hc }

Tactic:
refine SheafedSpace.hom_stalk_ext ⟨g, gc⟩ ⟨g, hc⟩ rfl fun x ↦ ?_

Result:
case right_cancellation
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f x)
Z : SheafedSpace C
g : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
gc hc : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
e : { base := g, c := gc } ≫ f = { base := g, c := hc } ≫ f
x : ↑↑Z.toPresheafedSpace
⊢ { base := g, c := gc }.stalkMap x = (X.presheaf.stalkCongr ⋯).hom ≫ { base := g, c := hc }.stalkMap x

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f x)
⊢ Mono f

Tactic:
constructor

Result:
case right_cancellation
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f x)
⊢ ∀ {Z : SheafedSpace C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean
lemma hom_inv_apply {M N : SemiNormedGrp} (e : M ≅ N) (s : N) : e.hom (e.inv s) = s

Proof state:
M N : SemiNormedGrp
e : M ≅ N
s : N.carrier
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Braiding.lean
lemma braiding_naturality_right [HasTensor X Y] [HasTensor Y X] [HasTensor X Z] [HasTensor Z X]
    (f : Y ⟶ Z) :
    whiskerLeft X f ≫ (braiding X Z).hom = (braiding X Y).hom ≫ whiskerRight f X

Proof state:
I : Type u_1
inst✝⁷ : AddCommMonoid I
C : Type u_2
inst✝⁶ : Category.{u_3, u_2} C
inst✝⁵ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝⁴ : BraidedCategory C
inst✝³ : X.HasTensor Y
inst✝² : Y.HasTensor X
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : Y ⟶ Z
⊢ (whiskerLeft X f ≫ fun k => tensorObjDesc fun i j hij => (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) =
    (fun k => tensorObjDesc fun i j hij => (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) ≫ whiskerRight f X

Tactic:
aesop_cat

Result:
no goals

Proof state:
I : Type u_1
inst✝⁷ : AddCommMonoid I
C : Type u_2
inst✝⁶ : Category.{u_3, u_2} C
inst✝⁵ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝⁴ : BraidedCategory C
inst✝³ : X.HasTensor Y
inst✝² : Y.HasTensor X
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : Y ⟶ Z
⊢ whiskerLeft X f ≫ (braiding X Z).hom = (braiding X Y).hom ≫ whiskerRight f X

Tactic:
dsimp [braiding]

Result:
I : Type u_1
inst✝⁷ : AddCommMonoid I
C : Type u_2
inst✝⁶ : Category.{u_3, u_2} C
inst✝⁵ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝⁴ : BraidedCategory C
inst✝³ : X.HasTensor Y
inst✝² : Y.HasTensor X
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : Y ⟶ Z
⊢ (whiskerLeft X f ≫ fun k => tensorObjDesc fun i j hij => (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) =
    (fun k => tensorObjDesc fun i j hij => (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) ≫ whiskerRight f X
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem isVanKampenColimit_extendCofan {n : ℕ} (f : Fin (n + 1) → C)
    {c₁ : Cofan fun i : Fin n ↦ f i.succ} {c₂ : BinaryCofan (f 0) c₁.pt}
    (t₁ : IsVanKampenColimit c₁) (t₂ : IsVanKampenColimit c₂)
    [∀ {Z} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i]
    [HasFiniteCoproducts C] :
    IsVanKampenColimit (extendCofan c₁ c₂)

Proof state:
case refine_1.w.h.mk.right
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
⊢ (Sigma.desc fun b => α.app { as := b.succ } ≫ c₁.inj b) ≫ c₂.inr = (Sigma.desc fun b => c.ι.app { as := b.succ }) ≫ i

Tactic:
ext j

Result:
case refine_1.w.h.mk.right.h
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i => f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j✝ : Fin (n + 1)
j : Fin n
⊢ Sigma.ι (fun j => F.obj { as := j.succ }) j ≫ (Sigma.desc fun b => α.app { as := b.succ } ≫ c₁.inj b) ≫ c₂.inr =
    Sigma.ι (fun j => F.obj { as := j.succ }) j ≫ (Sigma.desc fun b => c.ι.app { as := b.succ }) ≫ i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem lt_of_mul_lt_mul_left {a b c : Int} (w : a * b < a * c) (h : 0 ≤ a) : b < c

Proof state:
case inr.inr
a b c : Int
w : a * b < a * c
h : 0 ≤ a
gt : c < b
⊢ b < c

Tactic:
rcases Int.lt_trichotomy a 0 with a_lt | rfl | a_gt

Result:
case inr.inr.inl
a b c : Int
w : a * b < a * c
h : 0 ≤ a
gt : c < b
a_lt : a < 0
⊢ b < c

case inr.inr.inr.inl
b c : Int
gt : c < b
w : 0 * b < 0 * c
h : 0 ≤ 0
⊢ b < c

case inr.inr.inr.inr
a b c : Int
w : a * b < a * c
h : 0 ≤ a
gt : c < b
a_gt : 0 < a
⊢ b < c

Proof state:
case inr.inr.inr.inl
b c : Int
gt : c < b
w : 0 * b < 0 * c
h : 0 ≤ 0
⊢ b < c

Tactic:
exact False.elim (Int.lt_irrefl b (by simp at w))

Result:
no goals

Proof state:
case inr.inl
a b : Int
h : 0 ≤ a
w : a * b < a * b
⊢ b < b

Tactic:
exact False.elim (Int.lt_irrefl _ w)

Result:
no goals

Proof state:
case inr.inr.inr.inr
a b c : Int
w : a * b < a * c
h : 0 ≤ a
gt : c < b
a_gt : 0 < a
this : b ≤ c
⊢ b < c

Tactic:
exact False.elim (Int.lt_irrefl _ (Int.lt_of_lt_of_le gt this))

Result:
no goals

Proof state:
a b c : Int
w : a * b < a * c
h : 0 ≤ a
⊢ b < c

Tactic:
rcases Int.lt_trichotomy b c with lt | rfl | gt

Result:
case inl
a b c : Int
w : a * b < a * c
h : 0 ≤ a
lt : b < c
⊢ b < c

case inr.inl
a b : Int
h : 0 ≤ a
w : a * b < a * b
⊢ b < b

case inr.inr
a b c : Int
w : a * b < a * c
h : 0 ≤ a
gt : c < b
⊢ b < c

Proof state:
case inr.inr.inl
a b c : Int
w : a * b < a * c
h : 0 ≤ a
gt : c < b
a_lt : a < 0
⊢ b < c

Tactic:
exact False.elim (Int.lt_irrefl _ (Int.lt_of_lt_of_le a_lt h))

Result:
no goals

Proof state:
case inl
a b c : Int
w : a * b < a * c
h : 0 ≤ a
lt : b < c
⊢ b < c

Tactic:
exact lt

Result:
no goals

Proof state:
case inr.inr.inr.inr
a b c : Int
w : a * b < a * c
h : 0 ≤ a
gt : c < b
a_gt : 0 < a
⊢ b < c

Tactic:
have := le_of_mul_le_mul_left (Int.le_of_lt w) a_gt

Result:
case inr.inr.inr.inr
a b c : Int
w : a * b < a * c
h : 0 ≤ a
gt : c < b
a_gt : 0 < a
this : b ≤ c
⊢ b < c

Proof state:
b c : Int
gt : c < b
w : 0 * b < 0 * c
h : 0 ≤ 0
⊢ b < b

Tactic:
simp at w

Result:
no goals
-- Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean
theorem exists_partition_polynomial_aux (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : Fq[X]} (hb : b ≠ 0)
    (A : Fin n → Fq[X]) : ∃ t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (Fintype.card Fq)⌉₊),
      ∀ i₀ i₁ : Fin n, t i₀ = t i₁ ↔
        (cardPowDegree (A i₁ % b - A i₀ % b) : ℝ) < cardPowDegree b • ε

Proof state:
case intro.intro.intro.refine_1.refine_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : 0 ≠ j₁.succ
approx : ¬cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A (Classical.choose ⋯).succ % b))
this : cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A (Classical.choose ⋯).succ % b))
⊢ False

Tactic:
contradiction

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem isNormal_iff_lt_succ_and_bsup_eq {f : Ordinal.{u} → Ordinal.{max u v}} :
    IsNormal f ↔ (∀ a, f a < f (succ a)) ∧ ∀ o, IsLimit o → (bsup.{_, v} o fun x _ => f x) = f o :=
  ⟨fun h => ⟨h.1, @IsNormal.bsup_eq f h⟩, fun ⟨h₁, h₂⟩ =>
    ⟨h₁, fun o ho a => by
      rw [← h₂ o ho]
      exact bsup_le_iff⟩⟩

Proof state:
f : Ordinal.{u} → Ordinal.{max u v}
x✝ : (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o
h₁ : ∀ (a : Ordinal.{u}), f a < f (succ a)
h₂ : ∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{max u v}
⊢ (o.bsup fun x x_1 => f x) ≤ a ↔ ∀ b < o, f b ≤ a

Tactic:
exact bsup_le_iff

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{max u v}
x✝ : (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o
h₁ : ∀ (a : Ordinal.{u}), f a < f (succ a)
h₂ : ∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{max u v}
⊢ f o ≤ a ↔ ∀ b < o, f b ≤ a

Tactic:
rw [← h₂ o ho]

Result:
f : Ordinal.{u} → Ordinal.{max u v}
x✝ : (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o
h₁ : ∀ (a : Ordinal.{u}), f a < f (succ a)
h₂ : ∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o
o : Ordinal.{u}
ho : o.IsLimit
a : Ordinal.{max u v}
⊢ (o.bsup fun x x_1 => f x) ≤ a ↔ ∀ b < o, f b ≤ a
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem normSq_eq_zero_of_eq_zero {x : F} : x = 0 → normSqF x = 0

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
⊢ normSq 0 = 0

Tactic:
simp [normSq, inner_self_of_eq_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ x = 0 → normSq x = 0

Tactic:
rintro rfl

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
⊢ normSq 0 = 0
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem _root_.LieModule.isNilpotent_iff_exists_ucs_eq_top :
    LieModule.IsNilpotent L M ↔ ∃ k, (⊥ : LieSubmodule R L M).ucs k = ⊤

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ LieModule.IsNilpotent L M ↔ ∃ k, ucs k ⊥ = ⊤

Tactic:
rw [LieModule.isNilpotent_iff R]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ (∃ k, LieModule.lowerCentralSeries R L M k = ⊥) ↔ ∃ k, ucs k ⊥ = ⊤

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
⊢ LieModule.lowerCentralSeries R L M k = ⊥ ↔ ucs k ⊥ = ⊤

Tactic:
simp [ucs_eq_top_iff]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ (∃ k, LieModule.lowerCentralSeries R L M k = ⊥) ↔ ∃ k, ucs k ⊥ = ⊤

Tactic:
exact exists_congr fun k => by simp [ucs_eq_top_iff]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem LSeries_eq_mul_integral (f : ℕ → ℂ) {r : ℝ} (hr : 0 ≤ r) {s : ℂ} (hs : r < s.re)
    (hS : LSeriesSummable f s)
    (hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ (n : ℝ) ^ r) :
    LSeries f s = s * ∫ t in Set.Ioi (1 : ℝ), (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (-(s + 1))

Proof state:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n => ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n => ↑n ^ r
⊢ (fun n => if n = 0 then 0 else f n) =ᶠ[atTop] f

Tactic:
filter_upwards [eventually_ne_atTop 0] with n h using if_neg h

Result:
no goals

Proof state:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n => ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n => ↑n ^ r
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

Tactic:
rw [← LSeriesSummable_congr' s (f := fun n ↦ if n = 0 then 0 else f n)
  (by filter_upwards [eventually_ne_atTop 0] with n h using if_neg h)] at hS

Result:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n => if n = 0 then 0 else f n) s
hO : (fun n => ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n => ↑n ^ r
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

Proof state:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n => if n = 0 then 0 else f n) s
hO : (fun n => ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n => ↑n ^ r
n k : ℕ
hk : k ∈ Icc 1 n
⊢ (if k = 0 then 0 else f k) = f k

Tactic:
rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp hk).1).ne']

Result:
no goals

Proof state:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n => if n = 0 then 0 else f n) s
hO : (fun n => ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n => ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

Tactic:
rw [← LSeries_congr _ (fun _ ↦ if_neg _), LSeries_eq_mul_integral_aux (if_pos rfl) hr hs hS] <;>
simp_all

Result:
no goals

Proof state:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n => if n = 0 then 0 else f n) s
hO : (fun n => ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n => ↑n ^ r
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

Tactic:
have (n) : ∑ k ∈ Icc 1 n, (if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k :=
  Finset.sum_congr rfl fun k hk ↦ by rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp hk).1).ne']

Result:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n => if n = 0 then 0 else f n) s
hO : (fun n => ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n => ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))
-- Mathlib/Tactic/NormNum/Pow.lean
theorem intPow_ofNat (h1 : Nat.pow a b = c) :
    Int.pow (Int.ofNat a) b = Int.ofNat c

Proof state:
a b c : ℕ
h1 : a.pow b = c
⊢ (Int.ofNat a).pow b = Int.ofNat c

Tactic:
simp [← h1]

Result:
no goals
-- Mathlib/Data/Finsupp/ToDFinsupp.lean
theorem sigmaFinsuppEquivDFinsupp_add [AddZeroClass N] (f g : (Σi, η i) →₀ N) :
    sigmaFinsuppEquivDFinsupp (f + g) =
      (sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g : Π₀ i : ι, η i →₀ N)

Proof state:
case h.h
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ((sigmaFinsuppEquivDFinsupp (f + g)) i✝) a✝ = ((sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g) i✝) a✝

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
⊢ sigmaFinsuppEquivDFinsupp (f + g) = sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g

Tactic:
ext

Result:
case h.h
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ((sigmaFinsuppEquivDFinsupp (f + g)) i✝) a✝ = ((sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g) i✝) a✝
-- Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
theorem wrepr_wMk {α : TypeVec n} (a : q.P.A) (f' : q.P.drop.B a ⟹ α)
    (f : q.P.last.B a → q.P.W α) :
    wrepr (q.P.wMk a f' f) =
      q.P.wMk' (repr (abs (appendFun id wrepr <$$> ⟨a, q.P.appendContents f' f⟩)))

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ wrepr ((P F).wMk a f' f) = (P F).wMk' (repr (abs ((TypeVec.id ::: wrepr) <$$> ⟨a, (P F).appendContents f' f⟩)))

Tactic:
rw [wrepr, recF_eq', q.P.wDest'_wMk]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ ((P F).wMk' ∘ repr) (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, splitFun f' f⟩)) =
    (P F).wMk' (repr (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, (P F).appendContents f' f⟩)))

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ ((P F).wMk' ∘ repr) (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, splitFun f' f⟩)) =
    (P F).wMk' (repr (abs ((TypeVec.id ::: recF ((P F).wMk' ∘ repr)) <$$> ⟨a, (P F).appendContents f' f⟩)))

Tactic:
rfl

Result:
no goals