harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Binomial.lean
theorem smeval_ascPochhammer_self_neg : ∀ n : ℕ,
    smeval (ascPochhammer ℕ n) (-n : ℤ) = (-1)^n * n.factorial
  | 0 => by
    rw [Nat.cast_zero, neg_zero, ascPochhammer_zero, Nat.factorial_zero, smeval_one, pow_zero,
      one_smul, pow_zero, Nat.cast_one, one_mul]
  | n + 1 => by
    rw [ascPochhammer_succ_left, smeval_X_mul, smeval_comp, smeval_add, smeval_X, smeval_one,
      pow_zero, pow_one, one_smul, Nat.cast_add, Nat.cast_one, neg_add_rev, neg_add_cancel_comm,
      smeval_ascPochhammer_self_neg n, ← mul_assoc, mul_comm _ ((-1) ^ n),
      show (-1 + -↑n = (-1 : ℤ) * (n + 1)) by omega, ← mul_assoc, pow_add, pow_one,
      Nat.factorial, Nat.cast_mul, ← mul_assoc, Nat.cast_succ]

Proof state:
n : ℕ
⊢ (ascPochhammer ℕ (n + 1)).smeval (-↑(n + 1)) = (-1) ^ (n + 1) * ↑(n + 1).factorial

Tactic:
rw [ascPochhammer_succ_left, smeval_X_mul, smeval_comp, smeval_add, smeval_X, smeval_one,
  pow_zero, pow_one, one_smul, Nat.cast_add, Nat.cast_one, neg_add_rev, neg_add_cancel_comm,
  smeval_ascPochhammer_self_neg n, ← mul_assoc, mul_comm _ ((-1) ^ n),
  show (-1 + -↑n = (-1 : ℤ) * (n + 1)) by omega, ← mul_assoc, pow_add, pow_one,
  Nat.factorial, Nat.cast_mul, ← mul_assoc, Nat.cast_succ]

Result:
no goals

Proof state:
n : ℕ
⊢ -1 + -↑n = -1 * (↑n + 1)

Tactic:
omega

Result:
no goals

Proof state:
⊢ (ascPochhammer ℕ 0).smeval (-↑0) = (-1) ^ 0 * ↑(Nat.factorial 0)

Tactic:
rw [Nat.cast_zero, neg_zero, ascPochhammer_zero, Nat.factorial_zero, smeval_one, pow_zero,
  one_smul, pow_zero, Nat.cast_one, one_mul]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem not_isUnit [Nontrivial B] : ¬IsUnit (minpoly A x)

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ ¬IsUnit (minpoly A x)

Tactic:
haveI : Nontrivial A := (algebraMap A B).domain_nontrivial

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
⊢ ¬IsUnit (minpoly A x)

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit (minpoly A x)

Tactic:
rw [eq_zero hx]

Result:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit 0

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit 0

Tactic:
exact not_isUnit_zero

Result:
no goals

Proof state:
case pos
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : IsIntegral A x
⊢ ¬IsUnit (minpoly A x)

Tactic:
exact mt (monic hx).eq_one_of_isUnit (ne_one A x)

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
⊢ ¬IsUnit (minpoly A x)

Tactic:
by_cases hx : IsIntegral A x

Result:
case pos
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : IsIntegral A x
⊢ ¬IsUnit (minpoly A x)

case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit (minpoly A x)
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem isMaximal_of_irreducible [CommRing R] [IsPrincipalIdealRing R] {p : R}
    (hp : Irreducible p) : Ideal.IsMaximal (span R ({p} : Set R)) :=
  ⟨⟨mt Ideal.span_singleton_eq_top.1 hp.1, fun I hI => by
      rcases principal I with ⟨a, rfl⟩
      erw [Ideal.span_singleton_eq_top]
      rcases Ideal.span_singleton_le_span_singleton.1 (le_of_lt hI) with ⟨b, rfl⟩
      refine (of_irreducible_mul hp).resolve_right (mt (fun hb => ?_) (not_le_of_lt hI))
      erw [Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd hb]⟩⟩

Proof state:
case mk.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : span R {p} < span R {a}
⊢ IsUnit a

Tactic:
rcases Ideal.span_singleton_le_span_singleton.1 (le_of_lt hI) with ⟨b, rfl⟩

Result:
case mk.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : span R {a * b} < span R {a}
⊢ IsUnit a

Proof state:
case mk.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : span R {a * b} < span R {a}
hb : IsUnit b
⊢ span R {a} ≤ span R {a * b}

Tactic:
erw [Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd hb]

Result:
no goals

Proof state:
case mk.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : span R {a * b} < span R {a}
⊢ IsUnit a

