harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
lemma Over.map_comp {X Y Z : T} {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) :
    map Q (P.comp_mem f g hf hg) = map Q hf ⋙ map Q hg

Proof state:
T : Type u_1
inst✝² : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ map Q ⋯ = map Q hf ⋙ map Q hg

Tactic:
fapply Functor.ext

Result:
case h_obj
T : Type u_1
inst✝² : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ ∀ (X_1 : P.Over Q X), (map Q ⋯).obj X_1 = (map Q hf ⋙ map Q hg).obj X_1

case h_map
T : Type u_1
inst✝² : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ autoParam
    (∀ (X_1 Y_1 : P.Over Q X) (f_1 : X_1 ⟶ Y_1),
      (map Q ⋯).map f_1 = eqToHom ⋯ ≫ (map Q hf ⋙ map Q hg).map f_1 ≫ eqToHom ⋯)
    _auto✝

Proof state:
case h_map
T : Type u_1
inst✝² : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
U V : P.Over Q X
k : U ⟶ V
⊢ (map Q ⋯).map k = eqToHom ⋯ ≫ (map Q hf ⋙ map Q hg).map k ≫ eqToHom ⋯

Tactic:
ext

Result:
case h_map.h
T : Type u_1
inst✝² : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
U V : P.Over Q X
k : U ⟶ V
⊢ ((map Q ⋯).map k).left = (eqToHom ⋯ ≫ (map Q hf ⋙ map Q hg).map k ≫ eqToHom ⋯).left

Proof state:
case h_map
T : Type u_1
inst✝² : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ autoParam
    (∀ (X_1 Y_1 : P.Over Q X) (f_1 : X_1 ⟶ Y_1),
      (map Q ⋯).map f_1 = eqToHom ⋯ ≫ (map Q hf ⋙ map Q hg).map f_1 ≫ eqToHom ⋯)
    _auto✝

Tactic:
intro U V k

Result:
case h_map
T : Type u_1
inst✝² : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
U V : P.Over Q X
k : U ⟶ V
⊢ (map Q ⋯).map k = eqToHom ⋯ ≫ (map Q hf ⋙ map Q hg).map k ≫ eqToHom ⋯

Proof state:
case h_map.h
T : Type u_1
inst✝² : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
U V : P.Over Q X
k : U ⟶ V
⊢ ((map Q ⋯).map k).left = (eqToHom ⋯ ≫ (map Q hf ⋙ map Q hg).map k ≫ eqToHom ⋯).left

Tactic:
simp

Result:
no goals

