harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
@[simp]
lemma mapDomainAlgHom_comp (k A) {G₁ G₂ G₃} [CommSemiring k] [Semiring A] [Algebra k A]
    [Monoid G₁] [Monoid G₂] [Monoid G₃] (f : G₁ →* G₂) (g : G₂ →* G₃) :
    mapDomainAlgHom k A (g.comp f) = (mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f)

Proof state:
k : Type u_4
A : Type u_5
G₁ : Type u_6
G₂ : Type u_7
G₃ : Type u_8
inst✝⁵ : CommSemiring k
inst✝⁴ : Semiring A
inst✝³ : Algebra k A
inst✝² : Monoid G₁
inst✝¹ : Monoid G₂
inst✝ : Monoid G₃
f : G₁ →* G₂
g : G₂ →* G₃
⊢ mapDomainAlgHom k A (g.comp f) = (mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f)

Tactic:
ext

Result:
case H.H
k : Type u_4
A : Type u_5
G₁ : Type u_6
G₂ : Type u_7
G₃ : Type u_8
inst✝⁵ : CommSemiring k
inst✝⁴ : Semiring A
inst✝³ : Algebra k A
inst✝² : Monoid G₁
inst✝¹ : Monoid G₂
inst✝ : Monoid G₃
f : G₁ →* G₂
g : G₂ →* G₃
x✝¹ : MonoidAlgebra A G₁
x✝ : G₃
⊢ ((mapDomainAlgHom k A (g.comp f)) x✝¹) x✝ = (((mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f)) x✝¹) x✝

Proof state:
case H.H
k : Type u_4
A : Type u_5
G₁ : Type u_6
G₂ : Type u_7
G₃ : Type u_8
inst✝⁵ : CommSemiring k
inst✝⁴ : Semiring A
inst✝³ : Algebra k A
inst✝² : Monoid G₁
inst✝¹ : Monoid G₂
inst✝ : Monoid G₃
f : G₁ →* G₂
g : G₂ →* G₃
x✝¹ : MonoidAlgebra A G₁
x✝ : G₃
⊢ ((mapDomainAlgHom k A (g.comp f)) x✝¹) x✝ = (((mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f)) x✝¹) x✝

Tactic:
simp [mapDomain_comp]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem Ici_sSup (s : Set α) : Ici (sSup s) = ⋂ a ∈ s, Ici a

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ Ici (sSup s) = ⋂ a ∈ s, Ici a

Tactic:
rw [sSup_eq_iSup, Ici_iSup₂]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem comp_coimage_π_eq_zero {R : C} {g : Q ⟶ R} (h : f ≫ g = 0) : f ≫ Abelian.coimage.π g = 0 :=
  zero_of_comp_mono (Abelian.factorThruCoimage g) <| by simp [h]

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
R : C
g : Q ⟶ R
h : f ≫ g = 0
⊢ (f ≫ coimage.π g) ≫ Abelian.factorThruCoimage g = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem map_subtype_range_inclusion {p p' : Submodule R M} (h : p ≤ p') :
    map p'.subtype (range <| inclusion h) = p

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
h : p ≤ p'
⊢ map p'.subtype (range (inclusion h)) = p

Tactic:
simp [range_inclusion, map_comap_eq, h]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualDistribInvOfBasis_apply (b : Basis ι R M) (c : Basis κ R N) (f : Dual R (M ⊗[R] N)) :
    dualDistribInvOfBasis b c f = ∑ i, ∑ j, f (b i ⊗ₜ c j) • b.dualBasis i ⊗ₜ c.dualBasis j

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
f : Dual R (M ⊗[R] N)
⊢ (dualDistribInvOfBasis b c) f = ∑ i : ι, ∑ j : κ, f (b i ⊗ₜ[R] c j) • b.dualBasis i ⊗ₜ[R] c.dualBasis j

Tactic:
simp [dualDistribInvOfBasis]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem coe_sUnion (x : ZFSet.{u}) : ↑(⋃₀ x : ZFSet) = ⋃₀ (x : Class.{u}) :=
  ext fun y =>
    ZFSet.mem_sUnion.trans (sUnion_apply.trans <| by rfl).symm