Tactic:
refine (of_irreducible_mul hp).resolve_right (mt (fun hb => ?_) (not_le_of_lt hI))

Result:
case mk.intro.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : span R {a * b} < span R {a}
hb : IsUnit b
⊢ span R {a} ≤ span R {a * b}

Proof state:
case mk.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : span R {p} < span R {a}
⊢ span R {a} = ⊤

Tactic:
erw [Ideal.span_singleton_eq_top]

Result:
case mk.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : span R {p} < span R {a}
⊢ IsUnit a

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
hI : span R {p} < I
⊢ I = ⊤

Tactic:
rcases principal I with ⟨a, rfl⟩

Result:
case mk.intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : span R {p} < span R {a}
⊢ span R {a} = ⊤
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem descFactorial_eq_div {n k : ℕ} (h : k ≤ n) : n.descFactorial k = n ! / (n - k)!

Proof state:
n k : ℕ
h : k ≤ n
⊢ n.descFactorial k = n ! / (n - k)!

Tactic:
apply Nat.mul_left_cancel (n - k).factorial_pos

Result:
n k : ℕ
h : k ≤ n
⊢ (n - k)! * n.descFactorial k = (n - k)! * (n ! / (n - k)!)

Proof state:
n k : ℕ
h : k ≤ n
⊢ n ! = (n - k)! * (n ! / (n - k)!)

Tactic:
exact (Nat.mul_div_cancel' <| factorial_dvd_factorial <| Nat.sub_le n k).symm

Result:
no goals

Proof state:
n k : ℕ
h : k ≤ n
⊢ (n - k)! * n.descFactorial k = (n - k)! * (n ! / (n - k)!)

Tactic:
rw [factorial_mul_descFactorial h]

Result:
n k : ℕ
h : k ≤ n
⊢ n ! = (n - k)! * (n ! / (n - k)!)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_map (f : β → α) (l : Array β) : filter p (map f l) = map f (filter (p ∘ f) l)

Proof state:
case mk
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : List β
⊢ filter p (map f { toList := l }) = map f (filter (p ∘ f) { toList := l })

Tactic:
simp [List.filter_map]

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : Array β
⊢ filter p (map f l) = map f (filter (p ∘ f) l)

Tactic:
rcases l with ⟨l⟩

Result:
case mk
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : List β
⊢ filter p (map f { toList := l }) = map f (filter (p ∘ f) { toList := l })
-- Mathlib/Logic/Function/Iterate.lean
theorem iterate_left {g : ℕ → α → α} (H : ∀ n, Semiconj f (g n) (g <| n + 1)) (n k : ℕ) :
    Semiconj f^[n] (g k) (g <| n + k)

Proof state:
case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + (k + 1)))

Tactic:
exact (H k).trans (ihn (k + 1))

Result:
no goals

Proof state:
case zero
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
⊢ Semiconj f^[0] (g k) (g (0 + k))

Tactic:
rw [Nat.zero_add]

Result:
case zero
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
⊢ Semiconj f^[0] (g k) (g k)

Proof state:
case zero
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
⊢ Semiconj f^[0] (g k) (g k)

Tactic:
exact id_left

Result:
no goals

Proof state:
case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + 1 + k))

Tactic:
rw [Nat.add_right_comm, Nat.add_assoc]

Result:
case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + (k + 1)))

Proof state:
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n k : ℕ
⊢ Semiconj f^[n] (g k) (g (n + k))

Tactic:
induction n generalizing k with
| zero =>
  rw [Nat.zero_add]
  exact id_left
| succ n ihn =>
  rw [Nat.add_right_comm, Nat.add_assoc]
  exact (H k).trans (ihn (k + 1))

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem comp_range : (g.comp f).range = AddSubgroup.map g.toAddMonoidHom f.range

Proof state:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ (g.comp f).range = AddSubgroup.map g.toAddMonoidHom f.range

Tactic:
erw [AddMonoidHom.map_range]

Result:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ (g.comp f).range = (g.toAddMonoidHom.comp f.toAddMonoidHom).range

Proof state:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ (g.comp f).range = (g.toAddMonoidHom.comp f.toAddMonoidHom).range

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Defs.lean
theorem zero_eq_mul : 0 = a * b ↔ a = 0 ∨ b = 0

Proof state:
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
⊢ 0 = a * b ↔ a = 0 ∨ b = 0

Tactic:
rw [eq_comm, mul_eq_zero]

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem map_replicate (f : α → β) (k : ℕ) (a : α) : (replicate k a).map f = replicate k (f a)

Proof state:
α : Type u_1
β : Type v
f : α → β
k : ℕ
a : α
⊢ map f (replicate k a) = replicate k (f a)

