harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem image_emetric_closedBall (h : α ≃ᵢ β) (x : α) (r : ℝ≥0∞) :
    h '' EMetric.closedBall x r = EMetric.closedBall (h x) r

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
⊢ ⇑h '' EMetric.closedBall x r = EMetric.closedBall (h x) r

Tactic:
rw [← h.preimage_symm, h.symm.preimage_emetric_closedBall, symm_symm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.map_swap {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y)
    [HasColimitsOfShape (Discrete WalkingPair) C] :
    coprod.map (𝟙 X) f ≫ coprod.map g (𝟙 B) = coprod.map g (𝟙 A) ≫ coprod.map (𝟙 Y) f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
A B X Y : C
f : A ⟶ B
g : X ⟶ Y
inst✝ : HasColimitsOfShape (Discrete WalkingPair) C
⊢ map (𝟙 X) f ≫ map g (𝟙 B) = map g (𝟙 A) ≫ map (𝟙 Y) f

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Datatypes.lean
theorem StructuralOfExpr_monoidalComp {f g h i : C} [MonoidalCoherence g h]
    (η : f ⟶ g) (η' : f ≅ g) (ih_η : η'.hom = η) (θ : h ⟶ i) (θ' : h ≅ i) (ih_θ : θ'.hom = θ) :
    (η' ≪⊗≫ θ').hom = η ⊗≫ θ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
f g h i : C
inst✝ : MonoidalCoherence g h
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : h ⟶ i
θ' : h ≅ i
ih_θ : θ'.hom = θ
⊢ (η' ≪⊗≫ θ').hom = η ⊗≫ θ

Tactic:
simp [ih_η, ih_θ, monoidalIsoComp, monoidalComp, MonoidalCoherence.iso]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem exp_log {x : ℂ} (hx : x ≠ 0) : exp (log x) = x

Proof state:
x : ℂ
hx : x ≠ 0
⊢ cexp (log x) = x

Tactic:
rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
  Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
  mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
  mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/ZMod.lean
/-- Explicit formula for `LFunction Φ 0` when `Φ` is even. -/
@[simp] lemma LFunction_apply_zero_of_even (hΦ : Φ.Even) :
    LFunction Φ 0 = -Φ 0 / 2

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
⊢ LFunction Φ 0 = -Φ 0 / 2

Tactic:
simp only [LFunction_def_even hΦ, neg_zero, cpow_zero, hurwitzZetaEven_apply_zero,
  toAddCircle_eq_zero, mul_ite, mul_div, mul_neg_one, mul_zero, sum_ite_eq', Finset.mem_univ,
  ↓reduceIte, one_mul]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem omega_zero : ω_ 0 = ω

Proof state:
⊢ ω_ 0 = ω

Tactic:
rw [omega_eq_preOmega, add_zero, preOmega_omega0]

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive (attr := simp)]
lemma isMulFreimanHom_empty : IsMulFreimanHom n (∅ : Set α) B f where
  mapsTo := mapsTo_empty f B
  map_prod_eq_map_prod s t

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
B : Set β
f : α → β
n : ℕ
s t : Multiset α
⊢ (∀ ⦃x : α⦄, x ∈ s → x ∈ ∅) →
    (∀ ⦃x : α⦄, x ∈ t → x ∈ ∅) → s.card = n → t.card = n → s.prod = t.prod → (map f s).prod = (map f t).prod

Tactic:
aesop (add simp eq_zero_of_forall_not_mem)

Result:
no goals
-- Mathlib/Algebra/Ring/Rat.lean
lemma natCast_eq_divInt (n : ℕ) : ↑n = n /. 1

Proof state:
n : ℕ
⊢ ↑n = ↑n /. 1

Tactic:
rw [← Int.cast_natCast, intCast_eq_divInt]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem multipliable_iff_vanishing :
    Multipliable f ↔
    ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t, Disjoint t s → (∏ b ∈ t, f b) ∈ e

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
f : β → α
inst✝ : CompleteSpace α
⊢ Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_prod_vanishing]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem IsRoot.of_map {R} [CommRing R] {f : R →+* S} {x : R} {p : R[X]} (h : IsRoot (p.map f) (f x))
    (hf : Function.Injective f) : IsRoot p x

Proof state:
S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : CommRing R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ p.IsRoot x

