harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_eval_eq_ascPochhammer (r : R) (n : ℕ) :
    (descPochhammer R n).eval r = (ascPochhammer R n).eval (r - n + 1)

Proof state:
R : Type u
inst✝ : Ring R
r : R
n : ℕ
⊢ eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)

Tactic:
induction n with
| zero => rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]
| succ n ih =>
  rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
    ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
    (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
    Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)
⊢ X + 1 = map (algebraMap ℕ R) (X + 1)

Tactic:
simp only [Polynomial.map_add, map_X,
Polynomial.map_one]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Ring R
r : R
⊢ eval r (descPochhammer R 0) = eval (r - ↑0 + 1) (ascPochhammer R 0)

Tactic:
rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)
⊢ eval r (descPochhammer R (n + 1)) = eval (r - ↑(n + 1) + 1) (ascPochhammer R (n + 1))

Tactic:
rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
  ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
  (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
  Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem compl_sup_eq_top : xᶜ ⊔ x = ⊤

Proof state:
α : Type u
x : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ⊔ x = ⊤

Tactic:
rw [sup_comm, sup_compl_eq_top]

Result:
no goals
-- Mathlib/Data/Matrix/Basic.lean
@[simp] lemma mapMatrix_toLinearMap (f : α ≃ₗ[R] β) :
    (f.mapMatrix : _ ≃ₗ[R] Matrix m n β).toLinearMap = f.toLinearMap.mapMatrix

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
β : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Module R α
inst✝ : Module R β
f : α ≃ₗ[R] β
⊢ ↑f.mapMatrix = (↑f).mapMatrix

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
lemma LaurentSeriesRingEquiv_mem_valuationSubring (f : K⟦X⟧) :
    LaurentSeriesRingEquiv K f ∈ Valued.v.valuationSubring

Proof state:
K : Type u_2
inst✝ : Field K
f : K⟦X⟧
⊢ Valued.v ((LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) f)) ≤ 1

Tactic:
rw [LaurentSeriesRingEquiv_def, valuation_compare, val_le_one_iff_eq_coe]

Result:
K : Type u_2
inst✝ : Field K
f : K⟦X⟧
⊢ ∃ F, (ofPowerSeries ℤ K) F = (ofPowerSeries ℤ K) f

Proof state:
K : Type u_2
inst✝ : Field K
f : K⟦X⟧
⊢ ∃ F, (ofPowerSeries ℤ K) F = (ofPowerSeries ℤ K) f

Tactic:
use f

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
f : K⟦X⟧
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) f) ∈ Valued.v.valuationSubring

Tactic:
simp only [Valuation.mem_valuationSubring_iff]

Result:
K : Type u_2
inst✝ : Field K
f : K⟦X⟧
⊢ Valued.v ((LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) f)) ≤ 1
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_one : taylor r (1 : R[X]) = C 1

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
⊢ (taylor r) 1 = C 1

Tactic:
rw [← C_1, taylor_C]

Result:
no goals
-- Mathlib/NumberTheory/BernoulliPolynomials.lean
theorem bernoulli_eq_sub_sum (n : ℕ) :
    (n.succ : ℚ) • bernoulli n =
      monomial n (n.succ : ℚ) - ∑ k ∈ Finset.range n, ((n + 1).choose k : ℚ) • bernoulli k

Proof state:
n : ℕ
⊢ ↑n.succ • bernoulli n = (monomial n) ↑n.succ - ∑ k ∈ range n, ↑((n + 1).choose k) • bernoulli k

Tactic:
rw [Nat.cast_succ, ← sum_bernoulli n, sum_range_succ, add_sub_cancel_left, choose_succ_self_right,
  Nat.cast_succ]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
theorem eqToHom_apply {β : Type w} {X Y : β → C} (h : X = Y) (b : β) :
    (eqToHom h : X ⟶ Y) b = eqToHom (by rw [h])

Proof state:
C : Type u
inst✝ : Category.{v, u} C
β : Type w
X : β → C
b : β
⊢ eqToHom ⋯ b = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
β : Type w
X Y : β → C
h : X = Y
b : β
⊢ X b = Y b

Tactic:
rw [h]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
β : Type w
X Y : β → C
h : X = Y
b : β
⊢ eqToHom h b = eqToHom ⋯