Tactic:
simp only [← coe_replicate, map_coe, List.map_replicate]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem piecewise_empty [∀ i : α, Decidable (i ∈ (∅ : Set α))] : piecewise ∅ f g = g

Proof state:
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
⊢ ∅.piecewise f g = g

Tactic:
ext i

Result:
case h
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
i : α
⊢ ∅.piecewise f g i = g i

Proof state:
case h
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
i : α
⊢ ∅.piecewise f g i = g i

Tactic:
simp [piecewise]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean
@[to_additive] lemma lt_iff_exists_one_lt_mul [MulLeftStrictMono α]
    [MulLeftReflectLT α] : a < b ↔ ∃ c, 1 < c ∧ a * c = b :=
  ⟨exists_one_lt_mul_of_lt', by rintro ⟨c, hc, rfl⟩; exact lt_mul_of_one_lt_right' _ hc⟩

Proof state:
α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a b : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulLeftReflectLT α
⊢ (∃ c, 1 < c ∧ a * c = b) → a < b

Tactic:
rintro ⟨c, hc, rfl⟩

Result:
case intro.intro
α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulLeftReflectLT α
c : α
hc : 1 < c
⊢ a < a * c

Proof state:
case intro.intro
α : Type u
inst✝⁴ : MulOneClass α
inst✝³ : Preorder α
inst✝² : ExistsMulOfLE α
a : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulLeftReflectLT α
c : α
hc : 1 < c
⊢ a < a * c

Tactic:
exact lt_mul_of_one_lt_right' _ hc

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
@[simp] lemma not_even_iff_odd : ¬Even n ↔ Odd n

Proof state:
n : ℤ
⊢ ¬Even n ↔ Odd n