Tactic:
rwa [IsRoot, ← (injective_iff_map_eq_zero' f).mp hf, ← eval₂_hom, ← eval_map]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem zmodEquivZPowers_symm_apply_pow (i : ℕ) :
    h.zmodEquivZPowers.symm (Additive.ofMul (⟨ζ ^ i, i, rfl⟩ : Subgroup.zpowers ζ)) = i

Proof state:
R : Type u_4
k : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ h.zmodEquivZPowers.symm (Additive.ofMul ⟨ζ ^ i, ⋯⟩) = ↑i

Tactic:
rw [← h.zmodEquivZPowers.symm_apply_apply i, zmodEquivZPowers_apply_coe_nat]

Result:
no goals
-- Mathlib/Order/Interval/Basic.lean
theorem coe_eq_pure : (s : Interval α) = Interval.pure a ↔ s = pure a

Proof state:
α : Type u_1
inst✝ : Preorder α
s : NonemptyInterval α
a : α
⊢ ↑s = Interval.pure a ↔ s = pure a

Tactic:
rw [← Interval.coe_inj, coe_pure_interval]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₄_int_mod_four (n : ℤ) : χ₄ n = χ₄ (n % 4 : ℤ)

Proof state:
n : ℤ
⊢ χ₄ ↑n = χ₄ ↑(n % 4)

Tactic:
rw [← ZMod.intCast_mod n 4, Nat.cast_ofNat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_empty [Inhabited β] {a : α} {c} : get! (empty c : Raw α (fun _ => β)) a = default

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : Inhabited β
a : α
c : Nat
⊢ get! (empty c) a = default

Tactic:
simp_to_raw using Raw₀.Const.get!_empty

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem map_add_right (f : M →ₗ[R] P) (g₁ g₂ : N →ₗ[R] Q) :
    map f (g₁ + g₂) = map f g₁ + map f g₂

Proof state:
case H.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ (map f (g₁ + g₂))) x✝¹) x✝ = (((mk R M N).compr₂ (map f g₁ + map f g₂)) x✝¹) x✝

Tactic:
simp only [tmul_add, compr₂_apply, mk_apply, map_tmul, add_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g₁ g₂ : N →ₗ[R] Q
⊢ map f (g₁ + g₂) = map f g₁ + map f g₂

Tactic:
ext

Result:
case H.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f : M →ₗ[R] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ (map f (g₁ + g₂))) x✝¹) x✝ = (((mk R M N).compr₂ (map f g₁ + map f g₂)) x✝¹) x✝
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem lt_sup_iff_not_mem {I : Submodule R M} {a : M} : (I < I ⊔ R ∙ a) ↔ a ∉ I

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Submodule R M
a : M
⊢ I < I ⊔ span R {a} ↔ a ∉ I

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem sum_range_id (n : ℕ) : ∑ i ∈ range n, i = n * (n - 1) / 2

Proof state:
n : ℕ
⊢ ∑ i ∈ range n, i = n * (n - 1) / 2

Tactic:
rw [← sum_range_id_mul_two n, Nat.mul_div_cancel _ zero_lt_two]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_mul_pow_left {q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime]
    (n m : ℕ) (neq : p ≠ q) : padicValNat p (p^n * q^m) = n

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
neq : p ≠ q
⊢ padicValNat p (p ^ n * q ^ m) = n

