harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/RelSeries.lean
@[simp] lemma last_reverse (p : RelSeries r) : p.reverse.last = p.head

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
⊢ p.reverse.last = p.head

Tactic:
simp [RelSeries.last, RelSeries.head]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem opNorm_le_of_lipschitz {f : NormedAddGroupHom V₁ V₂} {K : ℝ≥0} (hf : LipschitzWith K f) :
    ‖f‖ ≤ K :=
  f.opNorm_le_bound K.2 fun x => by simpa only [dist_zero_right, map_zero] using hf.dist_le_mul x 0

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : ℝ≥0
hf : LipschitzWith K ⇑f
x : V₁
⊢ ‖f x‖ ≤ ↑K * ‖x‖

Tactic:
simpa only [dist_zero_right, map_zero] using hf.dist_le_mul x 0

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem max?_eq_toList_getLast? {t : RBNode α} : t.max? = t.toList.getLast?

Proof state:
α : Type u_1
t : RBNode α
⊢ t.reverse.toList.head? = t.toList.getLast?

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
t : RBNode α
⊢ t.max? = t.toList.getLast?

Tactic:
rw [← min?_reverse, min?_eq_toList_head?]

Result:
α : Type u_1
t : RBNode α
⊢ t.reverse.toList.head? = t.toList.getLast?
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem map_smul_univ [Fintype ι] (c : ι → R) (m : ∀ i, M₁ i) :
    (f fun i => c i • m i) = (∏ i, c i) • f m

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : Fintype ι
c : ι → R
m : (i : ι) → M₁ i
⊢ (f fun i => c i • m i) = (∏ i : ι, c i) • f m

Tactic:
classical simpa using map_piecewise_smul f c m Finset.univ

Result:
no goals

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : Fintype ι
c : ι → R
m : (i : ι) → M₁ i
⊢ (f fun i => c i • m i) = (∏ i : ι, c i) • f m

Tactic:
simpa using map_piecewise_smul f c m Finset.univ

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem IsRadical.comap (hK : K.IsRadical) : (comap f K).IsRadical

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
hK : K.IsRadical
⊢ (Ideal.comap f K).IsRadical

Tactic:
rw [← hK.radical, comap_radical]

Result:
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
hK : K.IsRadical
⊢ (Ideal.comap f K).radical.IsRadical

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
hK : K.IsRadical
⊢ (Ideal.comap f K).radical.IsRadical

Tactic:
apply radical_isRadical

Result:
no goals
-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem aeval_wittPolynomial {A : Type*} [CommRing A] [Algebra R A] (f : ℕ → A) (n : ℕ) :
    aeval f (W_ R n) = ∑ i ∈ range (n + 1), (p : A) ^ i * f i ^ p ^ (n - i)

Proof state:
p : ℕ
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ℕ → A
n : ℕ
⊢ (aeval f) (W_ R n) = ∑ i ∈ range (n + 1), ↑p ^ i * f i ^ p ^ (n - i)

Tactic:
simp [wittPolynomial, map_sum, aeval_monomial, Finsupp.prod_single_index]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem left_mem_Icc : a ∈ Icc a b ↔ a ≤ b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ a ∈ Icc a b ↔ a ≤ b

