harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem π_of_isColimit {f : J → C} {t : Bicone f} (ht : IsColimit t.toCocone) (j : J) :
    t.π j = ht.desc (Cofan.mk _ fun j' => if h : j' = j then eqToHom (congr_arg f h) else 0) :=
  ht.hom_ext fun j' => by
    rw [ht.fac]
    simp [t.ι_π]

Proof state:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j = (Cofan.mk (f j) fun j' => if h : j' = j then eqToHom ⋯ else 0).ι.app j'

Tactic:
simp [t.ι_π]

Result:
no goals

Proof state:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j =
    t.toCocone.ι.app j' ≫ ht.desc (Cofan.mk (f j) fun j' => if h : j' = j then eqToHom ⋯ else 0)

Tactic:
rw [ht.fac]

Result:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j = (Cofan.mk (f j) fun j' => if h : j' = j then eqToHom ⋯ else 0).ι.app j'
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal_diagonal [DecidableEq m] (d : o → m → α) :
    (blockDiagonal fun k => diagonal (d k)) = diagonal fun ik => d ik.2 ik.1

Proof state:
case a.mk.mk
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ blockDiagonal (fun k => diagonal (d k)) (i, k) (j, k') = diagonal (fun ik => d ik.2 ik.1) (i, k) (j, k')

Tactic:
simp only [blockDiagonal_apply, diagonal_apply, Prod.mk.inj_iff, ← ite_and]

Result:
case a.mk.mk
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (if k = k' ∧ i = j then d k i else 0) = if i = j ∧ k = k' then d k i else 0

Proof state:
case a.mk.mk
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (if k = k' ∧ i = j then d k i else 0) = if i = j ∧ k = k' then d k i else 0

Tactic:
congr 1

Result:
case a.mk.mk.e_c
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (k = k' ∧ i = j) = (i = j ∧ k = k')

Proof state:
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
⊢ (blockDiagonal fun k => diagonal (d k)) = diagonal fun ik => d ik.2 ik.1

Tactic:
ext ⟨i, k⟩ ⟨j, k'⟩

Result:
case a.mk.mk
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ blockDiagonal (fun k => diagonal (d k)) (i, k) (j, k') = diagonal (fun ik => d ik.2 ik.1) (i, k) (j, k')

Proof state:
case a.mk.mk.e_c
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (k = k' ∧ i = j) = (i = j ∧ k = k')

Tactic:
rw [and_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem subNatNat_sub (h : n ≤ m) (k : Nat) : subNatNat (m - n) k = subNatNat m (k + n)

Proof state:
n m : Nat
h : n ≤ m
k : Nat
⊢ subNatNat (m - n) k = subNatNat m (k + n)

Tactic:
rwa [← subNatNat_add_add _ _ n, Nat.sub_add_cancel]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem inr_of_isLimit {X Y : C} {t : BinaryBicone X Y} (ht : IsLimit t.toCone) :
    t.inr = ht.lift (BinaryFan.mk 0 (𝟙 Y))

Proof state:
case x
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ ∀ (j : Discrete WalkingPair), t.inr ≫ t.toCone.π.app j = (BinaryFan.mk 0 (𝟙 Y)).π.app j

Tactic:
rintro ⟨⟨⟩⟩ <;> dsimp <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ t.inr = ht.lift (BinaryFan.mk 0 (𝟙 Y))

Tactic:
apply ht.uniq (BinaryFan.mk 0 (𝟙 Y))

Result:
case x
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ ∀ (j : Discrete WalkingPair), t.inr ≫ t.toCone.π.app j = (BinaryFan.mk 0 (𝟙 Y)).π.app j
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_sub_eq_of_lt_right (h : v x < v y) : v (x - y) = v y

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x < v y
⊢ v (x - y) = v y

Tactic:
rw [sub_eq_add_neg, map_add_eq_of_lt_right, map_neg]

Result:
case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x < v y
⊢ v x < v (-y)

Proof state:
case h
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x < v y
⊢ v x < v (-y)

Tactic:
rwa [map_neg]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblXYZ_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy : P y * Q z ≠ W.negY Q * P z) :
    W.dblXYZ P = W.dblZ P •
      ![W.toAffine.addX (P x / P z) (Q x / Q z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)), 1]

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.dblXYZ P =
    W.dblZ P •
      ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
          ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]

