harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Iso.lean
@[reassoc (attr := simp)]
lemma map_inv_hom_id (F : C ⥤ D) :
    F.map e.inv ≫ F.map e.hom = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
X Y : C
e : X ≅ Y
F : C ⥤ D
⊢ F.map e.inv ≫ F.map e.hom = 𝟙 (F.obj Y)

Tactic:
rw [← F.map_comp, e.inv_hom_id, F.map_id]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem nhds_top : 𝓝 ∞ = ⨅ (a) (_ : a ≠ ∞), 𝓟 (Ioi a) :=
  nhds_top_order.trans <| by simp [lt_top_iff_ne_top, Ioi]

Proof state:
⊢ ⨅ l, ⨅ (_ : l < ⊤), 𝓟 (Ioi l) = ⨅ a, ⨅ (_ : a ≠ ⊤), 𝓟 (Ioi a)

Tactic:
simp [lt_top_iff_ne_top, Ioi]

Result:
no goals
-- Mathlib/RingTheory/Artinian/Module.lean
lemma primeSpectrum_asIdeal_range_eq :
    range PrimeSpectrum.asIdeal = (range <| MaximalSpectrum.asIdeal (R := R))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
⊢ range PrimeSpectrum.asIdeal = range MaximalSpectrum.asIdeal

Tactic:
simp only [PrimeSpectrum.range_asIdeal, MaximalSpectrum.range_asIdeal,
  isPrime_iff_isMaximal]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem mul_iff_right [CommGroup β] [IsTopologicalGroup β] (hf : AEStronglyMeasurable[m] f μ) :
    AEStronglyMeasurable[m] (f * g) μ ↔ AEStronglyMeasurable[m] g μ :=
  ⟨fun h ↦ show g = f * g * f⁻¹ by simp only [mul_inv_cancel_comm] ▸ h.mul hf.inv,
    fun h ↦ hf.mul h⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝¹ : CommGroup β
inst✝ : IsTopologicalGroup β
hf : AEStronglyMeasurable f μ
h : AEStronglyMeasurable (f * g) μ
⊢ g = f * g * f⁻¹

