harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Cover.lean
theorem mk_wcovBy_mk_iff : (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂

Proof state:
case refine_1.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) ⩿ (a₁, b₂)
⊢ a₁ ⩿ a₁ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₁

Tactic:
exact Or.inr ⟨mk_wcovBy_mk_iff_right.1 h, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂

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

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ⩿ (a₂, b₂)
⊢ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⩿ (a₂, b₂)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⩿ (a₂, b₂)

Tactic:
rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)

Result:
case refine_2.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : a₁ ⩿ a₂
⊢ (a₁, b₁) ⩿ (a₂, b₁)

case refine_2.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⩿ b₂
⊢ (a₁, b₁) ⩿ (a₁, b₂)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ⩿ (a₂, b₂)
⊢ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂

Tactic:
obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h

Result:
case refine_1.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) ⩿ (a₁, b₂)
⊢ a₁ ⩿ a₁ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₁

case refine_1.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : (a₁, b₁) ⩿ (a₂, b₁)
⊢ a₁ ⩿ a₂ ∧ b₁ = b₁ ∨ b₁ ⩿ b₁ ∧ a₁ = a₂

Proof state:
case refine_1.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : (a₁, b₁) ⩿ (a₂, b₁)
⊢ a₁ ⩿ a₂ ∧ b₁ = b₁ ∨ b₁ ⩿ b₁ ∧ a₁ = a₂

Tactic:
exact Or.inl ⟨mk_wcovBy_mk_iff_left.1 h, rfl⟩

Result:
no goals

Proof state:
case refine_2.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : a₁ ⩿ a₂
⊢ (a₁, b₁) ⩿ (a₂, b₁)

Tactic:
exact mk_wcovBy_mk_iff_left.2 h

Result:
no goals

Proof state:
case refine_2.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⩿ b₂
⊢ (a₁, b₁) ⩿ (a₁, b₂)

Tactic:
exact mk_wcovBy_mk_iff_right.2 h

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Mat.lean
@[reassoc (attr := simp)]
lemma ι_additiveObjIsoBiproduct_inv (F : Mat_ C ⥤ D) [Functor.Additive F] (M : Mat_ C) (i : M.ι) :
    biproduct.ι _ i ≫ (additiveObjIsoBiproduct F M).inv =
      F.map (biproduct.ι _ i ≫ M.isoBiproductEmbedding.inv)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ biproduct.ι (fun i => F.obj ((embedding C).obj (M.X i))) i ≫ (additiveObjIsoBiproduct F M).inv =
    F.map (biproduct.ι (fun i => (embedding C).obj (M.X i)) i ≫ M.isoBiproductEmbedding.inv)

Tactic:
dsimp [additiveObjIsoBiproduct, Functor.mapBiproduct, Functor.mapBicone]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ biproduct.ι (fun i => F.obj ((embedding C).obj (M.X i))) i ≫
      (biproduct.desc fun j => F.map (biproduct.ι (fun i => (embedding C).obj (M.X i)) j)) ≫
        F.map (biproduct.desc fun i x k => if h : i = k then eqToHom ⋯ else 0) =
    F.map
      (biproduct.ι (fun i => (embedding C).obj (M.X i)) i ≫
        biproduct.desc fun i x k => if h : i = k then eqToHom ⋯ else 0)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ biproduct.ι (fun i => F.obj ((embedding C).obj (M.X i))) i ≫
      (biproduct.desc fun j => F.map (biproduct.ι (fun i => (embedding C).obj (M.X i)) j)) ≫
        F.map (biproduct.desc fun i x k => if h : i = k then eqToHom ⋯ else 0) =
    F.map
      (biproduct.ι (fun i => (embedding C).obj (M.X i)) i ≫
        biproduct.desc fun i x k => if h : i = k then eqToHom ⋯ else 0)

Tactic:
simp only [biproduct.ι_desc, biproduct.ι_desc_assoc, ← F.map_comp]

