harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem negOfNat_mul_negSucc (m n : Nat) : negOfNat n * -[m+1] = ofNat (n * succ m)

Proof state:
m n : Nat
⊢ negOfNat n * -[m+1] = ofNat (n * m.succ)

Tactic:
rw [Int.mul_comm, negSucc_mul_negOfNat, Nat.mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : m.WF) :
    Const.get? (Const.alter m k f) k' =
      if k == k' then
        f (Const.get? m k)
      else
        Const.get? m k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : m.WF
⊢ get? (alter m k f) k' = if (k == k') = true then f (get? m k) else get? m k'

Tactic:
simp_to_raw using Raw₀.Const.get?_alter

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem support_nonempty_iff {x : HahnSeries Γ R} : x.support.Nonempty ↔ x ≠ 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x.support.Nonempty ↔ x ≠ 0

Tactic:
rw [support, support_nonempty_iff, Ne, coeff_fun_eq_zero_iff]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Set.Nonempty.ciSup_lt_iff {s : Set ι} {a : α} {f : ι → α} (h : s.Nonempty) (hs : s.Finite) :
    ⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a :=
  hs.ciSup_lt_iff (h.imp (by simp))

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set ι
a : α
f : ι → α
h : s.Nonempty
hs : s.Finite
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma fac' : p.map φ = eqToHom (domain_eq p f φ) ≫ f ≫ eqToHom (codomain_eq p f φ).symm

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯

Tactic:
subst_hom_lift p f φ

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem append_left_snoc {n m} {α : Sort*} (xs : Fin n → α) (x : α) (ys : Fin m → α) :
    Fin.append (Fin.snoc xs x) ys =
      Fin.append xs (Fin.cons x ys) ∘ Fin.cast (Nat.succ_add_eq_add_succ ..)