Tactic:
rw [not_even_iff, odd_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem Option.map_cast_apply {γ γ' : Type u} (h : γ = γ') (x : Option γ) :
    Option.map (cast h) x = cast (congrArg Option h) x

Proof state:
case refl
γ : Type u
x : Option γ
⊢ Option.map (cast ⋯) x = cast ⋯ x

Tactic:
cases x <;> simp

Result:
no goals

Proof state:
γ γ' : Type u
h : γ = γ'
x : Option γ
⊢ Option.map (cast h) x = cast ⋯ x

Tactic:
cases h

Result:
case refl
γ : Type u
x : Option γ
⊢ Option.map (cast ⋯) x = cast ⋯ x
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem ofFractionRing_eq :
    (ofFractionRing : FractionRing K[X] → RatFunc K) = IsLocalization.algEquiv K[X]⁰ _ _ :=
  funext fun x =>
    Localization.induction_on x fun x => by
      simp only [Localization.mk_eq_mk'_apply, ofFractionRing_mk', IsLocalization.algEquiv_apply,
        IsLocalization.map_mk', RingHom.id_apply]

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x✝ : FractionRing K[X]
x : K[X] × ↥K[X]⁰
⊢ { toFractionRing := Localization.mk x.1 x.2 } =
    (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) (RatFunc K)) (Localization.mk x.1 x.2)

Tactic:
simp only [Localization.mk_eq_mk'_apply, ofFractionRing_mk', IsLocalization.algEquiv_apply,
  IsLocalization.map_mk', RingHom.id_apply]

Result:
no goals
-- Mathlib/RingTheory/Extension.lean
lemma σ_injective : P.σ.Injective

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Function.Injective P.σ

Tactic:
intro x y e

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x y : S
e : P.σ x = P.σ y
⊢ x = y

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

Tactic:
rw [← P.algebraMap_σ x, ← P.algebraMap_σ y, e]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma nil_iff_length_eq {p : G.Walk v w} : p.Nil ↔ p.length = 0

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.Nil ↔ p.length = 0

Tactic:
cases p <;> simp

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem eval_eq_πJ (l : Products I) (hl : l.isGood (π C (· ∈ s))) :
    l.eval C = πJ C s (l.eval (π C (· ∈ s)))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
l : Products I
hl : Products.isGood (π C fun x => x ∈ s) l
⊢ Products.eval C l = (πJ C s) (Products.eval (π C fun x => x ∈ s) l)

Tactic:
ext f

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
l : Products I
hl : Products.isGood (π C fun x => x ∈ s) l
f : ↑C
⊢ (Products.eval C l) f = ((πJ C s) (Products.eval (π C fun x => x ∈ s) l)) f
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma range_glueDataObjι_ι (U : X.affineOpens) :
    Set.range ⇑(I.glueDataObjι U ≫ U.1.ι).base = X.zeroLocus (U := U) (I.ideal U) ∩ U

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(ConcreteCategory.hom (I.glueDataObjι U ≫ (↑U).ι).base) = X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
simp only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp, range_glueDataObjι]

Result:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(ConcreteCategory.hom (↑U).ι.base) ''
      ((fun a => (ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)) =
    X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(ConcreteCategory.hom (↑U).ι.base) ''
      ((fun a => (ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)) =
    X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
rw [← Set.image_comp, ← TopCat.coe_comp, ← Scheme.comp_base, IsAffineOpen.isoSpec_inv_ι,
  IsAffineOpen.fromSpec_image_zeroLocus]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
lemma apply_single' [Zero N] [Zero P] (e : N → P) (he : e 0 = 0) (a : α) (n : N) (b : α) :
    e ((single a n) b) = single a (e n) b

Proof state:
α : Type u_1
N : Type u_7
P : Type u_8
inst✝¹ : Zero N
inst✝ : Zero P
e : N → P
he : e 0 = 0
a : α
n : N
b : α
⊢ e ((single a n) b) = (single a (e n)) b

Tactic:
simp only [single_apply]

Result:
α : Type u_1
N : Type u_7
P : Type u_8
inst✝¹ : Zero N
inst✝ : Zero P
e : N → P
he : e 0 = 0
a : α
n : N
b : α
⊢ e (if a = b then n else 0) = if a = b then e n else 0

Proof state:
case pos
α : Type u_1
N : Type u_7
P : Type u_8
inst✝¹ : Zero N
inst✝ : Zero P
e : N → P
he : e 0 = 0
a : α
n : N
b : α
h✝ : a = b
⊢ e n = e n

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
N : Type u_7
P : Type u_8
inst✝¹ : Zero N
inst✝ : Zero P
e : N → P
he : e 0 = 0
a : α
n : N
b : α
⊢ e (if a = b then n else 0) = if a = b then e n else 0

Tactic:
split_ifs

Result:
case pos
α : Type u_1
N : Type u_7
P : Type u_8
inst✝¹ : Zero N
inst✝ : Zero P
e : N → P
he : e 0 = 0
a : α
n : N
b : α
h✝ : a = b
⊢ e n = e n

case neg
α : Type u_1
N : Type u_7
P : Type u_8
inst✝¹ : Zero N
inst✝ : Zero P
e : N → P
he : e 0 = 0
a : α
n : N
b : α
h✝ : ¬a = b
⊢ e 0 = 0

Proof state:
case neg
α : Type u_1
N : Type u_7
P : Type u_8
inst✝¹ : Zero N
inst✝ : Zero P
e : N → P
he : e 0 = 0
a : α
n : N
b : α
h✝ : ¬a = b
⊢ e 0 = 0

Tactic:
exact he

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma differentiableAt_negMulLog_iff {x : ℝ} : DifferentiableAt ℝ negMulLog x ↔ x ≠ 0

Proof state:
case mpr
x : ℝ
hx : x ≠ 0
this✝ : x ∈ {0}ᶜ
this : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ DifferentiableAt ℝ negMulLog x

Tactic:
apply DifferentiableWithinAt.differentiableAt (s := {0}ᶜ) <;>
simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true,
  compl_singleton_mem_nhds_iff]

Result:
no goals

Proof state:
x : ℝ
⊢ DifferentiableAt ℝ negMulLog x ↔ x ≠ 0

Tactic:
constructor

Result:
case mp
x : ℝ
⊢ DifferentiableAt ℝ negMulLog x → x ≠ 0

case mpr
x : ℝ
⊢ x ≠ 0 → DifferentiableAt ℝ negMulLog x

Proof state:
case mp
x : ℝ
h : DifferentiableAt ℝ (fun x => -x * log x) x
eq0 : x = 0
⊢ False

Tactic:
simp only [neg_mul, differentiableAt_neg_iff, eq0] at h

Result:
case mp
x : ℝ
eq0 : x = 0
h : DifferentiableAt ℝ (fun y => y * log y) 0
⊢ False

Proof state:
case mpr
x : ℝ
⊢ x ≠ 0 → DifferentiableAt ℝ negMulLog x

Tactic:
intro hx

Result:
case mpr
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ negMulLog x

Proof state:
case mpr
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ negMulLog x

Tactic:
have : x ∈ ({0} : Set ℝ)ᶜ := by
  simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true]

Result:
case mpr
x : ℝ
hx : x ≠ 0
this : x ∈ {0}ᶜ
⊢ DifferentiableAt ℝ negMulLog x

Proof state:
case mp
x : ℝ
eq0 : x = 0
h : DifferentiableAt ℝ (fun y => y * log y) 0
⊢ False

Tactic:
exact not_DifferentiableAt_log_mul_zero h

Result:
no goals

Proof state:
x : ℝ
hx : x ≠ 0
⊢ x ∈ {0}ᶜ

Tactic:
simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true]

