harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_sub_int [AddGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1]
    (f : F) (x : G) (n : ℤ) : f (x - n) = f x - n

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroupWithOne H
inst✝ : AddConstMapClass F G H 1 1
f : F
x : G
n : ℤ
⊢ f (x - ↑n) = f x - ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem rat_mul_iff (hr : r ≠ 0) : LiouvilleWith p (r * x) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
r : ℚ
hr : r ≠ 0
⊢ LiouvilleWith p (↑r * x) ↔ LiouvilleWith p x

Tactic:
rw [mul_comm, mul_rat_iff hr]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem homEquiv_symm_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G)
    (adj2 : F ⊣ G') (x : D) :
    (adj2.homEquiv _ _).symm ((rightAdjointUniq adj1 adj2).hom.app x) = adj1.counit.app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
⊢ (adj2.homEquiv (G.obj x) x).symm ((adj1.rightAdjointUniq adj2).hom.app x) = adj1.counit.app x

Tactic:
simp [rightAdjointUniq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_neg (a b : Int) : a % -b = a % b

Proof state:
a b : Int
⊢ a % -b = a % b

Tactic:
rw [emod_def, emod_def, Int.ediv_neg, Int.neg_mul_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.neg_mul (x y : BitVec w) : (~~~x + 1#w) * y = ~~~(x * y) + 1#w

Proof state:
w : Nat
x y : BitVec w
⊢ (~~~x + 1#w) * y = ~~~(x * y) + 1#w

Tactic:
rw [← BitVec.neg_eq_not_add, ← BitVec.neg_eq_not_add, _root_.BitVec.neg_mul]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem diam_subsingleton (hs : s.Subsingleton) : diam s = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Subsingleton
⊢ diam s = 0

Tactic:
simp only [diam, EMetric.diam_subsingleton hs, ENNReal.zero_toReal]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_closure_congr (hXY : M.closure X = M.closure Y) : M.cRk X = M.cRk Y

Proof state:
α : Type u
M : Matroid α
X Y : Set α
inst✝ : M.InvariantCardinalRank
hXY : M.closure X = M.closure Y
⊢ M.cRk X = M.cRk Y

Tactic:
rw [← cRk_closure, hXY, cRk_closure]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
lemma MeasurableSpace.pi_eq_generateFrom_projections {mα : ∀ i, MeasurableSpace (α i)} :
    pi = generateFrom {B | ∃ (i : ι) (A : Set (α i)), MeasurableSet A ∧ eval i ⁻¹' A = B}

Proof state:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
⊢ pi = generateFrom {B | ∃ i A, MeasurableSet A ∧ eval i ⁻¹' A = B}

Tactic:
simp only [pi, ← generateFrom_iUnion_measurableSet, iUnion_setOf, measurableSet_comap]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem sSameSide_comm {s : AffineSubspace R P} {x y : P} : s.SSameSide x y ↔ s.SSameSide y x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ s.SSameSide x y ↔ s.SSameSide y x

Tactic:
rw [SSameSide, SSameSide, wSameSide_comm, and_comm (b := x ∉ s)]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Basic.lean
theorem not_mem_union : a ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t

Tactic:
rw [mem_union, not_or]

Result:
no goals
-- Mathlib/Analysis/Normed/MulAction.lean
@[bound]
lemma enorm_smul_le : ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : BoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ

Tactic:
simpa [enorm, ← ENNReal.coe_mul] using nnnorm_smul_le ..

Result:
no goals
-- Mathlib/Data/Nat/Periodic.lean
theorem periodic_coprime (a : ℕ) : Periodic (Coprime a) a

Proof state:
a : ℕ
⊢ Periodic a.Coprime a

Tactic:
simp only [coprime_add_self_right, forall_const, eq_iff_iff, Periodic]

Result:
no goals
-- Mathlib/Order/Disjointed.lean
theorem disjointed_eq_inf_compl [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) (i : ι) :
    disjointed f i = f i ⊓ ⨅ j < i, (f j)ᶜ

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : CompleteBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ disjointed f i = f i ⊓ ⨅ j, ⨅ (_ : j < i), (f j)ᶜ

Tactic:
simp only [disjointed_apply, Finset.sup_eq_iSup, mem_Iio, sdiff_eq, compl_iSup]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem SuperpolynomialDecay.param_mul (hf : SuperpolynomialDecay l k f) :
    SuperpolynomialDecay l k (k * f) := fun z =>
  tendsto_nhds.2 fun s hs hs0 =>
    l.sets_of_superset ((tendsto_nhds.1 (hf <| z + 1)) s hs hs0) fun x hx => by
      simpa only [Set.mem_preimage, Pi.mul_apply, ← mul_assoc, ← pow_succ] using hx

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
z : ℕ
s : Set β
hs : IsOpen s
hs0 : 0 ∈ s
x : α
hx : x ∈ (fun a => k a ^ (z + 1) * f a) ⁻¹' s
⊢ x ∈ (fun a => k a ^ z * (k * f) a) ⁻¹' s

Tactic:
simpa only [Set.mem_preimage, Pi.mul_apply, ← mul_assoc, ← pow_succ] using hx

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedSup_infs_of_not_mem (ha : a ∉ lowerClosure s ⊓ lowerClosure t) :
    truncatedSup (s ⊼ t) a = ⊤ :=
  truncatedSup_of_not_mem <| by rwa [coe_infs, lowerClosure_infs]

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
ha : a ∉ lowerClosure ↑s ⊓ lowerClosure ↑t
⊢ a ∉ lowerClosure ↑(s ⊼ t)

Tactic:
rwa [coe_infs, lowerClosure_infs]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem union_insert (a : α) (s t : Finset α) : s ∪ insert a t = insert a (s ∪ t)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ s ∪ insert a t = insert a (s ∪ t)

Tactic:
simp only [insert_eq, union_left_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma mk₀_zero : mk₀ (0 : X ⟶ Y) = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ mk₀ 0 = 0

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (mk₀ 0).hom = hom 0

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (mk₀ 0).hom = hom 0

Tactic:
simp [this, zero_hom']

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
⊢ mk₀ 0 = 0

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ mk₀ 0 = 0
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem singleton_inter_of_mem {a : α} {s : Finset α} (H : a ∈ s) : {a} ∩ s = {a} :=
  show insert a ∅ ∩ s = insert a ∅ by rw [insert_inter_of_mem H, empty_inter]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∈ s
⊢ insert a ∅ ∩ s = insert a ∅

Tactic:
rw [insert_inter_of_mem H, empty_inter]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma congr_φQ {γ₁ γ₂ : RightHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.φQ = γ₂.φQ

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ₁ γ₂ : RightHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
⊢ γ₁.φQ = γ₂.φQ

Tactic:
rw [eq]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblXYZ_of_Y_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z = Q x * P z) (hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W.negY Q * P z) :
    W.dblXYZ P = W.dblU P • ![0, 1, 0]

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.dblXYZ P = W.dblU P • ![0, 1, 0]

Tactic:
erw [dblXYZ, dblX_of_Y_eq hP hPz hQz hx hy hy', dblY_of_Y_eq hP hPz hQz hx hy hy',
  dblZ_of_Y_eq hQz hx hy hy', smul_fin3, mul_zero, mul_one]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_zero : √0 = 0

Proof state:
⊢ √0 = 0

Tactic:
simp [Real.sqrt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem length_append (s t : String) : (s ++ t).length = s.length + t.length

Proof state:
s t : String
⊢ (s ++ t).length = s.length + t.length

Tactic:
simp only [length, append, List.length_append]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
    {l : List (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst) :
    (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKey! k' = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
⊢ (insertMany empty l).val.getKey! k' = k

Tactic:
rw [getKey!_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Restrict.lean
theorem AffineSubspace.nonempty_map {E : AffineSubspace k P₁} [Ene : Nonempty E] {φ : P₁ →ᵃ[k] P₂} :
    Nonempty (E.map φ)

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty ↥E
φ : P₁ →ᵃ[k] P₂
⊢ Nonempty ↥(map φ E)

Tactic:
obtain ⟨x, hx⟩ := id Ene

Result:
case intro.mk
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty ↥E
φ : P₁ →ᵃ[k] P₂
x : P₁
hx : x ∈ E
⊢ Nonempty ↥(map φ E)

Proof state:
case intro.mk
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty ↥E
φ : P₁ →ᵃ[k] P₂
x : P₁
hx : x ∈ E
⊢ Nonempty ↥(map φ E)

Tactic:
exact ⟨⟨φ x, AffineSubspace.mem_map.mpr ⟨x, hx, rfl⟩⟩⟩

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem tendsto_coe_infty : Tendsto (↑) (coclosedCompact X) (𝓝 (∞ : OnePoint X))

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Tendsto some (coclosedCompact X) (map some (coclosedCompact X) ⊔ pure ∞)

Tactic:
exact Filter.Tendsto.mono_right tendsto_map le_sup_left

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Tendsto some (coclosedCompact X) (𝓝 ∞)

Tactic:
rw [nhds_infty_eq]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Tendsto some (coclosedCompact X) (map some (coclosedCompact X) ⊔ pure ∞)
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem iUnion_disjUnion (h : Disjoint π₁.iUnion π₂.iUnion) :
    (π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion

Proof state:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion

Tactic:
simp [disjUnion, Prepartition.iUnion, iUnion_or, iUnion_union_distrib]

Result:
no goals
-- Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean
@[to_additive]
lemma subgroup {S : Type*} [SetLike S G] [SubgroupClass S G] {H : S} :
    IsApproximateSubgroup 1 (H : Set G) where
  one_mem := OneMemClass.one_mem H
  inv_eq_self := inv_coe_set
  sq_covBySMul := ⟨{1}, by simp⟩

Proof state:
G : Type u_1
inst✝² : Group G
S : Type u_2
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
H : S
⊢ ↑(#{1}) ≤ 1 ∧ ↑H ^ 2 ⊆ ↑{1} • ↑H

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/CompactOpen.lean
theorem isInducing_postcomp (g : C(Y, Z)) (hg : IsInducing g) :
    IsInducing (g.comp : C(X, Y) → C(X, Z)) where
  eq_induced

Proof state:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : C(Y, Z)
hg : IsInducing ⇑g
⊢ compactOpen = induced g.comp compactOpen

Tactic:
simp only [compactOpen_eq, induced_generateFrom_eq, image_image2, hg.setOf_isOpen,
  image2_image_right, MapsTo, mem_preimage, preimage_setOf_eq, comp_apply]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
/-- The function `fun x ↦ f x / r` tends to infinity along a nontrivial filter
if and only if `r > 0` and `f` tends to infinity or `r < 0` and `f` tends to negative infinity. -/
lemma tendsto_div_const_atTop_iff [NeBot l] :
    Tendsto (fun x ↦ f x / r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
⊢ Tendsto (fun x => f x / r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atTop_iff]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_im_symm (x y : E) : im ⟪x, y⟫ = -im ⟪y, x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ im ⟪x, y⟫_𝕜 = -im ⟪y, x⟫_𝕜

Tactic:
rw [← inner_conj_symm, conj_im]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `div_self` for the version with equality when `a ≠ 0`. -/
lemma div_self_le_one (a : G₀) : a / a ≤ 1

Proof state:
G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
⊢ a / a ≤ 1

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi_div_two_sub (x : ℝ) : sin (π / 2 - x) = cos x

Proof state:
x : ℝ
⊢ sin (π / 2 - x) = cos x

Tactic:
simp [sub_eq_add_neg, sin_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_push (a b : α) (l : Array α) :
    count a (l.push b) = count a l + if b == a then 1 else 0

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : Array α
⊢ count a (l.push b) = count a l + if (b == a) = true then 1 else 0

Tactic:
simp [count, countP_push]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertEntryIfNew_of_containsKey [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k}
    (h : containsKey k l) : insertEntryIfNew k v l = l

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = true
⊢ insertEntryIfNew k v l = l

Tactic:
simp_all [insertEntryIfNew]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem term_ord_aux {i : I} (ho : ord I i < Ordinal.type ((· < ·) : I → I → Prop)) :
    term I ho = i

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
i : I
ho : ord I i < Ordinal.type fun x1 x2 => x1 < x2
⊢ term I ho = i

Tactic:
simp only [term, ord, Ordinal.enum_typein]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_shiftConcat (x : BitVec w) (b : Bool) (i : Nat) :
    (shiftConcat x b).getLsbD i
    = (decide (i < w) && (if (i = 0) then b else x.getLsbD (i - 1)))

Proof state:
w : Nat
x : BitVec w
b : Bool
i : Nat
⊢ (x.shiftConcat b).getLsbD i = (decide (i < w) && if i = 0 then b else x.getLsbD (i - 1))

Tactic:
simp only [shiftConcat, getLsbD_setWidth, getLsbD_concat]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Hom.lean
@[to_additive]
lemma inverse_eq_inverse' (f : X →[M] Y₁) (g : Y₁ → X)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
  inverse f g h₁ h₂ =  inverse' f g (congrFun rfl) h₁ h₂

Proof state:
M : Type u_2
X : Type u_5
inst✝¹ : SMul M X
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[id] Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ f.inverse g h₁ h₂ = f.inverse' g ⋯ h₁ h₂

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Module/Projective.lean
theorem projective_def' :
    Projective R P ↔ ∃ s : P →ₗ[R] P →₀ R, Finsupp.linearCombination R id ∘ₗ s = .id

Proof state:
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
⊢ Projective R P ↔ ∃ s, linearCombination R id ∘ₗ s = LinearMap.id

Tactic:
simp_rw [projective_def, DFunLike.ext_iff, Function.LeftInverse, comp_apply, id_apply]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma eq_sub_of_add_eq (h : c + b = a) : c = a - b

Proof state:
a b c : ℕ
h : c + b = a
⊢ c = a - b

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_X_add_C (r : R) : roots (X + C r) = {-r}

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ (X + C r).roots = {-r}

Tactic:
simpa using roots_X_sub_C (-r)

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
@[simp] lemma hasLineDerivWithinAt_univ :
    HasLineDerivWithinAt 𝕜 f f' univ x v ↔ HasLineDerivAt 𝕜 f f' x v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
f' : F
x v : E
⊢ HasLineDerivWithinAt 𝕜 f f' univ x v ↔ HasLineDerivAt 𝕜 f f' x v

Tactic:
simp only [HasLineDerivWithinAt, HasLineDerivAt, preimage_univ, hasDerivWithinAt_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem min?_cons [Min α] [Std.Associative (min : α → α → α)] {xs : List α} :
    (x :: xs).min? = some (xs.min?.elim x (min x))

Proof state:
α : Type u_1
x : α
inst✝¹ : Min α
inst✝ : Std.Associative min
xs : List α
⊢ (x :: xs).min? = some (xs.min?.elim x (min x))

Tactic:
cases xs <;> simp [min?_cons', foldl_assoc]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_injective {n : ℕ} (hn : 0 < n) : Function.Injective (expand R n) := fun g g' H =>
  ext fun k => by rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
hn : 0 < n
g g' : R[X]
H : (expand R n) g = (expand R n) g'
k : ℕ
⊢ g.coeff k = g'.coeff k

Tactic:
rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
theorem IsSymmetric.restrictScalars {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :
    letI := InnerProductSpace.rclikeToReal 𝕜 E
    letI : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower _ _ _
    (T.restrictScalars ℝ).IsSymmetric :=
  fun x y => by simp [hT x y, real_inner_eq_re_inner, LinearMap.coe_restrictScalars ℝ]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
⊢ inner ((↑ℝ T) x) y = inner x ((↑ℝ T) y)

Tactic:
simp [hT x y, real_inner_eq_re_inner, LinearMap.coe_restrictScalars ℝ]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma succAbove_zero_apply (i : Fin n) : succAbove 0 i = succ i

Proof state:
n : ℕ
i : Fin n
⊢ succAbove 0 i = i.succ

Tactic:
rw [succAbove_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma singleObjHomologySelfIso_inv_naturality :
    (singleObjHomologySelfIso c j A).inv ≫ homologyMap ((single C c j).map f) j =
      f ≫ (singleObjHomologySelfIso c j B).inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjHomologySelfIso c j A).inv ≫ homologyMap ((single C c j).map f) j = f ≫ (singleObjHomologySelfIso c j B).inv

Tactic:
rw [← cancel_mono (singleObjHomologySelfIso c j B).hom, assoc, assoc,
  singleObjHomologySelfIso_hom_naturality,
  Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem bind_apply {m : Measure α} {f : α → Measure β} {s : Set β} (hs : MeasurableSet s)
    (hf : Measurable f) : bind m f s = ∫⁻ a, f a s ∂m

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : Measurable f
⊢ (m.bind f) s = ∫⁻ (a : α), (f a) s ∂m

Tactic:
rw [bind, join_apply hs, lintegral_map (measurable_coe hs) hf]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/MulOpposite.lean
theorem op_normalizer (H : Subgroup G) : H.normalizer.op = H.op.normalizer

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ H.normalizer.op = H.op.normalizer

Tactic:
ext x

Result:
case h
G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ x ∈ H.normalizer.op ↔ x ∈ H.op.normalizer

Proof state:
case h
G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ x ∈ H.normalizer.op ↔ x ∈ H.op.normalizer

Tactic:
simp [mem_normalizer_iff', MulOpposite.op_surjective.forall, iff_comm]

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem coeff_frobenius (f : Ring.Perfection R p) (n : ℕ) :
    coeff R p (n + 1) (frobenius _ p f) = coeff R p n f

Proof state:
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Ring.Perfection R p
n : ℕ
⊢ (coeff R p (n + 1)) ((frobenius (Ring.Perfection R p) p) f) = (coeff R p n) f

Tactic:
apply coeff_pow_p f n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem cons_merge_cons_neg (s : α → α → Bool) (l r) (h : ¬ s a b) :
    merge (a::l) (b::r) s = b :: merge (a::l) r s

Proof state:
α : Type u_1
a b : α
s : α → α → Bool
l r : List α
h : ¬s a b = true
⊢ (a :: l).merge (b :: r) s = b :: (a :: l).merge r s

Tactic:
rw [cons_merge_cons, if_neg h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem?_setWidth' (x : BitVec w) (i : Nat) (h : w ≤ v) :
    (setWidth' h x)[i]? = if i < v then some (x.getLsbD i) else none

Proof state:
w v : Nat
x : BitVec w
i : Nat
h : w ≤ v
⊢ (setWidth' h x)[i]? = if i < v then some (x.getLsbD i) else none

Tactic:
simp [getElem?_eq, getElem_setWidth']

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.comp_lift {V W X Y : C} [HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) :
    f ≫ prod.lift g h = prod.lift (f ≫ g) (f ≫ h)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryProduct X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ f ≫ lift g h = lift (f ≫ g) (f ≫ h)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
theorem algEquivOfAlgEquiv_mk' (x : R) (y : M) :
    algEquivOfAlgEquiv S Q h H (mk' S x y) =
      mk' Q (h x) ⟨h y, show h y ∈ T from H ▸ Set.mem_image_of_mem h y.2⟩

Proof state:
A : Type u_4
inst✝¹⁴ : CommSemiring A
R : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : Algebra A R
M : Submonoid R
S : Type u_6
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra A S
inst✝⁹ : Algebra R S
inst✝⁸ : IsScalarTower A R S
inst✝⁷ : IsLocalization M S
P : Type u_7
inst✝⁶ : CommSemiring P
inst✝⁵ : Algebra A P
T : Submonoid P
Q : Type u_8
inst✝⁴ : CommSemiring Q
inst✝³ : Algebra A Q
inst✝² : Algebra P Q
inst✝¹ : IsScalarTower A P Q
inst✝ : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x : R
y : ↥M
⊢ (algEquivOfAlgEquiv S Q h H) (mk' S x y) = mk' Q (h x) ⟨h ↑y, ⋯⟩

Tactic:
simp [map_mk']

Result:
no goals