Tactic:
simp only [mul_inv_cancel_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Iic_sub_one_eq_Iio (b : α) : Iic (b - 1) = Iio b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
b : α
⊢ Iic (b - 1) = Iio b

Tactic:
simpa [pred_eq_sub_one] using Iic_pred_eq_Iio b

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_finset_of_fintype [Fintype α] : #(Finset α) = 2 ^ Fintype.card α

Proof state:
α : Type u
inst✝ : Fintype α
⊢ #(Finset α) = 2 ^ Fintype.card α

Tactic:
simp [Pow.pow]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem mem_range_omega_iff {x : Ordinal} : x ∈ range omega ↔ ω ≤ x ∧ IsInitial x

Proof state:
x : Ordinal.{u_1}
⊢ x ∈ range ⇑ω_ ↔ ω ≤ x ∧ x.IsInitial

Tactic:
rw [range_omega, mem_setOf]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem AnalyticOnNhd.iteratedFDeriv_of_isOpen (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) (n : ℕ) :
    AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOnNhd 𝕜 f s
hs : IsOpen s
n : ℕ
⊢ AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s

Tactic:
rw [← hs.analyticOn_iff_analyticOnNhd] at h ⊢

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hs : IsOpen s
n : ℕ
⊢ AnalyticOn 𝕜 (iteratedFDeriv 𝕜 n f) s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hs : IsOpen s
n : ℕ
⊢ AnalyticOn 𝕜 (iteratedFDeriv 𝕜 n f) s

Tactic:
exact (h.iteratedFDerivWithin hs.uniqueDiffOn n).congr
  (fun x hx ↦ (iteratedFDerivWithin_of_isOpen n hs hx).symm)

Result:
no goals
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem contMDiff_toPartitionOfUnity {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {H : Type uH} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM}
    [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (f : BumpCovering ι M s)
    (hf : ∀ i, ContMDiff I 𝓘(ℝ) ∞ (f i)) (i : ι) : ContMDiff I 𝓘(ℝ) ∞ (f.toPartitionOfUnity i) :=
  (hf i).mul <| (contMDiff_finprod_cond fun j _ => contMDiff_const.sub (hf j)) <| by
    simp only [Pi.sub_def, mulSupport_one_sub]
    exact f.locallyFinite

Proof state:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : BumpCovering ι M s
hf : ∀ (i : ι), ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑(f i)
i : ι
⊢ LocallyFinite fun i => support ⇑(f i)

Tactic:
exact f.locallyFinite

Result:
no goals

Proof state:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : BumpCovering ι M s
hf : ∀ (i : ι), ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑(f i)
i : ι
⊢ LocallyFinite fun i => mulSupport fun x => 1 - (f i) x

Tactic:
simp only [Pi.sub_def, mulSupport_one_sub]

Result:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : BumpCovering ι M s
hf : ∀ (i : ι), ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑(f i)
i : ι
⊢ LocallyFinite fun i => support ⇑(f i)
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_one_iff {f : α → E'''} : f =o[l] (fun _x => 1 : α → F) ↔ Tendsto f l (𝓝 0)

Proof state:
α : Type u_1
F : Type u_4
E''' : Type u_12
inst✝³ : Norm F
inst✝² : SeminormedAddGroup E'''
l : Filter α
inst✝¹ : One F
inst✝ : NormOneClass F
f : α → E'''
⊢ (f =o[l] fun _x => 1) ↔ Tendsto f l (𝓝 0)

Tactic:
simp only [isLittleO_iff, norm_one, mul_one, Metric.nhds_basis_closedBall.tendsto_right_iff,
  Metric.mem_closedBall, dist_zero_right]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem im_eq_sub_conj (z : ℂ) : (z.im : ℂ) = (z - conj z) / (2 * I)

Proof state:
z : ℂ
⊢ ↑z.im = (z - (starRingEnd ℂ) z) / (2 * I)

Tactic:
simp only [sub_conj, ofReal_mul, ofReal_ofNat, mul_right_comm,
  mul_div_cancel_left₀ _ (mul_ne_zero two_ne_zero I_ne_zero : 2 * I ≠ 0)]

Result:
no goals
-- Mathlib/Order/Filter/Defs.lean
theorem sSup_lowerBounds (s : Set (Filter α)) : sSup (lowerBounds s) = sInf s

Proof state:
α : Type u_1
s : Set (Filter α)
⊢ sSup (lowerBounds s) = sInf s

Tactic:
simp [sInf, Filter.sInf]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma map_add_right_Ico (a b c : α) :
    (Ico a b).map (addRightEmbedding c) = Ico (a + c) (b + c)

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Ico a b = Set.Ico (a + c) (b + c)

Tactic:
exact Set.image_add_const_Ico _ _ _

Result:
no goals

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addRightEmbedding c) (Ico a b) = Ico (a + c) (b + c)

Tactic:
rw [← coe_inj, coe_map, coe_Ico, coe_Ico]

Result:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addRightEmbedding c) '' Set.Ico a b = Set.Ico (a + c) (b + c)
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem toList_formPerm_nil (x : α) : toList (formPerm ([] : List α)) x = []

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ [].formPerm.toList x = []

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs {a b : ℤ} :
    FiniteMultiplicity a b ↔ FiniteMultiplicity a.natAbs b.natAbs

Proof state:
a b : ℤ
⊢ FiniteMultiplicity a b ↔ FiniteMultiplicity a.natAbs b.natAbs

Tactic:
simp only [FiniteMultiplicity.def, ← Int.natAbs_dvd_natAbs, Int.natAbs_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem lt_irrefl (a : Fin n) : ¬ a < a

Proof state:
n : Nat
a : Fin n
⊢ ¬a < a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma natAbs_pow (n : ℤ) (k : ℕ) : Int.natAbs (n ^ k) = Int.natAbs n ^ k

Proof state:
n : ℤ
k : ℕ
⊢ (n ^ k).natAbs = n.natAbs ^ k

Tactic:
induction k with
| zero => rfl
| succ k ih => rw [Int.pow_succ, natAbs_mul, Nat.pow_succ, ih, Nat.mul_comm]

Result:
no goals

Proof state:
case succ
n : ℤ
k : ℕ
ih : (n ^ k).natAbs = n.natAbs ^ k
⊢ (n ^ (k + 1)).natAbs = n.natAbs ^ (k + 1)

Tactic:
rw [Int.pow_succ, natAbs_mul, Nat.pow_succ, ih, Nat.mul_comm]

Result:
no goals

Proof state:
case zero
n : ℤ
⊢ (n ^ 0).natAbs = n.natAbs ^ 0

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem homEquiv_naturality_left (f : X' ⟶ X) (g : F.obj X ⟶ Y) :
    (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g

Tactic:
rw [← Equiv.eq_symm_apply]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) g)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) g)