Proof state:
x y : ZFSet.{u}
⊢ (∃ z, ↑x z ∧ y ∈ z) ↔ ∃ z ∈ x, y ∈ z

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
lemma mem_of_egauge_lt_one (hs : Balanced 𝕜 s) (hx : egauge 𝕜 s x < 1) : x ∈ s :=
  let ⟨c, hxc, hc⟩ := egauge_lt_iff.1 hx
  hs c (by simpa [enorm] using hc.le) hxc

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : Balanced 𝕜 s
hx : egauge 𝕜 s x < 1
c : 𝕜
hxc : x ∈ c • s
hc : ‖c‖ₑ < 1
⊢ ‖c‖ ≤ 1

Tactic:
simpa [enorm] using hc.le

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem volume_box (ν : ι → ℤ) :
    volume (box n ν : Set (ι → ℝ)) = 1 / n ^ card ι

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ volume ↑(box n ν) = 1 / ↑n ^ card ι

Tactic:
simp_rw [volume_pi, BoxIntegral.Box.coe_eq_pi, Measure.pi_pi, Real.volume_Ioc,
  box.upper_sub_lower, Finset.prod_const, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr
  n.pos_of_neZero), ENNReal.ofReal_one, ENNReal.ofReal_natCast, one_div, ENNReal.inv_pow,
  Finset.card_univ]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem mem_leadingCoeffNth_zero (x) : x ∈ I.leadingCoeffNth 0 ↔ C x ∈ I :=
  (mem_leadingCoeffNth _ _ _).trans
    ⟨fun ⟨p, hpI, hpdeg, hpx⟩ => by
      rwa [← hpx, Polynomial.leadingCoeff,
        Nat.eq_zero_of_le_zero (natDegree_le_of_degree_le hpdeg), ← eq_C_of_degree_le_zero hpdeg],
      fun hx => ⟨C x, hx, degree_C_le, leadingCoeff_C x⟩⟩

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
x✝ : ∃ p ∈ I, p.degree ≤ ↑0 ∧ p.leadingCoeff = x
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑0
hpx : p.leadingCoeff = x
⊢ C x ∈ I

Tactic:
rwa [← hpx, Polynomial.leadingCoeff,
  Nat.eq_zero_of_le_zero (natDegree_le_of_degree_le hpdeg), ← eq_C_of_degree_le_zero hpdeg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_umod : eval .umod = ((· % ·) : BitVec w → BitVec w → BitVec w)

Proof state:
w : Nat
⊢ umod.eval = fun x1 x2 => x1 % x2

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem nhds_nhds (x : X) :
    𝓝 (𝓝 x) = ⨅ (s : Set X) (_ : IsOpen s) (_ : x ∈ s), 𝓟 (Iic (𝓟 s))

Proof state:
X : Type u_4
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 (𝓝 x) = ⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), 𝓟 (Iic (𝓟 s))

Tactic:
simp only [(nhds_basis_opens x).nhds.eq_biInf, iInf_and, @iInf_comm _ (_ ∈ _)]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem map_exp_comap_re_atBot : map exp (comap re atBot) = 𝓝[≠] 0

Proof state:
⊢ map cexp (comap re atBot) = 𝓝[≠] 0

Tactic:
rw [← comap_exp_nhds_zero, map_comap, range_exp, nhdsWithin]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
@[simp] lemma mem_measurableAtom_self (x : β) : x ∈ measurableAtom x

Proof state:
β : Type u_2
inst✝ : MeasurableSpace β
x : β
⊢ x ∈ measurableAtom x

Tactic:
simp +contextual [measurableAtom]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean
theorem ι_colimitPointwiseProductToProductColimit_π (k : ∀ i, I i) (s : α) :
    colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π _ s =
      Pi.π _ s ≫ colimit.ι (F s) (k s)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
α : Type w
I : α → Type u₁
inst✝³ : (i : α) → Category.{v₁, u₁} (I i)
inst✝² : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ C
inst✝¹ : ∀ (i : α), HasColimitsOfShape (I i) C
inst✝ : HasColimitsOfShape ((i : α) → I i) C
k : (i : α) → I i
s : α
⊢ colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s => colimit (F s)) s =
    Pi.π (fun s => (F s).obj (k s)) s ≫ colimit.ι (F s) (k s)

Tactic:
simp [colimitPointwiseProductToProductColimit]