Result:
no goals

Proof state:
case mpr
x : ℝ
hx : x ≠ 0
this : x ∈ {0}ᶜ
⊢ DifferentiableAt ℝ negMulLog x

Tactic:
have := differentiableOn_negMulLog x this

Result:
case mpr
x : ℝ
hx : x ≠ 0
this✝ : x ∈ {0}ᶜ
this : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ DifferentiableAt ℝ negMulLog x

Proof state:
case mp
x : ℝ
⊢ DifferentiableAt ℝ (fun x => -x * log x) x → x ≠ 0

Tactic:
intro h eq0

Result:
case mp
x : ℝ
h : DifferentiableAt ℝ (fun x => -x * log x) x
eq0 : x = 0
⊢ False

Proof state:
case mp
x : ℝ
⊢ DifferentiableAt ℝ negMulLog x → x ≠ 0

Tactic:
unfold negMulLog

Result:
case mp
x : ℝ
⊢ DifferentiableAt ℝ (fun x => -x * log x) x → x ≠ 0
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_mul_C' (h : Commute (f a) x) : eval₂ f x (p * C a) = eval₂ f x p * f a

Proof state:
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
⊢ eval₂ f x (p * C a) = eval₂ f x p * f a

Tactic:
rw [eval₂_mul_noncomm, eval₂_C]

Result:
case hf
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
⊢ ∀ (k : ℕ), Commute (f ((C a).coeff k)) x

Proof state:
case hf
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
⊢ ∀ (k : ℕ), Commute (f ((C a).coeff k)) x

Tactic:
intro k

Result:
case hf
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
k : ℕ
⊢ Commute (f ((C a).coeff k)) x

Proof state:
case hf
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
k : ℕ
⊢ Commute (f ((C a).coeff k)) x

Tactic:
by_cases hk : k = 0

Result:
case pos
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
k : ℕ
hk : k = 0
⊢ Commute (f ((C a).coeff k)) x

case neg
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
k : ℕ
hk : ¬k = 0
⊢ Commute (f ((C a).coeff k)) x

Proof state:
case pos
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
k : ℕ
hk : k = 0
⊢ Commute (f ((C a).coeff k)) x

Tactic:
simp only [hk, h, coeff_C_zero, coeff_C_ne_zero]

Result:
no goals

Proof state:
case neg
R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
k : ℕ
hk : ¬k = 0
⊢ Commute (f ((C a).coeff k)) x

Tactic:
simp only [coeff_C_ne_zero hk, RingHom.map_zero, Commute.zero_left]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_toNNReal {a : ℝ≥0∞} (ha : a ≠ ∞) :
    Tendsto ENNReal.toNNReal (𝓝 a) (𝓝 a.toNNReal)

Proof state:
case intro
a : ℝ≥0
⊢ Tendsto ENNReal.toNNReal (𝓝 ↑a) (𝓝 (↑a).toNNReal)

Tactic:
rw [nhds_coe, tendsto_map'_iff]

Result:
case intro
a : ℝ≥0
⊢ Tendsto (ENNReal.toNNReal ∘ ofNNReal) (𝓝 a) (𝓝 (↑a).toNNReal)

Proof state:
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ Tendsto ENNReal.toNNReal (𝓝 a) (𝓝 a.toNNReal)

Tactic:
lift a to ℝ≥0 using ha

Result:
case intro
a : ℝ≥0
⊢ Tendsto ENNReal.toNNReal (𝓝 ↑a) (𝓝 (↑a).toNNReal)

Proof state:
case intro
a : ℝ≥0
⊢ Tendsto (ENNReal.toNNReal ∘ ofNNReal) (𝓝 a) (𝓝 (↑a).toNNReal)

Tactic:
exact tendsto_id

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.balance {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂)
    (H : ∃ l' r', BalancedSz l' r' ∧
          (Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l')) :
    Valid' o₁ (@balance α l x r) o₂

Proof state:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : ∃ l' r', BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
⊢ Valid' o₁ (l.balance x r) o₂

Tactic:
rw [balance_eq_balance' hl.3 hr.3 hl.2 hr.2]

Result:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : ∃ l' r', BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
⊢ Valid' o₁ (l.balance' x r) o₂

Proof state:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : ∃ l' r', BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
⊢ Valid' o₁ (l.balance' x r) o₂

Tactic:
exact hl.balance' hr H

Result:
no goals