harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem isNoetherianRing_fin_0 [IsNoetherianRing R] :
    IsNoetherianRing (MvPolynomial (Fin 0) R)

Proof state:
case f
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ MvPolynomial (Fin 0) R ≃+* R

Tactic:
apply MvPolynomial.isEmptyRingEquiv R (Fin 0)

Result:
no goals

Proof state:
case f
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ R ≃+* MvPolynomial (Fin 0) R

Tactic:
symm

Result:
case f
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ MvPolynomial (Fin 0) R ≃+* R

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing (MvPolynomial (Fin 0) R)

Tactic:
apply isNoetherianRing_of_ringEquiv R

Result:
case f
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ R ≃+* MvPolynomial (Fin 0) R
-- Mathlib/Data/Seq/Seq.lean
theorem eq_or_mem_of_mem_cons {a b : α} : ∀ {s : Seq α}, a ∈ cons b s → a = b ∨ a ∈ s
  | ⟨_, _⟩, h => (Stream'.eq_or_mem_of_mem_cons h).imp_left fun h => by injection h

Proof state:
α : Type u
a b : α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
h✝ : a ∈ cons b ⟨val✝, property✝⟩
h : some a = some b
⊢ a = b

Tactic:
injection h

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem IsSeparator.of_equivalence {G : C} (h : IsSeparator G) (α : C ≌ D) :
    IsSeparator (α.functor.obj G)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
h : IsSeparator G
α : C ≌ D
⊢ IsSeparator (α.functor.obj G)

Tactic:
simpa using IsSeparating.of_equivalence h α

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
theorem eraseNone_map_some (s : Finset α) : eraseNone (s.map Embedding.some) = s

Proof state:
case h
α : Type u_1
s : Finset α
a✝ : α
⊢ a✝ ∈ eraseNone (map Embedding.some s) ↔ a✝ ∈ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
⊢ eraseNone (map Embedding.some s) = s

Tactic:
ext

Result:
case h
α : Type u_1
s : Finset α
a✝ : α
⊢ a✝ ∈ eraseNone (map Embedding.some s) ↔ a✝ ∈ s
-- Mathlib/Topology/Sheaves/Stalks.lean
theorem stalkFunctor_map_germ_apply [ConcreteCategory C FC]
    {F G : X.Presheaf C} (U : Opens X) (x : X) (hx : x ∈ U) (f : F ⟶ G) (s) :
    (stalkFunctor C x).map f (F.germ U x hx s) = G.germ U x hx (f.app (op U) s)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F G : Presheaf C X
U : Opens ↑X
x : ↑X
hx : x ∈ U
f : F ⟶ G
s : CC (F.obj (op U))
⊢ (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.germ U x hx)) s) =
    (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.germ U x hx)) s)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F G : Presheaf C X
U : Opens ↑X
x : ↑X
hx : x ∈ U
f : F ⟶ G
s : CC (F.obj (op U))
⊢ (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.germ U x hx)) s) =
    (ConcreteCategory.hom (G.germ U x hx)) ((ConcreteCategory.hom (f.app (op U))) s)

Tactic:
rw [← ConcreteCategory.comp_apply, ← stalkFunctor_map_germ, ConcreteCategory.comp_apply]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F G : Presheaf C X
U : Opens ↑X
x : ↑X
hx : x ∈ U
f : F ⟶ G
s : CC (F.obj (op U))
⊢ (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.germ U x hx)) s) =
    (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.germ U x hx)) s)
-- Mathlib/Data/Nat/Cast/SetInterval.lean
theorem image_cast_int_Ioc (a b : ℕ) : (↑) '' Ioc a b = Ioc (a : ℤ) b :=
  (castOrderEmbedding (α := ℤ)).image_Ioc (by simp [ordConnected_Ici]) a b

Proof state:
a b : ℕ
⊢ (range ⇑castOrderEmbedding).OrdConnected

Tactic:
simp [ordConnected_Ici]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_push_of_pos (l) (pa : p a) : countP p (l.push a) = countP p l + 1

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
pa : p a = true
l : List α
⊢ countP p ({ toList := l }.push a) = countP p { toList := l } + 1

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l : Array α
pa : p a = true
⊢ countP p (l.push a) = countP p l + 1

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
a : α
pa : p a = true
l : List α
⊢ countP p ({ toList := l }.push a) = countP p { toList := l } + 1
-- Mathlib/GroupTheory/Perm/Basic.lean
theorem swap_smul_self_smul [MulAction (Perm α) β] (i j : α) (x : β) :
    swap i j • swap i j • x = x

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : MulAction (Perm α) β
i j : α
x : β
⊢ swap i j • swap i j • x = x