Result:
no goals
-- Mathlib/RingTheory/Valuation/LocalSubring.lean
lemma IsLocalRing.exists_factor_valuationRing [IsLocalRing R] (f : R →+* K) :
    ∃ (A : ValuationSubring K) (h : _), IsLocalHom (f.codRestrict A.toSubring h)

Proof state:
case intro
R : Type u_1
K : Type u_3
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : IsLocalRing R
f : R →+* K
B : ValuationSubring K
hB : LocalSubring.range f ≤ B.toLocalSubring
⊢ IsLocalHom (f.codRestrict B.toSubring ⋯)

Tactic:
exact @RingHom.isLocalHom_comp _ _ _ _ _ _ _ _
  hB.2 (.of_surjective _ f.rangeRestrict_surjective)

Result:
no goals

Proof state:
R : Type u_1
K : Type u_3
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : IsLocalRing R
f : R →+* K
⊢ ∃ A, ∃ (h : ∀ (x : R), f x ∈ A.toSubring), IsLocalHom (f.codRestrict A.toSubring h)

Tactic:
obtain ⟨B, hB⟩  := (LocalSubring.range f).exists_le_valuationSubring

Result:
case intro
R : Type u_1
K : Type u_3
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : IsLocalRing R
f : R →+* K
B : ValuationSubring K
hB : LocalSubring.range f ≤ B.toLocalSubring
⊢ ∃ A, ∃ (h : ∀ (x : R), f x ∈ A.toSubring), IsLocalHom (f.codRestrict A.toSubring h)

Proof state:
case intro
R : Type u_1
K : Type u_3
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : IsLocalRing R
f : R →+* K
B : ValuationSubring K
hB : LocalSubring.range f ≤ B.toLocalSubring
⊢ ∃ A, ∃ (h : ∀ (x : R), f x ∈ A.toSubring), IsLocalHom (f.codRestrict A.toSubring h)

Tactic:
refine ⟨B, fun x ↦ hB.1 ⟨x, rfl⟩, ?_⟩

Result:
case intro
R : Type u_1
K : Type u_3
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : IsLocalRing R
f : R →+* K
B : ValuationSubring K
hB : LocalSubring.range f ≤ B.toLocalSubring
⊢ IsLocalHom (f.codRestrict B.toSubring ⋯)
-- Mathlib/Data/List/Rotate.lean
theorem rotate_eq_nil_iff {l : List α} {n : ℕ} : l.rotate n = [] ↔ l = []

Proof state:
case succ
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
l : List α
⊢ l.rotate (n + 1) = [] ↔ l = []

Tactic:
rcases l with - | ⟨hd, tl⟩

Result:
case succ.nil
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
⊢ [].rotate (n + 1) = [] ↔ [] = []

case succ.cons
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []

Proof state:
case succ.cons
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []

Tactic:
simp [rotate_cons_succ, hn]

Result:
no goals

Proof state:
case zero
α : Type u
l : List α
⊢ l.rotate 0 = [] ↔ l = []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
n : ℕ
⊢ l.rotate n = [] ↔ l = []

Tactic:
induction' n with n hn generalizing l

Result:
case zero
α : Type u
l : List α
⊢ l.rotate 0 = [] ↔ l = []

case succ
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
l : List α
⊢ l.rotate (n + 1) = [] ↔ l = []

Proof state:
case succ.nil
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
⊢ [].rotate (n + 1) = [] ↔ [] = []

Tactic:
simp

Result:
no goals
-- Mathlib/Data/DFinsupp/BigOperators.lean
theorem liftAddHom_apply_single [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (f : ∀ i, β i →+ γ)
    (i : ι) (x : β i) : liftAddHom (β := β) f (single i x) = f i x

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
f : (i : ι) → β i →+ γ
i : ι
x : β i
⊢ (liftAddHom f) (single i x) = (f i) x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive]
protected lemma mul_div_mul_right (h : IsUnit c) (a b : α) : a * c / (b * c) = a / b