Result:
no goals
-- Mathlib/Dynamics/OmegaLimit.lean
theorem omegaLimit_iUnion (p : ι → Set α) : ⋃ i, ω f ϕ (p i) ⊆ ω f ϕ (⋃ i, p i)

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
p : ι → Set α
⊢ ⋃ i, ω f ϕ (p i) ⊆ ω f ϕ (⋃ i, p i)

Tactic:
rw [iUnion_subset_iff]

Result:
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
p : ι → Set α
⊢ ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ i, p i)

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
p : ι → Set α
⊢ ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ i, p i)

Tactic:
exact fun i ↦ omegaLimit_mono_right _ _ (subset_iUnion _ _)

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem eq_left_iff_getLeft_eq {a : α} : x = inl a ↔ ∃ h, x.getLeft h = a

Proof state:
α : Type u
β : Type v
x : α ⊕ β
a : α
⊢ x = inl a ↔ ∃ h, x.getLeft h = a

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_mul_eq_div_div : a / (b * c) = a / b / c

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a / (b * c) = a / b / c

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Antidiagonal.lean
theorem antidiagonal_map_snd (s : Multiset α) : (antidiagonal s).map Prod.snd = powerset s :=
  Quotient.inductionOn s fun l ↦ by simp [powersetAux']

Proof state:
α : Type u_1
s : Multiset α
l : List α
⊢ map Prod.snd (antidiagonal ⟦l⟧) = powerset ⟦l⟧

Tactic:
simp [powersetAux']

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem sum_comapDomain [Zero M] [AddCommMonoid N] (f : α → β) (l : β →₀ M) (g : β → M → N)
    (hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support) :
    (comapDomain f l hf.injOn).sum (g ∘ f) = l.sum g

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α → β
l : β →₀ M
g : β → M → N
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ ∑ x ∈ l.support.preimage f ⋯,
      g (f x) ({ support := l.support.preimage f ⋯, toFun := fun a => l (f a), mem_support_toFun := ⋯ } x) =
    ∑ a ∈ l.support, g a (l a)

Tactic:
exact Finset.sum_preimage_of_bij f _ hf fun x => g x (l x)

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem pi_refl : (PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)) = .refl (∀ i, αi i)

Proof state:
ι : Type u_5
αi : ι → Type u_6
⊢ (PartialEquiv.pi fun i => PartialEquiv.refl (αi i)) = PartialEquiv.refl ((i : ι) → αi i)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertMany_empty_list_singleton {k : α} {v : β} :
    (insertMany empty [⟨k, v⟩]).1 = empty.insert k v

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
k : α
v : β
⊢ (insertMany empty [(k, v)]).val = empty.insert k v

Tactic:
simp only [insertMany_list_singleton]

Result:
no goals
-- Mathlib/Data/Int/Order/Units.lean
theorem units_mul_self (u : ℤˣ) : u * u = 1

Proof state:
u : ℤˣ
⊢ u * u = 1

Tactic:
rw [← sq, units_sq]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_iUnion₀ [Countable β] {s : β → Set α} (hm : ∀ i, NullMeasurableSet (s i) μ)
    (hd : Pairwise (AEDisjoint μ on s)) (f : α → ℝ≥0∞) :
    ∫⁻ a in ⋃ i, s i, f a ∂μ = ∑' i, ∫⁻ a in s i, f a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
s : β → Set α
hm : ∀ (i : β), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ i, s i, f a ∂μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ

Tactic:
simp only [Measure.restrict_iUnion_ae hd hm, lintegral_sum_measure]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Cartan.lean
theorem rootSpace_zero_eq (H : LieSubalgebra R L) [H.IsCartanSubalgebra] [IsNoetherian R L] :
    rootSpace H 0 = H.toLieSubmodule

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
H : LieSubalgebra R L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
⊢ rootSpace H 0 = H.toLieSubmodule

Tactic:
rw [← LieSubmodule.toSubmodule_inj, ← coe_zeroRootSubalgebra,
  zeroRootSubalgebra_eq_of_is_cartan R L H, LieSubalgebra.coe_toLieSubmodule]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
    {f : Option β → Option β} (h : m.WF) : Const.get! (Const.alter m k f) k' =
      if k == k' then
        f (Const.get? m k) |>.get!
      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' : α
inst✝ : Inhabited β
f : Option β → Option β
h : m.WF
⊢ get! (alter m k f) k' = if (k == k') = true then (f (get? m k)).get! else get! m k'

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

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem quot_out_zero : Quot.out (0 : Associates M) = 0

