harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/WithBot.lean
lemma unbotD_le_iff (hx : x = ⊥ → a ≤ b) : x.unbotD a ≤ b ↔ x ≤ b

Proof state:
α : Type u_1
a b : α
inst✝ : LE α
x : WithBot α
hx : x = ⊥ → a ≤ b
⊢ unbotD a x ≤ b ↔ x ≤ ↑b

Tactic:
cases x <;> simp [hx]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma inverseImage_map_eq_of_isEquivalence
    (P : MorphismProperty C) [P.RespectsIso] (F : C ⥤ D) [F.IsEquivalence] :
    (P.map F).inverseImage F = P

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{u_2, u_1} D
P : MorphismProperty C
inst✝¹ : P.RespectsIso
F : C ⥤ D
inst✝ : F.IsEquivalence
⊢ (P.map F).inverseImage F = P

Tactic:
erw [((P.map F).inverseImage_equivalence_inverse_eq_map_functor (F.asEquivalence)), map_map,
  P.map_eq_of_iso F.asEquivalence.unitIso.symm, map_id]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_lt_iff_lt_rpow (hx : 0 < x) : logb b x < y ↔ x < b ^ y

Proof state:
b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b x < y ↔ x < b ^ y

Tactic:
rw [← rpow_lt_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem Const.getD_eq_getDₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) (a : α) (fallback : β) :
    Const.getD m a fallback = Const.getDₘ m a fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
a : α
fallback : β
⊢ getD m a fallback = getDₘ m a fallback

Tactic:
simp [getD, getDₘ, get?ₘ, List.getValueD_eq_getValue?, bucket]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem hom_inv_whiskerRight {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) :
    η.hom ▷ h ≫ η.inv ▷ h = 𝟙 (f ≫ h)

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

Tactic:
rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem derivative_iterate_coeff (k : ℕ) (f : LaurentSeries V) (n : ℤ) :
    ((derivative R)^[k] f).coeff n = (descPochhammer ℤ k).smeval (n + k) • f.coeff (n + k)

Proof state:
R : Type u_1
inst✝² : Semiring R
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
k : ℕ
f : V⸨X⸩
n : ℤ
⊢ ((⇑(derivative R))^[k] f).coeff n = (descPochhammer ℤ k).smeval (n + ↑k) • f.coeff (n + ↑k)

Tactic:
rw [derivative_iterate, coeff_nsmul, Pi.smul_apply, hasseDeriv_coeff,
  Ring.descPochhammer_eq_factorial_smul_choose, smul_assoc]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem log_pos {b o : Ordinal} (hb : 1 < b) (ho : o ≠ 0) (hbo : b ≤ o) : 0 < log b o

Proof state:
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ 0 < log b o

