harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/Primrec.lean
theorem vec_iff {m n f} : @Vec m n f ↔ Primrec f :=
  ⟨fun h => by simpa using Primrec.vector_ofFn fun i => to_prim (h i), fun h i =>
    of_prim <| Primrec.vector_get.comp h (.const i)⟩

Proof state:
m n : ℕ
f : List.Vector ℕ m → List.Vector ℕ n
h : Vec f
⊢ Primrec f

Tactic:
simpa using Primrec.vector_ofFn fun i => to_prim (h i)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insert_self [LawfulBEq α] (h : m.1.WF) {k : α} {v : β k} :
    (m.insert k v).get? k = some v

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
v : β k
⊢ (m.insert k v).get? k = some v

Tactic:
simp_to_model [insert] using List.getValueCast?_insertEntry_self

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem mul_left_eq_zero (u : M₀ˣ) {a : M₀} : a * u = 0 ↔ a = 0 :=
  ⟨fun h => by simpa using mul_eq_zero_of_left h ↑u⁻¹, fun h => mul_eq_zero_of_left h u⟩

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : a * ↑u = 0
⊢ a = 0

Tactic:
simpa using mul_eq_zero_of_left h ↑u⁻¹

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem isClosed_image_coe {s : Set X} :
    IsClosed ((↑) '' s : Set (OnePoint X)) ↔ IsClosed s ∧ IsCompact s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed (some '' s) ↔ IsClosed s ∧ IsCompact s

Tactic:
rw [← isOpen_compl_iff, isOpen_compl_image_coe]

Result:
no goals
-- Mathlib/Algebra/Lie/Derivation/AdjointAction.lean
/-- The commutator of a derivation `D` and a derivation of the form `ad x` is `ad (D x)`. -/
lemma lie_der_ad_eq_ad_der (D : LieDerivation R L L) (x : L) : ⁅D, ad R L x⁆ = ad R L (D x)

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
x : L
⊢ ⁅D, (ad R L) x⁆ = (ad R L) (D x)

