harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem sum_const_nat {m : ℕ} {f : α → ℕ} (h₁ : ∀ x ∈ s, f x = m) : ∑ x ∈ s, f x = #s * m

Proof state:
α : Type u_3
s : Finset α
m : ℕ
f : α → ℕ
h₁ : ∀ x ∈ s, f x = m
⊢ ∑ x ∈ s, f x = #s * m

Tactic:
rw [← Nat.nsmul_eq_mul, ← sum_const]

Result:
α : Type u_3
s : Finset α
m : ℕ
f : α → ℕ
h₁ : ∀ x ∈ s, f x = m
⊢ ∑ x ∈ s, f x = ∑ _x ∈ s, m

Proof state:
α : Type u_3
s : Finset α
m : ℕ
f : α → ℕ
h₁ : ∀ x ∈ s, f x = m
⊢ ∑ x ∈ s, f x = ∑ _x ∈ s, m

Tactic:
apply sum_congr rfl h₁

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
theorem strictAntiOn_dual_iff :
    StrictAntiOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictAntiOn f s

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictAntiOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ StrictAntiOn f s

Tactic:
rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
@[reassoc]
lemma Scheme.Hom.liftQuotient_comp (f : X.Hom (Spec A)) (I : Ideal A)
    (hI : I ≤ RingHom.ker ((Scheme.ΓSpecIso A).inv ≫ f.appTop).hom) :
    f.liftQuotient I hI ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk _)) = f

Proof state:
X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal ↑A
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ f.liftQuotient I hI ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = f

Tactic:
rw [Scheme.Hom.liftQuotient, Category.assoc, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
  Ideal.Quotient.lift_comp_mk]

Result:
X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal ↑A
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))) = f

Proof state:
X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal ↑A
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ f ≫ Spec.map (ΓSpecIso A).hom ≫ Spec.map (ΓSpecIso A).inv = f

Tactic:
simp only [← Spec.map_comp, Iso.inv_hom_id, Spec.map_id, Category.comp_id]

Result:
no goals

Proof state:
X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal ↑A
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))) = f

Tactic:
simp only [CommRingCat.hom_comp, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom, Spec.map_comp, ←
  Scheme.toSpecΓ_naturality_assoc, ← SpecMap_ΓSpecIso_hom]

Result:
X : Scheme
A : CommRingCat
f : X.Hom (Spec A)
I : Ideal ↑A
hI : I ≤ RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso A).inv ≫ f.appTop))
⊢ f ≫ Spec.map (ΓSpecIso A).hom ≫ Spec.map (ΓSpecIso A).inv = f
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ici_succ_eq_Ioi_of_not_isMax (ha : ¬ IsMax a) : Ici (succ a) = Ioi a :=
  coe_injective <| by simpa using Set.Ici_succ_eq_Ioi_of_not_isMax ha

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ ↑(Ici (succ a)) = ↑(Ioi a)

Tactic:
simpa using Set.Ici_succ_eq_Ioi_of_not_isMax ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_partition : a ∈ l ↔ a ∈ (partition p l).1 ∨ a ∈ (partition p l).2

Proof state:
α✝ : Type u_1
l : List α✝
a : α✝
p : α✝ → Bool
⊢ a ∈ l ↔ a ∈ (partition p l).fst ∨ a ∈ (partition p l).snd

Tactic:
by_cases p a <;> simp_all

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
theorem ker_eval {s : S} (hs : IsIntegral R s) :
    RingHom.ker ((Polynomial.aeval s).toRingHom : R[X] →+* S) =
    Ideal.span ({minpoly R s} : Set R[X])

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
⊢ RingHom.ker (Polynomial.aeval s).toRingHom = Ideal.span {minpoly R s}

Tactic:
ext p

Result:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
⊢ p ∈ RingHom.ker (Polynomial.aeval s).toRingHom ↔ p ∈ Ideal.span {minpoly R s}

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
⊢ p ∈ RingHom.ker (Polynomial.aeval s).toRingHom ↔ p ∈ Ideal.span {minpoly R s}

Tactic:
simp_rw [RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
  isIntegrallyClosed_dvd_iff hs, ← Ideal.mem_span_singleton]

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
/-- An odd Dirichlet character is an odd function. -/
lemma Odd.to_fun {χ : DirichletCharacter S m} (hχ : Odd χ) : Function.Odd χ :=
  fun _ ↦ by rw [← neg_one_mul, map_mul, hχ, neg_one_mul]