Tactic:
rwa [← succ_le_iff, succ_zero, ← opow_le_iff_le_log hb ho, opow_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem sign_eq_tdiv_abs (a : Int) : sign a = a.tdiv (natAbs a) :=
  if az : a = 0 then by simp [az] else
    (Int.tdiv_eq_of_eq_mul_left (ofNat_ne_zero.2 <| natAbs_ne_zero.2 az)
      (sign_mul_natAbs _).symm).symm

Proof state:
a : Int
az : a = 0
⊢ a.sign = a.tdiv ↑a.natAbs

Tactic:
simp [az]

Result:
no goals
-- Mathlib/Data/Int/CardIntervalMod.lean
theorem Ioc_filter_modEq_card (v : ℕ) :
    #{x ∈ Ioc a b | x ≡ v [MOD r]} = max (⌊(b - v) / (r : ℚ)⌋ - ⌊(a - v) / (r : ℚ)⌋) 0

Proof state:
a b r : ℕ
hr : 0 < r
v : ℕ
⊢ ↑(#(filter (fun x => x ≡ v [MOD r]) (Ioc a b))) = (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) ⊔ 0

Tactic:
simp_rw [← Ioc_filter_modEq_cast _ _ ▸ card_map _,
  Int.Ioc_filter_modEq_card _ _ (cast_lt.mpr hr), Int.cast_natCast]

Result:
no goals
-- Mathlib/GroupTheory/Solvable.lean
theorem IsSolvable.commutator_lt_of_ne_bot [IsSolvable G] {H : Subgroup G} (hH : H ≠ ⊥) :
    ⁅H, H⁆ < H

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSolvable G
H : Subgroup G
hH : Nontrivial ↥H
⊢ ⁅⊤, ⊤⁆ < ⊤

Tactic:
exact commutator_lt_top_of_nontrivial H

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSolvable G
H : Subgroup G
hH : H ≠ ⊥
⊢ ⁅H, H⁆ < H

Tactic:
rw [← nontrivial_iff_ne_bot] at hH

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSolvable G
H : Subgroup G
hH : Nontrivial ↥H
⊢ ⁅H, H⁆ < H

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSolvable G
H : Subgroup G
hH : Nontrivial ↥H
⊢ ⁅H, H⁆ < H

Tactic:
rw [← H.range_subtype, MonoidHom.range_eq_map, ← map_commutator, map_subtype_lt_map_subtype]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSolvable G
H : Subgroup G
hH : Nontrivial ↥H
⊢ ⁅⊤, ⊤⁆ < ⊤
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem mulETransformLeft.card :
    (mulETransformLeft e x).1.card + (mulETransformRight e x).1.card = 2 * x.1.card :=
  (card_inter_add_card_union _ _).trans <| by rw [card_smul_finset, two_mul]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ #x.1 + #(op e • x.1) = 2 * #x.1

Tactic:
rw [card_smul_finset, two_mul]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma half_le_of_sub_le_half (h : a - b ≤ a / 2) : a / 2 ≤ b

Proof state:
a b : ℕ
h : a - b ≤ a / 2
⊢ a / 2 ≤ b

Tactic:
omega

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
/--
Variant of `coheight_le_iff` ranging only over those series that begin exactly on `a`.
-/
lemma coheight_le_iff' {a : α} {n : ℕ∞} :
    coheight a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, p.head = a → p.length ≤ n

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ coheight a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.head p = a → ↑p.length ≤ n

Tactic:
rw [coheight_eq_iSup_head_eq, iSup₂_le_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vectorSpan_range_eq_span_range_vsub_right (p : ι → P) (i0 : ι) :
    vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i : ι => p i -ᵥ p i0)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i0 : ι
⊢ Submodule.span k (range ((fun x => x -ᵥ p i0) ∘ p)) = Submodule.span k (range fun i => p i -ᵥ p i0)

Tactic:
congr

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i0 : ι
⊢ vectorSpan k (range p) = Submodule.span k (range fun i => p i -ᵥ p i0)

Tactic:
rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_range_self i0), ← Set.range_comp]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i0 : ι
⊢ Submodule.span k (range ((fun x => x -ᵥ p i0) ∘ p)) = Submodule.span k (range fun i => p i -ᵥ p i0)
-- Mathlib/RingTheory/Regular/RegularSequence.lean
lemma ofList_cons_smul {R} [CommSemiring R] (r : R) (rs : List R) {M}
    [AddCommMonoid M] [Module R M] (N : Submodule R M) :
    ofList (r :: rs) • N = r • N ⊔ ofList rs • N

Proof state:
R : Type u_7
inst✝² : CommSemiring R
r : R
rs : List R
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ ofList (r :: rs) • N = r • N ⊔ ofList rs • N

Tactic:
rw [ofList_cons, Submodule.sup_smul, Submodule.ideal_span_singleton_smul]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem smul_integral_comp_mul_sub (c d) :
    (c • ∫ x in a..b, f (c * x - d)) = ∫ x in c * a - d..c * b - d, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
⊢ c • ∫ (x : ℝ) in a..b, f (c * x - d) = ∫ (x : ℝ) in c * a - d..c * b - d, f x