Proof state:
M : Type u_1
inst✝ : MonoidWithZero M
⊢ Quot.out 0 = 0

Tactic:
rw [← mk_eq_zero, quot_out]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
lemma pairing_neg_one_neg_four_iff' (h2 : IsSMulRegular R (2 : R)) :
    P.pairing i j = -1 ∧ P.pairing j i = -4 ↔ P.root j = (-2 : R) • P.root i

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
⊢ P.pairing i j = -1 ∧ P.pairing j i = -4 ↔ P.root j = -2 • P.root i

Tactic:
simpa [neg_smul, ← neg_eq_iff_eq_neg] using P.pairing_one_four_iff' i (P.reflection_perm j j) h2

Result:
no goals
-- Mathlib/Combinatorics/Additive/Dissociation.lean
@[to_additive (attr := simp)]
lemma not_mulDissociated :
    ¬ MulDissociated s ↔
      ∃ t : Finset α, ↑t ⊆ s ∧ ∃ u : Finset α, ↑u ⊆ s ∧ t ≠ u ∧ ∏ x ∈ t, x = ∏ x ∈ u, x

Proof state:
α : Type u_1
inst✝ : CommGroup α
s : Set α
⊢ (∃ x, ↑x ⊆ s ∧ ∃ x_1, ↑x_1 ⊆ s ∧ ∏ x ∈ x, x = ∏ x ∈ x_1, x ∧ ¬x = x_1) ↔
    ∃ t, ↑t ⊆ s ∧ ∃ u, ↑u ⊆ s ∧ ¬t = u ∧ ∏ x ∈ t, x = ∏ x ∈ u, x

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommGroup α
s : Set α
⊢ ¬MulDissociated s ↔ ∃ t, ↑t ⊆ s ∧ ∃ u, ↑u ⊆ s ∧ t ≠ u ∧ ∏ x ∈ t, x = ∏ x ∈ u, x

Tactic:
simp [MulDissociated, InjOn]

Result:
α : Type u_1
inst✝ : CommGroup α
s : Set α
⊢ (∃ x, ↑x ⊆ s ∧ ∃ x_1, ↑x_1 ⊆ s ∧ ∏ x ∈ x, x = ∏ x ∈ x_1, x ∧ ¬x = x_1) ↔
    ∃ t, ↑t ⊆ s ∧ ∃ u, ↑u ⊆ s ∧ ¬t = u ∧ ∏ x ∈ t, x = ∏ x ∈ u, x
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem mem_target {x : B × F} : x ∈ e.target ↔ x.1 ∈ e.baseSet

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
⊢ x ∈ e.target ↔ x.1 ∈ e.baseSet

Tactic:
rw [e.target_eq, prod_univ, mem_preimage]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
@[simp]
lemma comp_zero [∀ (a : M), (shiftFunctor C a).PreservesZeroMorphisms]
    {a : M} (β : ShiftedHom X Y a) {b c : M} (h : b + a = c) :
    β.comp (0 : ShiftedHom Y Z b) h = 0

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
X Y Z : C
inst✝¹ : Preadditive C
inst✝ : ∀ (a : M), (shiftFunctor C a).PreservesZeroMorphisms
a : M
β : ShiftedHom X Y a
b c : M
h : b + a = c
⊢ β.comp 0 h = 0

Tactic:
rw [comp, Functor.map_zero, Limits.zero_comp, Limits.comp_zero]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_nhds_top_iff_nnreal {m : α → ℝ≥0∞} {f : Filter α} :
    Tendsto m f (𝓝 ∞) ↔ ∀ x : ℝ≥0, ∀ᶠ a in f, ↑x < m a

Proof state:
α : Type u_1
m : α → ℝ≥0∞
f : Filter α
⊢ Tendsto m f (𝓝 ⊤) ↔ ∀ (x : ℝ≥0), ∀ᶠ (a : α) in f, ↑x < m a

