harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem dpow_add' (hI : DividedPowers I) {n : ℕ} (ha : a ∈ I) (hb : b ∈ I) :
    hI.dpow n (a + b) = (range (n + 1)).sum fun k ↦ hI.dpow k a * hI.dpow (n - k) b

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
hb : b ∈ I
⊢ hI.dpow n (a + b) = ∑ k ∈ range (n + 1), hI.dpow k a * hI.dpow (n - k) b

Tactic:
rw [hI.dpow_add ha hb, sum_antidiagonal_eq_sum_range_succ_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem toListImpl_eq (arr : Array α) : arr.toListImpl = arr.toList

Proof state:
α : Type u_1
arr : Array α
⊢ arr.toListImpl = arr.toList

Tactic:
simp [toListImpl, ← foldr_toList]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem eval_of (η : f ⟶ g) :
    η = (Iso.refl _).hom ≫ η ≫ (Iso.refl _).hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
f g : C
η : f ⟶ g
⊢ η = (Iso.refl f).hom ≫ η ≫ (Iso.refl g).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem bindOnSupport_eq_bind (p : PMF α) (f : α → PMF β) :
    (p.bindOnSupport fun a _ => f a) = p.bind f

Proof state:
case h
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
⊢ (p.bindOnSupport fun a x => f a) b = (p.bind f) b

Tactic:
have : ∀ a, ite (p a = 0) 0 (p a * f a b) = p a * f a b :=
  fun a => ite_eq_right_iff.2 fun h => h.symm ▸ symm (zero_mul <| f a b)

Result:
case h
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
this : ∀ (a : α), (if p a = 0 then 0 else p a * (f a) b) = p a * (f a) b
⊢ (p.bindOnSupport fun a x => f a) b = (p.bind f) b

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
⊢ (p.bindOnSupport fun a x => f a) = p.bind f

Tactic:
ext b

Result:
case h
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
⊢ (p.bindOnSupport fun a x => f a) b = (p.bind f) b

Proof state:
case h
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
this : ∀ (a : α), (if p a = 0 then 0 else p a * (f a) b) = p a * (f a) b
⊢ (p.bindOnSupport fun a x => f a) b = (p.bind f) b

Tactic:
simp only [bindOnSupport_apply fun a _ => f a, p.bind_apply f, dite_eq_ite, mul_ite,
  mul_zero, this]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pos_of_pos_of_lt_pi {x : ℝ} (h0x : 0 < x) (hxp : x < π) : 0 < sin x :=
  if hx2 : x ≤ 2 then sin_pos_of_pos_of_le_two h0x hx2
  else
    have : (2 : ℝ) + 2 = 4

Proof state:
x : ℝ
h0x : 0 < x
hxp : x < π
hx2 : ¬x ≤ 2
⊢ 2 + 2 = 4

Tactic:
norm_num

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Basic.lean
theorem _root_.injective_iff_map_eq_one {G H} [Group G] [MulOneClass H]
    [FunLike F G H] [MonoidHomClass F G H]
    (f : F) : Function.Injective f ↔ ∀ a, f a = 1 → a = 1 :=
  ⟨fun h _ => (map_eq_one_iff f h).mp, fun h x y hxy =>
    mul_inv_eq_one.1 <| h _ <| by rw [map_mul, hxy, ← map_mul, mul_inv_cancel, map_one]⟩

Proof state:
F : Type u_7
G : Type u_8
H : Type u_9
inst✝³ : Group G
inst✝² : MulOneClass H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), f a = 1 → a = 1
x y : G
hxy : f x = f y
⊢ f (x * y⁻¹) = 1

Tactic:
rw [map_mul, hxy, ← map_mul, mul_inv_cancel, map_one]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigOWith_principal
    (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) :
    IsBigOWith (sSup (Norm.norm '' (f '' s)) / ‖c‖) (𝓟 s) f fun _ => c

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn f s
hs : IsCompact s
hc : ‖c‖ ≠ 0
⊢ ∀ x ∈ s, ‖f x‖ ≤ sSup (Norm.norm '' (f '' s))

Tactic:
exact fun x hx ↦ hs.image_of_continuousOn hf |>.image continuous_norm
 |>.isLUB_sSup (Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩)
 |>.left <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn f s
hs : IsCompact s
hc : ‖c‖ ≠ 0
⊢ IsBigOWith (sSup (Norm.norm '' (f '' s)) / ‖c‖) (𝓟 s) f fun x => c