Tactic:
subst h

Result:
C : Type u
inst✝ : Category.{v, u} C
β : Type w
X : β → C
b : β
⊢ eqToHom ⋯ b = eqToHom ⋯
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem cons_smul (f : MultilinearMap R M M₂) (m : ∀ i : Fin n, M i.succ) (c : R) (x : M 0) :
    f (cons (c • x) m) = c • f (cons x m)

Proof state:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring 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) → M i.succ
c : R
x : M 0
⊢ f (Fin.cons (c • x) m) = c • f (Fin.cons x m)

Tactic:
simp_rw [← update_cons_zero x m (c • x), f.map_update_smul, update_cons_zero]

Result:
no goals
-- Mathlib/Algebra/BigOperators/WithTop.lean
/-- A sum is infinite iff one term is infinite. -/
lemma sum_eq_bot_iff : ∑ i ∈ s, f i = ⊥ ↔ ∃ i ∈ s, f i = ⊥

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : AddCommMonoid α
s : Finset ι
f : ι → WithBot α
⊢ ∑ i ∈ s, f i = ⊥ ↔ ∃ i ∈ s, f i = ⊥

Tactic:
induction s using Finset.cons_induction <;> simp [*]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem card_isConj_mul_eq :
    Nat.card {h : Perm α | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum)! *
      g.cycleType.prod *
      (∏ n ∈ g.cycleType.toFinset, (g.cycleType.count n)!)) =
    (Fintype.card α)!

Proof state:
case h.e'_2.h.e'_5.h.h.e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ {h | IsConj g h} = orbit (ConjAct (Perm α)) g

Tactic:
ext h

Result:
case h.e'_2.h.e'_5.h.h.e'_2.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g h : Perm α
⊢ h ∈ {h | IsConj g h} ↔ h ∈ orbit (ConjAct (Perm α)) g

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Fintype.card ↑{h | IsConj g h} * Nat.card ↥(centralizer {g}) = (Fintype.card α)!

Tactic:
rw [Subgroup.nat_card_centralizer_nat_card_stabilizer, Nat.card_eq_fintype_card]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Fintype.card ↑{h | IsConj g h} * Fintype.card ↥(stabilizer (ConjAct (Perm α)) g) = (Fintype.card α)!

Proof state:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (Fintype.card α)! = Fintype.card (ConjAct (Perm α))

Tactic:
rw [ConjAct.card, Fintype.card_perm]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↑{h | IsConj g h} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!

Tactic:
rw [Nat.card_eq_fintype_card, ← nat_card_centralizer g]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Fintype.card ↑{h | IsConj g h} * Nat.card ↥(centralizer {g}) = (Fintype.card α)!

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Fintype.card ↑{h | IsConj g h} * Fintype.card ↥(stabilizer (ConjAct (Perm α)) g) = (Fintype.card α)!

Tactic:
convert MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Perm α)) g

Result:
case h.e'_2.h.e'_5.h.h.e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ {h | IsConj g h} = orbit (ConjAct (Perm α)) g

case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (Fintype.card α)! = Fintype.card (ConjAct (Perm α))

Proof state:
case h.e'_2.h.e'_5.h.h.e'_2.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g h : Perm α
⊢ h ∈ {h | IsConj g h} ↔ h ∈ orbit (ConjAct (Perm α)) g

Tactic:
simp only [Set.mem_setOf_eq, ConjAct.mem_orbit_conjAct, isConj_comm]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Defs.lean
@[simp] lemma nsmul_one {A} [AddMonoidWithOne A] : ∀ n : ℕ, n • (1 : A) = n
  | 0 => by simp [zero_nsmul]
  | n + 1 => by simp [succ_nsmul, nsmul_one n]

Proof state:
A : Type u_2
inst✝ : AddMonoidWithOne A
⊢ 0 • 1 = ↑0

Tactic:
simp [zero_nsmul]

Result:
no goals

Proof state:
A : Type u_2
inst✝ : AddMonoidWithOne A
n : ℕ
⊢ (n + 1) • 1 = ↑(n + 1)

Tactic:
simp [succ_nsmul, nsmul_one n]

