harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseIdx_eq_nil_iff {l : List α} {i : Nat} : eraseIdx l i = [] ↔ l = [] ∨ (length l = 1 ∧ i = 0)

Proof state:
α : Type u_1
l✝ : List α
i✝ : Nat
a : α
l : List α
i : Nat
⊢ (a :: l).eraseIdx (i + 1) = [] ↔ a :: l = [] ∨ (a :: l).length = 1 ∧ i + 1 = 0

Tactic:
simp [Nat.succ_inj']

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
⊢ l.eraseIdx i = [] ↔ l = [] ∨ l.length = 1 ∧ i = 0

Tactic:
match l, i with
| [], _
| a::l, 0
| a::l, i + 1 => simp [Nat.succ_inj']

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem inter_singleton_of_mem {a : α} {s : Finset α} (h : a ∈ s) : s ∩ {a} = {a}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s ∩ {a} = {a}

Tactic:
rw [inter_comm, singleton_inter_of_mem h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem set_mkArray_self : (mkArray n a).set i a h = mkArray n a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
h : i < (mkArray n a).size
⊢ (mkArray n a).set i a h = mkArray n a

Tactic:
apply Array.ext'

Result:
case h
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
h : i < (mkArray n a).size
⊢ ((mkArray n a).set i a h).toList = (mkArray n a).toList

Proof state:
case h
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
h : i < (mkArray n a).size
⊢ ((mkArray n a).set i a h).toList = (mkArray n a).toList

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
theorem map_subtype_embedding_Ico (hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x):
    (Ico a b).map (Embedding.subtype p) = (Ico a b : Finset α)

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a ≤ x ∧ x < ↑b
⊢ p x

Tactic:
exact hp hx.1 hx.2.le a.prop b.prop

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ico ↑a ↑b
⊢ p x

Tactic:
rw [mem_Ico] at hx

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a ≤ x ∧ x < ↑b
⊢ p x

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Ico a b) = Ico ↑a ↑b

Tactic:
rw [subtype_Ico_eq]

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ico ↑a ↑b)) = Ico ↑a ↑b

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ico ↑a ↑b)) = Ico ↑a ↑b