Proof state:
α : Type u
inst✝ : DivisionMonoid α
c : α
h : IsUnit c
a b : α
⊢ a * c / (b * c) = a / b

Tactic:
simp only [div_eq_mul_inv, mul_inv_rev, mul_assoc, h.mul_inv_cancel_left]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem reverse_transfer (hp) :
    (p.transfer H hp).reverse =
      p.reverse.transfer H (by simp only [edges_reverse, List.mem_reverse]; exact hp)

Proof state:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u✝ v✝ u' v' : V
p✝ : G.Walk u✝ v✝
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∀ e ∈ p.reverse.edges, e ∈ H.edgeSet

Tactic:
simp only [edges_reverse, List.mem_reverse]

Result:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u✝ v✝ u' v' : V
p✝ : G.Walk u✝ v✝
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∀ e ∈ p.edges, e ∈ H.edgeSet

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).reverse = p.reverse.transfer H ⋯

Tactic:
induction p with
| nil => simp
| cons _ _ ih => simp only [transfer_append, Walk.transfer, reverse_nil, reverse_cons, ih]

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), (p✝.transfer H hp).reverse = p✝.reverse.transfer H ⋯
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
⊢ ((cons h✝ p✝).transfer H hp).reverse = (cons h✝ p✝).reverse.transfer H ⋯

Tactic:
simp only [transfer_append, Walk.transfer, reverse_nil, reverse_cons, ih]

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u✝ : V
hp : ∀ e ∈ nil.edges, e ∈ H.edgeSet
⊢ (nil.transfer H hp).reverse = nil.reverse.transfer H ⋯

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u✝ v✝ u' v' : V
p✝ : G.Walk u✝ v✝
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∀ e ∈ p.edges, e ∈ H.edgeSet

Tactic:
exact hp

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem lt_to_int {m n : ZNum} : (m : ℤ) < n ↔ m < n :=
  show (m : ℤ) < n ↔ cmp m n = Ordering.lt from
    match cmp m n, cmp_to_int m n with
    | Ordering.lt, h => by simp only at h; simp [h]
    | Ordering.eq, h => by simp only at h; simp [h, lt_irrefl]
    | Ordering.gt, h => by simp [not_lt_of_gt h]

Proof state:
m n : ZNum
h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.gt = Ordering.lt

Tactic:
simp [not_lt_of_gt h]

Result:
no goals

Proof state:
m n : ZNum
h : Ordering.casesOn Ordering.lt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Tactic:
simp only at h

Result:
m n : ZNum
h : ↑m < ↑n
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Proof state:
m n : ZNum
h : m = n
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Tactic:
simp [h, lt_irrefl]

Result:
no goals

Proof state:
m n : ZNum
h : ↑m < ↑n
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Tactic:
simp [h]

Result:
no goals

Proof state:
m n : ZNum
h : Ordering.casesOn Ordering.eq (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Tactic:
simp only at h

Result:
m n : ZNum
h : m = n
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem cons_one {α : Fin (n + 2) → Sort*} (x : α 0) (p : ∀ i : Fin n.succ, α i.succ) :
    cons x p 1 = p 0

Proof state:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p 1 = p 0

Tactic:
rw [← cons_succ x p]

Result:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p 1 = cons x p (succ 0)

Proof state:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p 1 = cons x p (succ 0)

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem lift_comp_ι {A : Type*} [Semiring A] [Algebra R A] (g : TensorAlgebra R M →ₐ[R] A) :
    lift R (g.toLinearMap.comp (ι R)) = g

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ (lift R) ((lift R).symm g) = g

Tactic:
exact (lift R).apply_symm_apply g

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ (lift R) (g.toLinearMap ∘ₗ ι R) = g

Tactic:
rw [← lift_symm_apply]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ (lift R) ((lift R).symm g) = g
-- Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean
theorem hasFiniteColimits_of_hasFiniteColimits_of_size
    (h : ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), HasColimitsOfShape J C) :
    HasFiniteColimits C where
  out := fun J hJ hhJ => by
    haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
    have l : @Equivalence J (ULiftHom (ULift J)) hJ
                           (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
      @ULiftHomULiftCategory.equiv J hJ
    apply @hasColimitsOfShape_of_equivalence (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
      (@Equivalence.symm J hJ (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
⊢ HasColimitsOfShape J C

Tactic:
haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ

Result:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift.{w, 0} J)) C
⊢ HasColimitsOfShape J C

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift.{w, 0} J)) C
l : J ≌ ULiftHom (ULift.{?u.2400, 0} J)
⊢ HasColimitsOfShape J C