Proof state:
S : Type u_2
inst✝ : CommRing S
m : ℕ
χ : DirichletCharacter S m
hχ : χ.Odd
x✝ : ZMod m
⊢ χ (-x✝) = -χ x✝

Tactic:
rw [← neg_one_mul, map_mul, hχ, neg_one_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Slope.lean
@[simp] lemma slope_neg (f : k → E) (x y : k) : slope (fun t ↦ -f t) x y = -slope f x y

Proof state:
k : Type u_1
E : Type u_2
inst✝² : Field k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
f : k → E
x y : k
⊢ slope (fun t => -f t) x y = -slope f x y

Tactic:
simp only [slope_def_module, neg_sub_neg, ← smul_neg, neg_sub]

Result:
no goals
-- Mathlib/RingTheory/Localization/FractionRing.lean
lemma restrictScalars_fieldEquivOfAlgEquiv (f : B ≃ₐ[A] C) :
    (fieldEquivOfAlgEquiv FA FB FC f).restrictScalars A = algEquivOfAlgEquiv f

Proof state:
A : Type u_8
B : Type u_9
C : Type u_10
inst✝²¹ : CommRing A
inst✝²⁰ : CommRing B
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Algebra A C
FA : Type u_12
FB : Type u_13
FC : Type u_14
inst✝¹⁶ : Field FA
inst✝¹⁵ : Field FB
inst✝¹⁴ : Field FC
inst✝¹³ : Algebra A FA
inst✝¹² : Algebra B FB
inst✝¹¹ : Algebra C FC
inst✝¹⁰ : IsFractionRing A FA
inst✝⁹ : IsFractionRing B FB
inst✝⁸ : IsFractionRing C FC
inst✝⁷ : Algebra A FB
inst✝⁶ : IsScalarTower A B FB
inst✝⁵ : Algebra A FC
inst✝⁴ : IsScalarTower A C FC
inst✝³ : Algebra FA FB
inst✝² : IsScalarTower A FA FB
inst✝¹ : Algebra FA FC
inst✝ : IsScalarTower A FA FC
f : B ≃ₐ[A] C
⊢ AlgEquiv.restrictScalars A (fieldEquivOfAlgEquiv FA FB FC f) = algEquivOfAlgEquiv f

Tactic:
ext

Result:
case h
A : Type u_8
B : Type u_9
C : Type u_10
inst✝²¹ : CommRing A
inst✝²⁰ : CommRing B
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Algebra A C
FA : Type u_12
FB : Type u_13
FC : Type u_14
inst✝¹⁶ : Field FA
inst✝¹⁵ : Field FB
inst✝¹⁴ : Field FC
inst✝¹³ : Algebra A FA
inst✝¹² : Algebra B FB
inst✝¹¹ : Algebra C FC
inst✝¹⁰ : IsFractionRing A FA
inst✝⁹ : IsFractionRing B FB
inst✝⁸ : IsFractionRing C FC
inst✝⁷ : Algebra A FB
inst✝⁶ : IsScalarTower A B FB
inst✝⁵ : Algebra A FC
inst✝⁴ : IsScalarTower A C FC
inst✝³ : Algebra FA FB
inst✝² : IsScalarTower A FA FB
inst✝¹ : Algebra FA FC
inst✝ : IsScalarTower A FA FC
f : B ≃ₐ[A] C
a✝ : FB
⊢ (AlgEquiv.restrictScalars A (fieldEquivOfAlgEquiv FA FB FC f)) a✝ = (algEquivOfAlgEquiv f) a✝

Proof state:
case h
A : Type u_8
B : Type u_9
C : Type u_10
inst✝²¹ : CommRing A
inst✝²⁰ : CommRing B
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Algebra A C
FA : Type u_12
FB : Type u_13
FC : Type u_14
inst✝¹⁶ : Field FA
inst✝¹⁵ : Field FB
inst✝¹⁴ : Field FC
inst✝¹³ : Algebra A FA
inst✝¹² : Algebra B FB
inst✝¹¹ : Algebra C FC
inst✝¹⁰ : IsFractionRing A FA
inst✝⁹ : IsFractionRing B FB
inst✝⁸ : IsFractionRing C FC
inst✝⁷ : Algebra A FB
inst✝⁶ : IsScalarTower A B FB
inst✝⁵ : Algebra A FC
inst✝⁴ : IsScalarTower A C FC
inst✝³ : Algebra FA FB
inst✝² : IsScalarTower A FA FB
inst✝¹ : Algebra FA FC
inst✝ : IsScalarTower A FA FC
f : B ≃ₐ[A] C
a✝ : FB
⊢ (AlgEquiv.restrictScalars A (fieldEquivOfAlgEquiv FA FB FC f)) a✝ = (algEquivOfAlgEquiv f) a✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
/-- A sort of triangle inequality. -/
lemma uIcc_subset_uIcc_union_uIcc : [[a, c]] ⊆ [[a, b]] ∪ [[b, c]] := fun x => by
  simp only [mem_uIcc, mem_union]
  rcases le_total x b with h2 | h2 <;> tauto

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c x : α
⊢ x ∈ [[a, c]] → x ∈ [[a, b]] ∪ [[b, c]]

Tactic:
simp only [mem_uIcc, mem_union]

Result:
α : Type u_1
inst✝ : LinearOrder α
a b c x : α
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c x : α
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b

Tactic:
rcases le_total x b with h2 | h2 <;> tauto

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_mul (z1 z2 : ℤ_[p]) : ‖z1 * z2‖ = ‖z1‖ * ‖z2‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
⊢ ‖z1 * z2‖ = ‖z1‖ * ‖z2‖

Tactic:
simp [norm_def]

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
theorem HasCompactSupport.smul_left (hf : HasCompactSupport f') : HasCompactSupport (f • f')

Proof state:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝² : TopologicalSpace α
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
f' : α → M
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ (f • f') x = 0 x

Tactic:
simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]

Result:
no goals

Proof state:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝² : TopologicalSpace α
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
f' : α → M
hf : HasCompactSupport f'
⊢ HasCompactSupport (f • f')

Tactic:
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢

Result:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝² : TopologicalSpace α
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
f' : α → M
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0

Proof state:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝² : TopologicalSpace α
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
f' : α → M
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0

Tactic:
exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem unit_rightAdjointUniq_hom {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
    adj1.unit ≫ whiskerLeft F (rightAdjointUniq adj1 adj2).hom = adj2.unit

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'
⊢ adj1.unit ≫ whiskerLeft F (adj1.rightAdjointUniq adj2).hom = adj2.unit

Tactic:
ext x

Result:
case w.h
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 : C
⊢ (adj1.unit ≫ whiskerLeft F (adj1.rightAdjointUniq adj2).hom).app x = adj2.unit.app x

Proof state:
case w.h
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 : C
⊢ (adj1.unit ≫ whiskerLeft F (adj1.rightAdjointUniq adj2).hom).app x = adj2.unit.app x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem comap_map_eq (hf : f.ker = ⊥) : comap f (map f N) = N

Proof state:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : f.ker = ⊥
⊢ ↑(comap f (map f N)) = ↑N

Tactic:
exact (N : Set M).preimage_image_eq (f.ker_eq_bot.mp hf)

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : f.ker = ⊥
⊢ comap f (map f N) = N

Tactic:
rw [SetLike.ext'_iff]

Result:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₂
inst✝ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : f.ker = ⊥
⊢ ↑(comap f (map f N)) = ↑N
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma genWeightSpace_genWeightSpaceOf_map_incl (x : L) (χ : L → R) :
    (genWeightSpace (genWeightSpaceOf M (χ x) x) χ).map (genWeightSpaceOf M (χ x) x).incl =
    genWeightSpace M χ

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
x : L
χ : L → R
⊢ LieSubmodule.map (genWeightSpaceOf M (χ x) x).incl (genWeightSpace (↥(genWeightSpaceOf M (χ x) x)) χ) =
    genWeightSpace M χ

Tactic:
simpa [map_genWeightSpace_eq_of_injective (genWeightSpaceOf M (χ x) x).injective_incl]
  using genWeightSpace_le_genWeightSpaceOf M x χ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_inj_right {f : α → β} (w : ∀ x y, f x = f y → x = y) : map f l = map f l' ↔ l = l'

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
toList✝¹ toList✝ : List α
⊢ map f { toList := toList✝¹ } = map f { toList := toList✝ } ↔ { toList := toList✝¹ } = { toList := toList✝ }

Tactic:
simp [List.map_inj_right w]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
l' : Array α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
toList✝ : List α
⊢ map f { toList := toList✝ } = map f l' ↔ { toList := toList✝ } = l'

Tactic:
cases l'

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
toList✝¹ toList✝ : List α
⊢ map f { toList := toList✝¹ } = map f { toList := toList✝ } ↔ { toList := toList✝¹ } = { toList := toList✝ }

Proof state:
α : Type u_1
β : Type u_2
l l' : Array α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
⊢ map f l = map f l' ↔ l = l'

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
l' : Array α
f : α → β
w : ∀ (x y : α), f x = f y → x = y
toList✝ : List α
⊢ map f { toList := toList✝ } = map f l' ↔ { toList := toList✝ } = l'
-- Mathlib/NumberTheory/Fermat.lean
lemma fermatNumber_ne_one (n : ℕ) : fermatNumber n ≠ 1

Proof state:
n : ℕ
this : 3 ≤ n.fermatNumber
⊢ n.fermatNumber ≠ 1

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
⊢ n.fermatNumber ≠ 1

Tactic:
have := three_le_fermatNumber n

Result:
n : ℕ
this : 3 ≤ n.fermatNumber
⊢ n.fermatNumber ≠ 1
-- Mathlib/Data/Set/Insert.lean
lemma preimage_snd_singleton_eq_range : (Prod.snd ⁻¹' {b} : Set (α × β)) = range (·, b)

Proof state:
α : Type u_1
β : Type u_2
b : β
⊢ Prod.snd ⁻¹' {b} = range fun x => (x, b)

Tactic:
aesop

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem mem_degreeLE {n : WithBot ℕ} {f : R[X]} : f ∈ degreeLE R n ↔ degree f ≤ n

Proof state:
R : Type u
inst✝ : Semiring R
n : WithBot ℕ
f : R[X]
⊢ f ∈ degreeLE R n ↔ f.degree ≤ n

Tactic:
simp only [degreeLE, Submodule.mem_iInf, degree_le_iff_coeff_zero, LinearMap.mem_ker]

Result:
R : Type u
inst✝ : Semiring R
n : WithBot ℕ
f : R[X]
⊢ (∀ (i : ℕ), ↑i > n → (lcoeff R i) f = 0) ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0

Proof state:
R : Type u
inst✝ : Semiring R
n : WithBot ℕ
f : R[X]
⊢ (∀ (i : ℕ), ↑i > n → (lcoeff R i) f = 0) ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem multinomial_update (a : α) (f : α →₀ ℕ) :
    f.multinomial = (f.sum fun _ => id).choose (f a) * (f.update a 0).multinomial

Proof state:
case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : f a = 0
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x => id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)

Tactic:
rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]

Result:
no goals

Proof state:
case pos.e_a
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial (f.support.erase a) ⇑f = Nat.multinomial (f.support.erase a) ⇑(f.update a 0)

Tactic:
exact Nat.multinomial_congr fun _ h ↦ (Function.update_of_ne (mem_erase.1 h).1 0 f).symm

Result:
no goals

Proof state:
α : Type u_1
a : α
f : α →₀ ℕ
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x => id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)

Tactic:
by_cases h : a ∈ f.support

Result:
case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x => id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)

case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∉ f.support
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x => id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)