Tactic:
refine Finset.subtype_map_of_mem fun x hx => ?_

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ico ↑a ↑b
⊢ p x
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem IsNClique.of_induce {S : Subgraph G} {F : Set α} {s : Finset { x // x ∈ F }} {n : ℕ}
    (cc : (S.induce F).coe.IsNClique n s) :
    G.IsNClique n (Finset.map ⟨Subtype.val, Subtype.val_injective⟩ s)

Proof state:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsClique ↑s ∧ #s = n
⊢ G.IsClique ↑(map { toFun := Subtype.val, inj' := ⋯ } s) ∧ #(map { toFun := Subtype.val, inj' := ⋯ } s) = n

Tactic:
simp only [Subgraph.induce_verts, coe_map, card_map]

Result:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsClique ↑s ∧ #s = n
⊢ G.IsClique (⇑{ toFun := Subtype.val, inj' := ⋯ } '' ↑s) ∧ #s = n

Proof state:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsNClique n s
⊢ G.IsNClique n (map { toFun := Subtype.val, inj' := ⋯ } s)

Tactic:
rw [isNClique_iff] at cc ⊢

Result:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsClique ↑s ∧ #s = n
⊢ G.IsClique ↑(map { toFun := Subtype.val, inj' := ⋯ } s) ∧ #(map { toFun := Subtype.val, inj' := ⋯ } s) = n

Proof state:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
s : Finset { x // x ∈ F }
n : ℕ
cc : (S.induce F).coe.IsClique ↑s ∧ #s = n
⊢ G.IsClique (⇑{ toFun := Subtype.val, inj' := ⋯ } '' ↑s) ∧ #s = n

Tactic:
exact ⟨cc.left.of_induce, cc.right⟩

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Localization.lean
@[simp, reassoc]
lemma iso_hom_app (a : A) (X : C) :
    (commShiftOfLocalization.iso L W F F' a).hom.app (L.obj X) =
      F'.map ((L.commShiftIso a).inv.app X) ≫
      (Lifting.iso L W F F').hom.app (X⟦a⟧) ≫
        (F.commShiftIso a).hom.app X ≫
          (shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)

Proof state:
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a : A
X : C
⊢ (iso L W F F' a).hom.app (L.obj X) =
    F'.map ((L.commShiftIso a).inv.app X) ≫
      (Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X) ≫
        (F.commShiftIso a).hom.app X ≫ (shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)

Tactic:
simp [commShiftOfLocalization.iso]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem add_lt_iff {a b c : Int} : a + b < c ↔ a < -b + c

Proof state:
a b c : Int
⊢ a + b < c ↔ a < -b + c

Tactic:
rw [← Int.add_lt_add_iff_left (-b), Int.add_comm (-b), Int.add_neg_cancel_right]

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
theorem existsUnique_mem (ha : a ∈ s) : ∃! t, t ∈ P.parts ∧ a ∈ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ ∃! t, t ∈ P.parts ∧ a ∈ t

Tactic:
obtain ⟨t, ht, ht'⟩ := P.exists_mem ha

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
⊢ ∃! t, t ∈ P.parts ∧ a ∈ t

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
u : Finset α
hu : u ∈ P.parts
hu' : a ∈ u
⊢ u = t

Tactic:
exact P.eq_of_mem_parts hu ht hu' ht'

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
⊢ ∃! t, t ∈ P.parts ∧ a ∈ t

Tactic:
refine ⟨t, ⟨ht, ht'⟩, ?_⟩

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
⊢ ∀ (y : Finset α), (fun t => t ∈ P.parts ∧ a ∈ t) y → y = t

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
⊢ ∀ (y : Finset α), (fun t => t ∈ P.parts ∧ a ∈ t) y → y = t

Tactic:
rintro u ⟨hu, hu'⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ P.parts
ht' : a ∈ t
u : Finset α
hu : u ∈ P.parts
hu' : a ∈ u
⊢ u = t
-- Mathlib/Logic/Godel/GodelBetaFunction.lean
/-- **Gödel's Beta Function Lemma** -/
lemma beta_unbeta_coe (l : List ℕ) (i : Fin l.length) : beta (unbeta l) i = l[i]

Proof state:
l : List ℕ
i : Fin l.length
⊢ ∀ i ∈ Finset.univ, Nat.coprimes (fun x => l[x]) i ≠ 0

Tactic:
simp [coprimes]

Result:
no goals

Proof state:
l : List ℕ
i : Fin l.length
⊢ i ∈ Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
l : List ℕ
i : Fin l.length
⊢ (↑Finset.univ).Pairwise (Function.onFun Coprime (Nat.coprimes fun x => l[x]))

Tactic:
simpa using Set.pairwise_univ.mpr (pairwise_coprime_coprimes _)

Result:
no goals
-- Mathlib/CategoryTheory/Shift/SingleFunctors.lean
lemma shiftIso_add'_inv_app (n m mn : A) (hnm : m + n = mn) (a a' a'' : A)
    (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc])).inv.app X =
        (F.shiftIso n a a' ha').inv.app X ≫
        ((F.shiftIso m a' a'' ha'').inv.app X)⟦n⟧' ≫
      (shiftFunctorAdd' D m n mn hnm).inv.app ((F.functor a'').obj X)

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso mn a a'' ⋯).inv.app X =
    (F.shiftIso n a a' ha').inv.app X ≫
      (shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X) ≫
        (shiftFunctorAdd' D m n mn hnm).inv.app ((F.functor a'').obj X)

Tactic:
simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{?u.21482, u_1} C
inst✝⁶ : Category.{?u.21486, u_2} D
inst✝⁵ : Category.{?u.21490, u_3} E
inst✝⁴ : Category.{?u.21494, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ mn + a = a''

Tactic:
rw [← hnm, ← ha'', ← ha', add_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_one : ∀ a : Int, a.tdiv 1 = a
  | (n:Nat) => congrArg ofNat (Nat.div_one _)
  | -[n+1] => by simp [Int.tdiv, neg_ofNat_succ]; rfl

Proof state:
n : Nat
⊢ -[n+1].tdiv 1 = -[n+1]

Tactic:
simp [Int.tdiv, neg_ofNat_succ]

Result:
n : Nat
⊢ -(↑n + 1) = -[n+1]

Proof state:
n : Nat
⊢ -(↑n + 1) = -[n+1]

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean
theorem Ideal.minimalPrimes_eq_subsingleton_self [I.IsPrime] : I.minimalPrimes = {I}

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I.minimalPrimes = {I}

Tactic:
ext J

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
J : Ideal R
⊢ J ∈ I.minimalPrimes ↔ J ∈ {I}

Proof state:
case h.mpr
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
J : Ideal R
⊢ J ∈ {I} → J ∈ I.minimalPrimes

Tactic:
rintro (rfl : J = I)

Result:
case h.mpr
R : Type u_1
inst✝¹ : CommRing R
J : Ideal R
inst✝ : J.IsPrime
⊢ J ∈ J.minimalPrimes

Proof state:
case h.mpr
R : Type u_1
inst✝¹ : CommRing R
J : Ideal R
inst✝ : J.IsPrime
⊢ J ∈ J.minimalPrimes

Tactic:
exact ⟨⟨inferInstance, rfl.le⟩, fun _ h _ => h.2⟩

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
J : Ideal R
⊢ J ∈ I.minimalPrimes ↔ J ∈ {I}

Tactic:
constructor

Result:
case h.mp
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
J : Ideal R
⊢ J ∈ I.minimalPrimes → J ∈ {I}

case h.mpr
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
J : Ideal R
⊢ J ∈ {I} → J ∈ I.minimalPrimes

Proof state:
case h.mp
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
J : Ideal R
⊢ J ∈ I.minimalPrimes → J ∈ {I}

Tactic:
exact fun H => (H.2 ⟨inferInstance, rfl.le⟩ H.1.2).antisymm H.1.2

Result:
no goals
-- Mathlib/CategoryTheory/Limits/MonoCoprod.lean
theorem mk' (h : ∀ A B : C, ∃ (c : BinaryCofan A B) (_ : IsColimit c), Mono c.inl) : MonoCoprod C :=
  ⟨fun A B c' hc' => by
    obtain ⟨c, hc₁, hc₂⟩ := h A B
    simpa only [mono_inl_iff hc' hc₁] using hc₂⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (A B : C), ∃ c x, Mono c.inl
A B : C
c' : BinaryCofan A B
hc' : IsColimit c'
⊢ Mono c'.inl

Tactic:
obtain ⟨c, hc₁, hc₂⟩ := h A B

Result:
case intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (A B : C), ∃ c x, Mono c.inl
A B : C
c' : BinaryCofan A B
hc' : IsColimit c'
c : BinaryCofan A B
hc₁ : IsColimit c
hc₂ : Mono c.inl
⊢ Mono c'.inl

Proof state:
case intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (A B : C), ∃ c x, Mono c.inl
A B : C
c' : BinaryCofan A B
hc' : IsColimit c'
c : BinaryCofan A B
hc₁ : IsColimit c
hc₂ : Mono c.inl
⊢ Mono c'.inl

Tactic:
simpa only [mono_inl_iff hc' hc₁] using hc₂

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_top : f'' =o[⊤] g' ↔ ∀ x, f'' x = 0

Proof state:
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
⊢ f'' =o[⊤] g' ↔ ∀ (x : α), f'' x = 0

Tactic:
simp only [← principal_univ, isLittleO_principal, mem_univ, forall_true_left]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_le_factorization_mul_right {a b : ℕ} (ha : a ≠ 0) :
    b.factorization ≤ (a * b).factorization

Proof state:
a b : ℕ
ha : a ≠ 0
⊢ b.factorization ≤ (b * a).factorization

Tactic:
apply factorization_le_factorization_mul_left ha

Result:
no goals

Proof state:
a b : ℕ
ha : a ≠ 0
⊢ b.factorization ≤ (a * b).factorization

Tactic:
rw [mul_comm]

Result:
a b : ℕ
ha : a ≠ 0
⊢ b.factorization ≤ (b * a).factorization
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma refl {X Y : C} (z : W.LeftFraction X Y) : LeftFractionRel z z :=
  ⟨z.Y', 𝟙 _, 𝟙 _, rfl, rfl, by simpa only [Category.comp_id] using z.hs⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z : W.LeftFraction X Y
⊢ W (z.s ≫ 𝟙 z.Y')

Tactic:
simpa only [Category.comp_id] using z.hs

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem genEigenspace_eq_genEigenspace_finrank_of_le [FiniteDimensional K V]
    (f : End K V) (μ : K) {k : ℕ} (hk : finrank K V ≤ k) :
    f.genEigenspace μ k = f.genEigenspace μ (finrank K V) :=
  le_antisymm
    (genEigenspace_le_genEigenspace_finrank _ _ _)
    ((f.genEigenspace μ).monotone <| by simpa using hk)

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ
hk : finrank K V ≤ k
⊢ ↑(finrank K V) ≤ ↑k

Tactic:
simpa using hk

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma isGreatest_quasispectrum (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ IsGreatest (σₙ ℝ≥0 a) ‖a‖₊

Tactic:
simpa [cfcₙ_id ℝ≥0 a] using IsGreatest.nnnorm_cfcₙ_nnreal id a

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mul_one (a : Rat) : a * 1 = a

Proof state:
a : Rat
⊢ a * 1 = a

Tactic:
simp [mul_def, normalize_self]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem rootMultiplicity_pos' {p : R[X]} {x : R} :
    0 < rootMultiplicity x p ↔ p ≠ 0 ∧ IsRoot p x

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
⊢ 0 < rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x

Tactic:
rw [pos_iff_ne_zero, Ne, rootMultiplicity_eq_zero_iff, Classical.not_imp, and_comm]

Result:
no goals
-- Mathlib/NumberTheory/BernoulliPolynomials.lean
theorem bernoulli_def (n : ℕ) : bernoulli n =
    ∑ i ∈ range (n + 1), Polynomial.monomial i (_root_.bernoulli (n - i) * choose n i)

Proof state:
n : ℕ
⊢ ∑ i ∈ range (n + 1), (monomial (n - i)) (_root_.bernoulli i * ↑(n.choose i)) =
    ∑ j ∈ range (n + 1), (monomial (n - j)) (_root_.bernoulli (n - (n - j)) * ↑(n.choose (n - j)))

Tactic:
apply sum_congr rfl

Result:
n : ℕ
⊢ ∀ x ∈ range (n + 1),
    (monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) =
      (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))

Proof state:
n : ℕ
⊢ ∀ x ∈ range (n + 1),
    (monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) =
      (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))

Tactic:
rintro x hx

Result:
n x : ℕ
hx : x ∈ range (n + 1)
⊢ (monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) =
    (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))

Proof state:
n x : ℕ
hx : x ≤ n
⊢ (monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) =
    (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))

Tactic:
rw [choose_symm hx, tsub_tsub_cancel_of_le hx]

Result:
no goals

Proof state:
n x : ℕ
hx : x ∈ range (n + 1)
⊢ (monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) =
    (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))

Tactic:
rw [mem_range_succ_iff] at hx

Result:
n x : ℕ
hx : x ≤ n
⊢ (monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) =
    (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))

Proof state:
n : ℕ
⊢ bernoulli n = ∑ i ∈ range (n + 1), (monomial i) (_root_.bernoulli (n - i) * ↑(n.choose i))

Tactic:
rw [← sum_range_reflect, add_succ_sub_one, add_zero, bernoulli]

Result:
n : ℕ
⊢ ∑ i ∈ range (n + 1), (monomial (n - i)) (_root_.bernoulli i * ↑(n.choose i)) =
    ∑ j ∈ range (n + 1), (monomial (n - j)) (_root_.bernoulli (n - (n - j)) * ↑(n.choose (n - j)))
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_union (x y : ZFSet.{u}) : (x ∪ y).toSet = x.toSet ∪ y.toSet

Proof state:
x y : ZFSet.{u}
⊢ (⋃₀ {x, y}).toSet = x.toSet ∪ y.toSet

Tactic:
simp

Result:
no goals

Proof state:
x y : ZFSet.{u}
⊢ (x ∪ y).toSet = x.toSet ∪ y.toSet

Tactic:
change (⋃₀ {x, y}).toSet = _

Result:
x y : ZFSet.{u}
⊢ (⋃₀ {x, y}).toSet = x.toSet ∪ y.toSet
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem disjoint_mul_inv_of_mem_cycleFactorsFinset {f g : Perm α} (h : f ∈ cycleFactorsFinset g) :
    Disjoint (g * f⁻¹) f

Proof state:
case neg.a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : ¬f x = x
⊢ f⁻¹ x ∈ f.support

Tactic:
rwa [← support_inv, apply_mem_support, support_inv, mem_support]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ (g * f⁻¹).Disjoint f

Tactic:
intro x

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
⊢ (g * f⁻¹) x = x ∨ f x = x

Proof state:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : ¬f x = x
⊢ (g * f⁻¹) x = x

Tactic:
rw [mul_apply, ← h.right, apply_inv_self]

Result:
case neg.a
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : ¬f x = x
⊢ f⁻¹ x ∈ f.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f ∈ g.cycleFactorsFinset
⊢ (g * f⁻¹).Disjoint f

Tactic:
rw [mem_cycleFactorsFinset_iff] at h

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
⊢ (g * f⁻¹).Disjoint f

Proof state:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : ¬f x = x
⊢ (g * f⁻¹) x = x ∨ f x = x

Tactic:
refine Or.inl ?_

Result:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : ¬f x = x
⊢ (g * f⁻¹) x = x

Proof state:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : f x = x
⊢ (g * f⁻¹) x = x ∨ f x = x

Tactic:
exact Or.inr hx

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
⊢ (g * f⁻¹) x = x ∨ f x = x

Tactic:
by_cases hx : f x = x

Result:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : f x = x
⊢ (g * f⁻¹) x = x ∨ f x = x

case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : ¬f x = x
⊢ (g * f⁻¹) x = x ∨ f x = x
-- Mathlib/RingTheory/Norm/Defs.lean
theorem norm_eq_one_of_not_module_finite (h : ¬Module.Finite R S) (x : S) : norm R x = 1

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬Module.Finite R S
x : S
⊢ (norm R) x = 1

Tactic:
refine norm_eq_one_of_not_exists_basis _ (mt ?_ h) _

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬Module.Finite R S
x : S
⊢ (∃ s, Nonempty (Basis { x // x ∈ s } R S)) → Module.Finite R S

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬Module.Finite R S
x : S
⊢ (∃ s, Nonempty (Basis { x // x ∈ s } R S)) → Module.Finite R S

Tactic:
rintro ⟨s, ⟨b⟩⟩

Result:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬Module.Finite R S
x : S
s : Finset S
b : Basis { x // x ∈ s } R S
⊢ Module.Finite R S

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬Module.Finite R S
x : S
s : Finset S
b : Basis { x // x ∈ s } R S
⊢ Module.Finite R S

Tactic:
exact Module.Finite.of_basis b

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insertMany_empty_list_of_contains_eq_false [LawfulBEq α]
    {l : List (α × β)} {k : α}
    (h : (l.map Prod.fst).contains k = false) :
    get? (insertMany (empty : Raw₀ α (fun _ => β)) l).1 k = none

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k : α
h : (List.map Prod.fst l).contains k = false
⊢ get? (insertMany empty l).val k = none

Tactic:
rw [get?_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h]

Result:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k : α
h : (List.map Prod.fst l).contains k = false
⊢ get? empty k = none

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k : α
h : (List.map Prod.fst l).contains k = false
⊢ get? empty k = none

Tactic:
apply get?_empty

Result:
no goals