Tactic:
rw [isBigOWith_principal, div_mul_cancel₀ _ hc]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn f s
hs : IsCompact s
hc : ‖c‖ ≠ 0
⊢ ∀ x ∈ s, ‖f x‖ ≤ sSup (Norm.norm '' (f '' s))
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem eq' {a₁ b₁} {a₂ b₂ : S} :
    f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ Localization.r S (a₁, a₂) (b₁, b₂)

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a₁ b₁ : M
a₂ b₂ : ↥S
⊢ f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (Localization.r S) (a₁, a₂) (b₁, b₂)

Tactic:
rw [f.eq, Localization.r_iff_exists]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem toNat_negSucc (n : Nat) : (Int.negSucc n).toNat = 0

Proof state:
n : Nat
⊢ -[n+1].toNat = 0

Tactic:
simp [toNat]

Result:
no goals
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isNat_natMod : {a b : ℕ} → {a' b' c : ℕ} →
    IsNat a a' → IsNat b b' → Nat.mod a' b' = c → IsNat (a % b) c
  | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨by aesop⟩

Proof state:
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ % ↑n✝ = ↑(n✝¹.mod n✝)

Tactic:
aesop

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem zeta_isRoot [IsDomain B] [NeZero ((n : ℕ) : B)] : IsRoot (cyclotomic n B) (zeta n A B)

Proof state:
n : ℕ+
A : Type w
B : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsCyclotomicExtension {n} A B
inst✝¹ : IsDomain B
inst✝ : NeZero ↑↑n
⊢ (cyclotomic (↑n) B).IsRoot (zeta n A B)

Tactic:
convert aeval_zeta n A B using 0

Result:
case a
n : ℕ+
A : Type w
B : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsCyclotomicExtension {n} A B
inst✝¹ : IsDomain B
inst✝ : NeZero ↑↑n
⊢ (cyclotomic (↑n) B).IsRoot (zeta n A B) ↔ (aeval (zeta n A B)) (cyclotomic (↑n) A) = 0

Proof state:
case a
n : ℕ+
A : Type w
B : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsCyclotomicExtension {n} A B
inst✝¹ : IsDomain B
inst✝ : NeZero ↑↑n
⊢ (cyclotomic (↑n) B).IsRoot (zeta n A B) ↔ (aeval (zeta n A B)) (cyclotomic (↑n) A) = 0

Tactic:
rw [IsRoot.def, aeval_def, eval₂_eq_eval_map, map_cyclotomic]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem hasDerivAt_of_bilinear (hu : HasDerivAt u u' x) (hv : HasDerivAt v v' x) :
    HasDerivAt (fun x ↦ B (u x) (v x)) (B (u x) v' + B u' (v x)) x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : HasDerivAt u u' x