Tactic:
simp [smul_smul]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HomeomorphBall.lean
theorem PartialHomeomorph.univUnitBall_symm_apply_zero : univUnitBall.symm (0 : E) = 0

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ↑univUnitBall.symm 0 = 0

Tactic:
simp [PartialHomeomorph.univUnitBall_symm_apply]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem mem_admissibleIndex_of_mem_box_aux₁ (x : ℝ) (a : ℤ) :
    a < x ↔ a ≤ (⌈n * x⌉ - 1) / (n : ℝ)

Proof state:
n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ ↑n * ↑a + 1 = ↑(↑n * a + 1)

Tactic:
norm_cast

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
⊢ ↑a < x ↔ ↑a ≤ (↑⌈↑n * x⌉ - 1) / ↑n

Tactic:
have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero

Result:
n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ ↑a < x ↔ ↑a ≤ (↑⌈↑n * x⌉ - 1) / ↑n

Proof state:
n : ℕ
inst✝ : NeZero n
x : ℝ
a : ℤ
h : 0 < ↑n
⊢ ↑a < x ↔ ↑a ≤ (↑⌈↑n * x⌉ - 1) / ↑n

Tactic:
rw [le_div_iff₀' h, le_sub_iff_add_le,
  show (n : ℝ) * a + 1 = (n * a + 1 : ℤ) by norm_cast,
  Int.cast_le, Int.add_one_le_ceil_iff, Int.cast_mul, Int.cast_natCast, mul_lt_mul_left h]

Result:
no goals
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma sum_isBase_iff {M : Matroid α} {N : Matroid β} {B : Set (α ⊕ β)} :
    (M.sum N).IsBase B ↔ M.IsBase (.inl ⁻¹' B) ∧ N.IsBase (.inr ⁻¹' B)