Tactic:
rw [padicValNat.mul (NeZero.ne' (p^n)).symm (NeZero.ne' (q^m)).symm,
  padicValNat.prime_pow, padicValNat_prime_prime_pow m neq, add_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncGE.lean
/-- `K.restrictionToTruncGE' e).f i` is an isomorphism when `¬ e.BoundaryGE i`. -/
lemma isIso_restrictionToTruncGE' (i : ι) (hi : ¬ e.BoundaryGE i) :
    IsIso ((K.restrictionToTruncGE' e).f i)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ IsIso ((K.restrictionToTruncGE' e).f i)

Tactic:
rw [K.restrictionToTruncGE'_f_eq_iso_hom_iso_inv e rfl hi]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ IsIso ((K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ hi).inv)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ IsIso ((K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ hi).inv)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem neLocus_self_sub_right : neLocus f (f - g) = g.support

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus (f - g) = g.support

Tactic:
rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem map_zipIdx (f : α → β) (l : List α) (k : Nat) :
    map (Prod.map f id) (zipIdx l k) = zipIdx (l.map f) k

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
k : Nat
⊢ map (Prod.map f id) (l.zipIdx k) = (map f l).zipIdx k

Tactic:
induction l generalizing k <;> simp_all

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem normSq_I : normSq I = 1

Proof state:
⊢ normSq I = 1

Tactic:
simp [normSq]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
theorem inl_pushoutZeroZeroIso_inv (X Y : C) [HasBinaryCoproduct X Y] :
    coprod.inl ≫ (pushoutZeroZeroIso X Y).inv = pushout.inl _ _

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ coprod.inl ≫ (pushoutZeroZeroIso X Y).inv = pushout.inl 0 0

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one (x) : (x𝖣1) = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ (x𝖣1) = 0

Tactic:
rw [← (algebraMap R S).map_one, KaehlerDifferential.kerTotal_mkQ_single_algebraMap]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_fiberwise_eq_prod_filter (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → α) :
    ∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s with g i ∈ t, f i

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → α
⊢ ∏ j ∈ t, ∏ i ∈ filter (fun i => g i = j) s, f i = ∏ i ∈ filter (fun i => g i ∈ t) s, f i

Tactic:
rw [← prod_disjiUnion, disjiUnion_filter_eq]

Result:
no goals
-- Mathlib/Topology/Order/LeftRight.lean
theorem continuousAt_iff_continuous_left'_right' {a : α} {f : α → β} :
    ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a

Tactic:
rw [continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_Iio_iff_Iic,
  continuousAt_iff_continuous_left_right]

Result:
no goals
-- Mathlib/Algebra/Ring/Semiconj.lean
theorem neg_right (h : SemiconjBy a x y) : SemiconjBy a (-x) (-y)

Proof state:
R : Type u
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy a (-x) (-y)

Tactic:
simp only [SemiconjBy, h.eq, neg_mul, mul_neg]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_of_ge {a b : α} (h : b ≤ a) : a ∆ b = a \ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
⊢ a ∆ b = a \ b

Tactic:
rw [symmDiff, sdiff_eq_bot_iff.2 h, sup_bot_eq]

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem neg_birthday_le (x : Game) : -x.birthday.toGame ≤ x

Proof state:
x : Game
⊢ -x ≤ toGame (-x).birthday

Tactic:
exact le_birthday _

Result:
no goals

Proof state:
x : Game
⊢ -toGame x.birthday ≤ x

Tactic:
rw [neg_le, ← birthday_neg]

Result:
x : Game
⊢ -x ≤ toGame (-x).birthday
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem coe_mul (I J : FractionalIdeal S P) : (↑(I * J) : Submodule R P) = I * J

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
⊢ ↑(I * J) = ↑I * ↑J

Tactic:
simp only [mul_def, coe_mk]

Result:
no goals
-- Mathlib/Topology/Instances/CantorSet.lean
theorem zero_mem_cantorSet : 0 ∈ cantorSet

Proof state:
⊢ 0 ∈ cantorSet

Tactic:
simp [cantorSet, zero_mem_preCantorSet]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toArray_eraseIdx (a : Vector α n) (i) (h) :
    (a.eraseIdx i h).toArray = a.toArray.eraseIdx i (by simp [h]) := rfl

Proof state:
α : Type ?u.21910
n : Nat
a : Vector α n
i : Nat
h : i < n
⊢ i < a.size

Tactic:
simp [h]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Compare.lean
theorem toPadicInt_comp_fromPadicInt_ext (x) :
    (toPadicInt p).comp (fromPadicInt p) x = RingHom.id ℤ_[p] x

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ((toPadicInt p).comp (fromPadicInt p)) x = (RingHom.id ℤ_[p]) x

Tactic:
rw [toPadicInt_comp_fromPadicInt]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_eq_top : a / b = ∞ ↔ a ≠ 0 ∧ b = 0 ∨ a = ∞ ∧ b ≠ ∞

Proof state:
a b : ℝ≥0∞
⊢ a / b = ⊤ ↔ a ≠ 0 ∧ b = 0 ∨ a = ⊤ ∧ b ≠ ⊤

Tactic:
simp [div_eq_mul_inv, ENNReal.mul_eq_top]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsCircuit.closure_diff_singleton_eq (hC : M.IsCircuit C) (e : α) :
    M.closure (C \ {e}) = M.closure C :=
  (em (e ∈ C)).elim
    (fun he ↦ by rw [(hC.diff_singleton_isBasis he).closure_eq_closure])
    (fun he ↦ by rw [diff_singleton_eq_self he])

Proof state:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∉ C
⊢ M.closure (C \ {e}) = M.closure C

Tactic:
rw [diff_singleton_eq_self he]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
e : α
he : e ∈ C
⊢ M.closure (C \ {e}) = M.closure C

Tactic:
rw [(hC.diff_singleton_isBasis he).closure_eq_closure]

Result:
no goals
-- Mathlib/Topology/Instances/Rat.lean
theorem Int.isUniformEmbedding_coe_rat : IsUniformEmbedding ((↑) : ℤ → ℚ) :=
  isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one <| by simpa using Int.pairwise_one_le_dist

Proof state:
⊢ Pairwise fun x y => 1 ≤ dist ↑x ↑y

Tactic:
simpa using Int.pairwise_one_le_dist

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem ite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} (a b : α) (h : c = False) : (if c then a else b) = b

Proof state:
α : Sort u
c : Prop
x✝ : Decidable c
a b : α
h : c = False
⊢ ite c a b = b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem sub_iff_right :
    a₂ ≡ b₂ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p]) := fun ⟨m, hm⟩ =>
  (Equiv.subRight m).symm.exists_congr_left.trans <| by simp [sub_sub_sub_comm, hm, sub_smul, ModEq]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a₁ a₂ b₁ b₂ : α