Tactic:
simp only [nhds_top', tendsto_iInf, tendsto_principal, mem_Ioi]

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem const_append1 {β γ} (x : γ) {n} (α : TypeVec n) :
    TypeVec.const x (α ::: β) = appendFun (TypeVec.const x α) fun _ => x

Proof state:
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
⊢ TypeVec.const x (α ::: β) = (TypeVec.const x α ::: fun x_1 => x)

Tactic:
ext i : 1

Result:
case a
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 (n + 1)
⊢ TypeVec.const x (α ::: β) i = (TypeVec.const x α ::: fun x_1 => x) i

Proof state:
case a
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 (n + 1)
⊢ TypeVec.const x (α ::: β) i = (TypeVec.const x α ::: fun x_1 => x) i

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_natCast_mul (hx : 0 ≤ x) (n : ℕ) (z : ℝ) : x ^ (n * z) = (x ^ n) ^ z

Proof state:
x : ℝ
hx : 0 ≤ x
n : ℕ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul hx, rpow_natCast]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem unpair : Primrec Nat.unpair :=
  (pair (nat_iff.2 .left) (nat_iff.2 .right)).of_eq fun n => by simp

Proof state:
n : ℕ
⊢ ((Nat.unpair n).1, (Nat.unpair n).2) = Nat.unpair n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_sub : sin (x - y) = sin x * cos y - cos x * sin y

Proof state:
x y : ℝ
⊢ sin (x - y) = sin x * cos y - cos x * sin y

Tactic:
simp [sub_eq_add_neg, sin_add, sin_neg, cos_neg]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem mem_closure_one_iff_norm {x : E} : x ∈ closure ({1} : Set E) ↔ ‖x‖ = 0

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ x ∈ closure {1} ↔ ‖x‖ = 0

Tactic:
rw [← closedBall_zero', mem_closedBall_one_iff, (norm_nonneg' x).le_iff_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem continuousWithinAt_log_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :
    ContinuousWithinAt log { z : ℂ | 0 ≤ z.im } z

Proof state:
case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0

Tactic:
lift z to ℝ using him

Result:
case convert_1.intro
z : ℝ
hre : (↑z).re < 0
⊢ ‖↑z‖ ≠ 0

Proof state:
case convert_1.intro
z : ℝ
hre : (↑z).re < 0
⊢ ‖↑z‖ ≠ 0

Tactic:
simpa using hre.ne

Result:
no goals

Proof state:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ContinuousWithinAt log {z | 0 ≤ z.im} z

Tactic:
convert
  (continuous_ofReal.continuousAt.comp_continuousWithinAt
          (continuous_norm.continuousWithinAt.log _)).tendsto.add
    ((continuous_ofReal.continuousAt.comp_continuousWithinAt <|
          continuousWithinAt_arg_of_re_neg_of_im_zero hre him).mul
      tendsto_const_nhds) using 1

Result:
case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_range_one (f : ℕ → β) : ∏ k ∈ range 1, f k = f 0

Proof state:
β : Type u_4
inst✝ : CommMonoid β
f : ℕ → β
⊢ ∏ k ∈ range 1, f k = f 0