Result:
no goals
-- Mathlib/Analysis/Convex/GaugeRescale.lean
theorem image_gaugeRescaleHomeomorph_interior {s t : Set E}
    (hsc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) (hsb : IsVonNBounded ℝ s)
    (htc : Convex ℝ t) (ht₀ : t ∈ 𝓝 0) (htb : IsVonNBounded ℝ t) :
    gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb '' interior s = interior t :=
  Subset.antisymm (mapsTo_gaugeRescale_interior ht₀ htc).image_subset <| by
    rw [← Homeomorph.preimage_symm, ← image_subset_iff]
    exact (mapsTo_gaugeRescale_interior hs₀ hsc).image_subset

Proof state:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb).symm '' interior t ⊆ interior s

Tactic:
exact (mapsTo_gaugeRescale_interior hs₀ hsc).image_subset

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ interior t ⊆ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' interior s

Tactic:
rw [← Homeomorph.preimage_symm, ← image_subset_iff]

Result:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T1Space E
s t : Set E
hsc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
hsb : IsVonNBounded ℝ s
htc : Convex ℝ t
ht₀ : t ∈ 𝓝 0
htb : IsVonNBounded ℝ t
⊢ ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb).symm '' interior t ⊆ interior s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem reverse_attachWith {P : α → Prop} {xs : Array α}
    {H : ∀ (a : α), a ∈ xs → P a} :
    (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h)))

Proof state:
α : Type u_1
P : α → Prop
xs : Array α
H : ∀ (a : α), a ∈ xs → P a
⊢ (xs.attachWith P H).reverse = xs.reverse.attachWith P ⋯

Tactic:
cases xs

Result:
case mk
α : Type u_1
P : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ ({ toList := toList✝ }.attachWith P H).reverse = { toList := toList✝ }.reverse.attachWith P ⋯

Proof state:
α : Type ?u.129578
P : α → Prop
xs : Array α
H : ∀ (a : α), a ∈ xs → P a
a : α
h : a ∈ xs.reverse
⊢ a ∈ xs

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
P : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ ({ toList := toList✝ }.attachWith P H).reverse = { toList := toList✝ }.reverse.attachWith P ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_eraseIdx (as : Array α) (i : Nat) (h : i < as.size) :
    (as.eraseIdx i h).toList = as.toList.eraseIdx i

Proof state:
case mk
α : Type u_1
i : Nat
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ ({ toList := toList✝ }.eraseIdx i h).toList = { toList := toList✝ }.toList.eraseIdx i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i < as.size
⊢ (as.eraseIdx i h).toList = as.toList.eraseIdx i

Tactic:
induction as

Result:
case mk
α : Type u_1
i : Nat
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ ({ toList := toList✝ }.eraseIdx i h).toList = { toList := toList✝ }.toList.eraseIdx i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y

Proof state:
case a
n : Nat
x y : BitVec n
eq :
  (if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)) =
    if 2 * y.toNat < 2 ^ n then ↑y.toNat else ↑y.toNat - ↑(2 ^ n)
⊢ x.toNat = y.toNat

Tactic:
revert eq

Result:
case a
n : Nat
x y : BitVec n
⊢ ((if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)) =
      if 2 * y.toNat < 2 ^ n then ↑y.toNat else ↑y.toNat - ↑(2 ^ n)) →
    x.toNat = y.toNat

Proof state:
n : Nat
x y : BitVec n
eq :
  (if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)) =
    if 2 * y.toNat < 2 ^ n then ↑y.toNat else ↑y.toNat - ↑(2 ^ n)
⊢ x = y

Tactic:
apply eq_of_toNat_eq

Result:
case a
n : Nat
x y : BitVec n
eq :
  (if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)) =
    if 2 * y.toNat < 2 ^ n then ↑y.toNat else ↑y.toNat - ↑(2 ^ n)
⊢ x.toNat = y.toNat

Proof state:
n : Nat
x y : BitVec n
eq : x.toInt = y.toInt
⊢ x = y

Tactic:
simp only [toInt_eq_toNat_cond] at eq

Result:
n : Nat
x y : BitVec n
eq :
  (if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)) =
    if 2 * y.toNat < 2 ^ n then ↑y.toNat else ↑y.toNat - ↑(2 ^ n)
⊢ x = y