Tactic:
have hZ : IsUnit <| W.dblZ P := isUnit_dblZ_of_Y_ne' hP hQ hPz hQz hx hy

Result:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
hZ : IsUnit (W.dblZ P)
⊢ W.dblXYZ P =
    W.dblZ P •
      ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
          ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
hZ : IsUnit (W.dblZ P)
⊢ W.dblXYZ P =
    W.dblZ P •
      ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
          ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]

Tactic:
erw [dblXYZ, smul_fin3, ← dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel,
  ← dblY_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel, mul_one]

Result:
no goals
-- Mathlib/Tactic/Abel.lean
theorem zero_termg {α} [AddCommGroup α] (x a) : @termg α _ 0 x a = a

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
x a : α
⊢ termg 0 x a = a

Tactic:
simp [termg, zero_zsmul]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem eval_preimage [DecidableEq ι] {s : Set (α i)} :
    eval i ⁻¹' s = pi univ (update (fun _ => univ) i s)

Proof state:
ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
⊢ eval i ⁻¹' s = univ.pi (update (fun x => univ) i s)

Tactic:
ext x

Result:
case h
ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
x : (x : ι) → α x
⊢ x ∈ eval i ⁻¹' s ↔ x ∈ univ.pi (update (fun x => univ) i s)

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
x : (x : ι) → α x
⊢ x ∈ eval i ⁻¹' s ↔ x ∈ univ.pi (update (fun x => univ) i s)

Tactic:
simp [@forall_update_iff _ (fun i => Set (α i)) _ _ _ _ fun i' y => x i' ∈ y]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- We can express `ArithmeticFunction.vonMangoldt.residueClass` as a linear combination
of twists of the von Mangoldt function by Dirichlet characters. -/
lemma residueClass_eq (ha : IsUnit a) :
    ↗(residueClass a) = (q.totient : ℂ)⁻¹ •
      ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ • (fun n : ℕ ↦ χ n * vonMangoldt n)

Proof state:
case h
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
n : ℕ
⊢ ↑(residueClass a n) = ((↑q.totient)⁻¹ • ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ • fun n => χ ↑n * ↑(Λ n)) n

Tactic:
simpa only [Pi.smul_apply, Finset.sum_apply, smul_eq_mul, ← mul_assoc]
  using residueClass_apply ha n

Result:
no goals

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
⊢ (fun n => ↑(residueClass a n)) = (↑q.totient)⁻¹ • ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ • fun n => χ ↑n * ↑(Λ n)

Tactic:
ext1 n

Result:
case h
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
n : ℕ
⊢ ↑(residueClass a n) = ((↑q.totient)⁻¹ • ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ • fun n => χ ↑n * ↑(Λ n)) n
-- Mathlib/Computability/Tape.lean
theorem BlankExtends.refl {Γ} [Inhabited Γ] (l : List Γ) : BlankExtends l l :=
  ⟨0, by simp⟩

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
⊢ l = l ++ List.replicate 0 default

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem mem_prepartition_iff {B I : Box ι} :
    I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
⊢ I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I

Tactic:
classical
rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B I : Box ι
⊢ I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I

Tactic:
rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem map_pow (f : M →ₗ[R] M) (g : N →ₗ[R] N) (n : ℕ) :
    map f g ^ n = map (f ^ n) (g ^ n)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] M
g : N →ₗ[R] N
n : ℕ
⊢ map f g ^ n = map (f ^ n) (g ^ n)