Tactic:
apply @hasColimitsOfShape_of_equivalence (ULiftHom (ULift J))
  (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
  (@Equivalence.symm J hJ (ULiftHom (ULift J))
  (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift.{w, 0} J)) C
⊢ HasColimitsOfShape J C

Tactic:
have l : @Equivalence J (ULiftHom (ULift J)) hJ
                       (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
  @ULiftHomULiftCategory.equiv J hJ

Result:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift.{w, 0} J)) C
l : J ≌ ULiftHom (ULift.{?u.2400, 0} J)
⊢ HasColimitsOfShape J C
-- Mathlib/Data/Num/Lemmas.lean
theorem gcd_to_nat (a b) : (gcd a b : ℕ) = Int.gcd a b :=
  (Num.gcd_to_nat _ _).trans <| by simp only [abs_to_nat]; rfl

Proof state:
a b : ZNum
⊢ (↑a).natAbs.gcd (↑b).natAbs = (↑a).gcd ↑b

Tactic:
rfl

Result:
no goals

Proof state:
a b : ZNum
⊢ (↑a.abs).gcd ↑b.abs = (↑a).gcd ↑b

Tactic:
simp only [abs_to_nat]

Result:
a b : ZNum
⊢ (↑a).natAbs.gcd (↑b).natAbs = (↑a).gcd ↑b
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem nextCoeff_C_eq_zero (c : R) : nextCoeff (C c) = 0

Proof state:
R : Type u
inst✝ : Semiring R
c : R
⊢ (if (C c).natDegree = 0 then 0 else (C c).coeff ((C c).natDegree - 1)) = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
c : R
⊢ (C c).nextCoeff = 0

Tactic:
rw [nextCoeff]

Result:
R : Type u
inst✝ : Semiring R
c : R
⊢ (if (C c).natDegree = 0 then 0 else (C c).coeff ((C c).natDegree - 1)) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem add_not_self (x : BitVec w) : x + ~~~x = allOnes w

Proof state:
case step
w : Nat
x : BitVec w
⊢ ∀ (i : Fin w), adcb (x.getLsbD ↑i) ((~~~x).getLsbD ↑i) false = (false, (allOnes w).getLsbD ↑i)

Tactic:
simp [adcb, atLeastTwo]

Result:
no goals

Proof state:
case init
w : Nat
x : BitVec w
⊢ false = false

Tactic:
rfl

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x + ~~~x = allOnes w

Tactic:
rw [add_eq_adc, adc, iunfoldr_replace (fun _ => false) (allOnes w)]

Result:
case init
w : Nat
x : BitVec w
⊢ false = false

case step
w : Nat
x : BitVec w
⊢ ∀ (i : Fin w), adcb (x.getLsbD ↑i) ((~~~x).getLsbD ↑i) false = (false, (allOnes w).getLsbD ↑i)
-- Mathlib/Algebra/Group/Translate.lean
lemma translate_sum_right (a : G) (f : ι → G → M) (s : Finset ι) :
    τ a (∑ i ∈ s, f i) = ∑ i ∈ s, τ a (f i)

Proof state:
case h
ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : AddCommMonoid M
a : G
f : ι → G → M
s : Finset ι
x✝ : G
⊢ τ a (∑ i ∈ s, f i) x✝ = (∑ i ∈ s, τ a (f i)) x✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : AddCommMonoid M
a : G
f : ι → G → M
s : Finset ι
⊢ τ a (∑ i ∈ s, f i) = ∑ i ∈ s, τ a (f i)