Tactic:
simp only [mem_Icc, true_and, le_rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem iff_eq (p q : Prop) : (p ↔ q) = (p = q)

Proof state:
p q : Prop
⊢ (p ↔ q) = (p = q)

Tactic:
by_cases p <;> by_cases q <;> simp [*]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem succ_le_or_le_castSucc (p : Fin (n + 1)) (i : Fin n) : succ i ≤ p ∨ p ≤ i.castSucc

Proof state:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc < p ∨ p < i.succ

Tactic:
exact p.castSucc_lt_or_lt_succ i

Result:
no goals

Proof state:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.succ ≤ p ∨ p ≤ i.castSucc

Tactic:
rw [le_castSucc_iff, ← castSucc_lt_iff_succ_le]

Result:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc < p ∨ p < i.succ
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_zero_of_nmem_closure (h : x ∉ closure s) : derivWithin f s x = 0

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : x ∉ closure s
⊢ derivWithin f s x = 0

Tactic:
rw [derivWithin, fderivWithin_zero_of_nmem_closure h, ContinuousLinearMap.zero_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem perm_append_comm_assoc (l₁ l₂ l₃ : List α) :
    (l₁ ++ (l₂ ++ l₃)) ~ (l₂ ++ (l₁ ++ l₃))

Proof state:
α : Type u_1
l₁ l₂ l₃ : List α
⊢ l₁ ++ (l₂ ++ l₃) ~ l₂ ++ (l₁ ++ l₃)

Tactic:
simpa only [List.append_assoc] using perm_append_comm.append_right _

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_inv (x : G) : orderOf x⁻¹ = orderOf x

Proof state:
G : Type u_1
inst✝ : Group G
x : G
⊢ orderOf x⁻¹ = orderOf x

Tactic:
simp [orderOf_eq_orderOf_iff]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem cofinite.limsup_set_eq : limsup s cofinite = { x | { n | x ∈ s n }.Infinite }

Proof state:
α : Type u_1
ι : Type u_4
s : ι → Set α
⊢ limsup s cofinite = {x | {n | x ∈ s n}.Infinite}

Tactic:
simp only [← cofinite.blimsup_true s, cofinite.blimsup_set_eq, true_and]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma map₁_snd {G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (η : F ⟶ G)
    (p : YonedaCollection F X) : (YonedaCollection.map₁ η p).snd =
      G.map (eqToHom (by rw [YonedaCollection.map₁_fst])) (η.app _ p.snd)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).snd = G.map (eqToHom ⋯) (η.app (op (CostructuredArrow.mk p.fst)) p.snd)

Tactic:
simp [map₁]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ op (CostructuredArrow.mk p.fst) = op (CostructuredArrow.mk (map₁ η p).fst)

Tactic:
rw [YonedaCollection.map₁_fst]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem image_image [DecidableEq γ] {g : β → γ} : (s.image f).image g = s.image (g ∘ f) :=
  eq_of_veq <| by simp only [image_val, dedup_map_dedup_eq, Multiset.map_map]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
inst✝ : DecidableEq γ
g : β → γ
⊢ (image g (image f s)).val = (image (g ∘ f) s).val

Tactic:
simp only [image_val, dedup_map_dedup_eq, Multiset.map_map]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
/-- The negative logarithmic derivative of the L-function of a nontrivial Dirichlet character
is continuous away from the zeros of the L-function. -/
lemma continuousOn_neg_logDeriv_LFunction_of_nontriv (hχ : χ ≠ 1) :
    ContinuousOn (fun s ↦ -deriv (LFunction χ) s / LFunction χ s) {s | LFunction χ s ≠ 0}

Proof state:
n : ℕ
inst✝ : NeZero n
χ : DirichletCharacter ℂ n
hχ : χ ≠ 1
⊢ ContinuousOn (fun s => -deriv (LFunction χ) s / LFunction χ s) {s | LFunction χ s ≠ 0}

Tactic:
have h := differentiable_LFunction hχ

Result:
n : ℕ
inst✝ : NeZero n
χ : DirichletCharacter ℂ n
hχ : χ ≠ 1
h : Differentiable ℂ (LFunction χ)
⊢ ContinuousOn (fun s => -deriv (LFunction χ) s / LFunction χ s) {s | LFunction χ s ≠ 0}

Proof state:
n : ℕ
inst✝ : NeZero n
χ : DirichletCharacter ℂ n
hχ : χ ≠ 1
h : Differentiable ℂ (LFunction χ)
⊢ ContinuousOn (fun s => -deriv (LFunction χ) s / LFunction χ s) {s | LFunction χ s ≠ 0}

Tactic:
simpa [neg_div] using ((h.contDiff.continuous_deriv le_rfl).continuousOn.div
  h.continuous.continuousOn fun _ hw ↦ hw).neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem guard_false {α} :
    guard (fun (_ : α) => False) = fun _ => none

Proof state:
α : Type u_1
⊢ (guard fun x => False) = fun x => none

Tactic:
funext a

Result:
case h
α : Type u_1
a : α
⊢ guard (fun x => False) a = none

Proof state:
case h
α : Type u_1
a : α
⊢ guard (fun x => False) a = none

Tactic:
simp [guard]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
lemma image_injective (hf : Injective f) : Injective (image f)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
hf : Injective f
⊢ Injective (image f)

Tactic:
simpa only [funext (map_eq_image _)] using map_injective ⟨f, hf⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v fallback : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) :
    getD (insertMany m l).1 k' fallback = v

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v fallback : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
⊢ getD (insertMany m l).val k' fallback = v

Tactic:
simp_to_model [Const.insertMany] using List.getValueD_insertListConst_of_mem

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_add_of_limit {a b c : Ordinal.{u}} (h : IsLimit c) :
    a < b + c ↔ ∃ c' < c, a < b + c'

Proof state:
a b c : Ordinal.{u}
h : c.IsLimit
⊢ a < b + c ↔ ∃ c' < c, a < b + c'

Tactic:
rw [← IsNormal.bsup_eq.{u, u} (isNormal_add_right b) h, lt_bsup, bex_def]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_one_iff_of_pos (hx : 0 < x) : x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Proof state:
x y : ℝ
hx : 0 < x
⊢ x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Tactic:
rw [rpow_def_of_pos hx, exp_lt_one_iff, mul_neg_iff, log_pos_iff hx.le, log_neg_iff hx]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem one_mem_properDivisors_iff_one_lt : 1 ∈ n.properDivisors ↔ 1 < n

Proof state:
n : ℕ
⊢ 1 ∈ n.properDivisors ↔ 1 < n

Tactic:
rw [mem_properDivisors, and_iff_right (one_dvd _)]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem nndist_eq_iSup : nndist f g = ⨆ x : α, nndist (f x) (g x) :=
  Subtype.ext <| dist_eq_iSup.trans <| by simp_rw [val_eq_coe, coe_iSup, coe_nndist]

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ ⨆ x, dist (f x) (g x) = ↑(⨆ x, nndist (f x) (g x))

Tactic:
simp_rw [val_eq_coe, coe_iSup, coe_nndist]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
    {l : List ((_ : α) × β)} {k a : α} {v : β} :
    getValue! a (insertEntry k v l) = if k == a then v else getValue! a l

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
k a : α
v : β
⊢ getValue! a (insertEntry k v l) = if (k == a) = true then v else getValue! a l

Tactic:
simp [getValue!_eq_getValue?, getValue?_insertEntry, apply_ite Option.get!]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_eq_iff_sq_eq (hx : 0 ≤ x) (hy : 0 ≤ y) : √x = y ↔ y ^ 2 = x

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x = y ↔ y ^ 2 = x

Tactic:
rw [sqrt_eq_iff_eq_sq hx hy, eq_comm]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Span.lean
theorem span_singleton_mul_right_unit {a : α} (h2 : IsUnit a) (x : α) :
    span ({x * a} : Set α) = span {x}

Proof state:
α : Type u
inst✝ : CommSemiring α
a : α
h2 : IsUnit a
x : α
⊢ span {x * a} = span {x}

Tactic:
rw [mul_comm, span_singleton_mul_left_unit h2]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_smul' (f : V →ₗ[K] V₂) (a : K) :
    range (a • f) = ⨆ _ : a ≠ 0, range f

Proof state:
K : Type u_4
V : Type u_8
V₂ : Type u_9
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
a : K
⊢ range (a • f) = ⨆ (_ : a ≠ 0), range f

Tactic:
simpa only [range_eq_map] using Submodule.map_smul' f _ a

Result:
no goals
-- Mathlib/Algebra/Ring/CompTypeclasses.lean
theorem comp_apply_eq {x : R₁} : σ' (σ x) = x

Proof state:
R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ σ' (σ x) = x

Tactic:
rw [← RingHom.comp_apply, comp_eq]

Result:
R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ (RingHom.id R₁) x = x

Proof state:
R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ (RingHom.id R₁) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem eq_of_eqOn {f f' : α → E} {s : Set α} (h : EqOn f f' s) :
    eVariationOn f s = eVariationOn f' s :=
  eq_of_edist_zero_on fun x xs => by rw [h xs, edist_self]

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : EqOn f f' s
x : α
xs : x ∈ s
⊢ edist (f x) (f' x) = 0

Tactic:
rw [h xs, edist_self]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem frontier_empty : frontier (∅ : Set X) = ∅

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ frontier ∅ = ∅

Tactic:
simp [frontier]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
lemma associated_of_dvd_of_natDegree_le {K} [Field K] {p q : K[X]} (hpq : p ∣ q) (hq : q ≠ 0)
    (h₁ : q.natDegree ≤ p.natDegree) : Associated p q :=
  associated_of_dvd_of_natDegree_le_of_leadingCoeff hpq h₁
    (IsUnit.dvd (by rwa [← leadingCoeff_ne_zero, ← isUnit_iff_ne_zero] at hq))

Proof state:
K : Type u_1
inst✝ : Field K
p q : K[X]
hpq : p ∣ q
hq : q ≠ 0
h₁ : q.natDegree ≤ p.natDegree
⊢ IsUnit q.leadingCoeff

Tactic:
rwa [← leadingCoeff_ne_zero, ← isUnit_iff_ne_zero] at hq

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_insertListConst_of_mem [BEq α] [EquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ toInsert.map Prod.fst)
    {h} :
    getKey k' (insertListConst l toInsert) h = k

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : k ∈ List.map Prod.fst toInsert
h : containsKey k' (insertListConst l toInsert) = true
⊢ getKey k' (insertListConst l toInsert) h = k

Tactic:
rw [← Option.some_inj, ← getKey?_eq_some_getKey,
  getKey?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem length_toList (l : AssocList α β) : l.toList.length = l.length

Proof state:
α : Type u_1
β : Type u_2
l : AssocList α β
⊢ l.toList.length = l.length

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Data/Nat/Multiplicity.lean
theorem pow_dvd_factorial_iff {p : ℕ} {n r b : ℕ} (hp : p.Prime) (hbn : log p n < b) :
    p ^ r ∣ n ! ↔ r ≤ ∑ i ∈ Ico 1 b, n / p ^ i

Proof state:
p n r b : ℕ
hp : Prime p
hbn : log p n < b
⊢ p ^ r ∣ n ! ↔ r ≤ ∑ i ∈ Ico 1 b, n / p ^ i

Tactic:
rw [← WithTop.coe_le_coe, ENat.some_eq_coe, ← hp.emultiplicity_factorial hbn,
  pow_dvd_iff_le_emultiplicity]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Ioi_bot : (some : α → WithBot α) ⁻¹' Ioi ⊥ = univ

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ some ⁻¹' Ioi ⊥ = univ

Tactic:
rw [← range_coe, preimage_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/HashesTo.lean
theorem hashesTo_nil [BEq α] [Hashable α] {i : Nat} {size : Nat} :
    HashesTo ([] : List ((a : α) × β a)) i size where
  hash_self

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i size : Nat
⊢ ∀ (h : 0 < size) (p : (a : α) × β a), p ∈ [] → (mkIdx size h (hash p.fst)).val.toNat = i

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_bot_left : relfinrank ⊥ A = finrank F A

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A : IntermediateField F E
⊢ ⊥.relfinrank A = finrank F ↥A

Tactic:
simp [relfinrank_eq_toNat_relrank, finrank]

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem mk_inj {x y : F (M F)} (h : M.mk x = M.mk y) : x = y

Proof state:
F : PFunctor.{u}
x y : ↑F F.M
h : M.mk x = M.mk y
⊢ x = y

Tactic:
rw [← dest_mk x, h, dest_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_modify_self (h : m.1.WF) {k : α} [Inhabited (β k)] {f : β k → β k} :
    (m.modify k f).get! k = ((m.get? k).map f).get!

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
k : α
inst✝ : Inhabited (β k)
f : β k → β k
⊢ (m.modify k f).get! k = (Option.map f (m.get? k)).get!

Tactic:
simp_to_model [modify] using List.getValueCast!_modifyKey_self

Result:
no goals
-- Mathlib/Algebra/Lie/Sl2.lean
lemma lie_h_e_smul (t : IsSl2Triple h e f) : ⁅h, e⁆ = (2 : R) • e

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h e f : L
t : IsSl2Triple h e f
⊢ ⁅h, e⁆ = 2 • e

Tactic:
simp [t.lie_h_e_nsmul, two_smul]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem closedBall_diff_sphere : closedBall x ε \ sphere x ε = ball x ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε \ sphere x ε = ball x ε

Tactic:
rw [← ball_union_sphere, Set.union_diff_cancel_right sphere_disjoint_ball.symm.le_bot]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_X_pow [Nontrivial R] (s : σ) (n : ℕ) :
    (X s ^ n : MvPolynomial σ R).totalDegree = n

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
n : ℕ
⊢ (X s ^ n).totalDegree = n

Tactic:
simp [X_pow_eq_monomial, one_ne_zero]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
protected lemma add_right_inj : s + t = s + u ↔ t = u

Proof state:
α : Type u_1
s t u : Multiset α
⊢ s + t = s + u ↔ t = u

Tactic:
simp [Multiset.ext]

Result:
no goals

Proof state:
α : Type u_1
s t u : Multiset α
⊢ s + t = s + u ↔ t = u

Tactic:
classical simp [Multiset.ext]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem classToCong_empty : classToCong ∅ = ∅

Proof state:
case h
x✝ : Class.{u_1}
⊢ x✝ ∈ ∅.classToCong ↔ x✝ ∈ ∅

Tactic:
simp [classToCong]

Result:
no goals

Proof state:
⊢ ∅.classToCong = ∅

Tactic:
ext

Result:
case h
x✝ : Class.{u_1}
⊢ x✝ ∈ ∅.classToCong ↔ x✝ ∈ ∅
-- Mathlib/Algebra/Order/Module/Algebra.lean
@[mono] lemma algebraMap_mono : Monotone (algebraMap α β) :=
  fun a₁ a₂ ha ↦ by
    simpa only [Algebra.algebraMap_eq_smul_one] using smul_le_smul_of_nonneg_right ha zero_le_one

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : OrderedCommSemiring α
inst✝² : OrderedSemiring β
inst✝¹ : Algebra α β
inst✝ : SMulPosMono α β
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ (algebraMap α β) a₁ ≤ (algebraMap α β) a₂

Tactic:
simpa only [Algebra.algebraMap_eq_smul_one] using smul_le_smul_of_nonneg_right ha zero_le_one

Result:
no goals
-- Mathlib/Data/Finset/SymmDiff.lean
theorem coe_symmDiff : (↑(s ∆ t) : Set α) = (s : Set α) ∆ t :=
  Set.ext fun x => by simp [mem_symmDiff, Set.mem_symmDiff]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
x : α
⊢ x ∈ ↑(s ∆ t) ↔ x ∈ ↑s ∆ ↑t

Tactic:
simp [mem_symmDiff, Set.mem_symmDiff]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem of_mul_int (m : ℤ) (h : Irrational (x * m)) : Irrational x :=
  of_mul_rat m <| by rwa [cast_intCast]

Proof state:
x : ℝ
m : ℤ
h : Irrational (x * ↑m)
⊢ Irrational (x * ↑↑m)

Tactic:
rwa [cast_intCast]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_inter_add_ncard_union (s t : Set α) (hs : s.Finite

Proof state:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : autoParam t.Finite _auto✝
⊢ (s ∩ t).ncard + (s ∪ t).ncard = s.ncard + t.ncard

Tactic:
rw [add_comm, ncard_union_add_ncard_inter _ _ hs ht]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
/-- Corollary of Chinese Remainder Theorem: if `Iᵢ` are pairwise coprime ideals in a
commutative ring then given elements `xᵢ` you can find `r` with `r - xᵢ ∈ Iᵢ` for all `i`. -/
lemma exists_forall_sub_mem_ideal
    {I : ι → Ideal R} (hI : Pairwise fun i j ↦ IsCoprime (I i) (I j)) (x : ι → R) :
    ∃ r : R, ∀ i, r - x i ∈ I i

Proof state:
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise fun i j => IsCoprime (I i) (I j)
x : ι → R
⊢ ∃ r, ∀ (i : ι), r - x i ∈ I i

Tactic:
obtain ⟨y, hy⟩ := Ideal.pi_quotient_surjective hI (fun i ↦ x i)

Result:
case intro
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise fun i j => IsCoprime (I i) (I j)
x : ι → R
y : R
hy : ∀ (i : ι), (Quotient.mk (I i)) y = (Quotient.mk (I i)) (x i)
⊢ ∃ r, ∀ (i : ι), r - x i ∈ I i

Proof state:
case intro
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise fun i j => IsCoprime (I i) (I j)
x : ι → R
y : R
hy : ∀ (i : ι), (Quotient.mk (I i)) y = (Quotient.mk (I i)) (x i)
⊢ ∃ r, ∀ (i : ι), r - x i ∈ I i

Tactic:
exact ⟨y, fun i ↦ (Submodule.Quotient.eq (I i)).mp <| hy i⟩

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem sInf {ℐ : Set (Ideal A)} (h : ∀ I ∈ ℐ, Ideal.IsHomogeneous 𝒜 I) :
    (sInf ℐ).IsHomogeneous 𝒜

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (InfSet.sInf ℐ)

Tactic:
rw [sInf_eq_iInf]

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨅ a ∈ ℐ, a)

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
ℐ : Set (Ideal A)
h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I
⊢ IsHomogeneous 𝒜 (⨅ a ∈ ℐ, a)

Tactic:
exact iInf₂ h

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem aeval_T [Algebra R R'] (x : R') (n : ℤ) : aeval x (T R n) = (T R' n).eval x

Proof state:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R'
n : ℤ
⊢ (aeval x) (T R n) = eval x (T R' n)

Tactic:
rw [aeval_def, eval₂_eq_eval_map, map_T]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem boole_getElem_le_count (a : α) (l : List α) (i : Nat) (h : i < l.length) :
    (if l[i] == a then 1 else 0) ≤ l.count a

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
i : Nat
h : i < l.length
⊢ (if (l[i] == a) = true then 1 else 0) ≤ count a l

Tactic:
rw [count_eq_countP]

Result:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
i : Nat
h : i < l.length
⊢ (if (l[i] == a) = true then 1 else 0) ≤ countP (fun x => x == a) l