Tactic:
by_cases hc : c = 0 <;> simp [hc, integral_comp_mul_sub]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
@[simp]
lemma evalEval_natCast (x y : R) (n : ℕ) : (n : R[X][Y]).evalEval x y = n

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
n : ℕ
⊢ evalEval x y ↑n = ↑n

Tactic:
simp only [evalEval, eval_natCast]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem Multipliable.trans_div (hg : Multipliable g) (hfg : Multipliable fun b ↦ f b / g b) :
    Multipliable f

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
hg : Multipliable g
hfg : Multipliable fun b => f b / g b
⊢ Multipliable f

Tactic:
simpa only [div_mul_cancel] using hfg.mul hg

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
lemma tendstoLocallyUniformly_iff_forall_isCompact [LocallyCompactSpace α]  :
    TendstoLocallyUniformly F f p ↔ ∀ K : Set α, IsCompact K → TendstoUniformlyOn F f p K

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
⊢ TendstoLocallyUniformly F f p ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn F f p K

Tactic:
simp only [← tendstoLocallyUniformlyOn_univ,
  tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_univ, Set.subset_univ, forall_true_left]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Matrix.lean
theorem toMatrix_self [DecidableEq ι] : b.toMatrix b = (1 : Matrix ι ι k)

Proof state:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : DecidableEq ι
⊢ b.toMatrix ⇑b = 1

Tactic:
ext i j

Result:
case a
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : DecidableEq ι
i j : ι
⊢ b.toMatrix (⇑b) i j = 1 i j

Proof state:
case a
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : DecidableEq ι
i j : ι
⊢ b.toMatrix (⇑b) i j = 1 i j

Tactic:
rw [toMatrix_apply, coord_apply, Matrix.one_eq_pi_single, Pi.single_apply]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem symm_map (f : α ≃o β) : (map f).symm = map f.symm :=
  DFunLike.ext _ _ fun s => ext <| by convert Set.preimage_equiv_eq_image_symm s f.toEquiv

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : UpperSet β
⊢ ↑((map f).symm s) = ↑((map f.symm) s)