Tactic:
ext

Result:
case h
ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : AddCommMonoid M
a : G
f : ι → G → M
s : Finset ι
x✝ : G
⊢ τ a (∑ i ∈ s, f i) x✝ = (∑ i ∈ s, τ a (f i)) x✝
-- Mathlib/GroupTheory/Complement.lean
theorem isComplement_singleton_right {g : G} : IsComplement S {g} ↔ S = univ

Proof state:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
⊢ IsComplement S {g} ↔ S = univ

Tactic:
refine
  ⟨fun h => top_le_iff.mp fun x _ => ?_, fun h => h ▸ isComplement_univ_singleton⟩

Result:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
⊢ x ∈ S

Proof state:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
⊢ x ∈ S

Tactic:
obtain ⟨y, hy⟩ := h.2 (x * g)

Result:
case intro
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.1 * ↑x.2) y = x * g
⊢ x ∈ S

Proof state:
case intro
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.1 * ↑x.2) y = x * g
⊢ x ∈ S

Tactic:
conv_rhs at hy => rw [← show y.2.1 = g from y.2.2]

Result:
case intro
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.1 * ↑x.2) y = x * ↑y.2
⊢ x ∈ S

Proof state:
case intro
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.1 * ↑x.2) y = x * ↑y.2
⊢ ↑y.1 ∈ S

Tactic:
exact y.1.2

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.1 * ↑x.2) y = x * ↑y.2
⊢ x ∈ S

Tactic:
rw [← mul_right_cancel hy]

Result:
case intro
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.1 * ↑x.2) y = x * ↑y.2
⊢ ↑y.1 ∈ S
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ioc_pred_right_eq_Ioo (a b : α) : Ioc a (pred b) = Ioo a b :=
  coe_injective <| by simpa using Set.Ioc_pred_right_eq_Ioo _ _

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a b : α
⊢ ↑(Ioc a (pred b)) = ↑(Ioo a b)

Tactic:
simpa using Set.Ioc_pred_right_eq_Ioo _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
    as.contains a = decide (a ∈ as)

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Array α
⊢ as.contains a = decide (a ∈ as)

Tactic:
rw [← elem_eq_contains, elem_eq_mem]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem Ordinal.not_bddAbove_compl_of_small (s : Set Ordinal.{u}) [hs : Small.{u} s] :
    ¬BddAbove sᶜ

Proof state:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
⊢ False

Tactic:
have := small_union s sᶜ

Result:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
this : Small.{u, u + 1} ↑(s ∪ sᶜ)
⊢ False

Proof state:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ ¬BddAbove sᶜ

Tactic:
rw [bddAbove_iff_small]

Result:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ ¬Small.{u, u + 1} ↑sᶜ

Proof state:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
this : Small.{u, u + 1} Ordinal.{u}
⊢ False

Tactic:
exact not_small_ordinal this

Result:
no goals

Proof state:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
this : Small.{u, u + 1} ↑(s ∪ sᶜ)
⊢ False

Tactic:
rw [union_compl_self, small_univ_iff] at this

Result:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
this : Small.{u, u + 1} Ordinal.{u}
⊢ False

Proof state:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ ¬Small.{u, u + 1} ↑sᶜ

Tactic:
intro h

Result:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
h : Small.{u, u + 1} ↑sᶜ
⊢ False
-- Mathlib/Tactic/Abel.lean
theorem term_smulg {α} [AddCommGroup α] (c n x a n' a')
    (h₁ : c * n = n') (h₂ : smulg c a = a') :
    smulg c (@termg α _ n x a) = termg n' x a'

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
c n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : c * n = n'
h₂ : smulg c a = a'
⊢ smulg c (termg n x a) = termg n' x a'

Tactic:
simp [h₂.symm, h₁.symm, termg, smulg, zsmul_add, mul_zsmul]

Result:
no goals