hv : HasDerivAt v v' x
⊢ HasDerivAt (fun x => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

Tactic:
simpa using (B.hasFDerivAt_of_bilinear hu.hasFDerivAt hv.hasFDerivAt).hasDerivAt

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
@[simp]
lemma map_b₄ : (W.map φ).b₄ = φ W.b₄

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ 2 * φ W.a₄ + φ W.a₁ * φ W.a₃ = φ (2 * W.a₄ + W.a₁ * W.a₃)

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ (W.map φ).b₄ = φ W.b₄

Tactic:
simp only [b₄, map_a₁, map_a₃, map_a₄]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ 2 * φ W.a₄ + φ W.a₁ * φ W.a₃ = φ (2 * W.a₄ + W.a₁ * W.a₃)
-- Mathlib/Algebra/Order/SuccPred.lean
theorem IsPredPrelimit.lt_sub_one [Sub α] [One α] [PredSubOrder α]
    (hx : IsPredPrelimit x) (hy : x < y) : x < y - 1

Proof state:
α : Type u_1
x y : α
inst✝³ : PartialOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
⊢ x < y - 1

Tactic:
rw [← pred_eq_sub_one]

Result:
α : Type u_1
x y : α
inst✝³ : PartialOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
⊢ x < pred y

Proof state:
α : Type u_1
x y : α
inst✝³ : PartialOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
⊢ x < pred y

Tactic:
exact hx.lt_pred hy

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem upperCentralSeries_one : upperCentralSeries G 1 = center G

Proof state:
G : Type u_1
inst✝ : Group G
x✝ y : G
⊢ x✝ * y * x✝⁻¹ * y⁻¹ = 1 ↔ y * x✝ = x✝ * y

Tactic:
rw [mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝ : Group G
x✝ : G
⊢ x✝ ∈ upperCentralSeries G 1 ↔ x✝ ∈ center G

Tactic:
simp only [upperCentralSeries, upperCentralSeriesAux, upperCentralSeriesStep,
  Subgroup.mem_center_iff, mem_mk, mem_bot, Set.mem_setOf_eq]

Result:
case h
G : Type u_1
inst✝ : Group G
x✝ : G
⊢ (∀ (y : G), x✝ * y * x✝⁻¹ * y⁻¹ = 1) ↔ ∀ (g : G), g * x✝ = x✝ * g

Proof state:
case h
G : Type u_1
inst✝ : Group G
x✝ : G
⊢ (∀ (y : G), x✝ * y * x✝⁻¹ * y⁻¹ = 1) ↔ ∀ (g : G), g * x✝ = x✝ * g

Tactic:
exact forall_congr' fun y => by rw [mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
⊢ upperCentralSeries G 1 = center G

Tactic:
ext

Result:
case h
G : Type u_1
inst✝ : Group G
x✝ : G
⊢ x✝ ∈ upperCentralSeries G 1 ↔ x✝ ∈ center G
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biproduct.lift_desc {T U : C} {g : ∀ j, T ⟶ f j} {h : ∀ j, f j ⟶ U} :
    biproduct.lift g ≫ biproduct.desc h = ∑ j : J, g j ≫ h j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T U : C
g : (j : J) → T ⟶ f j
h : (j : J) → f j ⟶ U
⊢ lift g ≫ desc h = ∑ j : J, g j ≫ h j

Tactic:
classical
simp [biproduct.lift_eq, biproduct.desc_eq, comp_sum, sum_comp, biproduct.ι_π_assoc, comp_dite,
  dite_comp]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T U : C
g : (j : J) → T ⟶ f j
h : (j : J) → f j ⟶ U
⊢ lift g ≫ desc h = ∑ j : J, g j ≫ h j

Tactic:
simp [biproduct.lift_eq, biproduct.desc_eq, comp_sum, sum_comp, biproduct.ι_π_assoc, comp_dite,
  dite_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem assignmentsInvariant_of_strongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) :
    StrongAssignmentsInvariant f → AssignmentsInvariant f

Proof state:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ (i, b)

Tactic:
specialize h i b hb

Result:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
pf : p ⊨ f
h : unit (i, b) ∈ f.toList
⊢ p ⊨ (i, b)

Proof state:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ f.AssignmentsInvariant

Tactic:
apply Exists.intro hsize

Result:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → Limplies (PosFin n) f (i, b)

Proof state:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → Limplies (PosFin n) f (i, b)

Tactic:
intro i b hb p pf

Result:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ (i, b)

Proof state:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
h : unit (i, b) ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → Clause.eval p x = true
⊢ p ⊨ (i, b)

Tactic:
specialize pf (unit (i, b)) h

Result:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
h : unit (i, b) ∈ f.toList
pf : Clause.eval p (unit (i, b)) = true
⊢ p ⊨ (i, b)

Proof state:
n : Nat
f : DefaultFormula n
⊢ f.StrongAssignmentsInvariant → f.AssignmentsInvariant

Tactic:
intro ⟨hsize, h⟩

Result:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ f.AssignmentsInvariant
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldrM_reverse [Monad m] (l : List α) (f : α → β → m β) (b) :
    l.reverse.foldrM f b = l.foldlM (fun x y => f y x) b :=
  (foldlM_reverse ..).symm.trans <| by simp

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : List α
f : α → β → m β
b : β
⊢ List.foldlM (fun y x => f x y) b l.reverse.reverse = List.foldlM (fun x y => f y x) b l

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ColimCoyoneda.lean
lemma injectivity (j₀ : J) (y₁ y₂ : X ⟶ Y.obj j₀)
    (hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀) :
    ∃ (j : J) (φ : j₀ ⟶ j), y₁ ≫ Y.map φ = y₂ ≫ Y.map φ

Proof state:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
j : J
φ : j₀ ⟶ j
hφ : (y₁ - y₂) ≫ Y.map φ = 0
⊢ ∃ j φ, y₁ ≫ Y.map φ = y₂ ≫ Y.map φ

Tactic:
exact ⟨j, φ, by simpa only [Preadditive.sub_comp, sub_eq_zero] using hφ⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
⊢ (y₁ - y₂) ≫ c.ι.app j₀ = 0

Tactic:
rw [Preadditive.sub_comp, sub_eq_zero, hy]

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
j : J
φ : j₀ ⟶ j
hφ : (y₁ - y₂) ≫ Y.map φ = 0
⊢ y₁ ≫ Y.map φ = y₂ ≫ Y.map φ

Tactic:
simpa only [Preadditive.sub_comp, sub_eq_zero] using hφ

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
⊢ ∃ j φ, y₁ ≫ Y.map φ = y₂ ≫ Y.map φ

Tactic:
obtain ⟨j, φ, hφ⟩ := injectivity₀ hc hXκ (y₁ - y₂)
  (by rw [Preadditive.sub_comp, sub_eq_zero, hy])

Result:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
j : J
φ : j₀ ⟶ j
hφ : (y₁ - y₂) ≫ Y.map φ = 0
⊢ ∃ j φ, y₁ ≫ Y.map φ = y₂ ≫ Y.map φ
-- Mathlib/Data/Matroid/Loop.lean
lemma IsLoop.eq_of_isCircuit_mem (he : M.IsLoop e) (hC : M.IsCircuit C) (h : e ∈ C) : C = {e}

Proof state:
α : Type u_1
M : Matroid α
e : α
C : Set α
he : M.IsLoop e
hC : M.IsCircuit C
h : e ∈ C
⊢ C = {e}

Tactic:
rw [he.isCircuit.eq_of_subset_isCircuit hC (singleton_subset_iff.mpr h)]

Result:
no goals
-- Mathlib/Tactic/NoncommRing.lean
lemma nat_lit_mul_eq_nsmul [n.AtLeastTwo] : ofNat(n) * r = OfNat.ofNat n • r

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
r : R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ OfNat.ofNat n * r = OfNat.ofNat n • r

Tactic:
simp only [nsmul_eq_mul, Nat.cast_ofNat]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
theorem pushout.congrHom_inv {X Y Z : C} {f₁ f₂ : X ⟶ Y} {g₁ g₂ : X ⟶ Z} (h₁ : f₁ = f₂)
    (h₂ : g₁ = g₂) [HasPushout f₁ g₁] [HasPushout f₂ g₂] :
    (pushout.congrHom h₁ h₂).inv =
      pushout.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simp [h₁]) (by simp [h₂])

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ f₂ ≫ 𝟙 Y = 𝟙 X ≫ f₁

Tactic:
simp [h₁]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ (congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯

Tactic:
ext <;> simp [Iso.comp_inv_eq]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ g₂ ≫ 𝟙 Z = 𝟙 X ≫ g₁

Tactic:
simp [h₂]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem LipschitzWith.coordinate [PseudoMetricSpace α] {f : α → ℓ^∞(ι)} (K : ℝ≥0) :
    LipschitzWith K f ↔ ∀ i : ι, LipschitzWith K (fun a : α ↦ f a i)

Proof state:
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
⊢ LipschitzOnWith K f Set.univ ↔ ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) Set.univ

Tactic:
apply LipschitzOnWith.coordinate

Result:
no goals

Proof state:
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
⊢ LipschitzWith K f ↔ ∀ (i : ι), LipschitzWith K fun a => ↑(f a) i

Tactic:
simp_rw [← lipschitzOnWith_univ]

Result:
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun i => ℝ) ⊤)
K : ℝ≥0
⊢ LipschitzOnWith K f Set.univ ↔ ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) Set.univ
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem quasiMeasurePreserving_div_of_right_invariant [IsMulRightInvariant μ] :
    QuasiMeasurePreserving (fun p : G × G => p.1 / p.2) (μ.prod ν) μ