Tactic:
induction n with
| zero => simp only [pow_zero, TensorProduct.map_one]
| succ n ih => simp only [pow_succ', ih, TensorProduct.map_mul]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] M
g : N →ₗ[R] N
n : ℕ
ih : map f g ^ n = map (f ^ n) (g ^ n)
⊢ map f g ^ (n + 1) = map (f ^ (n + 1)) (g ^ (n + 1))

Tactic:
simp only [pow_succ', ih, TensorProduct.map_mul]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ map f g ^ 0 = map (f ^ 0) (g ^ 0)

Tactic:
simp only [pow_zero, TensorProduct.map_one]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_zero (x : ℂ) : x ^ (0 : ℂ) = 1

Proof state:
x : ℂ
⊢ x ^ 0 = 1

Tactic:
simp [cpow_def]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean
theorem ContinuousLinearMap.hasFDerivAt_of_bilinear {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E}
    {g' : G' →L[𝕜] F} {x : G'} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
    HasFDerivAt (fun y => B (f y) (g y)) (B.precompR G' (f x) g' + B.precompL G' f' (g x)) x

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
B : E →L[𝕜] F →L[𝕜] G
f : G' → E
g : G' → F
f' : G' →L[𝕜] E
g' : G' →L[𝕜] F
x : G'
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
⊢ HasFDerivAt (fun y => (B (f y)) (g y)) (((precompR G' B) (f x)) g' + ((precompL G' B) f') (g x)) x

Tactic:
exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp x (hf.prod hg)

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem isPreconnected_image {s : Set X} (h : X ≃ₜ Y) :
    IsPreconnected (h '' s) ↔ IsPreconnected s :=
  ⟨fun hs ↦ by simpa only [image_symm, preimage_image]
    using hs.image _ h.symm.continuous.continuousOn,
    fun hs ↦ hs.image _ h.continuous.continuousOn⟩

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
hs : IsPreconnected (⇑h '' s)
⊢ IsPreconnected s

Tactic:
simpa only [image_symm, preimage_image]
using hs.image _ h.symm.continuous.continuousOn

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem boundedLimitRec_limit {l} (lLim : l.IsLimit) {C} (o H₁ H₂ H₃ oLim) :
    @boundedLimitRecOn l lLim C o H₁ H₂ H₃ = H₃ o oLim (fun x _ ↦
    @boundedLimitRecOn l lLim C x H₁ H₂ H₃)

Proof state:
l : Ordinal.{u_4}
lLim : l.IsLimit
C : ↑(Iio l) → Sort u_5
o : ↑(Iio l)
H₁ : C ⟨0, ⋯⟩
H₂ : (o : ↑(Iio l)) → C o → C ⟨succ ↑o, ⋯⟩
H₃ : (o : ↑(Iio l)) → (↑o).IsLimit → ((o' : ↑(Iio l)) → o' < o → C o') → C o
oLim : (↑o).IsLimit
⊢ (H₃ ⟨↑o, ⋯⟩ ?h fun _o' h =>
      (fun x _h =>
          x.limitRecOn (fun x => H₁) (fun o ih h => H₂ ⟨o, ⋯⟩ (ih ⋯)) fun _o ho ih x =>
            H₃ ⟨_o, x⟩ ho fun _o' h => ih (↑_o') h ⋯)
        (↑_o') h ⋯) =
    H₃ o oLim fun x x_1 => boundedLimitRecOn lLim x H₁ H₂ H₃

case h
l : Ordinal.{u_4}
lLim : l.IsLimit
C : ↑(Iio l) → Sort u_5
o : ↑(Iio l)
H₁ : C ⟨0, ⋯⟩
H₂ : (o : ↑(Iio l)) → C o → C ⟨succ ↑o, ⋯⟩
H₃ : (o : ↑(Iio l)) → (↑o).IsLimit → ((o' : ↑(Iio l)) → o' < o → C o') → C o
oLim : (↑o).IsLimit
⊢ (↑o).IsLimit

Tactic:
rfl

Result:
no goals

Proof state:
l : Ordinal.{u_4}
lLim : l.IsLimit
C : ↑(Iio l) → Sort u_5
o : ↑(Iio l)
H₁ : C ⟨0, ⋯⟩
H₂ : (o : ↑(Iio l)) → C o → C ⟨succ ↑o, ⋯⟩
H₃ : (o : ↑(Iio l)) → (↑o).IsLimit → ((o' : ↑(Iio l)) → o' < o → C o') → C o
oLim : (↑o).IsLimit
⊢ boundedLimitRecOn lLim o H₁ H₂ H₃ = H₃ o oLim fun x x_1 => boundedLimitRecOn lLim x H₁ H₂ H₃

Tactic:
rw [boundedLimitRecOn, limitRecOn_limit]

Result:
l : Ordinal.{u_4}
lLim : l.IsLimit
C : ↑(Iio l) → Sort u_5
o : ↑(Iio l)
H₁ : C ⟨0, ⋯⟩
H₂ : (o : ↑(Iio l)) → C o → C ⟨succ ↑o, ⋯⟩
H₃ : (o : ↑(Iio l)) → (↑o).IsLimit → ((o' : ↑(Iio l)) → o' < o → C o') → C o
oLim : (↑o).IsLimit
⊢ (H₃ ⟨↑o, ⋯⟩ ?h fun _o' h =>
      (fun x _h =>
          x.limitRecOn (fun x => H₁) (fun o ih h => H₂ ⟨o, ⋯⟩ (ih ⋯)) fun _o ho ih x =>
            H₃ ⟨_o, x⟩ ho fun _o' h => ih (↑_o') h ⋯)
        (↑_o') h ⋯) =
    H₃ o oLim fun x x_1 => boundedLimitRecOn lLim x H₁ H₂ H₃

case h
l : Ordinal.{u_4}
lLim : l.IsLimit
C : ↑(Iio l) → Sort u_5
o : ↑(Iio l)
H₁ : C ⟨0, ⋯⟩
H₂ : (o : ↑(Iio l)) → C o → C ⟨succ ↑o, ⋯⟩
H₃ : (o : ↑(Iio l)) → (↑o).IsLimit → ((o' : ↑(Iio l)) → o' < o → C o') → C o
oLim : (↑o).IsLimit
⊢ (↑o).IsLimit
-- Mathlib/CategoryTheory/LiftingProperties/Limits.lean
lemma IsPullback.hasLiftingProperty (h : IsPullback s f g t)
    {X' Y' : C} (f' : X' ⟶ Y') [HasLiftingProperty f' g] : HasLiftingProperty f' f where
  sq_hasLift := fun {u v} sq ↦ by
    have w : (u ≫ s) ≫ g = f' ≫ v ≫ t

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ ⋯.lift ≫ g = v ≫ t

Tactic:
rw [CommSq.fac_right]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
⊢ (u ≫ s) ≫ g = f' ≫ v ≫ t

Tactic:
rw [Category.assoc, h.toCommSq.w, ← Category.assoc, ← Category.assoc, sq.w]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ (f' ≫ h.lift ⋯.lift v ⋯) ≫ f = u ≫ f

Tactic:
rw [Category.assoc, h.lift_snd, sq.w]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ (f' ≫ h.lift ⋯.lift v ⋯) ≫ s = u ≫ s

Tactic:
rw [Category.assoc, h.lift_fst, CommSq.fac_left]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ sq.HasLift

Tactic:
exact ⟨h.lift (CommSq.mk w).lift v (by rw [CommSq.fac_right]),
  h.hom_ext (by rw [Category.assoc, h.lift_fst, CommSq.fac_left])
    (by rw [Category.assoc, h.lift_snd, sq.w]), h.lift_snd _ _ _⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
⊢ sq.HasLift

Tactic:
have w : (u ≫ s) ≫ g = f' ≫ v ≫ t := by
  rw [Category.assoc, h.toCommSq.w, ← Category.assoc, ← Category.assoc, sq.w]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ sq.HasLift
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_add_two : ∀ n, C R (n + 2) = X * C R (n + 1) - C R n
  | (k : ℕ) => C.eq_3 R k
  | -(k + 1 : ℕ) => by linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) C.eq_4 R k

Proof state:
case a.a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ C R (-↑(k + 1) + 2) + (X * C R (-↑k) - C R (-↑k + 1)) -
      (X * C R (-↑(k + 1) + 1) - C R (-↑(k + 1)) + C R (Int.negSucc k)) =
    0

Tactic:
simp [Int.negSucc_eq]

Result:
case a.a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ C R (-1 + -↑k + 2) + (X * C R (-↑k) - C R (-↑k + 1)) - X * C R (-↑k) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ C R (-↑(k + 1) + 2) = X * C R (-↑(k + 1) + 1) - C R (-↑(k + 1))

Tactic:
linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) C.eq_4 R k

Result:
no goals

Proof state:
case a.a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ C R (-1 + -↑k + 2) + (X * C R (-↑k) - C R (-↑k + 1)) - X * C R (-↑k) = 0

Tactic:
ring_nf

Result:
no goals
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem intrinsicClosure_nonempty : (intrinsicClosure 𝕜 s).Nonempty ↔ s.Nonempty :=
  ⟨by simp_rw [nonempty_iff_ne_empty]; rintro h rfl; exact h intrinsicClosure_empty,
    Nonempty.mono subset_intrinsicClosure⟩

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
h : intrinsicClosure 𝕜 ∅ ≠ ∅
⊢ False

Tactic:
exact h intrinsicClosure_empty

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ intrinsicClosure 𝕜 s ≠ ∅ → s ≠ ∅

Tactic:
rintro h rfl

Result:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
h : intrinsicClosure 𝕜 ∅ ≠ ∅
⊢ False

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ (intrinsicClosure 𝕜 s).Nonempty → s.Nonempty

Tactic:
simp_rw [nonempty_iff_ne_empty]

Result:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ intrinsicClosure 𝕜 s ≠ ∅ → s ≠ ∅
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
/-- See `expGrowthInf_mul_le` for a version with swapped argument `u` and `v`. -/
lemma expGrowthInf_mul_le' {u v : ℕ → ℝ≥0∞} (h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤)
    (h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥) :
    expGrowthInf (u * v) ≤ expGrowthInf u + expGrowthSup v

Proof state:
u v : ℕ → ℝ≥0∞
h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthInf (u * v) ≤ expGrowthInf u + expGrowthSup v

Tactic:
rw [mul_comm, add_comm]

Result:
u v : ℕ → ℝ≥0∞
h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthInf (v * u) ≤ expGrowthSup v + expGrowthInf u

Proof state:
u v : ℕ → ℝ≥0∞
h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthInf (v * u) ≤ expGrowthSup v + expGrowthInf u

Tactic:
exact expGrowthInf_mul_le h'.symm h.symm

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Construction.lean
lemma ιFunctorObj_extension {i : I} (t : A i ⟶ X) (b : B i ⟶ S)
    (sq : CommSq t (f i) πX b) :
    ∃ (l : B i ⟶ functorObj f πX), f i ≫ l = t ≫ ιFunctorObj f πX ∧
      l ≫ πFunctorObj f πX = b :=
  ⟨Sigma.ι (functorObjTgtFamily f πX) (FunctorObjIndex.mk i t b sq.w) ≫
    ρFunctorObj f πX, (FunctorObjIndex.mk i t b _).comm, by simp⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
i : I
t : A i ⟶ X
b : B i ⟶ S
sq : CommSq t (f i) πX b
⊢ (Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := ⋯ } ≫ ρFunctorObj f πX) ≫ πFunctorObj f πX = b

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Connected/LocPathConnected.lean
theorem IsOpen.pathComponent (x : X) : IsOpen (pathComponent x)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x : X
⊢ IsOpen (pathComponentIn x univ)

Tactic:
exact isOpen_univ.pathComponentIn _

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x : X
⊢ IsOpen (pathComponent x)

Tactic:
rw [← pathComponentIn_univ]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x : X
⊢ IsOpen (pathComponentIn x univ)
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sSup_ord {s : Set Cardinal.{u}} (hs : BddAbove s) : (sSup s).ord = sSup (ord '' s) :=
  eq_of_forall_ge_iff fun a => by
    rw [csSup_le_iff'
        (bddAbove_iff_small.2 (@small_image _ _ _ s (Cardinal.bddAbove_iff_small.1 hs))),
      ord_le, csSup_le_iff' hs]
    simp [ord_le]

Proof state:
s : Set Cardinal.{u}
hs : BddAbove s
a : Ordinal.{u}
⊢ (sSup s).ord ≤ a ↔ sSup (ord '' s) ≤ a

Tactic:
rw [csSup_le_iff'
    (bddAbove_iff_small.2 (@small_image _ _ _ s (Cardinal.bddAbove_iff_small.1 hs))),
  ord_le, csSup_le_iff' hs]

Result:
s : Set Cardinal.{u}
hs : BddAbove s
a : Ordinal.{u}
⊢ (∀ x ∈ s, x ≤ a.card) ↔ ∀ x ∈ ord '' s, x ≤ a

Proof state:
s : Set Cardinal.{u}
hs : BddAbove s
a : Ordinal.{u}
⊢ (∀ x ∈ s, x ≤ a.card) ↔ ∀ x ∈ ord '' s, x ≤ a

Tactic:
simp [ord_le]

Result:
no goals