harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Coeff.lean
lemma coeff_list_sum_map {ι : Type*} (l : List ι) (f : ι → R[X]) (n : ℕ) :
    (l.map f).sum.coeff n = (l.map (fun a => (f a).coeff n)).sum

Proof state:
R : Type u
inst✝ : Semiring R
ι : Type u_1
l : List ι
f : ι → R[X]
n : ℕ
⊢ (List.map f l).sum.coeff n = (List.map (fun a => (f a).coeff n) l).sum

Tactic:
simp_rw [coeff_list_sum, List.map_map, Function.comp_def, lcoeff_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem average_zero : ⨍ _, (0 : E) ∂μ = 0

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
⊢ ⨍ (x : α), 0 ∂μ = 0

Tactic:
rw [average, integral_zero]

Result:
no goals
-- Mathlib/Data/Nat/Count.lean
theorem count_zero : count p 0 = 0

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p 0 = 0

Tactic:
rw [count, List.range_zero, List.countP, List.countP.go]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₈_int_mod_eight (n : ℤ) : χ₈ n = χ₈ (n % 8 : ℤ)

Proof state:
n : ℤ
⊢ χ₈ ↑n = χ₈ ↑(n % 8)

Tactic:
rw [← ZMod.intCast_mod n 8, Nat.cast_ofNat]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_C [CommRing S] [IsDomain S] [Algebra T S] (a : T) : (C a).aroots S = 0

Proof state:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ (C a).aroots S = 0

Tactic:
rw [aroots_def, map_C, roots_C]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_indicator_const_comp {mβ : MeasurableSpace β} {f : α → β} {s : Set β}
    (hf : Measurable f) (hs : MeasurableSet s) (c : ℝ≥0∞) :
    ∫⁻ a, s.indicator (fun _ => c) (f a) ∂μ = c * μ (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
f : α → β
s : Set β
hf : Measurable f
hs : MeasurableSet s
c : ℝ≥0∞
⊢ ∫⁻ (a : α), s.indicator (fun x => c) (f a) ∂μ = c * μ (f ⁻¹' s)

Tactic:
erw [lintegral_comp (measurable_const.indicator hs) hf, lintegral_indicator_const hs,
  Measure.map_apply hf hs]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
lemma coeff_single_X_pow [DecidableEq σ] (s s' : σ) (n n' : ℕ) :
    (X (R := R) s ^ n).coeff (Finsupp.single s' n')
    = if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
s s' : σ
n n' : ℕ
⊢ coeff (Finsupp.single s' n') (X s ^ n) = if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0

Tactic:
simp only [coeff_X_pow, single_eq_single_iff]

Result:
no goals
-- Mathlib/Algebra/FreeMonoid/Basic.lean
@[to_additive]
lemma prodAux_eq : ∀ l : List M, FreeMonoid.prodAux l = l.prod
  | [] => rfl
  | (_ :: xs) => by simp [prodAux, List.prod_eq_foldl]

Proof state:
M : Type u_4
inst✝ : Monoid M
head✝ : M
xs : List M
⊢ prodAux (head✝ :: xs) = (head✝ :: xs).prod

Tactic:
simp [prodAux, List.prod_eq_foldl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/UInt/Bitwise.lean
theorem Bool.toBitVec_toUInt16 {b : Bool} :
    b.toUInt16.toBitVec = (BitVec.ofBool b).setWidth 16

Proof state:
b : Bool
⊢ b.toUInt16.toBitVec = BitVec.setWidth 16 (BitVec.ofBool b)

Tactic:
cases b <;> simp [toUInt16]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_concat {l : List α} {e : α} :
    mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e]

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
e : α
⊢ mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e]

Tactic:
simp [mapIdx_append]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
lemma sin_sq_eq_half_sub : sin x ^ 2 = 1 / 2 - cos (2 * x) / 2

Proof state:
x : ℝ
⊢ sin x ^ 2 = 1 / 2 - cos (2 * x) / 2

Tactic:
rw [sin_sq, cos_sq, ← sub_sub, sub_half]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncGE.lean
@[reassoc, simp]
lemma truncGEMap_comp : truncGEMap (φ ≫ φ') e = truncGEMap φ e ≫ truncGEMap φ' e

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{u_4, u_3} C
inst✝⁵ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : HasZeroObject C
⊢ truncGEMap (φ ≫ φ') e = truncGEMap φ e ≫ truncGEMap φ' e

Tactic:
simp [truncGEMap, truncGE]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem weightedOrder_eq_top_iff :
    f.weightedOrder w = ⊤ ↔ f = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ weightedOrder w f = ⊤ ↔ f = 0

Tactic:
rw [← not_iff_not, ← ne_eq, ← ne_eq,   ne_zero_iff_weightedOrder_finite w, coe_toNat_eq_self]

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_comap'_iff {m : α → β} {f : Filter α} {g : Filter β} {i : γ → α} (h : range i ∈ f) :
    Tendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α → β
f : Filter α
g : Filter β
i : γ → α
h : range i ∈ f
⊢ Tendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g

Tactic:
rw [Tendsto, ← map_compose]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
m : α → β
f : Filter α
g : Filter β
i : γ → α
h : range i ∈ f
⊢ (map m ∘ map i) (comap i f) ≤ g ↔ Tendsto m f g
-- Mathlib/Data/Set/Prod.lean
theorem mk_preimage_prod_right_fn_eq_if [DecidablePred (· ∈ s)] (g : δ → β) :
    (fun b => (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
s : Set α
t : Set β
a : α
inst✝ : DecidablePred fun x => x ∈ s
g : δ → β
⊢ (fun b => (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅

Tactic:
rw [← mk_preimage_prod_right_eq_if, prod_preimage_right, preimage_preimage]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOn.congr_right {g : α → β} (hf : TendstoUniformlyOn F f p s)
    (hfg : EqOn f g s) : TendstoUniformlyOn F g p s := fun u hu => by
  filter_upwards [hf u hu] with i hi a ha using hfg ha ▸ hi a ha

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf : TendstoUniformlyOn F f p s
hfg : EqOn f g s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (g x, F n x) ∈ u

Tactic:
filter_upwards [hf u hu] with i hi a ha using hfg ha ▸ hi a ha

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma card_consEquiv_filter_piFinset (P : (∀ i, α (succ i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (tail r)}.card = (S 0).card * {r ∈ piFinset (tail S) | P r}.card

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
⊢ #(filter (fun r => P (tail r)) (piFinset S)) = #(S 0) * #(filter (fun r => P r) (piFinset (tail S)))

Tactic:
rw [← card_product, ← map_consEquiv_filter_piFinset, card_map]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Free.lean
theorem mk_freeRing : #(FreeRing α) = max #α ℵ₀

Proof state:
α : Type u
⊢ #(FreeRing α) = #α ⊔ ℵ₀

Tactic:
cases isEmpty_or_nonempty α <;> simp [FreeRing]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem UniqueMDiffWithinAt.mono_nhds {s t : Set M} {x : M} (hs : UniqueMDiffWithinAt I s x)
    (ht : 𝓝[s] x ≤ 𝓝[t] x) : UniqueMDiffWithinAt I t x :=
  hs.mono_nhds <| by simpa only [← map_extChartAt_nhdsWithin] using Filter.map_mono ht

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
hs : UniqueMDiffWithinAt I s x
ht : 𝓝[s] x ≤ 𝓝[t] x
⊢ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x ≤
    𝓝[↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I] ↑(extChartAt I x) x

Tactic:
simpa only [← map_extChartAt_nhdsWithin] using Filter.map_mono ht

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem map_eq_iff_sup_ker_eq_of_surjective {I J : Ideal R} (f : R →+* S)
    (hf : Function.Surjective f) : map f I = map f J ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ map f I = map f J ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f

Tactic:
rw [← (comap_injective_of_surjective f hf).eq_iff, comap_map_of_surjective f hf,
  comap_map_of_surjective f hf, RingHom.ker_eq_comap_bot]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem comp_ker_incl : f.comp f.ker.incl = 0

Proof state:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ f.comp f.ker.incl = 0

Tactic:
ext ⟨m, hm⟩

Result:
case h.mk
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m : M
hm : m ∈ f.ker
⊢ (f.comp f.ker.incl) ⟨m, hm⟩ = 0 ⟨m, hm⟩

Proof state:
case h.mk
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m : M
hm : m ∈ f.ker
⊢ (f.comp f.ker.incl) ⟨m, hm⟩ = 0 ⟨m, hm⟩

Tactic:
exact mem_ker.mp hm

Result:
no goals
-- Mathlib/Data/PNat/Find.lean
theorem find_le_iff (n : ℕ+) : PNat.find h ≤ n ↔ ∃ m ≤ n, p m

Proof state:
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ+
⊢ PNat.find h ≤ n ↔ ∃ m ≤ n, p m

Tactic:
simp only [exists_prop, ← lt_add_one_iff, find_lt_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem rightUnitor_naturality {f g : a ⟶ b} (η : f ⟶ g) :
    η ▷ 𝟙 b ≫ (ρ_ g).hom = (ρ_ f).hom ≫ η

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

Tactic:
simp

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

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
a : α
fallback : β a
⊢ m.getD a fallback = (m.get? a).getD fallback

Tactic:
simp_to_raw using Raw₀.getD_eq_getD_get?

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LSum.lean
theorem lcongr_single {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (i : ι) (m : M) :
    lcongr e₁ e₂ (Finsupp.single i m) = Finsupp.single (e₁ i) (e₂ m)

Proof state:
M : Type u_2
N : Type u_3
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
κ : Type u_8
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
i : ι
m : M
⊢ (lcongr e₁ e₂) (single i m) = single (e₁ i) (e₂ m)

Tactic:
simp [lcongr]

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem inv {x : R} (hx : IsSelfAdjoint x) : IsSelfAdjoint x⁻¹

Proof state:
R : Type u_1
inst✝¹ : Group R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint x⁻¹

Tactic:
simp only [isSelfAdjoint_iff, star_inv, hx.star_eq]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ioc_sub_one_right_eq_Ioo (a b : α) : Ioc a (b - 1) = Ioo a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
⊢ Ioc a (b - 1) = Ioo a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_right_eq_Ioo a b

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive]
lemma mul_right_iterate_apply_one (a : M) : (· * a)^[n] 1 = a ^ n

Proof state:
M : Type u_4
inst✝ : Monoid M
n : ℕ
a : M
⊢ (fun x => x * a)^[n] 1 = a ^ n

Tactic:
simp [mul_right_iterate]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem summable_mul_right_iff (h : a ≠ 0) : (Summable fun i ↦ f i * a) ↔ Summable f :=
  ⟨fun H ↦ by simpa only [mul_inv_cancel_right₀ h] using H.mul_right a⁻¹, fun H ↦ H.mul_right _⟩

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a : α
h : a ≠ 0
H : Summable fun i => f i * a
⊢ Summable f

Tactic:
simpa only [mul_inv_cancel_right₀ h] using H.mul_right a⁻¹

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast!_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    [Inhabited (β a)] (hl : DistinctKeys l) :
    getValueCast! a (eraseKey k l) = if k == a then default else getValueCast! a l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
inst✝ : Inhabited (β a)
hl : DistinctKeys l
⊢ getValueCast! a (eraseKey k l) = if (k == a) = true then default else getValueCast! a l

Tactic:
simp [getValueCast!_eq_getValueCast?, getValueCast?_eraseKey hl, apply_ite Option.get!]

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
lemma StrictAnti.mem_upperBounds_image (hf : StrictAnti f) :
    f a ∈ upperBounds (f '' s) ↔ a ∈ lowerBounds s

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ f a ∈ upperBounds (f '' s) ↔ a ∈ lowerBounds s

Tactic:
simp [upperBounds, lowerBounds, hf.le_iff_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eq_false_iff [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} :
    containsKey a l = false ↔ ∀ (b : ((a : α) × β a)), b ∈ l → (a == b.fst) = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a : α
⊢ containsKey a l = false ↔ ∀ (b : (a : α) × β a), b ∈ l → (a == b.fst) = false

Tactic:
simp [containsKey_eq_false_iff_forall_mem_keys, keys_eq_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem splitInTwo_fst_append_splitInTwo_snd (l : { l : List α // l.length = n }) : (splitInTwo l).1.1 ++ (splitInTwo l).2.1 = l.1

Proof state:
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ (splitInTwo l).fst.val ++ (splitInTwo l).snd.val = l.val

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem div_mul_cancel : ∀ {a b : Ordinal}, a ≠ 0 → a ∣ b → a * (b / a) = b
  | a, _, a0, ⟨b, rfl⟩ => by rw [mul_div_cancel _ a0]

Proof state:
a : Ordinal.{u_4}
a0 : a ≠ 0
b : Ordinal.{u_4}
⊢ a * (a * b / a) = a * b

Tactic:
rw [mul_div_cancel _ a0]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma presheaf_map_eqToHom_op (X : Scheme) (U V : X.Opens) (i : U = V) :
    X.presheaf.map (eqToHom i).op = eqToHom (i ▸ rfl)

Proof state:
X : Scheme
U V : X.Opens
i : U = V
⊢ X.presheaf.map (eqToHom i).op = eqToHom ⋯

Tactic:
rw [eqToHom_op, eqToHom_map]

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rtakeWhile_concat_pos (x : α) (h : p x) :
    rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]

Proof state:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rtakeWhile p (l ++ [x]) = rtakeWhile p l ++ [x]

Tactic:
rw [rtakeWhile_concat, if_pos h]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem mem_fundamentalFrontier :
    x ∈ fundamentalFrontier G s ↔ x ∈ s ∧ ∃ g : G, g ≠ 1 ∧ x ∈ g • s

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x : α
⊢ x ∈ fundamentalFrontier G s ↔ x ∈ s ∧ ∃ g, g ≠ 1 ∧ x ∈ g • s

Tactic:
simp [fundamentalFrontier]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `inv_lt_iff_one_lt_mul₀'` for a version with multiplication on the other side. -/
lemma inv_lt_iff_one_lt_mul₀ (ha : 0 < a) : a⁻¹ < b ↔ 1 < b * a

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : MulPosStrictMono G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ 1 < b * a

Tactic:
rw [← mul_inv_lt_iff₀ ha, one_mul]

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem card_image_polynomial_eval [DecidableEq R] [Fintype R] {p : R[X]} (hp : 0 < p.degree) :
    Fintype.card R ≤ natDegree p * #(univ.image fun x => eval x p) :=
  Finset.card_le_mul_card_image _ _ (fun a _ =>
    calc
      _ = #(p - C a).roots.toFinset :=
        congr_arg card (by simp [Finset.ext_iff, ← mem_roots_sub_C hp])
      _ ≤ Multiset.card (p - C a).roots := Multiset.toFinset_card_le _
      _ ≤ _ := card_roots_sub_C' hp)

Proof state:
R : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : Fintype R
p : R[X]
hp : 0 < p.degree
a : R
x✝ : a ∈ image (fun x => eval x p) univ
⊢ filter (fun a_1 => eval a_1 p = a) univ = (p - C a).roots.toFinset

Tactic:
simp [Finset.ext_iff, ← mem_roots_sub_C hp]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem subgroupOf_inj {H₁ H₂ K : Subgroup G} :
    H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K

Proof state:
G : Type u_1
inst✝ : Group G
H₁ H₂ K : Subgroup G
⊢ H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K

Tactic:
simpa only [SetLike.ext_iff, mem_inf, mem_subgroupOf, and_congr_left_iff] using Subtype.forall

Result:
no goals
-- Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
theorem nilpotent_iff_not_unit_of_minimal {x : Localization I.primeCompl} :
    IsNilpotent x ↔ x ∈ nonunits _

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
hMin : I ∈ minimalPrimes R
x : Localization I.primeCompl
⊢ IsNilpotent x ↔ x ∈ nonunits (Localization I.primeCompl)

Tactic:
simpa only [← IsLocalRing.mem_maximalIdeal] using nilpotent_iff_mem_maximal_of_minimal hMin

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
theorem Spanning.isBase_of_minimal (hX : M.Spanning X) (h : ∀ ⦃Y⦄, M.Spanning Y → Y ⊆ X → X = Y) :
    M.IsBase X

Proof state:
α : Type u_2
M : Matroid α
X : Set α
hX : M.Spanning X
h : ∀ ⦃Y : Set α⦄, M.Spanning Y → Y ⊆ X → X = Y
⊢ M.IsBase X

Tactic:
rwa [isBase_iff_minimal_spanning, minimal_subset_iff, and_iff_right hX]

Result:
no goals
-- Mathlib/Algebra/Algebra/Unitization.lean
theorem inl_star [Star R] [AddMonoid A] [StarAddMonoid A] (r : R) :
    inl (star r) = star (inl r : Unitization R A) :=
  ext rfl (by simp only [snd_star, star_zero, snd_inl])

Proof state:
R : Type u_1
A : Type u_2
inst✝² : Star R
inst✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
r : R
⊢ (inl (star r)).snd = (star (inl r)).snd

Tactic:
simp only [snd_star, star_zero, snd_inl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertMany_nil :
    insertMany m [] = m

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw₀ α fun x => β
⊢ (insertMany m []).val = m

Tactic:
simp [insertMany, Id.run]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem star_fuzzy_down : star ‖ down

Proof state:
⊢ star ‖ up

Tactic:
exact star_fuzzy_up

Result:
no goals

Proof state:
⊢ star ‖ down

Tactic:
rw [← neg_fuzzy_neg_iff, neg_down, neg_star]

Result:
⊢ star ‖ up
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsOpen.closure_div (ht : IsOpen t) (s : Set G) : closure s / t = s / t

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : IsOpen t
s : Set G
⊢ closure s / t = s / t

Tactic:
simp_rw [div_eq_mul_inv, ht.inv.closure_mul]

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Membership.lean
theorem mem_sSup_of_directed_on {S : Set (Subsemigroup M)} (hS : DirectedOn (· ≤ ·) S) {x : M} :
    x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Proof state:
M : Type u_2
inst✝ : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk,
  exists_prop]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma baseChange_slope [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K]
  [IsScalarTower R S K] (f : F →ₐ[S] K) (x₁ x₂ y₁ y₂ : F) :
  (W'.baseChange K).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) =
    f ((W'.baseChange F).toAffine.slope x₁ x₂ y₁ y₂)

Proof state:
R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Field F
inst✝⁷ : Field K
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
x₁ x₂ y₁ y₂ : F
⊢ (baseChange W' K).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f ((baseChange W' F).toAffine.slope x₁ x₂ y₁ y₂)

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

Result:
no goals
-- Mathlib/Data/Matrix/Invertible.lean
theorem mul_invOf_cancel_right (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
    A * B * ⅟ B = A

Proof state:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A * B * ⅟B = A

Tactic:
rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
@[simp]
lemma dynEntourage_univ {T : X → X} {n : ℕ} :
    dynEntourage T univ n = univ

Proof state:
X : Type u_1
T : X → X
n : ℕ
⊢ dynEntourage T univ n = univ

Tactic:
simp [dynEntourage]

Result:
no goals
-- Mathlib/RingTheory/Generators.lean
@[simp]
lemma σ_smul (x y) : P.σ x • y = x * y

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
x y : S
⊢ P.σ x • y = x * y

Tactic:
rw [Algebra.smul_def, algebraMap_apply, aeval_val_σ]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mk_eq_divInt (num den nz c) : ⟨num, den, nz, c⟩ = num /. (den : Nat)

Proof state:
num : Int
den : Nat
nz : den ≠ 0
c : num.natAbs.Coprime den
⊢ { num := num, den := den, den_nz := nz, reduced := c } = num /. ↑den

Tactic:
simp [mk_eq_mkRat]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_ofReal_im (x : ℝ) : (sinh x).im = 0

Proof state:
x : ℝ
⊢ (sinh ↑x).im = 0

Tactic:
rw [← ofReal_sinh_ofReal_re, ofReal_im]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
@[simp]
lemma card_sub {s t : Multiset α} (h : t ≤ s) : card (s - t) = card s - card t :=
  Nat.eq_sub_of_add_eq <| by rw [← card_add, Multiset.sub_add_cancel h]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : t ≤ s
⊢ (s - t).card + t.card = s.card

Tactic:
rw [← card_add, Multiset.sub_add_cancel h]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
@[simp, rclike_simps] lemma nnnorm_conj (z : K) : ‖conj z‖₊ = ‖z‖₊

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖(starRingEnd K) z‖₊ = ‖z‖₊

Tactic:
simp [nnnorm]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_eq_cfcL {a : A} {f : R → R} (ha : p a) (hf : ContinuousOn f (spectrum R a)) :
    cfc f a = cfcL ha ⟨_, hf.restrict⟩

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
a : A
f : R → R
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc f a = (cfcL ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }

Tactic:
rw [cfc_def, dif_pos ⟨ha, hf⟩, cfcL_apply]

Result:
no goals