Proof state:
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Group G
inst✝⁴ : MeasurableMul₂ G
μ ν : Measure G
inst✝³ : SFinite ν
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
⊢ QuasiMeasurePreserving (fun p => p.1 / p.2) (μ.prod ν) μ

Tactic:
refine QuasiMeasurePreserving.prod_of_left measurable_div (Eventually.of_forall fun y => ?_)

Result:
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Group G
inst✝⁴ : MeasurableMul₂ G
μ ν : Measure G
inst✝³ : SFinite ν
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
y : G
⊢ QuasiMeasurePreserving (fun x => (x, y).1 / (x, y).2) μ μ

Proof state:
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Group G
inst✝⁴ : MeasurableMul₂ G
μ ν : Measure G
inst✝³ : SFinite ν
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
y : G
⊢ QuasiMeasurePreserving (fun x => (x, y).1 / (x, y).2) μ μ

Tactic:
exact (measurePreserving_div_right μ y).quasiMeasurePreserving

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem pairwise_disjoint_Ioc_add_intCast :
    Pairwise (Disjoint on fun n : ℤ => Ioc (a + n) (a + n + 1))

Proof state:
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ioc (a + ↑n) (a + ↑n + 1))

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
  pairwise_disjoint_Ioc_add_zsmul a (1 : α)

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem pairwise_disjoint_Ioc_intCast : Pairwise (Disjoint on fun n : ℤ => Ioc (n : α) (n + 1)) :=
  by simpa only [zero_add] using pairwise_disjoint_Ioc_add_intCast (0 : α)