Proof state:
n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ (append xs (cons (cons x elim0 0) ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯ = append xs (cons x ys) ∘ Fin.cast ⋯

Tactic:
rfl

Result:
no goals

Proof state:
n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ append (snoc xs x) ys = append xs (cons x ys) ∘ Fin.cast ⋯

Tactic:
rw [snoc_eq_append, append_assoc, append_left_eq_cons, append_cast_right]

Result:
n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ (append xs (cons (cons x elim0 0) ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯ = append xs (cons x ys) ∘ Fin.cast ⋯
-- Mathlib/Algebra/Prime/Defs.lean
theorem not_irreducible_one [Monoid M] : ¬Irreducible (1 : M)

Proof state:
M : Type u_1
inst✝ : Monoid M
⊢ ¬Irreducible 1

Tactic:
simp [irreducible_iff]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem not_modEq_iff_ne_add_zsmul : ¬a ≡ b [PMOD p] ↔ ∀ z : ℤ, b ≠ a + z • p

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
⊢ ¬a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b ≠ a + z • p

Tactic:
rw [modEq_iff_eq_add_zsmul, not_exists]

Result:
no goals
-- Mathlib/Topology/Sequences.lean
theorem IsSeqCompact.range [SeqCompactSpace X] (f_cont : SeqContinuous f) :
    IsSeqCompact (Set.range f)

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : SeqCompactSpace X
f_cont : SeqContinuous f
⊢ IsSeqCompact (Set.range f)

Tactic:
simpa using isSeqCompact_univ.image f_cont

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
lemma integral_const_sub (f : X →ᵇ ℝ) (c : ℝ) :
    ∫ x, (const X c - f) x ∂μ = ENNReal.toReal (μ (Set.univ)) • c - ∫ x, f x ∂μ

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
inst✝¹ : OpensMeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ
c : ℝ
⊢ ∫ (x : X), (const X c - f) x ∂μ = (μ Set.univ).toReal • c - ∫ (x : X), f x ∂μ

Tactic:
simp [integral_sub (integrable_const c) (f.integrable _)]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem List.measurable_prod (l : List (α → M)) (hl : ∀ f ∈ l, Measurable f) :
    Measurable fun x => (l.map fun f : α → M => f x).prod

Proof state:
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, Measurable f
⊢ Measurable fun x => (map (fun f => f x) l).prod

Tactic:
simpa only [← Pi.list_prod_apply] using l.measurable_prod' hl

Result:
no goals
-- Mathlib/Analysis/MellinTransform.lean
theorem mellin_const_smul (f : ℝ → E) (s : ℂ) {𝕜 : Type*} [NontriviallyNormedField 𝕜]
    [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] (c : 𝕜) :
    mellin (fun t => c • f t) s = c • mellin f s

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℂ 𝕜 E
c : 𝕜
⊢ mellin (fun t => c • f t) s = c • mellin f s

Tactic:
simp only [mellin, smul_comm, integral_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem exists_add_one_eq : (∃ n, n + 1 = a) ↔ 0 < a :=
  ⟨fun ⟨n, h⟩ => by omega, fun h => ⟨a - 1, by omega⟩⟩

Proof state:
a : Nat
x✝ : ∃ n, n + 1 = a
n : Nat
h : n + 1 = a
⊢ 0 < a

Tactic:
omega

Result:
no goals

Proof state:
a : Nat
h : 0 < a
⊢ a - 1 + 1 = a

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
lemma iInf_sUnion (S : Set (Set α)) (f : α → β) :
    (⨅ x ∈ ⋃₀ S, f x) = ⨅ (s ∈ S) (x ∈ s), f x

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨅ x ∈ ⋃₀ S, f x = ⨅ s ∈ S, ⨅ x ∈ s, f x

Tactic:
rw [sUnion_eq_iUnion, iInf_iUnion, ← iInf_subtype'']

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rtake_zero : rtake l 0 = []

Proof state:
α : Type u_1
l : List α
⊢ l.rtake 0 = []

Tactic:
simp [rtake]

Result:
no goals
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem equivQuotientZPowOfEquiv_trans :
    (equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) =
      equivQuotientZPowOfEquiv (e.trans d) n

Proof state:
case h
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ ((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n)) x = (equivQuotientZPowOfEquiv (e.trans d) n) x

Tactic:
rw [← Quotient.out_eq' x]

Result:
case h
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ ((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n)) (Quotient.mk'' (Quotient.out x)) =
    (equivQuotientZPowOfEquiv (e.trans d) n) (Quotient.mk'' (Quotient.out x))

Proof state:
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
⊢ (equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) = equivQuotientZPowOfEquiv (e.trans d) n

Tactic:
ext x

Result:
case h
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ ((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n)) x = (equivQuotientZPowOfEquiv (e.trans d) n) x

Proof state:
case h
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ ((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n)) (Quotient.mk'' (Quotient.out x)) =
    (equivQuotientZPowOfEquiv (e.trans d) n) (Quotient.mk'' (Quotient.out x))

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem ofNat_add_negSucc_of_lt (h : m < n.succ) : ofNat m + -[n+1] = -[n - m+1] :=
  show subNatNat .. = _ by simp [succ_sub (le_of_lt_succ h), subNatNat]

Proof state:
m n : Nat
h : m < n.succ
⊢ subNatNat m n.succ = -[n - m+1]

Tactic:
simp [succ_sub (le_of_lt_succ h), subNatNat]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.triangle (X Y : C) :
    (coprod.associator X (⊥_ C) Y).hom ≫ coprod.map (𝟙 X) (coprod.leftUnitor Y).hom =
      coprod.map (coprod.rightUnitor X).hom (𝟙 Y)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ (associator X (⊥_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom = map (rightUnitor X).hom (𝟙 Y)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/DFinsupp/Order.lean
lemma support_monotone : Monotone (support (ι := ι) (β := α)) :=
  fun f g h a ha ↦ by rw [mem_support_iff, ← pos_iff_ne_zero] at ha ⊢; exact ha.trans_le (h _)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
h : f ≤ g
a : ι
ha : 0 < f a
⊢ 0 < g a

Tactic:
exact ha.trans_le (h _)

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
h : f ≤ g
a : ι
ha : a ∈ f.support
⊢ a ∈ g.support

Tactic:
rw [mem_support_iff, ← pos_iff_ne_zero] at ha ⊢

Result:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
h : f ≤ g
a : ι
ha : 0 < f a
⊢ 0 < g a
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[simp]
lemma Scheme.isoOfEq_rfl (X : Scheme.{u}) (U : X.Opens) : X.isoOfEq (refl U) = Iso.refl _

Proof state:
X : Scheme
U : X.Opens
⊢ X.isoOfEq ⋯ = Iso.refl ↑U

Tactic:
ext1

Result:
case w
X : Scheme
U : X.Opens
⊢ (X.isoOfEq ⋯).hom = (Iso.refl ↑U).hom

Proof state:
case w
X : Scheme
U : X.Opens
⊢ (X.isoOfEq ⋯).hom = (Iso.refl ↑U).hom

Tactic:
rw [← cancel_mono U.ι, Scheme.isoOfEq_hom_ι, Iso.refl_hom, Category.id_comp]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/House.lean
theorem supOfBasis_nonneg : 0 ≤ supOfBasis K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 0 ≤ NumberField.house.supOfBasis K

Tactic:
simp only [supOfBasis, le_sup'_iff, mem_univ, and_self,
  exists_const, house_nonneg]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_neg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : x ^ (-y) = (x ^ y)⁻¹

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if x = 0 then if -y = 0 then 1 else 0 else rexp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y))⁻¹

Tactic:
split_ifs <;> simp_all [exp_neg]

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x ^ (-y) = (x ^ y)⁻¹

Tactic:
simp only [rpow_def_of_nonneg hx]

Result:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if x = 0 then if -y = 0 then 1 else 0 else rexp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y))⁻¹
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem mkAtom_le_size (aig : AIG α) (var : α) :
    aig.decls.size ≤ (aig.mkAtom var).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
var : α
⊢ aig.decls.size ≤ (aig.mkAtom var).aig.decls.size

Tactic:
simp_arith [mkAtom]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem ImageMap.map_uniq {f g : Arrow C} [HasImage f.hom] [HasImage g.hom]
    {sq : f ⟶ g} (F G : ImageMap sq) : F.map = G.map

Proof state:
C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
F G : ImageMap sq
⊢ F.map = G.map

Tactic:
apply ImageMap.map_uniq_aux _ F.map_ι _ G.map_ι

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem exists_dist_lt_lt (hδ : 0 < δ) (hε : 0 < ε) (h : dist x z < ε + δ) :
    ∃ y, dist x y < δ ∧ dist y z < ε

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z / (ε + δ) < 1
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε

Tactic:
exact ⟨mul_lt_of_lt_one_left hδ h, mul_lt_of_lt_one_left hε h⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε

Tactic:
rw [← div_lt_one (add_pos hε hδ)] at h

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z / (ε + δ) < 1
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ε / (ε + δ) + δ / (ε + δ) = 1

Tactic:
rw [← add_div, div_self (add_pos hε hδ).ne']

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ∃ y, dist x y < δ ∧ dist y z < ε

Tactic:
refine (exists_dist_eq x z (div_nonneg hε.le <| add_nonneg hε.le hδ.le)
  (div_nonneg hδ.le <| add_nonneg hε.le hδ.le) <| by
    rw [← add_div, div_self (add_pos hε hδ).ne']).imp
  fun y hy => ?_

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y < δ ∧ dist y z < ε

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y < δ ∧ dist y z < ε

Tactic:
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε
-- Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean
lemma prop_of_isZero [P.ContainsZero] [P.IsClosedUnderIsomorphisms]
    {Z : C} (hZ : IsZero Z) :
    P Z

Proof state:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero Z
⊢ P Z

Tactic:
obtain ⟨Z₀, hZ₀, h₀⟩ := P.exists_prop_of_containsZero

Result:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero Z
Z₀ : C
hZ₀ : IsZero Z₀
h₀ : P Z₀
⊢ P Z

Proof state:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero Z
Z₀ : C
hZ₀ : IsZero Z₀
h₀ : P Z₀
⊢ P Z

Tactic:
exact P.prop_of_iso (hZ₀.iso hZ) h₀

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem leftUnitor_comp (f : a ⟶ b) (g : b ⟶ c) :
    (λ_ (f ≫ g)).hom = (α_ (𝟙 a) f g).inv ≫ (λ_ f).hom ▷ g

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ (f ≫ g)).hom = (α_ (𝟙 a) f g).inv ≫ (λ_ f).hom ▷ g

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean
lemma smul_eq_zero_iff_right (hc : c ≠ 0) : c • x = 0 ↔ x = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
hc : c ≠ 0
⊢ c • x = 0 ↔ x = 0

Tactic:
simp [hc]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem productMap_left_apply (a : A) : productMap f g (a ⊗ₜ 1) = f a

Proof state:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
a : A
⊢ (productMap f g) (a ⊗ₜ[R] 1) = f a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
@[simp]
lemma card_sdiff_add_card_inter (s t : Finset α) :
    #(s \ t) + #(s ∩ t) = #s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s \ t) + #(s ∩ t) = #s

Tactic:
rw [← card_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]

Result:
no goals
-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem monotone_iUnionUpTo : Monotone p.iUnionUpTo

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
⊢ Monotone p.iUnionUpTo

Tactic:
intro i j hij

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
i j : Ordinal.{u}
hij : i ≤ j
⊢ p.iUnionUpTo i ≤ p.iUnionUpTo j

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
i j : Ordinal.{u}
hij : i ≤ j
⊢ ⋃ j, ball (p.c (p.index ↑j)) (p.r (p.index ↑j)) ≤ ⋃ j_1, ball (p.c (p.index ↑j_1)) (p.r (p.index ↑j_1))

Tactic:
exact iUnion_mono' fun r => ⟨⟨r, r.2.trans_le hij⟩, Subset.rfl⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
i j : Ordinal.{u}
hij : i ≤ j
⊢ p.iUnionUpTo i ≤ p.iUnionUpTo j

Tactic:
simp only [iUnionUpTo]

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
i j : Ordinal.{u}
hij : i ≤ j
⊢ ⋃ j, ball (p.c (p.index ↑j)) (p.r (p.index ↑j)) ≤ ⋃ j_1, ball (p.c (p.index ↑j_1)) (p.r (p.index ↑j_1))
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem isLittleO_pow_exp_atTop {n : ℕ} : (fun x : ℝ => x ^ n) =o[atTop] Real.exp

Proof state:
n : ℕ
⊢ (fun x => x ^ n) =o[atTop] rexp

Tactic:
simpa [isLittleO_iff_tendsto fun x hx => ((exp_pos x).ne' hx).elim] using
  tendsto_div_pow_mul_exp_add_atTop 1 0 n zero_ne_one

Result:
no goals
-- Mathlib/Data/Finset/Fold.lean
theorem fold_map {g : γ ↪ α} {s : Finset γ} : (s.map g).fold op b f = s.fold op b (f ∘ g)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
g : γ ↪ α
s : Finset γ
⊢ fold op b f (map g s) = fold op b (f ∘ ⇑g) s

Tactic:
simp only [fold, map, Multiset.map_map]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem coe_algEquivOfEq {p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) :
    (algEquivOfEq hp h_eq).toFun = liftHom p (root q) (by rw [h_eq, aeval_eq, mk_self]) :=
  rfl

Proof state:
K : Type ?u.365805
L : Type ?u.365808
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p q : K[X]
hp : p ≠ 0
h_eq : p = q
⊢ (aeval (root q)) p = 0

Tactic:
rw [h_eq, aeval_eq, mk_self]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem le_of_dvd : ∀ {a b : Ordinal}, b ≠ 0 → a ∣ b → a ≤ b
  -- Porting note: `⟨b, rfl⟩ => by` → `⟨b, e⟩ => by subst e`
  | a, _, b0, ⟨b, e⟩ => by
    subst e
    -- Porting note: `Ne` is required.
    simpa only [mul_one] using
      mul_le_mul_left'
        (one_le_iff_ne_zero.2 fun h : b = 0 => by
          simp only [h, mul_zero, Ne, not_true_eq_false] at b0) a

Proof state:
a b : Ordinal.{u_4}
b0 : a * b ≠ 0
h : b = 0
⊢ False

Tactic:
simp only [h, mul_zero, Ne, not_true_eq_false] at b0

Result:
no goals

Proof state:
a x✝ : Ordinal.{u_4}
b0 : x✝ ≠ 0
b : Ordinal.{u_4}
e : x✝ = a * b
⊢ a ≤ x✝

Tactic:
subst e

Result:
a b : Ordinal.{u_4}
b0 : a * b ≠ 0
⊢ a ≤ a * b

Proof state:
a b : Ordinal.{u_4}
b0 : a * b ≠ 0
⊢ a ≤ a * b

Tactic:
simpa only [mul_one] using
  mul_le_mul_left'
    (one_le_iff_ne_zero.2 fun h : b = 0 => by
      simp only [h, mul_zero, Ne, not_true_eq_false] at b0) a

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem inv (h : Irrational x) : Irrational x⁻¹ :=
  of_inv <| by rwa [inv_inv]

Proof state:
x : ℝ
h : Irrational x
⊢ Irrational x⁻¹⁻¹

Tactic:
rwa [inv_inv]

Result:
no goals
-- Mathlib/Algebra/Colimit/Ring.lean
theorem exists_inv {p : Ring.DirectLimit G f} : p ≠ 0 → ∃ y, p * y = 1 :=
  Ring.DirectLimit.induction_on p fun i x H ↦
    ⟨Ring.DirectLimit.of G f i x⁻¹, by
      rw [← (Ring.DirectLimit.of _ _ _).map_mul,
        mul_inv_cancel₀ fun h : x = 0 ↦ H <| by rw [h, (Ring.DirectLimit.of _ _ _).map_zero],
        (Ring.DirectLimit.of _ _ _).map_one]⟩

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
i : ι
x : G i
H : (Ring.DirectLimit.of G f i) x ≠ 0
h : x = 0
⊢ (Ring.DirectLimit.of G f i) x = 0

Tactic:
rw [h, (Ring.DirectLimit.of _ _ _).map_zero]

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
i : ι
x : G i
H : (Ring.DirectLimit.of G f i) x ≠ 0
⊢ (Ring.DirectLimit.of G f i) x * (Ring.DirectLimit.of G f i) x⁻¹ = 1

Tactic:
rw [← (Ring.DirectLimit.of _ _ _).map_mul,
  mul_inv_cancel₀ fun h : x = 0 ↦ H <| by rw [h, (Ring.DirectLimit.of _ _ _).map_zero],
  (Ring.DirectLimit.of _ _ _).map_one]

Result:
no goals
-- Mathlib/Data/Finset/Dedup.lean
theorem val_toFinset [DecidableEq α] (s : Finset α) : s.val.toFinset = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.val.toFinset = s

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ s.val.toFinset ↔ a✝ ∈ s

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ s.val.toFinset ↔ a✝ ∈ s

Tactic:
rw [Multiset.mem_toFinset, ← mem_def]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem terminates_congr {c₁ c₂ : Computation α} (h : c₁ ~ c₂) : Terminates c₁ ↔ Terminates c₂

Proof state:
α : Type u
c₁ c₂ : Computation α
h : c₁ ~ c₂
⊢ c₁.Terminates ↔ c₂.Terminates

Tactic:
simp only [terminates_iff, exists_congr h]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem lt_succ_castPred_iff {a b : Fin (n + 1)} (ha : a ≠ last n) :
    b < succ (a.castPred ha) ↔ b ≤ a

Proof state:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ b < (a.castPred ha).succ ↔ b ≤ a

Tactic:
rw [succ_castPred_eq_castPred_succ ha, lt_castPred_succ_iff]

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem inclusion_injective : Function.Injective (inclusion h) := fun x y ↦ by
  simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x y : ↥K
⊢ (inclusion h) x = (inclusion h) y → x = y

Tactic:
simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem ext_norm_arg {x y : ℂ} (h₁ : ‖x‖ = ‖y‖) (h₂ : x.arg = y.arg) : x = y

Proof state:
x y : ℂ
h₁ : ‖x‖ = ‖y‖
h₂ : x.arg = y.arg
⊢ x = y

Tactic:
rw [← norm_mul_exp_arg_mul_I x, ← norm_mul_exp_arg_mul_I y, h₁, h₂]

Result:
no goals