harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Group/Integral.lean
theorem integral_div_right_eq_self [IsMulRightInvariant μ] (f : G → E) (g : G) :
    (∫ x, f (x / g) ∂μ) = ∫ x, f x ∂μ

Proof state:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → E
g : G
⊢ ∫ (x : G), f (x / g) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
simp_rw [div_eq_mul_inv, integral_mul_right_eq_self f g⁻¹]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_add_left (a b : α) : toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1

Tactic:
rw [add_comm, toIcoDiv_add_right]

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp)]
lemma mulConst_empty_right (A : Finset G) : σₘ[A, ∅] = 0

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
⊢ σₘ[A, ∅] = 0

Tactic:
simp [mulConst]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
@[simp]
lemma pairing_reflection_perm_self_left (P : RootPairing ι R M N) (i j : ι) :
    P.pairing (P.reflection_perm i i) j = - P.pairing i j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.pairing ((P.reflection_perm i) i) j = -P.pairing i j

Tactic:
rw [pairing, root', ← reflection_perm_root, root'_coroot_eq_pairing, pairing_same, two_smul,
  sub_add_cancel_left, ← toLin_toPerfectPairing, LinearMap.map_neg₂, toLin_toPerfectPairing,
  root'_coroot_eq_pairing]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem trailingDegree_C_mul_X_pow (n : ℕ) (ha : a ≠ 0) : trailingDegree (C a * X ^ n) = n

Proof state:
R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ (C a * X ^ n).trailingDegree = ↑n

Tactic:
rw [C_mul_X_pow_eq_monomial, trailingDegree_monomial ha]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem denom_one : denom (1 : RatFunc K) = 1

Proof state:
K : Type u
inst✝ : Field K
⊢ denom 1 = 1

Tactic:
convert denom_div (1 : K[X]) one_ne_zero <;> simp

Result:
no goals
-- Mathlib/RingTheory/Noetherian/Defs.lean
theorem set_has_maximal_iff_noetherian :
    (∀ a : Set <| Submodule R M, a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M

Tactic:
rw [isNoetherian_iff, WellFounded.wellFounded_iff_has_min]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[simp] lemma ofEpiOfIsIsoOfMono_g' : (ofEpiOfIsIsoOfMono φ h).g' = h.g' ≫ φ.τ₃

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
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono φ h).g' = h.g' ≫ φ.τ₃

Tactic:
simp [ofEpiOfIsIsoOfMono, opMap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
    arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp)

Proof state:
α : Type u_1
arr : Array α
a : α
l : List α
⊢ (arr ++ a :: l).toList = (arr.push a ++ l).toList

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem cardinal_le_rank {ι : Type v} {v : ι → M}
    (hv : LinearIndependent R v) : #ι ≤ Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type v
v : ι → M
hv : LinearIndependent R v
⊢ #ι ≤ Module.rank R M

Tactic:
simpa using hv.cardinal_lift_le_rank

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_sum_measure {m : MeasurableSpace α} {ι} (f : α → ℝ≥0∞) (μ : ι → Measure α) :
    ∫⁻ a, f a ∂Measure.sum μ = ∑' i, ∫⁻ a, f a ∂μ i

Proof state:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
f : α → ℝ≥0∞
μ : ι → Measure α
⊢ ∫⁻ (a : α), f a ∂Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_sum, ← lintegral_finset_sum_measure,
  lintegral, SimpleFunc.lintegral_sum, ENNReal.tsum_eq_iSup_sum,
  SimpleFunc.lintegral_finset_sum, iSup_comm (ι := Finset ι)]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ioc_sub_one_left_eq_Icc_of_not_isMin (ha : ¬ IsMin a) (b : α) : Ioc (a - 1) b = Icc a b

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc_of_not_isMin ha b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem bind_congr [Bind m] {x : m α} {f g : α → m β} (h : ∀ a, f a = g a) : x >>= f = x >>= g

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝ : Bind m
x : m α
f g : α → m β
h : ∀ (a : α), f a = g a
⊢ x >>= f = x >>= g

Tactic:
simp [funext h]

Result:
no goals
-- Mathlib/CategoryTheory/EssentiallySmall.lean
theorem essentiallySmall_iff_of_thin {C : Type u} [Category.{v} C] [Quiver.IsThin C] :
    EssentiallySmall.{w} C ↔ Small.{w} (Skeleton C)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
⊢ EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (Skeleton C)

Tactic:
simp [essentiallySmall_iff, CategoryTheory.locallySmall_of_thin]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem edges_reverse {u v : V} (p : G.Walk u v) : p.reverse.edges = p.edges.reverse

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.edges = p.edges.reverse