Tactic:
rw [ad_apply_lieDerivation, ← lie_ad, lie_skew]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem lineMap_le_lineMap_iff_of_lt (h : r < r') : lineMap a b r ≤ lineMap a b r' ↔ a ≤ b

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : r < r'
⊢ (lineMap a b) r ≤ (lineMap a b) r' ↔ a ≤ b

Tactic:
simp only [lineMap_apply_module]

Result:
k : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : r < r'
⊢ (1 - r) • a + r • b ≤ (1 - r') • a + r' • b ↔ a ≤ b

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : r < r'
⊢ (1 - r) • a + r • b ≤ (1 - r') • a + r' • b ↔ a ≤ b

Tactic:
rw [← le_sub_iff_add_le, add_sub_assoc, ← sub_le_iff_le_add', ← sub_smul, ← sub_smul,
  sub_sub_sub_cancel_left, smul_le_smul_iff_of_pos_left (sub_pos.2 h)]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Basic.lean
theorem dvd_of_eq (h : a = b) : a ∣ b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
h : a = b
⊢ a ∣ b

Tactic:
rw [h]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem scaleRoots_eval₂_eq_zero {p : S[X]} (f : S →+* R) {r : R} {s : S} (hr : eval₂ f r p = 0) :
    eval₂ f (f s * r) (scaleRoots p s) = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring S
inst✝ : CommSemiring R
p : S[X]
f : S →+* R
r : R
s : S
hr : eval₂ f r p = 0
⊢ eval₂ f (f s * r) (p.scaleRoots s) = 0

Tactic:
rw [scaleRoots_eval₂_mul, hr, mul_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem ContinuousLinearEquiv.integrable_comp_iff {φ : α → H} (L : H ≃L[𝕜] E) :
    Integrable (fun a : α ↦ L (φ a)) μ ↔ Integrable φ μ :=
  ⟨fun h ↦ by simpa using ContinuousLinearMap.integrable_comp (L.symm : E →L[𝕜] H) h,
  fun h ↦ ContinuousLinearMap.integrable_comp (L : H →L[𝕜] E) h⟩

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_7
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
φ : α → H
L : H ≃L[𝕜] E
h : Integrable (fun a => L (φ a)) μ
⊢ Integrable φ μ

Tactic:
simpa using ContinuousLinearMap.integrable_comp (L.symm : E →L[𝕜] H) h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_eq_singleton_iff {l : Vector α 1} {f : Nat → α → β} {b : β} :
    mapIdx f l = #v[b] ↔ ∃ (a : α), l = #v[a] ∧ f 0 a = b

Proof state:
α : Type u_1
β : Type u_2
l : Vector α 1
f : Nat → α → β
b : β
⊢ mapIdx f l = { toArray := #[b], size_toArray := ⋯ } ↔ ∃ a, l = { toArray := #[a], size_toArray := ⋯ } ∧ f 0 a = b

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
b : β
l : Array α
size_toArray✝ : l.size = 1
⊢ mapIdx f { toArray := l, size_toArray := size_toArray✝ } = { toArray := #[b], size_toArray := ⋯ } ↔
    ∃ a, { toArray := l, size_toArray := size_toArray✝ } = { toArray := #[a], size_toArray := ⋯ } ∧ f 0 a = b

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
b : β
l : Array α
size_toArray✝ : l.size = 1
⊢ mapIdx f { toArray := l, size_toArray := size_toArray✝ } = { toArray := #[b], size_toArray := ⋯ } ↔
    ∃ a, { toArray := l, size_toArray := size_toArray✝ } = { toArray := #[a], size_toArray := ⋯ } ∧ f 0 a = b

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
theorem inner_map_complex [SeminormedAddCommGroup G] [InnerProductSpace ℝ G] (f : G ≃ₗᵢ[ℝ] ℂ)
    (x y : G) : ⟪x, y⟫_ℝ = (conj (f x) * f y).re

Proof state:
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
f : G ≃ₗᵢ[ℝ] ℂ
x y : G
⊢ ⟪x, y⟫_ℝ = ((starRingEnd ℂ) (f x) * f y).re

Tactic:
rw [← Complex.inner, f.inner_map_map]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_lt_of_neg (ha : a < 0) (hb : b < 0) : 1 / a < b ↔ 1 / b < a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
ha : a < 0
hb : b < 0
⊢ 1 / a < b ↔ 1 / b < a

Tactic:
simpa using inv_lt_of_neg ha hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[]

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → m β
⊢ mapM f #[] = pure #[]

Tactic:
rw [mapM, mapM.map]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → m β
⊢ (if hlt : 0 < #[].size then do
      let __do_lift ← f #[][0]
      mapM.map f #[] (0 + 1) ((mkEmpty #[].size).push __do_lift)
    else pure (mkEmpty #[].size)) =
    pure #[]

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → m β
⊢ (if hlt : 0 < #[].size then do
      let __do_lift ← f #[][0]
      mapM.map f #[] (0 + 1) ((mkEmpty #[].size).push __do_lift)
    else pure (mkEmpty #[].size)) =
    pure #[]

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Single.lean
@[reassoc (attr := simp)]
lemma singleObjApplyIso_inv_single_map (j : J) {X Y : C} (f : X ⟶ Y) :
    (singleObjApplyIso j X).inv ≫ (single j).map f j = f ≫ (singleObjApplyIso j Y).inv

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
j : J
X Y : C
f : X ⟶ Y
⊢ (singleObjApplyIso j X).inv ≫ (single j).map f j = f ≫ (singleObjApplyIso j Y).inv

Tactic:
apply singleObjApplyIsoOfEq_inv_single_map

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_preimage_inter (f : α → β) (s : Set α) (t : Set β) :
    f '' (f ⁻¹' t ∩ s) = t ∩ f '' s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (f ⁻¹' t ∩ s) = t ∩ f '' s

Tactic:
simp only [inter_comm, image_inter_preimage]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem setParent_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
    (h : arr[x.1].rank < arr[y.1].rank) {i : Nat}
    (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)) :
    let arr' := arr.set x ⟨y, arr[x].rank⟩
    parentD arr' i ≠ i → rankD arr' i < rankD arr' (parentD arr' i) :=
  setParentBump_rankD_lt (.inl h) (Nat.le_of_lt h) rankD_lt parentD_set
    (by simp [rankD_set, Nat.ne_of_lt h, rankD_eq, -Array.get_eq_getElem])

Proof state:
arr : Array UFNode
x y : Fin arr.size
h : arr[↑x].rank < arr[↑y].rank
i : Nat
rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)
⊢ ∀ {i : Nat},
    rankD (arr.set ↑x { parent := ↑y, rank := arr[x].rank } ⋯) i =
      if ↑y = i ∧ arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else rankD arr i

Tactic:
simp [rankD_set, Nat.ne_of_lt h, rankD_eq, -Array.get_eq_getElem]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ico_pred_right_eq_insert (h : a ≤ b) : Ioc (pred a) b = insert a (Ioc a b)

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
h : a ≤ b
⊢ Ioc (pred a) b = insert a (Ioc a b)

Tactic:
simp_rw [← Ioi_inter_Iic, Ioi_pred_eq_insert, insert_inter_of_mem (mem_Iic.2 h)]

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

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝ : LawfulBEq α
h : m.val.WF
a : α
⊢ get? m a = m.get? a

Tactic:
simp_to_model using List.getValue?_eq_getValueCast?

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bot_symmDiff : ⊥ ∆ a = a

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ ⊥ ∆ a = a

Tactic:
rw [symmDiff_comm, symmDiff_bot]

Result:
no goals
-- Mathlib/Topology/UrysohnsLemma.lean
theorem lim_of_nmem_U (c : CU P) (x : X) (h : x ∉ c.U) : c.lim x = 1

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
x : X
h : x ∉ c.U
⊢ c.lim x = 1

Tactic:
simp only [CU.lim, approx_of_nmem_U c _ h, ciSup_const]

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

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
k : α
v : β
⊢ getValue! k (insertEntry k v l) = v

Tactic:
simp [getValue!_insertEntry, BEq.refl]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem HasDerivAtFilter.add (hf : HasDerivAtFilter f f' x L)
    (hg : HasDerivAtFilter g g' x L) : HasDerivAtFilter (fun y => f y + g y) (f' + g') x L

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
f' g' : F
x : 𝕜
L : Filter 𝕜
hf : HasDerivAtFilter f f' x L
hg : HasDerivAtFilter g g' x L
⊢ HasDerivAtFilter (fun y => f y + g y) (f' + g') x L

Tactic:
simpa using (hf.add hg).hasDerivAtFilter

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem tensor_zero {W X Y Z : C} (f : W ⟶ X) : f ⊗ (0 : Y ⟶ Z) = 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
W X Y Z : C
f : W ⟶ X
⊢ f ⊗ 0 = 0

Tactic:
simp [tensorHom_def]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_insert_div {M : Type*} [CommGroup M] [DecidableEq α] (ha : a ∉ s) {f : α → M} :
    (∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x

Proof state:
α : Type u_3
s : Finset α
a : α
M : Type u_6
inst✝¹ : CommGroup M
inst✝ : DecidableEq α
ha : a ∉ s
f : α → M
⊢ (∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_mul_expect [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (s : Finset ι)
    (t : Finset κ) (f : ι → M) (g : κ → M) :
    (𝔼 i ∈ s, f i) * 𝔼 j ∈ t, g j = 𝔼 i ∈ s, 𝔼 j ∈ t, f i * g j

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝³ : Semiring M
inst✝² : Module ℚ≥0 M
inst✝¹ : IsScalarTower ℚ≥0 M M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
⊢ (𝔼 i ∈ s, f i) * 𝔼 j ∈ t, g j = 𝔼 i ∈ s, 𝔼 j ∈ t, f i * g j

Tactic:
simp_rw [expect_mul, mul_expect]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem norm_def (f : α →₁[μ] β) : ‖f‖ = (∫⁻ a, ‖f a‖ₑ ∂μ).toReal

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ ‖f‖ = (∫⁻ (a : α), ‖↑↑f a‖ₑ ∂μ).toReal

Tactic:
simp [Lp.norm_def, eLpNorm, eLpNorm'_eq_lintegral_enorm]

Result:
no goals
-- Mathlib/Computability/NFA.lean
theorem evalFrom_append_singleton (S : Set σ) (x : List α) (a : α) :
    M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a

Proof state:
α : Type u
σ : Type v
M : NFA α σ
S : Set σ
x : List α
a : α
⊢ M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a

Tactic:
simp only [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleNumber.lean
theorem remainder_pos {m : ℝ} (hm : 1 < m) (k : ℕ) : 0 < remainder m k :=
  tsum_pos (remainder_summable hm k) (fun _ => by positivity) 0 (by positivity)

Proof state:
m : ℝ
hm : 1 < m
k x✝ : ℕ
⊢ 0 ≤ 1 / m ^ (x✝ + (k + 1))!

Tactic:
positivity

Result:
no goals

Proof state:
m : ℝ
hm : 1 < m
k : ℕ
⊢ 0 < 1 / m ^ (0 + (k + 1))!

Tactic:
positivity

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem eq_rotation_self_iff (x : V) (θ : Real.Angle) : x = o.rotation θ x ↔ x = 0 ∨ θ = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
θ : Real.Angle
⊢ x = (o.rotation θ) x ↔ x = 0 ∨ θ = 0

Tactic:
rw [← rotation_eq_self_iff, eq_comm]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem eq_spanSingleton_of_principal (I : FractionalIdeal S P) [IsPrincipal (I : Submodule R P)] :
    I = spanSingleton S (generator (I : Submodule R P))

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
inst✝¹ : IsLocalization S P
I : FractionalIdeal S P
inst✝ : (↑I).IsPrincipal
⊢ I = spanSingleton S (generator ↑I)

Tactic:
rw [spanSingleton, ← coeToSubmodule_inj, coe_mk, span_singleton_generator]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_const_on_unit_interval : ∫ _ in a..a + 1, b = b

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..a + 1, b = b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem sym_nonempty : (s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ (s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty

Tactic:
simp only [nonempty_iff_ne_empty, ne_eq, sym_eq_empty, not_and_or, not_ne_iff]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem two_mul_C_half_eq_one [Invertible (2 : R)] : 2 * C (⅟ 2 : R) = 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ 2 * C ⅟2 = 1

Tactic:
rw [two_mul, ← C_add, invOf_two_add_invOf_two, C_1]

Result:
no goals
-- Mathlib/Computability/Reduce.lean
theorem oneOneReducible_refl {α} [Primcodable α] (p : α → Prop) : p ≤₁ p :=
  ⟨id, Computable.id, injective_id, by simp⟩

Proof state:
α : Type u_1
inst✝ : Primcodable α
p : α → Prop
⊢ ∀ (a : α), p a ↔ p (id a)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem Q_is_eventually_constant {q n : ℕ} (hqn : n ≤ q) :
    ((Q (q + 1)).f n : X _⦋n⦌ ⟶ _) = (Q q).f n

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n ≤ q
⊢ (Q (q + 1)).f n = (Q q).f n

Tactic:
simp only [Q, HomologicalComplex.sub_f_apply, P_is_eventually_constant hqn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_fmod_right (a b : Int) : (a * b).fmod a = 0

Proof state:
a b : Int
⊢ (a * b).fmod a = 0

Tactic:
rw [Int.mul_comm, mul_fmod_left]

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem rightHom_inr (g : G) : rightHom (inr g : N ⋊[φ] G) = g

Proof state:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
⊢ rightHom (inr g) = g

Tactic:
simp [rightHom]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem nonempty_Ico : (Ico a b).Nonempty ↔ a < b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ (Ico a b).Nonempty ↔ a < b

Tactic:
rw [← coe_nonempty, coe_Ico, Set.nonempty_Ico]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem toFinset_nonempty_iff (l : List α) : l.toFinset.Nonempty ↔ l ≠ []

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.toFinset.Nonempty ↔ l ≠ []

Tactic:
simp [Finset.nonempty_iff_ne_empty]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Submodule.le_of_localization_maximal {N₁ N₂ : Submodule R M}
    (h : ∀ (P : Ideal R) [P.IsMaximal],
      N₁.localized₀ P.primeCompl (f P) ≤ N₂.localized₀ P.primeCompl (f P)) :
    N₁ ≤ N₂ :=
  fun m hm ↦ mem_of_localization_maximal _ f _ _ fun P hP ↦ h P ⟨m, hm, 1, by simp⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
N₁ N₂ : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], localized₀ P.primeCompl (f P) N₁ ≤ localized₀ P.primeCompl (f P) N₂
m : M
hm : m ∈ N₁
P : Ideal R
hP : P.IsMaximal
⊢ IsLocalizedModule.mk' (f P) m 1 = (f P) m

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma μ_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) :
    F.map f ▷ F.obj X' ≫ μ F Y X' = μ F X X' ≫ F.map (f ▷ X')

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y : C
f : X ⟶ Y
X' : C
⊢ F.map f ▷ F.obj X' ≫ μ F Y X' = μ F X X' ≫ F.map (f ▷ X')

Tactic:
apply μ'_natural_left

Result:
no goals
-- Mathlib/MeasureTheory/Covering/VitaliFamily.lean
theorem mem_filterAt_iff {x : X} {s : Set (Set X)} :
    s ∈ v.filterAt x ↔ ∃ ε > (0 : ℝ), ∀ t ∈ v.setsAt x, t ⊆ closedBall x ε → t ∈ s

Proof state:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
s : Set (Set X)
⊢ s ∈ v.filterAt x ↔ ∃ ε > 0, ∀ t ∈ v.setsAt x, t ⊆ closedBall x ε → t ∈ s

Tactic:
simp only [(v.filterAt_basis_closedBall x).mem_iff, ← and_imp, subset_def, mem_setOf]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem pushoutIsoUnopPullback_inr_hom {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g]
    [HasPullback f.op g.op] :
    pushout.inr _ _ ≫ (pushoutIsoUnopPullback f g).hom = (pullback.snd f.op g.op).unop :=
  (IsColimit.comp_coconePointUniqueUpToIso_hom _ _ _).trans (by simp)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ (PullbackCone.unop (limit.cone (cospan f.op g.op))).ι.app WalkingSpan.right = (pullback.snd f.op g.op).unop

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_update_same (p : R[X]) (n : ℕ) (a : R) : (p.update n a).coeff n = a

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).coeff n = a

Tactic:
rw [p.coeff_update_apply, if_pos rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_pos_iff {p} : 0 < countP p l ↔ ∃ a ∈ l, p a

Proof state:
α✝ : Type u_1
l : List α✝
p : α✝ → Bool
⊢ 0 < countP p l ↔ ∃ a, a ∈ l ∧ p a = true

Tactic:
simp only [countP_eq_length_filter, length_pos_iff_exists_mem, mem_filter, exists_prop]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_eq_zero_iff {θ : Angle} : θ.sign = 0 ↔ θ = 0 ∨ θ = π

Proof state:
θ : Angle
⊢ θ.sign = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
rw [sign, _root_.sign_eq_zero_iff, sin_eq_zero_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem cramer_transpose_apply (i : n) : cramer Aᵀ b i = (A.updateRow i b).det

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
⊢ Aᵀ.cramer b i = (A.updateRow i b).det

Tactic:
rw [cramer_apply, updateCol_transpose, det_transpose]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε :=
  ⟨_, sub_pos.2 h, ball_subset <| by rw [sub_sub_self]⟩

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : y ∈ ball x ε
⊢ dist y x ≤ ε - (ε - dist y x)

Tactic:
rw [sub_sub_self]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem isUnit_nonsing_inv_det_iff {A : Matrix n n α} : IsUnit A⁻¹.det ↔ IsUnit A.det

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ IsUnit A⁻¹.det ↔ IsUnit A.det

Tactic:
rw [Matrix.det_nonsing_inv, isUnit_ring_inverse]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem mem_supported_support (p : α →₀ M) : p ∈ Finsupp.supported M R (p.support : Set α)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : α →₀ M
⊢ p ∈ supported M R ↑p.support

Tactic:
rw [Finsupp.mem_supported]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_replicate {n : Nat} {a : α} :
    (replicate n a).all f = if n = 0 then true else f a

Proof state:
α : Type u_1
f : α → Bool
n : Nat
a : α
⊢ (replicate n a).all f = if n = 0 then true else f a

Tactic:
cases n <;> simp +contextual [replicate_succ]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem image_mul_left : (a * ·) '' t = (a⁻¹ * ·) ⁻¹' t

Proof state:
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x => a * x) '' t = (fun x => a⁻¹ * x) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse] <;> intro c <;> simp

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem edist_of_im_eq {z w : ℂ} (h : z.im = w.im) : edist z w = edist z.re w.re

Proof state:
z w : ℂ
h : z.im = w.im
⊢ edist z w = edist z.re w.re

Tactic:
rw [edist_nndist, edist_nndist, nndist_of_im_eq h]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Instances.lean
theorem one_minus_pos (x : Ioo (0 : β) 1) : 0 < 1 - (x : β)

Proof state:
β : Type u_2
inst✝ : OrderedRing β
x : ↑(Ioo 0 1)
⊢ 0 < 1 - ↑x

Tactic:
simpa using x.2.2

Result:
no goals
-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
@[reassoc]
lemma homMap_comp (f : L₁.obj X ⟶ L₁.obj Y) (g : L₁.obj Y ⟶ L₁.obj Z) :
    Φ.homMap L₁ L₂ (f ≫ g) = Φ.homMap L₁ L₂ f ≫ Φ.homMap L₁ L₂ g

Proof state:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{u_9, u_2} C₁
inst✝⁴ : Category.{u_11, u_3} C₂
inst✝³ : Category.{u_8, u_5} D₁
inst✝² : Category.{u_10, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y Z : C₁
f : L₁.obj X ⟶ L₁.obj Y
g : L₁.obj Y ⟶ L₁.obj Z
⊢ Φ.homMap L₁ L₂ (f ≫ g) = Φ.homMap L₁ L₂ f ≫ Φ.homMap L₁ L₂ g

Tactic:
simp [homMap]

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
nonrec lemma StrongConvexOn.mono (hmn : m ≤ n) (hf : StrongConvexOn s n f) : StrongConvexOn s m f :=
  hf.mono fun r ↦ by gcongr

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
f : E → ℝ
m n : ℝ
hmn : m ≤ n
hf : StrongConvexOn s n f
r : ℝ
⊢ m / 2 * r ^ 2 ≤ n / 2 * r ^ 2

Tactic:
gcongr

Result:
no goals