x✝ : a₂ ≡ b₂ [PMOD p]
m : ℤ
hm : b₂ - a₂ = m • p
⊢ (∃ b, b₁ - b₂ - (a₁ - a₂) = (Equiv.subRight m).symm.symm b • p) ↔ a₁ ≡ b₁ [PMOD p]

Tactic:
simp [sub_sub_sub_comm, hm, sub_smul, ModEq]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_val [CommMonoid α] (s : Finset α) : s.1.prod = s.prod id

Proof state:
α : Type u_3
inst✝ : CommMonoid α
s : Finset α
⊢ s.val.prod = s.prod id

Tactic:
rw [Finset.prod, Multiset.map_id]

Result:
no goals
-- Mathlib/Combinatorics/Digraph/Basic.lean
theorem iInf_adj {f : ι → Digraph V} : (⨅ i, f i).Adj a b ↔ (∀ i, (f i).Adj a b)

Proof state:
ι : Sort u_1
V : Type u_2
a b : V
f : ι → Digraph V
⊢ (⨅ i, f i).Adj a b ↔ ∀ (i : ι), (f i).Adj a b

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive boole_nsmul]
lemma pow_boole (P : Prop) [Decidable P] (a : M) :
    (a ^ if P then 1 else 0) = if P then a else 1

Proof state:
M : Type u_4
inst✝¹ : Monoid M
P : Prop
inst✝ : Decidable P
a : M
⊢ (a ^ if P then 1 else 0) = if P then a else 1

Tactic:
simp only [pow_ite, pow_one, pow_zero]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem erase_add_left_neg {a : α} (s) (h : a ∉ t) : (s + t).erase a = s.erase a + t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : a ∉ t
⊢ (s + t).erase a = s.erase a + t

Tactic:
rw [Multiset.add_comm, erase_add_right_neg s h, Multiset.add_comm]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toMeasureOfZeroLE_apply (hi : 0 ≤[i] s) (hi₁ : MeasurableSet i) (hj₁ : MeasurableSet j) :
    s.toMeasureOfZeroLE i hi₁ hi j = ((↑) : ℝ≥0 → ℝ≥0∞) ⟨s (i ∩ j), nonneg_of_zero_le_restrict
      s (zero_le_restrict_subset s hi₁ Set.inter_subset_left hi)⟩

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ (s.toMeasureOfZeroLE i hi₁ hi) j = ↑⟨↑s (i ∩ j), ⋯⟩