Proof state:
case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ (∑ x ∈ f.support, f x).choose (f a) * Nat.multinomial (f.support.erase a) ⇑f =
    (f.sum fun x => id).choose (f a) * Nat.multinomial (f.support.erase a) ⇑(f.update a 0)

Tactic:
congr 1

Result:
case pos.e_a
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial (f.support.erase a) ⇑f = Nat.multinomial (f.support.erase a) ⇑(f.update a 0)

Proof state:
α : Type u_1
a : α
f : α →₀ ℕ
⊢ f.multinomial = (f.sum fun x => id).choose (f a) * (f.update a 0).multinomial

Tactic:
simp only [multinomial_eq]

Result:
α : Type u_1
a : α
f : α →₀ ℕ
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x => id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)

Proof state:
case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x => id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)

Tactic:
rw [← Finset.insert_erase h, Nat.multinomial_insert (Finset.not_mem_erase a _),
  Finset.add_sum_erase _ f h, support_update_zero]

Result:
case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ (∑ x ∈ f.support, f x).choose (f a) * Nat.multinomial (f.support.erase a) ⇑f =
    (f.sum fun x => id).choose (f a) * Nat.multinomial (f.support.erase a) ⇑(f.update a 0)

Proof state:
case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∉ f.support
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x => id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)