Tactic:
convert Set.preimage_equiv_eq_image_symm s f.toEquiv

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_zero_one (b : α) : toIcoDiv (zero_lt_one' α) 0 b = ⌊b⌋

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
b : α
⊢ toIcoDiv ⋯ 0 b = ⌊b⌋

Tactic:
simp [toIcoDiv_eq_floor]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
lemma HurwitzZeta.completedCosZeta₀_zero (s : ℂ) :
    completedCosZeta₀ 0 s = completedRiemannZeta₀ s

Proof state:
s : ℂ
⊢ completedCosZeta₀ 0 s = completedRiemannZeta₀ s

Tactic:
rw [completedRiemannZeta₀, completedHurwitzZetaEven₀, completedCosZeta₀,
  hurwitzEvenFEPair_zero_symm]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_get' [CommMonoid β] (l : List α) (f : α → β) :
    ∏ i : Fin l.length, f l[i.1] = (l.map f).prod

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
l : List α
f : α → β
⊢ ∏ i : Fin l.length, f l[↑i] = (List.map f l).prod

Tactic:
simp [Finset.prod_eq_multiset_prod]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
@[simp] lemma toNat_bne_one (b : Bool) : (b.toNat != 1) = !b

Proof state:
b : Bool
⊢ (b.toNat != 1) = !b

Tactic:
simp [bne]

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_nsmul_const [AddMonoid G] [AddMonoid H] [AddConstMapClass F G H a b]
    (f : F) (n : ℕ) : f (n • a) = f 0 + n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddMonoid G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℕ
⊢ f (n • a) = f 0 + n • b

Tactic:
simpa using map_add_nsmul f 0 n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.lo_eq_false_of_lo (u v k₁ k₂ : Nat) : isLt 0 (k₁+k₂) = true → u + k₁ ≤ v → (v + k₂ ≤ u) = False

Proof state:
u v k₁ k₂ : Nat
⊢ isLt 0 (k₁ + k₂) = true → u + k₁ ≤ v → (v + k₂ ≤ u) = False

Tactic:
simp [isLt]

Result:
u v k₁ k₂ : Nat
⊢ 0 < k₁ + k₂ → u + k₁ ≤ v → u < v + k₂

Proof state:
u v k₁ k₂ : Nat
⊢ 0 < k₁ + k₂ → u + k₁ ≤ v → u < v + k₂

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
@[simp]
lemma quasispectrum.zero_mem [Nontrivial R] (a : A) : 0 ∈ quasispectrum R a :=
  quasispectrum.not_isUnit_mem a <| by simp

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : NonUnitalRing A
inst✝¹ : Module R A
inst✝ : Nontrivial R
a : A
⊢ ¬IsUnit 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
lemma find?_ofFn_eq_some_of_injective {n} {f : Fin n → α} {p : α → Bool} {i : Fin n}
    (h : Function.Injective f) :
    (ofFn f).find? p = some (f i) ↔ p (f i) = true ∧ ∀ j < i, ¬(p (f j) = true)

Proof state:
α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
i : Fin n
h : Function.Injective f
⊢ find? p (ofFn f) = some (f i) ↔ p (f i) = true ∧ ∀ j < i, ¬p (f j) = true

Tactic:
simp only [find?_ofFn_eq_some, h.eq_iff, Bool.not_eq_true, exists_eq_left]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem mul_div_mul_left (a b : ℝ≥0∞) (hc : c ≠ 0) (hc' : c ≠ ⊤) :
    c * a / (c * b) = a / b

Proof state:
c a b : ℝ≥0∞
hc : c ≠ 0
hc' : c ≠ ⊤
⊢ c * a / (c * b) = a / b

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ENNReal.mul_inv (Or.inl hc) (Or.inl hc'), mul_mul_mul_comm,
  ENNReal.mul_inv_cancel hc hc', one_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem aemeasurable_const_smul_iff (c : G) :
    AEMeasurable (fun x => c • f x) μ ↔ AEMeasurable f μ :=
  ⟨fun h => by simpa [inv_smul_smul, Pi.smul_def] using h.const_smul c⁻¹, fun h => h.const_smul c⟩

Proof state:
β : Type u_3
α : Type u_4
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace α
f : α → β
μ : Measure α
G : Type u_5
inst✝³ : Group G
inst✝² : MeasurableSpace G
inst✝¹ : MulAction G β
inst✝ : MeasurableSMul G β
c : G
h : AEMeasurable (fun x => c • f x) μ
⊢ AEMeasurable f μ

Tactic:
simpa [inv_smul_smul, Pi.smul_def] using h.const_smul c⁻¹

Result:
no goals
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingDist_eq_zero {x y : ∀ i, β i} : hammingDist x y = 0 ↔ x = y :=
  ⟨eq_of_hammingDist_eq_zero, fun H => by
    rw [H]
    exact hammingDist_self _⟩

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
H : x = y
⊢ hammingDist x y = 0

Tactic:
rw [H]

Result:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
H : x = y
⊢ hammingDist y y = 0

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
H : x = y
⊢ hammingDist y y = 0

Tactic:
exact hammingDist_self _

Result:
no goals
-- Mathlib/Data/PNat/Interval.lean
theorem card_fintype_uIcc : Fintype.card (Set.uIcc a b) = (b - a : ℤ).natAbs + 1

Proof state:
a b : ℕ+
⊢ Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 1

Tactic:
rw [← card_uIcc, Fintype.card_ofFinset]

Result:
no goals
-- Mathlib/FieldTheory/Laurent.lean
theorem laurentAux_algebraMap : laurentAux r (algebraMap _ _ p) = algebraMap _ _ (taylor r p)

Proof state:
R : Type u
inst✝¹ : CommRing R
r : R
p : R[X]
inst✝ : IsDomain R
⊢ (laurentAux r) ((algebraMap R[X] (RatFunc R)) p) = (algebraMap R[X] (RatFunc R)) ((taylor r) p)

Tactic:
rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one]

Result:
no goals
-- Mathlib/Topology/Exterior.lean
theorem exterior_iUnion (s : ι → Set X) : exterior (⋃ i, s i) = ⋃ i, exterior (s i)

Proof state:
ι : Sort u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
⊢ exterior (⋃ i, s i) = ⋃ i, exterior (s i)

Tactic:
simp only [exterior, nhdsSet_iUnion, ker_iSup]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem zneg_toZNumNeg (n : Num) : -n.toZNumNeg = n.toZNum

Proof state:
n : Num
⊢ -n.toZNumNeg = n.toZNum

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Order/GameAdd.lean
theorem gameAdd_swap_swap : ∀ a b : α × β, GameAdd rβ rα a.swap b.swap ↔ GameAdd rα rβ a b :=
  fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => by rw [Prod.swap, Prod.swap, gameAdd_mk_iff, gameAdd_mk_iff, or_comm]

Proof state:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ GameAdd rβ rα (a₁, b₁).swap (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)

Tactic:
rw [Prod.swap, Prod.swap, gameAdd_mk_iff, gameAdd_mk_iff, or_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem zero_addChar_eq (c : Char) : (0 : Pos) + c = ⟨c.utf8Size⟩

Proof state:
c : Char
⊢ 0 + c = { byteIdx := c.utf8Size }

Tactic:
rw [← zero_addChar_byteIdx]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem smul_inf (a : α) (S T : Subgroup G) : a • (S ⊓ T) = a • S ⊓ a • T

Proof state:
α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : Group α
inst✝ : MulDistribMulAction α G
a : α
S T : Subgroup G
⊢ a • (S ⊓ T) = a • S ⊓ a • T

Tactic:
simp [SetLike.ext_iff, mem_pointwise_smul_iff_inv_smul_mem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem coordinate_eval_4 :
    (coordinate 4).eval (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: t)) = a4

Proof state:
a0 a1 a2 a3 a4 : Int
t : List Int
⊢ (coordinate 4).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: t)) = a4

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_eq_pred_iff_of_not_isMin (ha : ¬IsMin a) (hb : ¬IsMin b) :
    pred a = pred b ↔ a = b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
hb : ¬IsMin b
⊢ pred a = pred b ↔ a = b

Tactic:
rw [eq_iff_le_not_lt, eq_iff_le_not_lt, pred_le_pred_iff_of_not_isMin ha hb,
  pred_lt_pred_iff_of_not_isMin ha hb]

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ioi_pred_eq_Ici_of_not_isMin (ha : ¬ IsMin a) : Ioi (pred a) = Ici a :=
  coe_injective <| by simpa using Set.Ioi_pred_eq_Ici_of_not_isMin ha

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
⊢ ↑(Ioi (pred a)) = ↑(Ici a)

Tactic:
simpa using Set.Ioi_pred_eq_Ici_of_not_isMin ha

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem sup_eq_closure_mul (H K : Subgroup G) : H ⊔ K = closure ((H : Set G) * (K : Set G)) :=
  le_antisymm
    (sup_le (fun h hh => subset_closure ⟨h, hh, 1, K.one_mem, mul_one h⟩) fun k hk =>
      subset_closure ⟨1, H.one_mem, k, hk, one_mul k⟩)
    ((closure_mul_le _ _).trans <| by rw [closure_eq, closure_eq])

Proof state:
G : Type u_2
inst✝ : Group G
H K : Subgroup G
⊢ closure ↑H ⊔ closure ↑K ≤ H ⊔ K

Tactic:
rw [closure_eq, closure_eq]

Result:
no goals
-- Mathlib/Algebra/Ring/Invertible.lean
theorem one_sub_invOf_two [Ring α] [Invertible (2 : α)] : 1 - (⅟ 2 : α) = ⅟ 2 :=
  (isUnit_of_invertible (2 : α)).mul_right_inj.1 <| by
    rw [mul_sub, mul_invOf_self, mul_one, ← one_add_one_eq_two, add_sub_cancel_right]

Proof state:
α : Type u
inst✝¹ : Ring α
inst✝ : Invertible 2
⊢ 2 * (1 - ⅟2) = 2 * ⅟2

Tactic:
rw [mul_sub, mul_invOf_self, mul_one, ← one_add_one_eq_two, add_sub_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Order/CompleteField.lean
theorem inducedMap_inv_self (b : β) : inducedMap γ β (inducedMap β γ b) = b

Proof state:
β : Type u_3
γ : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : ConditionallyCompleteLinearOrderedField γ
b : β
⊢ inducedMap γ β (inducedMap β γ b) = b

Tactic:
rw [inducedMap_inducedMap, inducedMap_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toArray_set (a : Vector α n) (i x h) :
    (a.set i x).toArray = a.toArray.set i x (by simpa using h):= rfl

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

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem eqOn_singleton : Set.EqOn f₁ f₂ {a} ↔ f₁ a = f₂ a

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
a : α
⊢ EqOn f₁ f₂ {a} ↔ f₁ a = f₂ a

Tactic:
simp [Set.EqOn]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
theorem disjSups_singleton : ({a} ○ {b} : Finset α) = if Disjoint a b then {a ⊔ b} else ∅

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
a b : α
⊢ {a} ○ {b} = if Disjoint a b then {a ⊔ b} else ∅

Tactic:
split_ifs with h <;> simp [disjSups, filter_singleton, h]

Result:
no goals
-- Mathlib/Data/Finset/Empty.lean
theorem coe_empty : ((∅ : Finset α) : Set α) = ∅ :=
  Set.ext <| by simp

Proof state:
α : Type u_1
⊢ ∀ (x : α), x ∈ ↑∅ ↔ x ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem le_compl_self : a ≤ aᶜ ↔ a = ⊥

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ≤ aᶜ ↔ a = ⊥

Tactic:
rw [le_compl_iff_disjoint_left, disjoint_self]

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Basic.lean
theorem div_div_div_comm (hbc : Commute b c) (hbd : Commute b⁻¹ d) (hcd : Commute c⁻¹ d) :
    a / b / (c / d) = a / c / (b / d)

Proof state:
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a / b / (c / d) = a / c / (b / d)

Tactic:
simp_rw [div_eq_mul_inv, mul_inv_rev, inv_inv, hbd.symm.eq, hcd.symm.eq,
  hbc.inv_inv.mul_mul_mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List α} {k k' fallback : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a == b) = false))
    (mem : k ∈ l ) :
    getKeyD (unitOfList l) k' fallback = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' fallback : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
⊢ (unitOfList l).getKeyD k' fallback = k

Tactic:
simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_mem

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/OfFn.lean
theorem head_ofFn {n} (f : Fin n → α) (h : ofFn f ≠ []) :
    (ofFn f).head h = f ⟨0, Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)⟩

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
h : ofFn f ≠ []
⊢ (ofFn f).head h = f ⟨0, ⋯⟩

Tactic:
rw [← getElem_zero (length_ofFn _ ▸ Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)),
  List.getElem_ofFn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem two_mul (n) : 2 * n = n + n

Proof state:
n : Nat
⊢ 2 * n = n + n

Tactic:
rw [Nat.succ_mul, Nat.one_mul]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_iUnion_le {ι : Type*} [Fintype ι] (f : α → ℝ≥0∞) (t : ι → Set α) :
    ∑' x : ⋃ i, t i, f x ≤ ∑ i, ∑' x : t i, f x

Proof state:
α : Type u_1
ι : Type u_4
inst✝ : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x

Tactic:
exact tsum_iUnion_le_tsum f t

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_4
inst✝ : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑ i : ι, ∑' (x : ↑(t i)), f ↑x

Tactic:
rw [← tsum_fintype]

Result:
α : Type u_1
ι : Type u_4
inst✝ : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x