harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_umod {x y : BitVec w} :
    (x % y).toInt = (x.toNat % y.toNat : Int).bmod (2 ^ w)

Proof state:
w : Nat
x y : BitVec w
⊢ (x % y).toInt = (↑x.toNat % ↑y.toNat).bmod (2 ^ w)

Tactic:
simp [toInt_eq_toNat_bmod]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderivWithin_id (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 id s x = id 𝕜 E

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 _root_.id x = ContinuousLinearMap.id 𝕜 E

Tactic:
exact fderiv_id

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 _root_.id s x = ContinuousLinearMap.id 𝕜 E

Tactic:
rw [DifferentiableAt.fderivWithin differentiableAt_id hxs]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 _root_.id x = ContinuousLinearMap.id 𝕜 E
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
lemma binEntropy_eq_negMulLog_add_negMulLog_one_sub (p : ℝ) :
    binEntropy p = negMulLog p + negMulLog (1 - p)

Proof state:
p : ℝ
⊢ binEntropy p = p.negMulLog + (1 - p).negMulLog

Tactic:
simp [binEntropy, negMulLog, ← neg_mul]

Result:
no goals
-- Mathlib/Algebra/Algebra/Basic.lean
@[simp]
lemma algebraMap_comp_natCast (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] :
    algebraMap R A ∘ Nat.cast = Nat.cast

Proof state:
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ⇑(algebraMap R A) ∘ Nat.cast = Nat.cast

Tactic:
ext

Result:
case h
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : ℕ
⊢ (⇑(algebraMap R A) ∘ Nat.cast) x✝ = ↑x✝

Proof state:
case h
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : ℕ
⊢ (⇑(algebraMap R A) ∘ Nat.cast) x✝ = ↑x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Choose/Sum.lean
/-- **Zhu Shijie's identity** aka hockey-stick identity, version with `range`.
Summing `(i + k).choose k` for `i ∈ [0, n]` gives `(n + k + 1).choose (k + 1)`.

Combinatorial interpretation: `(i + k).choose k` is the number of decompositions of `[0, i)` in
`k + 1` (possibly empty) intervals (this follows from a stars and bars description). In particular,
`(n + k + 1).choose (k + 1)` corresponds to decomposing `[0, n)` into `k + 2` intervals.
By putting away the last interval (of some length `n - i`),
we have to decompose the remaining interval `[0, i)` into `k + 1` intervals, hence the sum. -/
lemma sum_range_add_choose (n k : ℕ) :
    ∑ i ∈ Finset.range (n + 1), (i + k).choose k = (n + k + 1).choose (k + 1)

Proof state:
n k : ℕ
⊢ ∑ i ∈ range (n + 1), (i + k).choose k = (n + k + 1).choose (k + 1)

Tactic:
rw [← sum_Icc_choose, range_eq_Ico]

Result:
n k : ℕ
⊢ ∑ i ∈ Ico 0 (n + 1), (i + k).choose k = ∑ m ∈ Icc k (n + k), m.choose k

Proof state:
case h.e'_3.h
n k : ℕ
⊢ Icc k (n + k) = map (addRightEmbedding k) (Ico 0 (n + 1))

Tactic:
rw [map_add_right_Ico, zero_add, add_right_comm, Nat.Ico_succ_right]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
lemma ciSup_eq_ite {p : Prop} [Decidable p] {f : p → α} :
    (⨆ h : p, f h) = if h : p then f h else sSup (∅ : Set α)

Proof state:
α : Type u_1
inst✝¹ : ConditionallyCompleteLattice α
p : Prop
inst✝ : Decidable p
f : p → α
⊢ ⨆ (h : p), f h = if h : p then f h else sSup ∅

Tactic:
by_cases H : p <;> simp [ciSup_neg, H]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_not {x : BitVec w} : (~~~x).msb = (decide (0 < w) && !x.msb)

Proof state:
w : Nat
x : BitVec w
⊢ (~~~x).msb = (decide (0 < w) && !x.msb)

Tactic:
simp [BitVec.msb]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem const_min (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => min a (f x)

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
Kf : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith Kf fun x => a ⊓ f x

Tactic:
simpa only [min_comm] using hf.min_const a

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConstantSheaf.lean
/--
The property of a sheaf of being constant is invariant under equivalence of sheaf
categories.
-/
lemma Sheaf.isConstant_iff_of_equivalence (F : Sheaf K D) :
    ((sheafEquiv G J K D).inverse.obj F).IsConstant J ↔ IsConstant K F

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_6, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_5, u_2} D
inst✝⁴ : HasWeakSheafify J D
C' : Type u_3
inst✝³ : Category.{u_4, u_3} C'
K : GrothendieckTopology C'
inst✝² : HasWeakSheafify K D
G : C ⥤ C'
inst✝¹ : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst✝ : IsDenseSubsite J K G
T : C
hT : IsTerminal T
hT' : IsTerminal (G.obj T)
F : Sheaf K D
⊢ IsConstant J ((sheafEquiv G J K D).inverse.obj F) ↔ IsConstant K F

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝⁶ : Category.{u_6, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_5, u_2} D
inst✝⁴ : HasWeakSheafify J D
C' : Type u_3
inst✝³ : Category.{u_4, u_3} C'
K : GrothendieckTopology C'
inst✝² : HasWeakSheafify K D
G : C ⥤ C'
inst✝¹ : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst✝ : IsDenseSubsite J K G
T : C
hT : IsTerminal T
hT' : IsTerminal (G.obj T)
F : Sheaf K D
⊢ IsConstant J ((sheafEquiv G J K D).inverse.obj F) → IsConstant K F

case mpr
C : Type u_1
inst✝⁶ : Category.{u_6, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_5, u_2} D
inst✝⁴ : HasWeakSheafify J D
C' : Type u_3
inst✝³ : Category.{u_4, u_3} C'
K : GrothendieckTopology C'
inst✝² : HasWeakSheafify K D
G : C ⥤ C'
inst✝¹ : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst✝ : IsDenseSubsite J K G
T : C
hT : IsTerminal T
hT' : IsTerminal (G.obj T)
F : Sheaf K D
⊢ IsConstant K F → IsConstant J ((sheafEquiv G J K D).inverse.obj F)

Proof state:
case mp
C : Type u_1
inst✝⁶ : Category.{u_6, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_5, u_2} D
inst✝⁴ : HasWeakSheafify J D
C' : Type u_3
inst✝³ : Category.{u_4, u_3} C'
K : GrothendieckTopology C'
inst✝² : HasWeakSheafify K D
G : C ⥤ C'
inst✝¹ : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst✝ : IsDenseSubsite J K G
T : C
hT : IsTerminal T
hT' : IsTerminal (G.obj T)
F : Sheaf K D
⊢ IsConstant J ((sheafEquiv G J K D).inverse.obj F) → IsConstant K F

Tactic:
exact fun ⟨Y, ⟨i⟩⟩ ↦ ⟨_, ⟨(equivCommuteConstant J D K G hT hT').symm.app _ ≪≫
  (sheafEquiv G J K D).functor.mapIso i ≪≫ (sheafEquiv G J K D).counitIso.app _⟩⟩

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝⁶ : Category.{u_6, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{u_5, u_2} D
inst✝⁴ : HasWeakSheafify J D
C' : Type u_3
inst✝³ : Category.{u_4, u_3} C'
K : GrothendieckTopology C'
inst✝² : HasWeakSheafify K D
G : C ⥤ C'
inst✝¹ : ∀ (X : C'ᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) D
inst✝ : IsDenseSubsite J K G
T : C
hT : IsTerminal T
hT' : IsTerminal (G.obj T)
F : Sheaf K D
⊢ IsConstant K F → IsConstant J ((sheafEquiv G J K D).inverse.obj F)

Tactic:
exact fun ⟨Y, ⟨i⟩⟩ ↦ ⟨_, ⟨(equivCommuteConstant' J D K G hT hT').app _ ≪≫
  (sheafEquiv G J K D).inverse.mapIso i⟩⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem shiftLeft_shiftRight (x n : Nat) : x <<< n >>> n = x

Proof state:
x n : Nat
⊢ x <<< n >>> n = x

Tactic:
rw [Nat.shiftLeft_eq, Nat.shiftRight_eq_div_pow, Nat.mul_div_cancel _ (Nat.two_pow_pos _)]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_singleton_true (p : α → Prop) : p ⁻¹' {True} = {a | p a}

Proof state:
case h
α : Type u_1
p : α → Prop
x✝ : α
⊢ x✝ ∈ p ⁻¹' {True} ↔ x✝ ∈ {a | p a}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
⊢ p ⁻¹' {True} = {a | p a}

Tactic:
ext

Result:
case h
α : Type u_1
p : α → Prop
x✝ : α
⊢ x✝ ∈ p ⁻¹' {True} ↔ x✝ ∈ {a | p a}
-- Mathlib/Algebra/RingQuot.lean
theorem mkRingHom_rel {r : R → R → Prop} {x y : R} (w : r x y) : mkRingHom r x = mkRingHom r y

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x y : R
w : r x y
⊢ (mkRingHom r) x = (mkRingHom r) y

Tactic:
simp [mkRingHom_def, Quot.sound (Rel.of w)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
@[simp]
lemma stalkMap_inv_hom_apply (e : X ≅ Y) (x : X) (y) :
    e.hom.stalkMap x (e.inv.stalkMap (e.hom.base x) y) =
      (X.presheaf.stalkCongr (.of_eq (by simp))).hom y :=
  DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_inv_hom e x)) y

Proof state:
X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
x : ↑↑X.toPresheafedSpace
y : ↑(X.presheaf.stalk ((ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x)))
⊢ (ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_neg (A : Matrix n n R) : det (-A) = (-1) ^ Fintype.card n * det A

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
⊢ (-A).det = (-1) ^ Fintype.card n * A.det

Tactic:
rw [← det_smul, neg_one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem insertMany_cons (h : m.WF) {l : List (α × β)}
    {k : α} {v : β} :
    insertMany m (⟨k, v⟩ :: l) = insertMany (m.insert k v) l

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw α fun x => β
h : m.WF
l : List (α × β)
k : α
v : β
⊢ insertMany m ((k, v) :: l) = insertMany (m.insert k v) l

Tactic:
simp_to_raw

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw α fun x => β
h : m.WF
l : List (α × β)
k : α
v : β
⊢ (Raw₀.Const.insertMany ⟨m, ⋯⟩ ((k, v) :: l)).val.val = (Raw₀.Const.insertMany (Raw₀.insert ⟨m, ⋯⟩ k v) l).val.val

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw α fun x => β
h : m.WF
l : List (α × β)
k : α
v : β
⊢ (Raw₀.Const.insertMany ⟨m, ⋯⟩ ((k, v) :: l)).val.val = (Raw₀.Const.insertMany (Raw₀.insert ⟨m, ⋯⟩ k v) l).val.val

Tactic:
rw [Raw₀.Const.insertMany_cons]

Result:
no goals
-- Mathlib/Algebra/Group/Pi/Basic.lean
theorem extend_one [One γ] (f : α → β) : Function.extend f (1 : α → γ) (1 : β → γ) = 1 :=
  funext fun _ => by apply ite_self

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One γ
f : α → β
x✝ : β
⊢ extend f 1 1 x✝ = 1 x✝

Tactic:
apply ite_self

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
/-- The lower part of the third column of the snake diagram is exact. -/
lemma exact_C₃_down : (ShortComplex.mk S.v₁₂.τ₃ S.v₂₃.τ₃
    (by rw [← comp_τ₃, S.w₁₃, zero_τ₃])).Exact :=
  exact_of_g_is_cokernel _ S.h₃τ₃

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.47750, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₁₂.τ₃ ≫ S.v₂₃.τ₃ = 0

Tactic:
rw [← comp_τ₃, S.w₁₃, zero_τ₃]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_eval_comp {R : Type*} [CommSemiring R] (n : ℕ) (p : R[X]) [Algebra R S]
    (x : S) : ((ascPochhammer S n).comp (p.map (algebraMap R S))).eval x =
    (ascPochhammer S n).eval (p.eval₂ (algebraMap R S) x)

Proof state:
S : Type u
inst✝² : Semiring S
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
p : R[X]
inst✝ : Algebra R S
x : S
⊢ eval x ((ascPochhammer S n).comp (map (algebraMap R S) p)) = eval (eval₂ (algebraMap R S) x p) (ascPochhammer S n)

Tactic:
rw [ascPochhammer_eval₂ (algebraMap R S), ← eval₂_comp', ← ascPochhammer_map (algebraMap R S),
  ← map_comp, eval_map]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem apply_zpow_apply_eq_iff (f : Perm α) (n : ℤ) {x : α} :
    f ((f ^ n) x) = (f ^ n) x ↔ f x = x

Proof state:
α : Type u_1
f : Perm α
n : ℤ
x : α
⊢ f ((f ^ n) x) = (f ^ n) x ↔ f x = x

Tactic:
rw [← mul_apply, Commute.self_zpow f, mul_apply, apply_eq_iff_eq]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem count_map {α β : Type*} (f : α → β) (s : Multiset α) [DecidableEq β] (b : β) :
    count b (map f s) = card (s.filter fun a => b = f a)

Proof state:
α : Type u_3
β : Type u_4
f : α → β
s : Multiset α
inst✝ : DecidableEq β
b : β
⊢ count b (map f s) = (filter (fun a => b = f a) s).card

Tactic:
simp [Bool.beq_eq_decide_eq, eq_comm, count, countP_map]

Result:
no goals
-- Mathlib/Logic/Hydra.lean
lemma cutExpand_add_right {s' s} (t) : CutExpand r (s' + t) (s + t) ↔ CutExpand r s' s

Proof state:
α : Type u_1
r : α → α → Prop
s' s t : Multiset α
⊢ CutExpand r (s' + t) (s + t) ↔ CutExpand r s' s

Tactic:
convert cutExpand_add_left t using 2 <;> apply add_comm

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem cauchy_map_iff {l : Filter β} {f : β → α} :
    Cauchy (l.map f) ↔ NeBot l ∧ Tendsto (fun p : β × β => (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
⊢ Cauchy (map f l) ↔ l.NeBot ∧ Tendsto (fun p => (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)

Tactic:
rw [Cauchy, map_neBot_iff, prod_map_map_eq, Tendsto]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_flatten (f : α → β) (L : List (List α)) :
    (flatten L).map f = (map (map f) L).flatten

Proof state:
α : Type u_1
β : Type u_2
f : α → β
L : List (List α)
⊢ map f L.flatten = (map (map f) L).flatten

Tactic:
induction L <;> simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@[deprecated map_add_of_iInf_genEigenspace_ne_bot_of_commute (since := "2024-10-23")]
lemma map_add_of_iInf_iSup_genEigenspace_ne_bot_of_commute [NoZeroSMulDivisors R M]
    {L F : Type*} [Add L] [FunLike F L (End R M)] [AddHomClass F L (End R M)] (f : F)
    (μ : L → R) (h_ne : ⨅ x, ⨆ k : ℕ, (f x).genEigenspace (μ x) k ≠ ⊥)
    (h : ∀ x y, Commute (f x) (f y)) (x y : L) :
    μ (x + y) = μ x + μ y

Proof state:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) ↑k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
⊢ μ (x + y) = μ x + μ y

Tactic:
simp_rw [iSup_genEigenspace_eq] at h_ne

Result:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
h_ne : ⨅ x, (f x).maxGenEigenspace (μ x) ≠ ⊥
⊢ μ (x + y) = μ x + μ y

Proof state:
R : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : NoZeroSMulDivisors R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
h_ne : ⨅ x, (f x).maxGenEigenspace (μ x) ≠ ⊥
⊢ μ (x + y) = μ x + μ y

Tactic:
apply map_add_of_iInf_genEigenspace_ne_bot_of_commute f μ ⊤ h_ne h x y

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
lemma Real.singleton_eq_inter_Icc (b : ℝ) : {b} = ⋂ (r > 0), Icc (b - r) (b + r)

Proof state:
b : ℝ
⊢ {b} = ⋂ r, ⋂ (_ : r > 0), Icc (b - r) (b + r)

Tactic:
simp [Icc_eq_closedBall, biInter_basis_nhds Metric.nhds_basis_closedBall]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Finite.lean
theorem card_eq_iff_eq_top [Finite H] : Nat.card H = Nat.card G ↔ H = ⊤ :=
  Iff.intro (eq_top_of_card_eq H) (fun h ↦ by simpa only [h] using card_top)

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↥H
h : H = ⊤
⊢ Nat.card ↥H = Nat.card G

Tactic:
simpa only [h] using card_top

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma map_freeOn (f : α → β) (hf) : (freeOn E).map f hf = freeOn (f '' E)

Proof state:
α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (freeOn E).E
⊢ (freeOn E).map f hf = freeOn (f '' E)

Tactic:
rw [← dual_inj]

Result:
α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (freeOn E).E
⊢ ((freeOn E).map f hf)✶ = (freeOn (f '' E))✶

Proof state:
α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (freeOn E).E
⊢ ((freeOn E).map f hf)✶ = (freeOn (f '' E))✶

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem get_reverse' (l : List α) (n) (hn') :
    l.reverse.get n = l.get ⟨l.length - 1 - n, hn'⟩

Proof state:
α : Type u
l : List α
n : Fin l.reverse.length
hn' : l.length - 1 - ↑n < l.length
⊢ l.reverse.get n = l.get ⟨l.length - 1 - ↑n, hn'⟩

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
lemma charpoly_of_upperTriangular [LinearOrder n] (M : Matrix n n R) (h : M.BlockTriangular id) :
    M.charpoly = ∏ i : n, (X - C (M i i))

Proof state:
R : Type u_1
inst✝³ : CommRing R
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : LinearOrder n
M : Matrix n n R
h : M.BlockTriangular id
⊢ M.charpoly = ∏ i : n, (X - C (M i i))

Tactic:
simp [charpoly, det_of_upperTriangular h.charmatrix]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma IsBasis.spanning_iff_spanning (hIX : M.IsBasis I X) : M.Spanning I ↔ M.Spanning X

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
⊢ M.Spanning I ↔ M.Spanning X

Tactic:
rw [spanning_iff_closure_eq, spanning_iff_closure_eq, hIX.closure_eq_closure]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem monotoneOn_iff_monotone : MonotoneOn f s ↔
    Monotone fun a : s => f a

Proof state:
α : Type u
β : Type v
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ MonotoneOn f s ↔ Monotone fun a => f ↑a

Tactic:
simp [Monotone, MonotoneOn]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem diff_cons (l₁ l₂ : List α) (a : α) : l₁.diff (a :: l₂) = (l₁.erase a).diff l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
⊢ l₁.diff (a :: l₂) = (l₁.erase a).diff l₂

Tactic:
simp_all [List.diff, erase_of_not_mem]

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
nonrec lemma IsSelfAdjoint.imaginaryPart {x : A} (hx : IsSelfAdjoint x) :
    ℑ x = 0

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
hx : IsSelfAdjoint x
⊢ ℑ x = 0

Tactic:
rw [imaginaryPart, LinearMap.comp_apply, hx.skewAdjointPart_apply _, map_zero]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem two_zsmul_oangle_smul_left_of_ne_zero (x y : V) {r : ℝ} (hr : r ≠ 0) :
    (2 : ℤ) • o.oangle (r • x) y = (2 : ℤ) • o.oangle x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : r ≠ 0
⊢ 2 • o.oangle (r • x) y = 2 • o.oangle x y

Tactic:
rcases hr.lt_or_lt with (h | h) <;> simp [h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma ΨSq_odd_ofNat (m : ℕ) : W.ΨSq (2 * (m + 2) + 1) =
    (W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * (if Even m then W.Ψ₂Sq ^ 2 else 1) -
      W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * (if Even m then 1 else W.Ψ₂Sq ^ 2)) ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℕ
⊢ W.ΨSq (2 * (↑m + 2) + 1) =
    ((W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
        W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) ^
      2

Tactic:
rw_mod_cast [ΨSq_ofNat, preΨ'_odd, if_neg (m + 2).not_even_two_mul_add_one, mul_one]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma Monic.ne_zero [Nonempty A] [Nontrivial R] (hp : p.Monic D) : p ≠ 0 := fun h => by
  simp_rw [Monic, h, leadingCoeff_zero, zero_ne_one] at hp

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁴ : Semiring R
inst✝³ : LinearOrder B
inst✝² : OrderBot B
p : R[A]
D : A → B
inst✝¹ : Nonempty A
inst✝ : Nontrivial R
hp : Monic D p
h : p = 0
⊢ False

Tactic:
simp_rw [Monic, h, leadingCoeff_zero, zero_ne_one] at hp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem _root_.MeasurableSet.exists_isClosed_diff_lt [OpensMeasurableSpace α] [WeaklyRegular μ]
    ⦃A : Set α⦄ (hA : MeasurableSet A) (h'A : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ F, F ⊆ A ∧ IsClosed F ∧ μ (A \ F) < ε

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.WeaklyRegular
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ F ⊆ A, IsClosed F ∧ μ (A \ F) < ε

Tactic:
rcases hA.exists_isClosed_lt_add h'A hε with ⟨F, hFA, hFc, hF⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.WeaklyRegular
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hFA : F ⊆ A
hFc : IsClosed F
hF : μ A < μ F + ε
⊢ ∃ F ⊆ A, IsClosed F ∧ μ (A \ F) < ε

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.WeaklyRegular
A : Set α
hA : MeasurableSet A
h'A : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hFA : F ⊆ A
hFc : IsClosed F
hF : μ A < μ F + ε
⊢ ∃ F ⊆ A, IsClosed F ∧ μ (A \ F) < ε

Tactic:
exact ⟨F, hFA, hFc, measure_diff_lt_of_lt_add hFc.nullMeasurableSet hFA
  (ne_top_of_le_ne_top h'A <| measure_mono hFA) hF⟩

Result:
no goals
-- Mathlib/Tactic/Peel.lean
private lemma and_imp_left_of_imp_imp {p q r : Prop} (h : r → p → q) : r ∧ p → r ∧ q

Proof state:
p q r : Prop
h : r → p → q
⊢ r ∧ p → r ∧ q

Tactic:
tauto

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem eq_univ_iff_ncard [Finite α] (s : Set α) :
    s = univ ↔ ncard s = Nat.card α

Proof state:
α : Type u_1
inst✝ : Finite α
s : Set α
⊢ s = univ ↔ s.ncard = Nat.card α

Tactic:
rw [← compl_empty_iff, ← ncard_eq_zero, ← ncard_add_ncard_compl s, self_eq_add_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_eq_get!_getKey? [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} :
    m.getKey! a = (m.getKey? a).get!

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
a : α
⊢ m.getKey! a = (m.getKey? a).get!

Tactic:
simp_to_model using List.getKey!_eq_getKey?

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem getElem?_range' (start size step i) :
   (range' start size step)[i]? = if i < size then some (start + step * i) else none

Proof state:
start size step i : Nat
⊢ (range' start size step)[i]? = if i < size then some (start + step * i) else none

Tactic:
simp [getElem?_def, range']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_tdiv : ∀ a b : Int, (-a).tdiv b = -(a.tdiv b)
  | 0, n => by simp [Int.neg_zero]
  | succ _, (n:Nat) | -[_+1], 0 | -[_+1], -[_+1] => rfl
  | succ _, -[_+1] | -[_+1], succ _ => (Int.neg_neg _).symm

Proof state:
n : Int
⊢ (-0).tdiv n = -tdiv 0 n

Tactic:
simp [Int.neg_zero]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
theorem zpowers_le {g : G} {H : Subgroup G} : zpowers g ≤ H ↔ g ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
g : G
H : Subgroup G
⊢ zpowers g ≤ H ↔ g ∈ H

Tactic:
rw [zpowers_eq_closure, closure_le, Set.singleton_subset_iff, SetLike.mem_coe]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNormEssSup_measure_zero {f : α → ε} : eLpNormEssSup f (0 : Measure α) = 0

Proof state:
α : Type u_1
ε : Type u_2
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
⊢ eLpNormEssSup f 0 = 0

Tactic:
simp [eLpNormEssSup]

Result:
no goals