Tactic:
rw [not_mem_support_iff] at h

Result:
case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : f a = 0
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x => id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)
-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
lemma hilbertPoly_mul_one_sub_pow_add (p : F[X]) (d e : ℕ) :
    hilbertPoly (p * (1 - X) ^ e) (d + e) = hilbertPoly p d

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d e : ℕ
⊢ (p * (1 - X) ^ e).hilbertPoly (d + e) = p.hilbertPoly d

Tactic:
induction e with
| zero => simp
| succ e he => rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]

Result:
no goals

Proof state:
case zero
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (p * (1 - X) ^ 0).hilbertPoly (d + 0) = p.hilbertPoly d

Tactic:
simp

Result:
no goals

Proof state:
case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d e : ℕ
he : (p * (1 - X) ^ e).hilbertPoly (d + e) = p.hilbertPoly d
⊢ (p * (1 - X) ^ (e + 1)).hilbertPoly (d + (e + 1)) = p.hilbertPoly d

Tactic:
rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/CompTypeclasses.lean
theorem comp_assoc {Q : Type*} [Monoid Q]
    {φ₁ : M →* N} {φ₂ : N →* P} {φ₁₂ : M →* P}
    (κ : CompTriple φ₁ φ₂ φ₁₂)
    {φ₃ : P →* Q} {φ₂₃ : N →* Q} (κ' : CompTriple φ₂ φ₃ φ₂₃)
    {φ₁₂₃ : M →* Q} :
    CompTriple φ₁ φ₂₃ φ₁₂₃ ↔ CompTriple φ₁₂ φ₃ φ₁₂₃

Proof state:
case mpr
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁₂.CompTriple φ₃ φ₁₂₃ → φ₁.CompTriple φ₂₃ φ₁₂₃

Tactic:
rintro ⟨h⟩

Result:
case mpr.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₃.comp φ₁₂ = φ₁₂₃
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃

Proof state:
case mpr.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₃.comp φ₁₂ = φ₁₂₃
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃

Tactic:
exact ⟨by simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]⟩

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₃.comp φ₁₂ = φ₁₂₃
⊢ φ₂₃.comp φ₁ = φ₁₂₃