Proof state:
case h_obj
T : Type u_1
inst✝² : Category.{u_2, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : P.IsStableUnderComposition
X Y Z : T
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ ∀ (X_1 : P.Over Q X), (map Q ⋯).obj X_1 = (map Q hf ⋙ map Q hg).obj X_1

Tactic:
simp [map, Comma.mapRight, CategoryTheory.Comma.mapRight, Comma.lift]

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc (attr := simp)]
lemma XXIsoOfEq_inv_ιTotal {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂)
    (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (x₁, x₂) = i₁₂) :
    (K.XXIsoOfEq _ _ _ h₁ h₂).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h =
      K.ιTotal c₁₂ y₁ y₂ i₁₂ (by rw [← h, h₁, h₂])

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
x₁ : I₁
x₂ : I₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
⊢ (XXIsoOfEq C c₁ c₂ K ⋯ ⋯).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h = K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{?u.69778, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
⊢ c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂

Tactic:
rw [← h, h₁, h₂]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
⊢ (XXIsoOfEq C c₁ c₂ K h₁ h₂).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h = K.ιTotal c₁₂ y₁ y₂ i₁₂ ⋯

Tactic:
subst h₁ h₂

Result:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
x₁ : I₁
x₂ : I₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
⊢ (XXIsoOfEq C c₁ c₂ K ⋯ ⋯).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h = K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯
-- Mathlib/MeasureTheory/Measure/Prod.lean
@[simp] lemma snd_map_swap : (ρ.map Prod.swap).snd = ρ.fst

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ map (Prod.snd ∘ Prod.swap) ρ = ρ.fst

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ (map Prod.swap ρ).snd = ρ.fst

Tactic:
rw [Measure.snd, Measure.map_map measurable_snd measurable_swap]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ map (Prod.snd ∘ Prod.swap) ρ = ρ.fst
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem one_div_pow {A : M} (n : ℕ) : (1 / A) ^ n = 1 / A ^ n

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ (1 / A) ^ n = 1 / A ^ n

Tactic:
simp only [one_div, inv_pow']

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem posSemidef {M : Matrix n n R} (hM : M.PosDef) : M.PosSemidef

Proof state:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n → R
⊢ 0 ≤ star x ⬝ᵥ M *ᵥ x

Tactic:
by_cases hx : x = 0

Result:
case pos
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : x = 0
⊢ 0 ≤ star x ⬝ᵥ M *ᵥ x

case neg
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : ¬x = 0
⊢ 0 ≤ star x ⬝ᵥ M *ᵥ x

Proof state:
case pos
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : x = 0
⊢ 0 ≤ 0

Tactic:
exact le_rfl

Result:
no goals

Proof state:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
⊢ M.PosSemidef

Tactic:
refine ⟨hM.1, ?_⟩

Result:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
⊢ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ M *ᵥ x

Proof state:
case pos
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : x = 0
⊢ 0 ≤ star x ⬝ᵥ M *ᵥ x

Tactic:
simp only [hx, zero_dotProduct, star_zero, RCLike.zero_re']

Result:
case pos
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : x = 0
⊢ 0 ≤ 0

Proof state:
case neg
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : ¬x = 0
⊢ 0 ≤ star x ⬝ᵥ M *ᵥ x

Tactic:
exact le_of_lt (hM.2 x hx)

Result:
no goals

Proof state:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
⊢ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ M *ᵥ x

Tactic:
intro x

Result:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n → R
⊢ 0 ≤ star x ⬝ᵥ M *ᵥ x
-- Mathlib/Topology/Order/LocalExtr.lean
/-- If `f` is monotone to the left and antitone to the right, then it has a local maximum. -/
lemma isLocalMax_of_mono_anti' {α : Type*} [TopologicalSpace α] [LinearOrder α]
    {β : Type*} [Preorder β] {b : α} {f : α → β}
    {a : Set α} (ha : a ∈ 𝓝[≤] b) {c : Set α} (hc : c ∈ 𝓝[≥] b)
    (h₀ : MonotoneOn f a) (h₁ : AntitoneOn f c) : IsLocalMax f b :=
  have : b ∈ a := mem_of_mem_nhdsWithin (by simp) ha
  have : b ∈ c := mem_of_mem_nhdsWithin (by simp) hc
  mem_of_superset (nhds_of_Ici_Iic ha hc) (fun x _ => by rcases le_total x b <;> aesop)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
this : b ∈ a
⊢ b ∈ Ici b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
⊢ b ∈ Iic b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
β : Type u_2
inst✝ : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
this✝ : b ∈ a
this : b ∈ c
x : α
x✝ : x ∈ a ∩ Iic b ∪ c ∩ Ici b
⊢ x ∈ {x | (fun x => f x ≤ f b) x}

Tactic:
rcases le_total x b <;> aesop

Result:
no goals
-- Mathlib/Data/Quot.lean
theorem ext {α : Sort*} : ∀ {s t : Setoid α}, (∀ a b, s a b ↔ t a b) → s = t
  | ⟨r, _⟩, ⟨p, _⟩, Eq =>
  by have : r = p := funext fun a ↦ funext fun b ↦ propext <| Eq a b
     subst this
     rfl

Proof state:
α : Sort u_3
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), { r := r, iseqv := iseqv✝¹ } a b ↔ { r := p, iseqv := iseqv✝ } a b
this : r = p
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }

Tactic:
subst this

Result:
α : Sort u_3
r : α → α → Prop
iseqv✝¹ iseqv✝ : Equivalence r
Eq : ∀ (a b : α), { r := r, iseqv := iseqv✝¹ } a b ↔ { r := r, iseqv := iseqv✝ } a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := r, iseqv := iseqv✝ }

Proof state:
α : Sort u_3
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), { r := r, iseqv := iseqv✝¹ } a b ↔ { r := p, iseqv := iseqv✝ } a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }

Tactic:
have : r = p := funext fun a ↦ funext fun b ↦ propext <| Eq a b

Result:
α : Sort u_3
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), { r := r, iseqv := iseqv✝¹ } a b ↔ { r := p, iseqv := iseqv✝ } a b
this : r = p
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }

Proof state:
α : Sort u_3
r : α → α → Prop
iseqv✝¹ iseqv✝ : Equivalence r
Eq : ∀ (a b : α), { r := r, iseqv := iseqv✝¹ } a b ↔ { r := r, iseqv := iseqv✝ } a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := r, iseqv := iseqv✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/TransfiniteIteration.lean
lemma top_mem_range_transfiniteIterate
    (hφ' : ∀ i ≠ (⊤ : I), i < φ i) (φtop : φ ⊤ = ⊤)
    (H : ¬ Function.Injective (fun (j : J) ↦ transfiniteIterate φ j i₀)) :
    ∃ (j : J), transfiniteIterate φ j i₀ = ⊤

Proof state:
case intro.intro.intro
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
hj₁ : ¬IsMax j₁
⊢ transfiniteIterate φ (Order.succ j₁) i₀ ≤ transfiniteIterate φ j₂ i₀

Tactic:
exact monotone_transfiniteIterate _ _ hφ (Order.succ_le_of_lt hj)

Result:
no goals

Proof state:
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
i : I
⊢ i ≤ φ i

Tactic:
by_cases hi : i = ⊤

Result:
case pos
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
i : I
hi : i = ⊤
⊢ i ≤ φ i

case neg
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
i : I
hi : ¬i = ⊤
⊢ i ≤ φ i

Proof state:
case intro.intro.intro
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
hj₁ : ¬IsMax j₁
⊢ φ (transfiniteIterate φ j₁ i₀) ≤ transfiniteIterate φ j₂ i₀

Tactic:
rw [← transfiniteIterate_succ φ i₀ j₁ hj₁]

Result:
case intro.intro.intro
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j => transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
hj₁ : ¬IsMax j₁
⊢ transfiniteIterate φ (Order.succ j₁) i₀ ≤ transfiniteIterate φ j₂ i₀
-- Mathlib/Data/Fin/Basic.lean
theorem heq_fun₂_iff {α : Sort*} {k l k' l' : ℕ} (h : k = l) (h' : k' = l')
    {f : Fin k → Fin k' → α} {g : Fin l → Fin l' → α} :
    HEq f g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨(i : ℕ), h ▸ i.2⟩ ⟨(j : ℕ), h' ▸ j.2⟩

Proof state:
α : Sort u_1
k k' : ℕ
f g : Fin k → Fin k' → α
⊢ HEq f g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

Tactic:
simp [funext_iff]

Result:
no goals

Proof state:
α : Sort u_1
k l k' l' : ℕ
h : k = l
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin l → Fin l' → α
⊢ HEq f g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

Tactic:
subst h

Result:
α : Sort u_1
k k' l' : ℕ
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin k → Fin l' → α
⊢ HEq f g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

Proof state:
α : Sort u_1
k k' l' : ℕ
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin k → Fin l' → α
⊢ HEq f g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

Tactic:
subst h'

Result:
α : Sort u_1
k k' : ℕ
f g : Fin k → Fin k' → α
⊢ HEq f g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩
-- Mathlib/SetTheory/Surreal/Multiplication.lean
theorem main (a : Args) : a.Numeric → P124 a

Proof state:
case P24
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
⊢ P124 (Args.P24 x₁ x₂ y)

Tactic:
obtain ⟨h₁₂x, h₁₂y⟩ := ih24_neg h₁₂

Result:
case P24.intro
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
⊢ P124 (Args.P24 x₁ x₂ y)

Proof state:
a : Args
⊢ ∀ (x : Args), (∀ (y : Args), ArgsRel y x → y.Numeric → P124 y) → x.Numeric → P124 x

Tactic:
intros a ih ha

Result:
a✝ a : Args
ih : ∀ (y : Args), ArgsRel y a → y.Numeric → P124 y
ha : a.Numeric
⊢ P124 a

Proof state:
case P24.intro
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
⊢ P124 (Args.P24 x₁ x₂ y)

Tactic:
obtain ⟨h4x, h4y⟩ := ih4_neg h4

Result:
case P24.intro.intro
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
h₂₁ : IH24 x₂ x₁ y
h4 : IH4 x₁ x₂ y
h₁₂x : IH24 (-x₂) (-x₁) y
h₁₂y : IH24 x₁ x₂ (-y)
h4x : IH4 (-x₂) (-x₁) y
h4y : IH4 x₁ x₂ (-y)
⊢ P124 (Args.P24 x₁ x₂ y)

Proof state:
case P24
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
⊢ P124 (Args.P24 x₁ x₂ y)

Tactic:
have h₁₂ := ih₁₂ ih

Result:
case P24
a : Args
x₁ x₂ y : PGame
ha : (Args.P24 x₁ x₂ y).Numeric
ih : ∀ (a' : Args), ArgsRel a' (Args.P24 x₁ x₂ y) → P124 a'
h₁₂ : IH24 x₁ x₂ y
⊢ P124 (Args.P24 x₁ x₂ y)
-- Mathlib/Data/Rat/Floor.lean
theorem ceil_def (q : ℚ) : ⌈q⌉ = -(-q.num / ↑q.den)

Proof state:
q : ℚ
⊢ -⌊-q⌋ = -(-q.num / ↑q.den)

Tactic:
rw [Rat.floor_def, num_neg_eq_neg_num, den_neg_eq_den]

Result:
no goals

Proof state:
q : ℚ
⊢ ⌈q⌉ = -(-q.num / ↑q.den)

Tactic:
change -⌊-q⌋ = _

Result:
q : ℚ
⊢ -⌊-q⌋ = -(-q.num / ↑q.den)
-- Mathlib/GroupTheory/Nilpotent.lean
theorem least_ascending_central_series_length_eq_nilpotencyClass :
    Nat.find ((nilpotent_iff_finite_ascending_central_series G).mp hG) =
    Group.nilpotencyClass G

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), upperCentralSeries G n = ⊤ → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
intro n hn

Result:
case refine_1
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤

Proof state:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ upperCentralSeries G n = ⊤

Tactic:
rw [← top_le_iff, ← hn]

Result:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsAscendingCentralSeries H ∧ H n = ⊤) → upperCentralSeries G n = ⊤

Tactic:
rintro n ⟨H, ⟨hH, hn⟩⟩

Result:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ upperCentralSeries G n = ⊤

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
exact ⟨upperCentralSeries G, upperCentralSeries_isAscendingCentralSeries G, hn⟩

Result:
no goals

Proof state:
case refine_2.intro.intro
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n

Tactic:
exact ascending_central_series_le_upper H hH n

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ Nat.find ⋯ = nilpotencyClass G

Tactic:
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)