Tactic:
simp only [Equiv.symm_apply_apply, eq_self_iff_true, homEquiv_naturality_left_symm]

Result:
no goals
-- Mathlib/Probability/Kernel/Condexp.lean
theorem condExp_ae_eq_integral_condExpKernel [NormedAddCommGroup F] {f : Ω → F}
    [NormedSpace ℝ F] [CompleteSpace F] (hm : m ≤ mΩ) (hf_int : Integrable f μ) :
    μ[f|m] =ᵐ[μ] fun ω => ∫ y, f y ∂condExpKernel μ m ω :=
  ((condExp_ae_eq_integral_condExpKernel' hf_int).symm.trans (by rw [inf_of_le_left hm])).symm

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ μ[f|m ⊓ mΩ] =ᶠ[ae μ] μ[f|m]

Tactic:
rw [inf_of_le_left hm]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_mul_of_isRegular_left {f g : MvPolynomial σ R}
    (hf : IsRegular (m.leadingCoeff f)) (hg : g ≠ 0) :
    m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g ≠ 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp only [leadingCoeff, degree_mul_of_isRegular_left hf hg, coeff_mul_of_degree_add]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_pos : 0 < ⌊a⌋₊ ↔ 1 ≤ a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ 0 < ⌊a⌋₊ ↔ 1 ≤ a

Tactic:
rw [Nat.lt_iff_add_one_le, zero_add, le_floor_iff' Nat.one_ne_zero, cast_one]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem mul_one (x : A ⊗[R] B) : mul x (1 ⊗ₜ 1) = x

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ (mul x) (1 ⊗ₜ[R] 1) = x

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_ <;> simp +contextual

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem map_comap_eq_self_of_surjective
    {f : R →+* S} (hf : Function.Surjective f) (t : Subring S) : (t.comap f).map f = t :=
  map_comap_eq_self <| by simp [hf]

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
t : Subring S
⊢ t ≤ f.range

Tactic:
simp [hf]

Result:
no goals
-- Mathlib/Algebra/BigOperators/WithTop.lean
/-- A sum is finite iff all terms are finite. -/
lemma bot_lt_sum_iff : ⊥ < ∑ i ∈ s, f i ↔ ∀ i ∈ s, ⊥ < f i

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
s : Finset ι
f : ι → WithBot α
inst✝ : LT α
⊢ ⊥ < ∑ i ∈ s, f i ↔ ∀ i ∈ s, ⊥ < f i

Tactic:
simp only [WithBot.bot_lt_iff_ne_bot, ne_eq, sum_eq_bot_iff, not_exists, not_and]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean
@[reassoc, to_app]
lemma mapComp_assoc_right {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
    F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h = F.map₂ (α_ f g h).inv ≫
    F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h ≫
    (α_ (F.map f) (F.map g) (F.map h)).hom

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : OplaxFunctor B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h =
    F.map₂ (α_ f g h).inv ≫ F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom

Tactic:
rw [← F.map₂_associator, ← F.map₂_comp_assoc]

Result:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : OplaxFunctor B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h =
    F.map₂ ((α_ f g h).inv ≫ (α_ f g h).hom) ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : OplaxFunctor B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h =
    F.map₂ ((α_ f g h).inv ≫ (α_ f g h).hom) ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem abs_cos_eq_sqrt_one_sub_sin_sq (x : ℝ) : |cos x| = √(1 - sin x ^ 2)

Proof state:
x : ℝ
⊢ |cos x| = √(1 - sin x ^ 2)

Tactic:
rw [← cos_sq', sqrt_sq_eq_abs]

Result:
no goals
-- Mathlib/Data/Finsupp/ToDFinsupp.lean
theorem DFinsupp.toFinsupp_support (f : Π₀ _ : ι, M) : f.toFinsupp.support = f.support

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
⊢ f.toFinsupp.support = f.support

Tactic:
ext

Result:
case h
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
a✝ : ι
⊢ a✝ ∈ f.toFinsupp.support ↔ a✝ ∈ f.support

Proof state:
case h
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
a✝ : ι
⊢ a✝ ∈ f.toFinsupp.support ↔ a✝ ∈ f.support

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_empty (ne : s.Nonempty) : hausdorffEdist s ∅ = ∞

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ne : s.Nonempty
⊢ hausdorffEdist s ∅ = ⊤

Tactic:
rcases ne with ⟨x, xs⟩

Result:
case intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
xs : x ∈ s
⊢ hausdorffEdist s ∅ = ⊤

Proof state:
case intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
xs : x ∈ s
this : infEdist x ∅ ≤ hausdorffEdist s ∅
⊢ hausdorffEdist s ∅ = ⊤

Tactic:
simpa using this

Result:
no goals

Proof state:
case intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
xs : x ∈ s
⊢ hausdorffEdist s ∅ = ⊤

Tactic:
have : infEdist x ∅ ≤ hausdorffEdist s ∅ := infEdist_le_hausdorffEdist_of_mem xs

Result:
case intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
xs : x ∈ s
this : infEdist x ∅ ≤ hausdorffEdist s ∅
⊢ hausdorffEdist s ∅ = ⊤
-- Mathlib/Data/Set/Function.lean
theorem SurjOn.invOn_invFunOn [Nonempty α] (h : SurjOn f s t) :
    InvOn (invFunOn f s) f (invFunOn f s '' t) t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ InvOn (invFunOn f s) f (invFunOn f s '' t) t

Tactic:
refine ⟨?_, h.rightInvOn_invFunOn⟩

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ LeftInvOn (invFunOn f s) f (invFunOn f s '' t)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ LeftInvOn (invFunOn f s) f (invFunOn f s '' t)

Tactic:
rintro _ ⟨y, hy, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ invFunOn f s (f (invFunOn f s y)) = invFunOn f s y

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ invFunOn f s (f (invFunOn f s y)) = invFunOn f s y

Tactic:
rw [h.rightInvOn_invFunOn hy]

Result:
no goals
-- Mathlib/Algebra/Order/Kleene.lean
theorem kstar_le_of_mul_le_left (hb : 1 ≤ b) : b * a ≤ b → a∗ ≤ b

Proof state:
α : Type u_1
inst✝ : KleeneAlgebra α
a b : α
hb : 1 ≤ b
⊢ b * a ≤ b → a∗ ≤ b

Tactic:
simpa using mul_kstar_le hb

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem hsymmPart_indiscrete (n : ℕ) : hsymmPart σ R (.indiscrete n) = hsymm σ R n

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
n : ℕ
⊢ hsymmPart σ R (Nat.Partition.indiscrete n) = hsymm σ R n

Tactic:
cases n <;> simp [hsymmPart]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffOn_univ : ContMDiffOn I I' n f univ ↔ ContMDiff I I' n f

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
⊢ ContMDiffOn I I' n f univ ↔ ContMDiff I I' n f

Tactic:
simp only [ContMDiffOn, ContMDiff, contMDiffWithinAt_univ, forall_prop_of_true, mem_univ]

Result:
no goals
-- Mathlib/Order/Interval/Set/Image.lean
lemma AntitoneOn.mapsTo_Ici (h : AntitoneOn f (Ici a)) : MapsTo f (Ici a) (Iic (f a)) :=
  fun _ _ ↦ by aesop

Proof state:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : AntitoneOn f (Ici a)
x✝¹ : α
x✝ : x✝¹ ∈ Ici a
⊢ f x✝¹ ∈ Iic (f a)

Tactic:
aesop

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_isColimit {c : PushoutCocone f g} (h : Limits.IsColimit c) : IsPushout f g c.inl c.inr :=
  { w := c.condition
    isColimit' :=
      ⟨IsColimit.ofIsoColimit h (Limits.PushoutCocone.ext (Iso.refl _)
        (by simp) (by simp))⟩ }

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
f : Z ⟶ X
g : Z ⟶ Y
c : PushoutCocone f g
h : IsColimit c
⊢ c.inr ≫ (Iso.refl c.pt).hom = (PushoutCocone.mk c.inl c.inr ⋯).inr

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
f : Z ⟶ X
g : Z ⟶ Y
c : PushoutCocone f g
h : IsColimit c
⊢ c.inl ≫ (Iso.refl c.pt).hom = (PushoutCocone.mk c.inl c.inr ⋯).inl

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_eq (s : Multiset α) (b : α) : s.filter (Eq b) = replicate (count b s) b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
⊢ filter (Eq b) s = replicate (count b s) b

Tactic:
simp_rw [← filter_eq', eq_comm]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem bUnion_ptsOfPeriod : ⋃ n > 0, ptsOfPeriod f n = periodicPts f :=
  Set.ext fun x => by simp [mem_periodicPts]

Proof state:
α : Type u_1
f : α → α
x : α
⊢ x ∈ ⋃ n, ⋃ (_ : n > 0), ptsOfPeriod f n ↔ x ∈ periodicPts f

Tactic:
simp [mem_periodicPts]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Ultra.lean
@[to_additive]
lemma norm_tprod_le_of_forall_le_of_nonneg {f : ι → M} {C : ℝ} (hC : 0 ≤ C) (h : ∀ i, ‖f i‖ ≤ C) :
    ‖∏' i, f i‖ ≤ C

Proof state:
case inl
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
h✝ : IsEmpty ι
⊢ ‖∏' (i : ι), f i‖ ≤ C

Tactic:
simpa only [tprod_empty, norm_one'] using hC

Result:
no goals

Proof state:
case inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
h✝ : Nonempty ι
⊢ ‖∏' (i : ι), f i‖ ≤ C

Tactic:
exact norm_tprod_le_of_forall_le h

Result:
no goals

Proof state:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
⊢ ‖∏' (i : ι), f i‖ ≤ C

Tactic:
rcases isEmpty_or_nonempty ι

Result:
case inl
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
h✝ : IsEmpty ι
⊢ ‖∏' (i : ι), f i‖ ≤ C

case inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
h✝ : Nonempty ι
⊢ ‖∏' (i : ι), f i‖ ≤ C
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem getElem_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) (i : Nat)
    (h : i < (mapFinIdx a f).size) :
    (a.mapFinIdx f)[i] = f i (a[i]'(by simp_all))  (by simp_all) :=
  (mapFinIdx_spec _ _ (fun i b h => b = f i a[i] h) fun _ _ => rfl).2 i _

Proof state:
α : Type ?u.29766
β : Type ?u.29790
a : Array α
f : (i : Nat) → α → i < a.size → β
i : Nat
h : i < (a.mapFinIdx f).size
⊢ i < a.size

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem buckets_empty {c} {i : Nat} {h} :
    (empty c : DHashMap α β).1.buckets[i]'h = AssocList.nil

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
c i : Nat
h : i < (empty c).val.buckets.size
⊢ (empty c).val.buckets[i] = AssocList.nil

Tactic:
simp [empty]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem coequalizerComparison_map_desc [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)]
    {Z : C} {h : Y ⟶ Z} (w : f ≫ h = g ≫ h) :
    coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) =
      coequalizer.desc (G.map h) (by simp only [← G.map_comp, w])

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) =
    coequalizer.π (G.map f) (G.map g) ≫ coequalizer.desc (G.map h) ⋯

Tactic:
simp [← G.map_comp]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ G.map f ≫ G.map h = G.map g ≫ G.map h

Tactic:
simp only [← G.map_comp, w]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) = coequalizer.desc (G.map h) ⋯

Tactic:
apply coequalizer.hom_ext

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) =
    coequalizer.π (G.map f) (G.map g) ≫ coequalizer.desc (G.map h) ⋯