Tactic:
simp_rw [toMeasureOfZeroLE, Measure.ofMeasurable_apply _ hj₁, toMeasureOfZeroLE',
  s.restrict_apply hi₁ hj₁, Set.inter_comm]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Completion.lean
theorem ofRat_inv (x : β) : ofRat x⁻¹ = ((ofRat x)⁻¹ : (Cauchy abv)) :=
  congr_arg mk <| by split_ifs with h <;>
    [simp only [const_limZero.1 h, GroupWithZero.inv_zero, const_zero]; rfl]

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
⊢ const abv x⁻¹ = if h : (const abv x).LimZero then 0 else (const abv x).inv h

Tactic:
split_ifs with h <;>
[simp only [const_limZero.1 h, GroupWithZero.inv_zero, const_zero]; rfl]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zeroIsoInitial_inv [HasInitial C] : zeroIsoInitial.inv = (0 : ⊥_ C ⟶ 0)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
⊢ zeroIsoInitial.inv = 0

Tactic:
ext

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem add_div (a b c : K) : (a + b) / c = a / c + b / c

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
⊢ (a + b) / c = a / c + b / c

Tactic:
simp_rw [div_eq_mul_inv, add_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_iff_right_iff_imp : ∀ {a b : Bool}, ((a || b) = b) ↔ (a → b)

Proof state:
⊢ ∀ {a b : Bool}, (a || b) = b ↔ a = true → b = true

Tactic:
decide

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem measure_union_null (hs : μ s = 0) (ht : μ t = 0) : μ (s ∪ t) = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
hs : μ s = 0
ht : μ t = 0
⊢ μ (s ∪ t) = 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Data/Tree/Basic.lean
theorem numLeaves_eq_numNodes_succ (x : Tree α) : x.numLeaves = x.numNodes + 1

Proof state:
α : Type u
x : Tree α
⊢ x.numLeaves = x.numNodes + 1

Tactic:
induction x <;> simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/WithTop.lean
@[simp] lemma mul_top (h : a ≠ 0) : a * ⊤ = ⊤

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : WithTop α
h : a ≠ 0
⊢ a * ⊤ = ⊤

Tactic:
rw [mul_top', if_neg h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
lemma toSpec_base_isIso {f} {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
    IsIso (toSpec 𝒜 f).base

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ IsIso (toSpec 𝒜 f).base

Tactic:
convert (projIsoSpecTopComponent f_deg hm).isIso_hom

Result:
case h.e'_5
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ (toSpec 𝒜 f).base = (projIsoSpecTopComponent f_deg hm).hom

Proof state:
case h.e'_5
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ (toSpec 𝒜 f).base = (projIsoSpecTopComponent f_deg hm).hom

Tactic:
exact ConcreteCategory.hom_ext _ _ <| toSpec_base_apply_eq 𝒜

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean
lemma dominant_eq_topologically :
    @IsDominant = topologically DenseRange

Proof state:
⊢ @IsDominant = topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => DenseRange

Tactic:
ext

Result:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsDominant x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => DenseRange) x✝

Proof state:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsDominant x✝ ↔ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => DenseRange) x✝

Tactic:
exact isDominant_iff _

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem nontrivial_iff_ne_bot : Nontrivial p ↔ p ≠ ⊥

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ Nontrivial ↥p ↔ p ≠ ⊥

Tactic:
rw [iff_not_comm, not_nontrivial_iff_subsingleton, subsingleton_iff_eq_bot]

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem lift_inr (g : G) : lift fn fg h (inr g) = fg g

Proof state:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
g : G
⊢ (lift fn fg h) (inr g) = fg g

Tactic:
simp [lift]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCastD_modifyKey_self [BEq α] [LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
    getValueCastD k (modifyKey k f l) fallback = ((getValueCast? k l).map f).getD fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
fallback : β k
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getValueCastD k (modifyKey k f l) fallback = (Option.map f (getValueCast? k l)).getD fallback

Tactic:
simp [getValueCastD_modifyKey, hl, List.cast_eq_id, List.function_id_comp]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_zpow_abs (a : E) (n : ℤ) : ‖a ^ |n|‖ = ‖a ^ n‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ |n|‖ = ‖a ^ n‖

Tactic:
rcases le_total 0 n with hn | hn <;> simp [hn, abs_of_nonneg, abs_of_nonpos]

Result:
no goals