Result:
case refine_1
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), upperCentralSeries G n = ⊤ → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤

case refine_2
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsAscendingCentralSeries H ∧ H n = ⊤) → upperCentralSeries G n = ⊤
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem scanlTR_go_eq : ∀ l, scanlTR.go f l a acc = acc.toList ++ scanl f a l
  | [] => by simp [scanlTR.go, scanl]
  | a :: l => by simp [scanlTR.go, scanl, scanlTR_go_eq l]

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝ → α✝¹
a : α✝¹
acc : Array α✝¹
⊢ scanlTR.go f [] a acc = acc.toList ++ scanl f a []

Tactic:
simp [scanlTR.go, scanl]

Result:
no goals

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝ → α✝¹
a✝ : α✝¹
acc : Array α✝¹
a : α✝
l : List α✝
⊢ scanlTR.go f (a :: l) a✝ acc = acc.toList ++ scanl f a✝ (a :: l)

Tactic:
simp [scanlTR.go, scanl, scanlTR_go_eq l]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_mkVector (a b : α) (n : Nat) : count a (mkVector n b) = if b == a then n else 0

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
⊢ count a (mkVector n b) = if (b == a) = true then n else 0

Tactic:
simp only [mkVector_eq_mk_mkArray, count_cast, count_mk]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
⊢ Array.count a (mkArray n b) = if (b == a) = true then n else 0

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
⊢ Array.count a (mkArray n b) = if (b == a) = true then n else 0

Tactic:
simp [Array.count_mkArray]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem mul : @Primrec' 2 fun v => v.head * v.tail.head :=
  (prec (const 0) (tail (add.comp₂ _ (tail head) head))).of_eq fun v => by
    simp; induction v.head <;> simp [*, Nat.succ_mul]; rw [add_comm]

Proof state:
case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec 0 (fun y IH => v.tail.head + IH) n✝ = n✝ * v.tail.head
⊢ v.tail.head + n✝ * v.tail.head = n✝ * v.tail.head + v.tail.head

Tactic:
rw [add_comm]

Result:
no goals

Proof state:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec 0 (fun y IH => (y ::ᵥ IH ::ᵥ v.tail).tail.tail.head + (y ::ᵥ IH ::ᵥ v.tail).tail.head) v.head =
    v.head * v.tail.head

Tactic:
simp

Result:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec 0 (fun y IH => v.tail.head + IH) v.head = v.head * v.tail.head

Proof state:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec 0 (fun y IH => v.tail.head + IH) v.head = v.head * v.tail.head

Tactic:
induction v.head <;> simp [*, Nat.succ_mul]

Result:
case succ
v : List.Vector ℕ (Nat.succ 0 + 1)
n✝ : ℕ
a✝ : Nat.rec 0 (fun y IH => v.tail.head + IH) n✝ = n✝ * v.tail.head
⊢ v.tail.head + n✝ * v.tail.head = n✝ * v.tail.head + v.tail.head
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem spanExt_app_right : (spanExt iX iY iZ wf wg).app WalkingSpan.right = iZ

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).app WalkingSpan.right = iZ

Tactic:
dsimp [spanExt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_alter_eq_add_one [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)}
    (h₁ : m.contains k = false) (h₂ : (f (m.get? k)).isSome) :
    (m.alter k f).1.size = m.1.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : Option (β k) → Option (β k)
h₁ : m.contains k = false
h₂ : (f (m.get? k)).isSome = true
⊢ (m.alter k f).val.size = m.val.size + 1

Tactic:
simp [size_alter, h, h₁, h₂]

Result:
no goals