Proof state:
case a
n : Nat
x y : BitVec n
_xlt : x.toNat < 2 ^ n
⊢ ((if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)) =
      if 2 * y.toNat < 2 ^ n then ↑y.toNat else ↑y.toNat - ↑(2 ^ n)) →
    x.toNat = y.toNat

Tactic:
have _ylt := y.isLt

Result:
case a
n : Nat
x y : BitVec n
_xlt : x.toNat < 2 ^ n
_ylt : y.toNat < 2 ^ n
⊢ ((if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)) =
      if 2 * y.toNat < 2 ^ n then ↑y.toNat else ↑y.toNat - ↑(2 ^ n)) →
    x.toNat = y.toNat

Proof state:
case a
n : Nat
x y : BitVec n
⊢ ((if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)) =
      if 2 * y.toNat < 2 ^ n then ↑y.toNat else ↑y.toNat - ↑(2 ^ n)) →
    x.toNat = y.toNat

Tactic:
have _xlt := x.isLt

Result:
case a
n : Nat
x y : BitVec n
_xlt : x.toNat < 2 ^ n
⊢ ((if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)) =
      if 2 * y.toNat < 2 ^ n then ↑y.toNat else ↑y.toNat - ↑(2 ^ n)) →
    x.toNat = y.toNat

Proof state:
case a
n : Nat
x y : BitVec n
_xlt : x.toNat < 2 ^ n
_ylt : y.toNat < 2 ^ n
⊢ ((if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)) =
      if 2 * y.toNat < 2 ^ n then ↑y.toNat else ↑y.toNat - ↑(2 ^ n)) →
    x.toNat = y.toNat

Tactic:
split <;> split <;> omega

Result:
no goals

Proof state:
n : Nat
x y : BitVec n
⊢ x.toInt = y.toInt → x = y

Tactic:
intro eq

Result:
n : Nat
x y : BitVec n
eq : x.toInt = y.toInt
⊢ x = y
-- Mathlib/Data/Multiset/UnionInter.lean
theorem replicate_inter (n : ℕ) (x : α) (s : Multiset α) :
    replicate n x ∩ s = replicate (min n (s.count x)) x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
⊢ replicate n x ∩ s = replicate (n ⊓ count x s) x

Tactic:
ext y

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ count y (replicate n x ∩ s) = count y (replicate (n ⊓ count x s) x)

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ count y (replicate n x ∩ s) = count y (replicate (n ⊓ count x s) x)

Tactic:
rw [count_inter, count_replicate, count_replicate]

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ (if x = y then n else 0) ⊓ count y s = if x = y then n ⊓ count x s else 0

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : ¬x = y
⊢ (if x = y then n else 0) ⊓ count y s = if x = y then n ⊓ count x s else 0

Tactic:
simp only [h, if_false, Nat.zero_min]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : x = y
⊢ (if x = y then n else 0) ⊓ count y s = if x = y then n ⊓ count x s else 0

Tactic:
simp only [h, if_true]

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ (if x = y then n else 0) ⊓ count y s = if x = y then n ⊓ count x s else 0

Tactic:
by_cases h : x = y

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : x = y
⊢ (if x = y then n else 0) ⊓ count y s = if x = y then n ⊓ count x s else 0

case neg
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : ¬x = y
⊢ (if x = y then n else 0) ⊓ count y s = if x = y then n ⊓ count x s else 0
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem HasStrictDerivAt.add (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) :
    HasStrictDerivAt (fun y => f y + g y) (f' + g') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
f' g' : F
x : 𝕜
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
⊢ HasStrictDerivAt (fun y => f y + g y) (f' + g') x

Tactic:
simpa using (hf.add hg).hasStrictDerivAt

Result:
no goals
-- Mathlib/AlgebraicGeometry/FunctionField.lean
theorem genericPoint_eq_bot_of_affine (R : CommRingCat) [IsDomain R] :
    genericPoint (Spec R) = (⊥ : PrimeSpectrum R)

Proof state:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = Set.univ

Tactic:
rw [← PrimeSpectrum.zeroLocus_singleton_zero]

Result:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = PrimeSpectrum.zeroLocus {0}

Proof state:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = PrimeSpectrum.zeroLocus {0}

Tactic:
rfl

Result:
no goals

Proof state:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IsGenericPoint ⊥ Set.univ