Tactic:
rw [range_one, prod_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Monadic.lean
theorem forIn'_pure_yield_eq_pelim [Monad m] [LawfulMonad m]
    (o : Option α) (f : (a : α) → a ∈ o → β → β) (b : β) :
    forIn' o b (fun a m b => pure (.yield (f a m b))) =
      pure (f := m) (o.pelim b (fun a h => f a h b))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
o : Option α
f : (a : α) → a ∈ o → β → β
b : β
⊢ (forIn' o b fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) = pure (o.pelim b fun a h => f a h b)

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem tendsto_dist_left_atTop_iff (c : α) {f : β → α} {l : Filter β} :
    Tendsto (fun x ↦ dist c (f x)) l atTop ↔ Tendsto f l (cobounded α)

Proof state:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
c : α
f : β → α
l : Filter β
⊢ Tendsto (fun x => dist c (f x)) l atTop ↔ Tendsto f l (cobounded α)

Tactic:
simp only [dist_comm c, tendsto_dist_right_atTop_iff]

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Icc_left (b : α) : ⋃ a, Icc a b = Iic b

Proof state:
α : Type v
inst✝ : Preorder α
b : α
⊢ ⋃ a, Icc a b = Iic b

Tactic:
simp only [← Ici_inter_Iic, ← iUnion_inter, iUnion_Ici, univ_inter]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem AnalyticOn.differentiableOn (h : AnalyticOn 𝕜 f s) : DifferentiableOn 𝕜 f s :=
  fun y hy ↦ (h y hy).differentiableWithinAt.mono (by simp)

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
y : E
hy : y ∈ s
⊢ s ⊆ insert y s

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem spanSingleton_mul_spanSingleton (x y : P) :
    spanSingleton S x * spanSingleton S y = spanSingleton S (x * y)

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y : P
⊢ spanSingleton S x * spanSingleton S y = spanSingleton S (x * y)

Tactic:
apply coeToSubmodule_injective

Result:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y : P
⊢ (fun I => ↑I) (spanSingleton S x * spanSingleton S y) = (fun I => ↑I) (spanSingleton S (x * y))

Proof state:
case a
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x y : P
⊢ (fun I => ↑I) (spanSingleton S x * spanSingleton S y) = (fun I => ↑I) (spanSingleton S (x * y))

Tactic:
simp only [coe_mul, coe_spanSingleton, span_mul_span, singleton_mul_singleton]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem succ_top {n m : ℕ} (h : n ≤ m) : Ico n (m + 1) = Ico n m ++ [m]

Proof state:
case hml
n m : ℕ
h : n ≤ m
⊢ m ≤ m + 1

Tactic:
exact Nat.le_succ _

Result:
no goals

Proof state:
n m : ℕ
h : n ≤ m
⊢ Ico n (m + 1) = Ico n m ++ [m]

Tactic:
rwa [← succ_singleton, append_consecutive]

Result:
case hml
n m : ℕ
h : n ≤ m
⊢ m ≤ m + 1
-- Mathlib/Analysis/Convex/Combination.lean
theorem Set.Finite.convexHull_eq {s : Set E} (hs : s.Finite) : convexHull R s =
    { x : E | ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ hs.toFinset, w y = 1 ∧
      hs.toFinset.centerMass w id = x }

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
⊢ (convexHull R) s = {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ hs.toFinset, w y = 1 ∧ hs.toFinset.centerMass w id = x}

Tactic:
simpa only [Set.Finite.coe_toFinset, Set.Finite.mem_toFinset, exists_prop] using
  hs.toFinset.convexHull_eq

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem finSuccEquiv_X_succ {j : Fin n} : finSuccEquiv R n (X j.succ) = Polynomial.C (X j)

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin n
⊢ (finSuccEquiv R n) (X j.succ) = Polynomial.C (X j)

Tactic:
simp [finSuccEquiv_apply]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem zero_bot (n : ℕ) : Ico 0 n = range n

Proof state:
n : ℕ
⊢ Ico 0 n = range n

Tactic:
rw [Ico, Nat.sub_zero, range_eq_range']

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_ne_zero : Nat.card α ≠ 0 ↔ Nonempty α ∧ Finite α

Proof state:
α : Type u_1
⊢ Nat.card α ≠ 0 ↔ Nonempty α ∧ Finite α

Tactic:
simp [card_eq_zero, not_or]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem one_le_inv : 1 ≤ a⁻¹ ↔ a ≤ 1

Proof state:
a : ℝ≥0∞
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
rw [le_inv_iff_le_inv, inv_one]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem coe_toAffineIsometryEquiv : ⇑(e.toAffineIsometryEquiv : V ≃ᵃⁱ[𝕜] V₂) = e

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : NormedSpace 𝕜 V₂
e : V ≃ₗᵢ[𝕜] V₂
⊢ ⇑e.toAffineIsometryEquiv = ⇑e

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem zeroLocus_singleton_pow (f : A) (n : ℕ) (hn : 0 < n) :
    zeroLocus 𝒜 ({f ^ n} : Set A) = zeroLocus 𝒜 {f} :=
  Set.ext fun x => by simpa using x.isPrime.pow_mem_iff_mem n hn

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
n : ℕ
hn : 0 < n
x : ProjectiveSpectrum 𝒜
⊢ x ∈ zeroLocus 𝒜 {f ^ n} ↔ x ∈ zeroLocus 𝒜 {f}

Tactic:
simpa using x.isPrime.pow_mem_iff_mem n hn

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_ofReal_im (x : ℝ) : (sin x).im = 0

Proof state:
x : ℝ
⊢ (sin ↑x).im = 0

Tactic:
rw [← ofReal_sin_ofReal_re, ofReal_im]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem isCycleOn_empty : f.IsCycleOn ∅

Proof state:
α : Type u_2
f : Perm α
⊢ f.IsCycleOn ∅

Tactic:
simp [IsCycleOn, Set.bijOn_empty]

Result:
no goals