Proof state:
α : Type u_1
inst✝ : OrderedRing α
⊢ Pairwise (Disjoint on fun n => Ioc (↑n) (↑n + 1))

Tactic:
simpa only [zero_add] using pairwise_disjoint_Ioc_add_intCast (0 : α)

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
theorem involutory_invAct_eq_act {R : Type*} [Rack R] (h : IsInvolutory R) (x y : R) :
    x ◃⁻¹ y = x ◃ y

Proof state:
R : Type u_2
inst✝ : Rack R
h : IsInvolutory R
x y : R
⊢ x ◃⁻¹ y = x ◃ y

Tactic:
rw [← left_cancel x, right_inv, h x]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem isUnit_iff_isUnit_det : IsUnit A ↔ IsUnit A.det

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ IsUnit A ↔ IsUnit A.det

Tactic:
simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivDetInvertible A).nonempty_congr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem zero_tdiv : ∀ b : Int, tdiv 0 b = 0
  | ofNat _ => show ofNat _ = _ by simp
  | -[_+1] => show -ofNat _ = _ by simp

Proof state:
a✝ : Nat
⊢ ofNat (0 / a✝) = 0

Tactic:
simp

Result:
no goals

Proof state:
a✝ : Nat
⊢ -ofNat (0 / a✝.succ) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lcm.lean
theorem lcm_one_left (m : Nat) : lcm 1 m = m

Proof state:
m : Nat
⊢ lcm 1 m = m

Tactic:
simp [lcm]

Result:
no goals
-- Mathlib/Tactic/CongrExclamation.lean
theorem eq_imp_of_iff_imp {x y : Prop} {p : x = y → Prop}
    (h : (he : x ↔ y) → p (propext he)) (he : x = y) : p he

Proof state:
x y : Prop
p : x = y → Prop
h : ∀ (he : x ↔ y), p ⋯
he : x = y
⊢ p he

Tactic:
cases he

Result:
case refl
x : Prop
p : x = x → Prop
h : ∀ (he : x ↔ x), p ⋯
⊢ p ⋯

Proof state:
case refl
x : Prop
p : x = x → Prop
h : ∀ (he : x ↔ x), p ⋯
⊢ p ⋯

Tactic:
exact h Iff.rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/NormPow.lean
lemma enorm_fderiv_norm_rpow_le {f : F → E} (hf : Differentiable ℝ f)
    {x : F} {p : ℝ≥0} (hp : 1 < p) :
    ‖fderiv ℝ (fun x ↦ ‖f x‖ ^ (p : ℝ)) x‖ₑ ≤ p * ‖f x‖ₑ ^ ((p : ℝ) - 1) * ‖fderiv ℝ f x‖ₑ

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ≥0
hp : 1 < p
⊢ ‖fderiv ℝ (fun x => ‖f x‖ ^ ↑p) x‖ₑ ≤ ↑p * ‖f x‖ₑ ^ (↑p - 1) * ‖fderiv ℝ f x‖ₑ

Tactic:
simpa [enorm, ← ENNReal.coe_rpow_of_nonneg _ (sub_nonneg.2 <| NNReal.one_le_coe.2 hp.le),
  ← ENNReal.coe_mul] using nnnorm_fderiv_norm_rpow_le hf hp

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
lemma pow_div_factorial_le_exp (hx : 0 ≤ x) (n : ℕ) : x ^ n / n ! ≤ exp x :=
  calc
    x ^ n / n ! ≤ ∑ k ∈ range (n + 1), x ^ k / k ! :=
        single_le_sum (f := fun k ↦ x ^ k / k !) (fun k _ ↦ by positivity) (self_mem_range_succ n)
    _ ≤ exp x := sum_le_exp_of_nonneg hx _

Proof state:
x : ℝ
hx : 0 ≤ x
n k : ℕ
x✝ : k ∈ range (n + 1)
⊢ 0 ≤ (fun k => x ^ k / ↑k !) k

Tactic:
positivity

Result:
no goals