Tactic:
rw [isGenericPoint_def]

Result:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ closure {⊥} = Set.univ

Proof state:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ genericPoint ↑↑(Spec R).toPresheafedSpace = ⊥

Tactic:
apply (genericPoint_spec (Spec R)).eq

Result:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IsGenericPoint ⊥ Set.univ

Proof state:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ closure {⊥} = Set.univ

Tactic:
rw [← PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure, PrimeSpectrum.vanishingIdeal_singleton]

Result:
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ PrimeSpectrum.zeroLocus ↑⊥.asIdeal = Set.univ
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_sub_self (a b : α) : toIocMod hp a b - b = -toIocDiv hp a b • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b - b = -toIocDiv hp a b • p

Tactic:
rw [toIocMod, sub_sub_cancel_left, neg_smul]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Icc_pred_right_of_not_isMin (ha : ¬IsMin b) : Icc a (pred b) = Ico a b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin b
⊢ Icc a (pred b) = Ico a b

Tactic:
rw [← Ici_inter_Iic, Iic_pred_of_not_isMin ha, Ici_inter_Iio]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean
lemma image_out (C : Set G.ConnectedComponent) :
    Represents (Quot.out '' C) C :=
  Set.BijOn.mk (by rintro c ⟨x, ⟨hx, rfl⟩⟩; simp_all [connectedComponentMk]) (by
    rintro x ⟨c, ⟨hc, rfl⟩⟩ y ⟨d, ⟨hd, rfl⟩⟩ hxy
    simp only [connectedComponentMk] at hxy
    aesop) (fun _ _ ↦ by simpa [connectedComponentMk])

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
x✝¹ : G.ConnectedComponent
x✝ : x✝¹ ∈ C
⊢ x✝¹ ∈ G.connectedComponentMk '' (Quot.out '' C)

Tactic:
simpa [connectedComponentMk]

Result:
no goals

Proof state:
case intro.intro.intro.intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
c : Quot G.Reachable
hc : c ∈ C
d : Quot G.Reachable
hd : d ∈ C
hxy : Quot.mk G.Reachable c.out = Quot.mk G.Reachable d.out
⊢ c.out = d.out

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
⊢ Set.MapsTo G.connectedComponentMk (Quot.out '' C) C

Tactic:
rintro c ⟨x, ⟨hx, rfl⟩⟩

Result:
case intro.intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
x : Quot G.Reachable
hx : x ∈ C
⊢ G.connectedComponentMk x.out ∈ C

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
⊢ Set.InjOn G.connectedComponentMk (Quot.out '' C)

Tactic:
rintro x ⟨c, ⟨hc, rfl⟩⟩ y ⟨d, ⟨hd, rfl⟩⟩ hxy

Result:
case intro.intro.intro.intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
c : Quot G.Reachable
hc : c ∈ C
d : Quot G.Reachable
hd : d ∈ C
hxy : G.connectedComponentMk c.out = G.connectedComponentMk d.out
⊢ c.out = d.out

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
x : Quot G.Reachable
hx : x ∈ C
⊢ G.connectedComponentMk x.out ∈ C

Tactic:
simp_all [connectedComponentMk]

Result:
no goals

Proof state:
case intro.intro.intro.intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
c : Quot G.Reachable
hc : c ∈ C
d : Quot G.Reachable
hd : d ∈ C
hxy : G.connectedComponentMk c.out = G.connectedComponentMk d.out
⊢ c.out = d.out

Tactic:
simp only [connectedComponentMk] at hxy

Result:
case intro.intro.intro.intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
c : Quot G.Reachable
hc : c ∈ C
d : Quot G.Reachable
hd : d ∈ C
hxy : Quot.mk G.Reachable c.out = Quot.mk G.Reachable d.out
⊢ c.out = d.out
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_add_intCast' {n : ℤ} (h : y + n ≠ 0) (x : ℝ≥0) : x ^ (y + n) = x ^ y * x ^ n

Proof state:
y : ℝ
n : ℤ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
ext

Result:
case a
y : ℝ
n : ℤ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)

Proof state:
case a
y : ℝ
n : ℤ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)

Tactic:
exact Real.rpow_add_intCast' (mod_cast x.2) h

Result:
no goals