Proof state:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ M.IsBase
        ((fun a => Equiv.ulift a) ''
          (Sigma.mk false ⁻¹'
            ((fun a => (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
              ((fun a => Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B)))) ∧
      N.IsBase
        ((fun a => Equiv.ulift a) ''
          (Sigma.mk true ⁻¹'
            ((fun a => (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
              ((fun a => Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B)))) ↔
    M.IsBase (Sum.inl ⁻¹' B) ∧ N.IsBase (Sum.inr ⁻¹' B)

Tactic:
convert Iff.rfl <;>
  simp [Set.ext_iff, Equiv.ulift, Equiv.sumEquivSigmaBool]

Result:
no goals

Proof state:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ (M.sum N).IsBase B ↔ M.IsBase (Sum.inl ⁻¹' B) ∧ N.IsBase (Sum.inr ⁻¹' B)

Tactic:
simp only [Matroid.sum, mapEquiv_isBase_iff, Equiv.sumCongr_symm, Equiv.sumCongr_apply,
  Equiv.symm_symm, sigma_isBase_iff, Bool.forall_bool, Equiv.ulift_apply]

Result:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ M.IsBase
        ((fun a => Equiv.ulift a) ''
          (Sigma.mk false ⁻¹'
            ((fun a => (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
              ((fun a => Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B)))) ∧
      N.IsBase
        ((fun a => Equiv.ulift a) ''
          (Sigma.mk true ⁻¹'
            ((fun a => (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) ''
              ((fun a => Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B)))) ↔
    M.IsBase (Sum.inl ⁻¹' B) ∧ N.IsBase (Sum.inr ⁻¹' B)
-- Mathlib/Topology/ContinuousMap/Compact.lean
theorem dist_le_iff_of_nonempty [Nonempty α] : dist f g ≤ C ↔ ∀ x, dist (f x) (g x) ≤ C

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
inst✝ : Nonempty α
⊢ dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C

Tactic:
simp only [← dist_mkOfCompact, BoundedContinuousFunction.dist_le_iff_of_nonempty,
  mkOfCompact_apply]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
lemma shatterer_compress_subset_shatterer (a : α) (𝒜 : Finset (Finset α)) :
    (𝓓 a 𝒜).shatterer ⊆ 𝒜.shatterer

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ (𝓓 a 𝒜).shatterer ⊆ 𝒜.shatterer

Tactic:
simp only [subset_iff, mem_shatterer]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ ⦃x : Finset α⦄, (𝓓 a 𝒜).Shatters x → 𝒜.Shatters x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ ⦃x : Finset α⦄, (𝓓 a 𝒜).Shatters x → 𝒜.Shatters x

Tactic:
exact fun s hs ↦ hs.of_compression

Result:
no goals
-- Mathlib/Algebra/Algebra/Unitization.lean
theorem inl_mul [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r₁ r₂ : R) :
    (inl (r₁ * r₂) : Unitization R A) = inl r₁ * inl r₂ :=
  ext rfl <|
    show (0 : A) = r₁ • (0 : A) + r₂ • (0 : A) + 0 * 0 by
      simp only [smul_zero, add_zero, mul_zero]

Proof state:
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
r₁ r₂ : R
⊢ 0 = r₁ • 0 + r₂ • 0 + 0 * 0

Tactic:
simp only [smul_zero, add_zero, mul_zero]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem sInter_prod {S : Set (Set α)} (hS : S.Nonempty) (t : Set β) :
    ⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t

Proof state:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ r ∈ S ×ˢ {t}, r.1 ×ˢ r.2 = ⋂ s ∈ S, s ×ˢ t

Tactic:
simp_rw [prod_singleton, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t

Tactic:
rw [← sInter_singleton t, sInter_prod_sInter hS (singleton_nonempty t), sInter_singleton]

Result:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ r ∈ S ×ˢ {t}, r.1 ×ˢ r.2 = ⋂ s ∈ S, s ×ˢ t
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insert [LawfulBEq α] (h : m.1.WF) {k a : α} [Inhabited (β a)] {v : β k} :
    (m.insert k v).get! a =
      if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.get! a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
k a : α
inst✝ : Inhabited (β a)
v : β k
⊢ (m.insert k v).get! a = if h : (k == a) = true then cast ⋯ v else m.get! a

Tactic:
simp_to_model [insert] using List.getValueCast!_insertEntry

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem idRel_subset {s : Set (α × α)} : idRel ⊆ s ↔ ∀ a, (a, a) ∈ s

Proof state:
α : Type ua
s : Set (α × α)
⊢ idRel ⊆ s ↔ ∀ (a : α), (a, a) ∈ s

Tactic:
simp [subset_def]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal'_zero : blockDiagonal' (0 : ∀ i, Matrix (m' i) (n' i) α) = 0

Proof state:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ blockDiagonal' 0 i✝ j✝ = 0 i✝ j✝

Tactic:
simp [blockDiagonal'_apply]

Result:
no goals

Proof state:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
⊢ blockDiagonal' 0 = 0

Tactic:
ext

Result:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ blockDiagonal' 0 i✝ j✝ = 0 i✝ j✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Bool.lean
theorem Bool.and_left (lhs rhs : Bool) (h : (lhs && rhs) = true) : lhs = true

Proof state:
⊢ ∀ (lhs rhs : Bool), (lhs && rhs) = true → lhs = true

Tactic:
decide

Result:
no goals

Proof state:
lhs rhs : Bool
h : (lhs && rhs) = true
⊢ lhs = true

Tactic:
revert lhs rhs

Result:
⊢ ∀ (lhs rhs : Bool), (lhs && rhs) = true → lhs = true
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem ker_eq_bot_of_cancel {f : A →* B} (h : ∀ u v : f.ker →* A, f.comp u = f.comp v → u = v) :
    f.ker = ⊥

Proof state:
A : Type u
B : Type v
inst✝¹ : Group A
inst✝ : Group B
f : A →* B
h : ∀ (u v : ↥f.ker →* A), f.comp u = f.comp v → u = v
⊢ f.comp f.ker.subtype = f.comp 1

Tactic:
aesop_cat

Result:
no goals

Proof state:
A : Type u
B : Type v
inst✝¹ : Group A
inst✝ : Group B
f : A →* B
h : ∀ (u v : ↥f.ker →* A), f.comp u = f.comp v → u = v
⊢ f.ker = ⊥

Tactic:
simpa using congr_arg range (h f.ker.subtype 1 (by aesop_cat))

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem equiv_rootD_r : Equiv self a (self.rootD b) ↔ Equiv self a b

Proof state:
self : UnionFind
a b : Nat
⊢ self.Equiv a (self.rootD b) ↔ self.Equiv a b

Tactic:
simp [Equiv, rootD_rootD]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem minimal_eq_iff : Minimal (· = y) x ↔ x = y

Proof state:
α : Type u_1
x y : α
inst✝ : LE α
⊢ Minimal (fun x => x = y) x ↔ x = y

Tactic:
simp (config := {contextual := true}) [Minimal]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_div_cancel_left (a b : G) : a * b / a = b

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a * b / a = b

Tactic:
rw [div_eq_inv_mul, inv_mul_cancel_left]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem zero_rpow_le_one (x : ℝ) : (0 : ℝ) ^ x ≤ 1

Proof state:
x : ℝ
⊢ 0 ^ x ≤ 1

Tactic:
by_cases h : x = 0 <;> simp [h, zero_le_one]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem map_eq (f g : X ⟶ Y) (h : f = g) : map f = map g

Proof state:
X Y : TopCat
f g : X ⟶ Y
h : f = g
⊢ map f = map g

Tactic:
subst h

Result:
X Y : TopCat
f : X ⟶ Y
⊢ map f = map f

Proof state:
X Y : TopCat
f : X ⟶ Y
⊢ map f = map f

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem entries_insert_of_not_mem {a} {b : β a} {s : AList β} (h : a ∉ s) :
    (insert a b s).entries = ⟨a, b⟩ :: s.entries

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
h : a ∉ s
⊢ (insert a b s).entries = ⟨a, b⟩ :: s.entries

Tactic:
rw [entries_insert, kerase_of_not_mem_keys h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_isBilimit {b : BinaryBicone X Y} (h : b.IsBilimit) :
    IsPushout (0 : 0 ⟶ X) (0 : 0 ⟶ Y) b.inl b.inr

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout 0 0 b.inl b.inr

Tactic:
convert IsPushout.of_is_coproduct' h.isColimit HasZeroObject.zeroIsInitial
  <;> subsingleton

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Basic.lean
@[simp] lemma neg_last (n : ℕ) : -Fin.last n = 1

Proof state:
n : ℕ
⊢ -last n = 1

Tactic:
simp [neg_eq_iff_add_eq_zero]

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem Polynomial.quotQuotEquivComm_mk (p : R[X]) :
    (Polynomial.quotQuotEquivComm I f) (Ideal.Quotient.mk _ (p.map (Ideal.Quotient.mk I))) =
      Ideal.Quotient.mk (span ({(Ideal.Quotient.mk (I.map C)) f} : Set (R[X] ⧸ (I.map C))))
      (Ideal.Quotient.mk (I.map C) p)

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotQuotEquivComm I f)
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) =
    (Ideal.Quotient.mk (span {(Ideal.Quotient.mk (Ideal.map C I)) f})) ((Ideal.Quotient.mk (Ideal.map C I)) p)

Tactic:
simp only [Polynomial.quotQuotEquivComm, quotientEquiv_mk,
  polynomialQuotientEquivQuotientPolynomial_map_mk]

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem HasLineDerivWithinAt.hasLineDerivAt
    (h : HasLineDerivWithinAt 𝕜 f f' s x v) (hs : s ∈ 𝓝 x) :
    HasLineDerivAt 𝕜 f f' x v :=
  h.hasLineDerivAt' <| (Continuous.tendsto' (by fun_prop) 0 _ (by simp)).eventually hs

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
f' : F
s : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' s x v
hs : s ∈ 𝓝 x
⊢ x + 0 • v = x

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
f' : F
s : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' s x v
hs : s ∈ 𝓝 x
⊢ Continuous fun t => x + t • v

Tactic:
fun_prop

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean
theorem tmul_one_mul_coe_tmul {i₂ : ι} (a₁ : A) (a₂ : 𝒜 i₂) (b₂ : B) :
    (a₁ ᵍ⊗ₜ[R] (1 : B) * (a₂ : A) ᵍ⊗ₜ[R] b₂ : 𝒜 ᵍ⊗[R] ℬ) = (a₁ * a₂ : A) ᵍ⊗ₜ (b₂ : B)

Proof state:
case h.e'_3.h.e'_17
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
i₂ : ι
a₁ : A
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ b₂ = ↑GradedMonoid.GOne.one * b₂

Tactic:
rw [SetLike.coe_gOne, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    [Inhabited β] (h : m.WF) {l : List (α × β)} {k : α}
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    get! (insertMany m l) k = get! m k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
l : List (α × β)
k : α
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ get! (insertMany m l) k = get! m k

Tactic:
simp_to_raw using Raw₀.Const.get!_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Data/Set/Sigma.lean
theorem sigma_eq_empty_iff : s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅ :=
  not_nonempty_iff_eq_empty.symm.trans <|
    sigma_nonempty_iff.not.trans <| by
      simp only [not_nonempty_iff_eq_empty, not_and, not_exists]

Proof state:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
⊢ (¬∃ i ∈ s, (t i).Nonempty) ↔ ∀ i ∈ s, t i = ∅

Tactic:
simp only [not_nonempty_iff_eq_empty, not_and, not_exists]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Curry.lean
theorem MultilinearMap.uncurry_curryLeft (f : MultilinearMap R M M₂) :
    f.curryLeft.uncurryLeft = f

Proof state:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
⊢ f.curryLeft.uncurryLeft = f

Tactic:
ext m

Result:
case H
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n.succ) → M i
⊢ f.curryLeft.uncurryLeft m = f m

Proof state:
case H
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n.succ) → M i
⊢ f.curryLeft.uncurryLeft m = f m

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive enorm_add_le]
lemma enorm_mul_le' (a b : E) : ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

Tactic:
simpa [enorm, ← ENNReal.coe_add] using nnnorm_mul_le' a b

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem SameCycle.trans : SameCycle f x y → SameCycle f y z → SameCycle f x z :=
  fun ⟨i, hi⟩ ⟨j, hj⟩ => ⟨j + i, by rw [zpow_add, mul_apply, hi, hj]⟩

Proof state:
α : Type u_2
f : Perm α
x y z : α
x✝¹ : f.SameCycle x y
x✝ : f.SameCycle y z
i : ℤ
hi : (f ^ i) x = y
j : ℤ
hj : (f ^ j) y = z
⊢ (f ^ (j + i)) x = z

Tactic:
rw [zpow_add, mul_apply, hi, hj]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean
theorem factors_zero : factors (0 : α) = 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ factors 0 = 0

Tactic:
simp [factors]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp] lemma expect_singleton (f : ι → M) (i : ι) : 𝔼 j ∈ {i}, f j = f i

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
f : ι → M
i : ι
⊢ 𝔼 j ∈ {i}, f j = f i

Tactic:
simp [expect]

Result:
no goals
-- Mathlib/Topology/NoetherianSpace.lean
theorem NoetherianSpace.exists_finset_irreducible [NoetherianSpace α] (s : Closeds α) :
    ∃ S : Finset (Closeds α), (∀ k : S, IsIrreducible (k : Set α)) ∧ s = S.sup id

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, (∀ (k : { x // x ∈ S }), IsIrreducible ↑↑k) ∧ s = S.sup id

Tactic:
simpa [Set.exists_finite_iff_finset, Finset.sup_id_eq_sSup]
  using NoetherianSpace.exists_finite_set_closeds_irreducible s

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem hom_inv_id_tensor {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
    (f.hom ⊗ g) ≫ (f.inv ⊗ h) = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ 𝟙 V ⊗ g ≫ h = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)

Tactic:
simp [id_tensorHom]

Result:
no goals

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f.hom ⊗ g) ≫ (f.inv ⊗ h) = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)

Tactic:
rw [← tensor_comp, f.hom_inv_id]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ 𝟙 V ⊗ g ≫ h = (𝟙 V ⊗ g) ≫ (𝟙 V ⊗ h)
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₄_of_isCharTwoJNeZeroNF : W.c₄ = W.b₂ ^ 2

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₂ ^ 2 - 24 * 0 = W.b₂ ^ 2

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.c₄ = W.b₂ ^ 2

Tactic:
rw [c₄, b₄_of_isCharTwoJNeZeroNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₂ ^ 2 - 24 * 0 = W.b₂ ^ 2
-- Mathlib/GroupTheory/Coset/Defs.lean
theorem eq {a b : α} : (a : α ⧸ s) = b ↔ a⁻¹ * b ∈ s :=
  calc
    _ ↔ leftRel s a b := Quotient.eq''
    _ ↔ _

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ (leftRel s) a b ↔ a⁻¹ * b ∈ s

Tactic:
rw [leftRel_apply]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
theorem lt_sin_mul {x : ℝ} (hx : 0 < x) (hx' : x < 1) : x < sin (π / 2 * x)

Proof state:
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ x < sin (π / 2 * x)

Tactic:
simpa [mul_comm x] using
  strictConcaveOn_sin_Icc.2 ⟨le_rfl, pi_pos.le⟩ ⟨pi_div_two_pos.le, half_le_self pi_pos.le⟩
    pi_div_two_pos.ne (sub_pos.2 hx') hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_inj : range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s')

Proof state:
s n s' n' : Nat
⊢ (range' s n).toList = (range' s' n').toList ↔ n = n' ∧ (n = 0 ∨ s = s')

Tactic:
simp [List.range'_inj]

Result:
no goals

Proof state:
s n s' n' : Nat
⊢ range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s')

Tactic:
rw [← toList_inj]

Result:
s n s' n' : Nat
⊢ (range' s n).toList = (range' s' n').toList ↔ n = n' ∧ (n = 0 ∨ s = s')