Tactic:
simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]

Result:
no goals
-- Mathlib/Topology/Compactness/SigmaCompact.lean
theorem exists_mem_nhds (x : X) : ∃ n, K n ∈ 𝓝 x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ ∃ n, K n ∈ 𝓝 x

Tactic:
rcases K.exists_mem x with ⟨n, hn⟩

Result:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
hn : x ∈ K n
⊢ ∃ n, K n ∈ 𝓝 x

Proof state:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
hn : x ∈ K n
⊢ ∃ n, K n ∈ 𝓝 x

Tactic:
exact ⟨n + 1, mem_interior_iff_mem_nhds.mp <| K.subset_interior_succ n hn⟩

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc]
lemma liftK_π_eq_zero_of_boundary (k : A ⟶ S.X₂) (x : A ⟶ S.X₁) (hx : k = x ≫ S.f) :
    h.liftK k (by rw [hx, assoc, S.zero, comp_zero]) ≫ h.π = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.12118, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ k ≫ S.g = 0

Tactic:
rw [hx, assoc, S.zero, comp_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ 0 = (x ≫ h.f') ≫ h.π

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ h.liftK k ⋯ ≫ h.π = 0

Tactic:
rw [show 0 = (x ≫ h.f') ≫ h.π by simp]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ h.liftK k ⋯ ≫ h.π = (x ≫ h.f') ≫ h.π

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ h.liftK k ⋯ ≫ h.π = (x ≫ h.f') ≫ h.π

Tactic:
congr 1

Result:
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ h.liftK k ⋯ = x ≫ h.f'

Proof state:
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ h.liftK k ⋯ = x ≫ h.f'

Tactic:
simp only [← cancel_mono h.i, hx, liftK_i, assoc, f'_i]

Result:
no goals