Tactic:
simp [edges, List.map_reverse]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
theorem sat_iff_exists [Clause α β] (p : α → Bool) (c : β) : p ⊨ c ↔ ∃ l ∈ toList c, p ⊨ l

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Clause α β
p : α → Bool
c : β
⊢ (List.any (toList c) fun l => decide (p l.fst = l.snd)) = true ↔ ∃ l, l ∈ toList c ∧ p l.fst = l.snd

Tactic:
simp only [List.any_eq_true, decide_eq_true_eq, Prod.exists, Bool.exists_bool]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
theorem hσ'_eq' {q n a : ℕ} (ha : n = a + q) :
    (hσ' q n (n + 1) rfl : X _⦋n⦌ ⟶ X _⦋n + 1⦌) =
      (-1 : ℤ) ^ a • X.σ ⟨a, Nat.lt_succ_iff.mpr (Nat.le.intro (Eq.symm ha))⟩

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a : ℕ
ha : n = a + q
⊢ hσ' q n (n + 1) ⋯ = (-1) ^ a • X.σ ⟨a, ⋯⟩

Tactic:
rw [hσ'_eq ha rfl, eqToHom_refl, comp_id]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.isBasis (h : l.HasBasis p s) : IsBasis p s where
  nonempty := h.ex_mem
  inter hi hj

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
i✝ j✝ : ι
hi : p i✝
hj : p j✝
⊢ ∃ k, p k ∧ s k ⊆ s i✝ ∩ s j✝

Tactic:
simpa only [h.mem_iff] using inter_mem (h.mem_of_mem hi) (h.mem_of_mem hj)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem T_mul_apply_one (g : SL(2, ℤ)) : (T * g) 1 = g 1

Proof state:
g : SL(2, ℤ)
⊢ ↑(T * g) 1 = ↑g 1

Tactic:
simpa using T_pow_mul_apply_one 1 g

Result:
no goals
-- Mathlib/Analysis/Convex/Extreme.lean
theorem isExtreme_sInter {F : Set (Set E)} (hF : F.Nonempty) (hAF : ∀ B ∈ F, IsExtreme 𝕜 A B) :
    IsExtreme 𝕜 A (⋂₀ F)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
F : Set (Set E)
hF : F.Nonempty
hAF : ∀ B ∈ F, IsExtreme 𝕜 A B
⊢ IsExtreme 𝕜 A (⋂₀ F)

Tactic:
simpa [sInter_eq_biInter] using isExtreme_biInter hF hAF

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma val_inv_mul (hmn : m.Coprime n) : ((m⁻¹ : ZMod n).val * m : ZMod n) = 1

Proof state:
m n : ℕ
hmn : m.Coprime n
⊢ ↑(↑m)⁻¹.val * ↑m = 1

Tactic:
rw [mul_comm, mul_val_inv hmn]

Result:
no goals
-- Mathlib/Order/Zorn.lean
lemma exists_mem_mem (hab : a ≤ b) : ∃ s : Flag α, a ∈ s ∧ b ∈ s

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a ≤ b
⊢ ∃ s, a ∈ s ∧ b ∈ s

Tactic:
simpa [Set.insert_subset_iff] using (IsChain.pair hab).exists_subset_flag

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem IsCompact.div_closedBall_one (hs : IsCompact s) (hδ : 0 ≤ δ) :
    s / closedBall 1 δ = cthickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s / closedBall 1 δ = cthickening δ s

Tactic:
simp [div_eq_mul_inv, hs.mul_closedBall_one hδ]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem comap_ker (f : S →+* R) (g : T →+* S) : f.ker.comap g = ker (f.comp g)

Proof state:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* R
g : T →+* S
⊢ Ideal.comap g (ker f) = ker (f.comp g)

Tactic:
rw [RingHom.ker_eq_comap_bot, Ideal.comap_comap, RingHom.ker_eq_comap_bot]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem self_mem_span_image [Nontrivial R] {i : ι} {s : Set ι} :
    b i ∈ span R (b '' s) ↔ i ∈ s

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Nontrivial R
i : ι
s : Set ι
⊢ b i ∈ span R (⇑b '' s) ↔ i ∈ s

Tactic:
simp [mem_span_image, Finsupp.support_single_ne_zero]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_comp_const_mul (r : R) (f : R → R) (a : A)
    (hf : ContinuousOn f ((r * ·) '' (spectrum R a))

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
r : R
f : R → R
a : A
hf : autoParam (ContinuousOn f ((fun x => r * x) '' spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f (r * x)) a = cfc f (r • a)

Tactic:
rw [cfc_comp' .., cfc_const_mul_id ..]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem monotone_rpow_of_nonneg {z : ℝ} (h : 0 ≤ z) : Monotone fun x : ℝ≥0 => x ^ z :=
  h.eq_or_lt.elim (fun h0 => h0 ▸ by simp only [rpow_zero, monotone_const]) fun h0 =>
    (strictMono_rpow_of_pos h0).monotone

Proof state:
z : ℝ
h : 0 ≤ z
h0 : 0 = z
⊢ Monotone fun x => x ^ 0

Tactic:
simp only [rpow_zero, monotone_const]

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem projIcc_eq_right (h : a < b) : projIcc a b h.le x = ⟨b, right_mem_Icc.2 h.le⟩ ↔ b ≤ x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b x : α
h : a < b
⊢ projIcc a b ⋯ x = ⟨b, ⋯⟩ ↔ b ≤ x

Tactic:
simp [projIcc, Subtype.ext_iff, max_min_distrib_left, h.le, h.not_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_range {n : Nat} {i : Nat} (h : i < (Array.range n).size) : (Array.range n)[i] = i

Proof state:
n i : Nat
h : i < (range n).size
⊢ (range n)[i] = i

Tactic:
simp [← getElem_toList]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem not_dep_iff (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ¬M.Dep X ↔ M.Indep X

Tactic:
rw [Dep, and_iff_left hX, not_not]

Result:
no goals
-- Mathlib/Algebra/Homology/Single.lean
@[simp]
lemma fromSingle₀Equiv_symm_apply_f_zero {C : CochainComplex V ℕ} {X : V}
    (f : X ⟶ C.X 0) (hf : f ≫ C.d 0 1 = 0) :
    ((fromSingle₀Equiv C X).symm ⟨f, hf⟩).f 0 = f

Proof state:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
hf : f ≫ C.d 0 1 = 0
⊢ ((C.fromSingle₀Equiv X).symm ⟨f, hf⟩).f 0 = f

Tactic:
simp [fromSingle₀Equiv]

Result:
no goals
-- Mathlib/Topology/Category/Compactum.lean
theorem le_nhds_of_str_eq {X : Compactum} (F : Ultrafilter X) (x : X) : X.str F = x → ↑F ≤ 𝓝 x :=
  fun h => le_nhds_iff.mpr fun s hx hs => hs _ <| by rwa [h]

Proof state:
X : Compactum
F : Ultrafilter X.A
x : X.A
h : X.str F = x
s : Set X.A
hx : x ∈ s
hs : IsOpen s
⊢ X.str F ∈ s

Tactic:
rwa [h]

Result:
no goals
-- Mathlib/NumberTheory/Rayleigh.lean
theorem beattySeq'_symmDiff_beattySeq_pos {r s : ℝ} (hrs : r.IsConjExponent s) :
    {beattySeq' r k | k > 0} ∆ {beattySeq s k | k > 0} = {n | 0 < n}

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
⊢ {x | ∃ k > 0, beattySeq' r k = x} ∆ {x | ∃ k > 0, beattySeq s k = x} = {n | 0 < n}

Tactic:
rw [symmDiff_comm, beattySeq_symmDiff_beattySeq'_pos hrs.symm]

Result:
no goals
-- Mathlib/Algebra/Module/NatInt.lean
theorem map_natCast_smul [AddCommMonoid M] [AddCommMonoid M₂] {F : Type*} [FunLike F M M₂]
    [AddMonoidHomClass F M M₂] (f : F) (R S : Type*) [Semiring R] [Semiring S] [Module R M]
    [Module S M₂] (x : ℕ) (a : M) : f ((x : R) • a) = (x : S) • f a

Proof state:
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : ℕ
a : M
⊢ f (↑x • a) = ↑x • f a

Tactic:
simp only [Nat.cast_smul_eq_nsmul, AddMonoidHom.map_nsmul, map_nsmul]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma div_le_div_iff₀ (hb : 0 < b) (hd : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c * b

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
this : MulPosMono G₀
⊢ a / b ≤ c / d ↔ a * d ≤ c * b

Tactic:
rw [div_le_iff₀ hb, ← mul_div_right_comm, le_div_iff₀ hd]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
⊢ a / b ≤ c / d ↔ a * d ≤ c * b

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c d : G₀
hb : 0 < b
hd : 0 < d
this : MulPosMono G₀
⊢ a / b ≤ c / d ↔ a * d ≤ c * b
-- Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
theorem associator_inv_fst_snd (X Y Z : C) :
    (α_ X Y Z).inv ≫ prod.fst ≫ prod.snd = prod.snd ≫ prod.fst

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ prod.fst ≫ prod.snd = prod.snd ≫ prod.fst

Tactic:
simp [associator_inv]

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma even_mul_pred_self (n : ℤ) : Even (n * (n - 1))

Proof state:
n : ℤ
⊢ Even (n * (n - 1))

Tactic:
simpa [even_mul, parity_simps] using n.even_or_odd

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem re_ofReal_mul (r : ℝ) (z : ℂ) : (r * z).re = r * z.re

Proof state:
r : ℝ
z : ℂ
⊢ (↑r * z).re = r * z.re

Tactic:
simp [ofReal]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem one_lt_inv : 1 < a⁻¹ ↔ a < 1

Proof state:
a : ℝ≥0∞
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
rw [lt_inv_iff_lt_inv, inv_one]

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra.lean
theorem _root_.Algebra.adjoin_eq_range_freeAlgebra_lift (s : Set A) :
    Algebra.adjoin R s = (FreeAlgebra.lift R ((↑) : s → A)).range

Proof state:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Algebra.adjoin R s = ((lift R) Subtype.val).range

Tactic:
rw [← Algebra.adjoin_range_eq_range_freeAlgebra_lift, Subtype.range_coe]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem neg_modEq_neg : -a ≡ -b [PMOD p] ↔ a ≡ b [PMOD p] :=
  modEq_comm.trans <| by simp [ModEq, neg_add_eq_sub]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
⊢ -b ≡ -a [PMOD p] ↔ a ≡ b [PMOD p]

Tactic:
simp [ModEq, neg_add_eq_sub]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem vec3_dotProduct' {a₀ a₁ a₂ b₀ b₁ b₂ : α} :
    ![a₀, a₁, a₂] ⬝ᵥ ![b₀, b₁, b₂] = a₀ * b₀ + a₁ * b₁ + a₂ * b₂

Proof state:
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₀ a₁ a₂ b₀ b₁ b₂ : α
⊢ ![a₀, a₁, a₂] ⬝ᵥ ![b₀, b₁, b₂] = a₀ * b₀ + a₁ * b₁ + a₂ * b₂

Tactic:
rw [cons_dotProduct_cons, cons_dotProduct_cons, cons_dotProduct_cons, dotProduct_empty,
  add_zero, add_assoc]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem smul_mem_smul_iff {a : A} {s : R} {r : Rˣ} : r • s ∈ σ (r • a) ↔ s ∈ σ a

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
s : R
r : Rˣ
⊢ r • s ∈ σ (r • a) ↔ s ∈ σ a

Tactic:
simp only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, smul_assoc, ← smul_sub,
  isUnit_smul_iff]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem ULift.isClosed_iff [TopologicalSpace X] {s : Set (ULift.{v} X)} :
    IsClosed s ↔ IsClosed (ULift.up ⁻¹' s)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set (ULift.{v, u} X)
⊢ IsClosed s ↔ IsClosed (up ⁻¹' s)

Tactic:
rw [← isOpen_compl_iff, ← isOpen_compl_iff, isOpen_iff, preimage_compl]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[ext]
lemma leftHomology_ext {A : C} (f₁ f₂ : S.leftHomology ⟶ A)
    (h : S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂) : f₁ = f₂

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
f₁ f₂ : S.leftHomology ⟶ A
h : S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂
⊢ f₁ = f₂

Tactic:
simpa only [leftHomology_ext_iff] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem dvd_sub {k m n : Nat} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n :=
  (Nat.dvd_add_iff_left h₂).2 <| by rwa [Nat.sub_add_cancel H]

Proof state:
k m n : Nat
H : n ≤ m
h₁ : k ∣ m
h₂ : k ∣ n
⊢ k ∣ m - n + n

Tactic:
rwa [Nat.sub_add_cancel H]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_mul_Ioi_of_neg (a : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Ioi a = Iio (a / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a c : α
h : c < 0
⊢ (fun x => c * x) ⁻¹' Ioi a = Iio (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Ioi_of_neg a h

Result:
no goals
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusIntegral_sub (hf : TorusIntegrable f c R) (hg : TorusIntegrable g c R) :
    (∯ x in T(c, R), f x - g x) = (∯ x in T(c, R), f x) - ∯ x in T(c, R), g x

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
hf : TorusIntegrable f c R
hg : TorusIntegrable g c R
⊢ (∯ (x : Fin n → ℂ) in T(c, R), f x - g x) = (∯ (x : Fin n → ℂ) in T(c, R), f x) - ∯ (x : Fin n → ℂ) in T(c, R), g x

Tactic:
simpa only [sub_eq_add_neg, ← torusIntegral_neg] using torusIntegral_add hf hg.neg

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma natCast_ne_zero_iff_pos {n : ℕ} : (n : ℤ) ≠ 0 ↔ 0 < n

Proof state:
n : ℕ
⊢ ↑n ≠ 0 ↔ 0 < n

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Action/Basic.lean
theorem inv_hom_hom {M N : Action V G} (f : M ≅ N) :
    f.inv.hom ≫ f.hom.hom = 𝟙 N.V

Proof state:
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : Type u
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 N.V

Tactic:
rw [← comp_hom, Iso.inv_hom_id, id_hom]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem esymmPart_zero : esymmPart σ R (.indiscrete 0) = 1

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ esymmPart σ R (Nat.Partition.indiscrete 0) = 1

Tactic:
simp [esymmPart]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_negDblY (P : Fin 3 → A) : (W'.baseChange B).toJacobian.negDblY (f ∘ P) =
    f ((W'.baseChange A).toJacobian.negDblY P)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toJacobian.negDblY (⇑f ∘ P) = f ((baseChange W' A).toJacobian.negDblY P)

Tactic:
rw [← RingHom.coe_coe, ← map_negDblY, map_baseChange]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_equation (hf : Function.Injective f) (P : Fin 3 → R) :
    (W'.map f).toJacobian.Equation (f ∘ P) ↔ W'.Equation P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ⇑f
P : Fin 3 → R
⊢ (map W' f).toJacobian.Equation (⇑f ∘ P) ↔ W'.Equation P

Tactic:
simp only [Equation, map_polynomial, eval_map, ← eval₂_comp, map_eq_zero_iff f hf]

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem sSup_simples_le (N : Submodule R M) :
    sSup { m : Submodule R M | IsSimpleModule R m ∧ m ≤ N } = N

Proof state:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
N : Submodule R M
⊢ sSup {m | IsSimpleModule R ↥m ∧ m ≤ N} = N

Tactic:
simpa only [isSimpleModule_iff_isAtom] using sSup_atoms_le_eq _

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_singleton_prod (a : α) (t : Set β) : Nat.card ({a} ×ˢ t) = Nat.card t

Proof state:
α : Type u_1
β : Type u_2
a : α
t : Set β
⊢ Nat.card ↑({a} ×ˢ t) = Nat.card ↑t

Tactic:
rw [singleton_prod, Nat.card_image_of_injective (Prod.mk.inj_left a)]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem exists_s_a_of_partNum {a : α} (nth_partNum_eq : g.partNums.get? n = some a) :
    ∃ gp, g.s.get? n = some gp ∧ gp.a = a

Proof state:
α : Type u_1
g : GenContFract α
n : ℕ
a : α
nth_partNum_eq : g.partNums.get? n = some a
⊢ ∃ gp, g.s.get? n = some gp ∧ gp.a = a

Tactic:
simpa [partNums, Stream'.Seq.map_get?] using nth_partNum_eq

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem add_eq_one_iff : I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

Proof state:
R : Type u
inst✝ : Semiring R
I J : Ideal R
⊢ I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

Tactic:
rw [one_eq_top, eq_top_iff_one, add_eq_sup, Submodule.mem_sup]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma le_add_one_iff : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1

Proof state:
m n : ℤ
⊢ m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/QuadraticMap.lean
theorem hasLineDerivAt (f : QuadraticMap 𝕜 E F) (a b : E) :
    HasLineDerivAt 𝕜 f (polar f a b) a b

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : QuadraticMap 𝕜 E F
a b : E
⊢ HasLineDerivAt 𝕜 (⇑f) (polar (⇑f) a b) a b

Tactic:
simpa [HasLineDerivAt, QuadraticMap.map_add, f.map_smul] using
  ((hasDerivAt_const (0 : 𝕜) (f a)).add <|
    ((hasDerivAt_id 0).mul (hasDerivAt_id 0)).smul (hasDerivAt_const 0 (f b))).add
    ((hasDerivAt_id 0).smul (hasDerivAt_const 0 (polar f a b)))

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
private lemma muFun'_apply (a b : α) :
    muFun' 𝕜 b a = if a = b then 1 else -∑ x ∈ (Ioc a b).attach, muFun' 𝕜 b x

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ IncidenceAlgebra.muFun' 𝕜 b a = if a = b then 1 else -∑ x ∈ (Ioc a b).attach, IncidenceAlgebra.muFun' 𝕜 b ↑x

Tactic:
rw [muFun']

Result:
no goals