harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean
lemma div_zero_subset (s : Set α) : s / 0 ⊆ 0

Proof state:
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
⊢ s / 0 ⊆ 0

Tactic:
simp [subset_def, mem_div]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem resolvent_isBigO_inv (a : A) : resolvent a =O[cobounded 𝕜] Inv.inv :=
  have h : (fun z ↦ resolvent (z⁻¹ • a) (1 : 𝕜)) =O[cobounded 𝕜] (fun _ ↦ (1 : ℝ))

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
⊢ (fun z => resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x => 1

Tactic:
simpa [Function.comp_def, resolvent] using
  (NormedRing.inverse_one_sub_norm (R := A)).comp_tendsto
    (by simpa using (tendsto_inv₀_cobounded (α := 𝕜)).smul_const a)

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
h : (fun z => resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x => 1
z : 𝕜
hz : z ∈ {0}ᶜ
⊢ resolvent a z = z⁻¹ • resolvent (z⁻¹ • a) 1

Tactic:
lift z to 𝕜ˣ using Ne.isUnit hz

Result:
case h.intro
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
h : (fun z => resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x => 1
z : 𝕜ˣ
hz : ↑z ∈ {0}ᶜ
⊢ resolvent a ↑z = (↑z)⁻¹ • resolvent ((↑z)⁻¹ • a) 1

Proof state:
case h.intro
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
h : (fun z => resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x => 1
z : 𝕜ˣ
hz : ↑z ∈ {0}ᶜ
⊢ resolvent a ↑z = (↑z)⁻¹ • resolvent ((↑z)⁻¹ • a) 1

Tactic:
simpa [Units.smul_def] using congr(z⁻¹ • $(units_smul_resolvent_self (r := z) (a := a)))

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
⊢ Tendsto (fun x => x⁻¹ • a) (cobounded 𝕜) (𝓝 0)

Tactic:
simpa using (tendsto_inv₀_cobounded (α := 𝕜)).smul_const a

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
h : (fun z => resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x => 1
⊢ resolvent a =ᶠ[cobounded 𝕜] fun z => z⁻¹ • resolvent (z⁻¹ • a) 1

Tactic:
filter_upwards [isBounded_singleton (x := 0)] with z hz

Result:
case h
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
h : (fun z => resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x => 1
z : 𝕜
hz : z ∈ {0}ᶜ
⊢ resolvent a z = z⁻¹ • resolvent (z⁻¹ • a) 1
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsPath.of_append_right {u v w : V} {p : G.Walk u v} {q : G.Walk v w}
    (h : (p.append q).IsPath) : q.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (p.append q).reverse.IsPath
⊢ q.reverse.IsPath

Tactic:
rw [reverse_append] at h

Result:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (q.reverse.append p.reverse).IsPath
⊢ q.reverse.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (q.reverse.append p.reverse).IsPath
⊢ q.reverse.IsPath

Tactic:
apply h.of_append_left

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (p.append q).IsPath
⊢ q.IsPath

Tactic:
rw [← isPath_reverse_iff] at h ⊢

Result:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (p.append q).reverse.IsPath
⊢ q.reverse.IsPath
-- Mathlib/Analysis/SumOverResidueClass.lean
/-- A decreasing sequence of real numbers is summable on a residue class
if and only if it is summable. -/
lemma summable_indicator_mod_iff {m : ℕ} [NeZero m] {f : ℕ → ℝ} (hf : Antitone f) (k : ZMod m) :
    Summable ({n : ℕ | (n : ZMod m) = k}.indicator f) ↔ Summable f

Proof state:
case h.e'_5.h
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
H : Summable ({n | ↑n = k}.indicator f)
x✝ : ℕ
⊢ (∑ a : ZMod m, {n | ↑n = a}.indicator f) x✝ = ∑ i : ZMod m, {n | ↑n = i}.indicator f x✝

Tactic:
simp only [Finset.sum_apply]

Result:
no goals

Proof state:
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
H : Summable ({n | ↑n = k}.indicator f)
⊢ Summable (∑ a : ZMod m, {n | ↑n = a}.indicator f)

Tactic:
convert summable_sum (s := Finset.univ)
  fun a _ ↦ summable_indicator_mod_iff_summable_indicator_mod hf a H

Result:
case h.e'_5.h
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
H : Summable ({n | ↑n = k}.indicator f)
x✝ : ℕ
⊢ (∑ a : ZMod m, {n | ↑n = a}.indicator f) x✝ = ∑ i : ZMod m, {n | ↑n = i}.indicator f x✝

Proof state:
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
H : Summable ({n | ↑n = k}.indicator f)
⊢ Summable f

Tactic:
rw [Finset.sum_indicator_mod m f]

Result:
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
H : Summable ({n | ↑n = k}.indicator f)
⊢ Summable (∑ a : ZMod m, {n | ↑n = a}.indicator f)

Proof state:
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
⊢ Summable ({n | ↑n = k}.indicator f) ↔ Summable f

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ Summable.indicator H _⟩

Result:
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
H : Summable ({n | ↑n = k}.indicator f)
⊢ Summable f
-- Mathlib/ModelTheory/Basic.lean
theorem card_sum :
    (L.sum L').card = Cardinal.lift.{max u' v'} L.card + Cardinal.lift.{max u v} L'.card

Proof state:
L : Language
L' : Language
⊢ (L.sum L').card = lift.{max u' v', max u v} L.card + lift.{max u v, max u' v'} L'.card

Tactic:
simp only [card, mk_sum, mk_sigma, card_functions_sum, sum_add_distrib', lift_add, lift_sum,
  lift_lift, card_relations_sum, add_assoc,
  add_comm (Cardinal.sum fun i => (#(L'.Functions i)).lift)]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem mem_vectorSpan_pair {p₁ p₂ : P} {v : V} :
    v ∈ vectorSpan k ({p₁, p₂} : Set P) ↔ ∃ r : k, r • (p₁ -ᵥ p₂) = v

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
v : V
⊢ v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v

Tactic:
rw [vectorSpan_pair, Submodule.mem_span_singleton]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem count_of_coprime {a : Associates α} (ha : a ≠ 0)
    {b : Associates α} (hb : b ≠ 0) (hab : ∀ d, d ∣ a → d ∣ b → ¬Prime d) {p : Associates α}
    (hp : Irreducible p) : count p a.factors = 0 ∨ count p b.factors = 0

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
⊢ p.count a.factors = 0 ∨ p.count b.factors = 0

Tactic:
rw [or_iff_not_imp_left, ← Ne]

Result:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
⊢ p.count a.factors ≠ 0 → p.count b.factors = 0

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
⊢ p.count a.factors ≠ 0 → p.count b.factors = 0

Tactic:
intro hca

Result:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
hca : p.count a.factors ≠ 0
⊢ p.count b.factors = 0

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
hca : p.count a.factors ≠ 0
⊢ p.count b.factors = 0

Tactic:
contrapose! hab with hcb

Result:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hca : p.count a.factors ≠ 0
hcb : p.count b.factors ≠ 0
⊢ ∃ d, d ∣ a ∧ d ∣ b ∧ Prime d

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hca : p.count a.factors ≠ 0
hcb : p.count b.factors ≠ 0
⊢ ∃ d, d ∣ a ∧ d ∣ b ∧ Prime d

Tactic:
exact ⟨p, le_of_count_ne_zero ha hp hca, le_of_count_ne_zero hb hp hcb,
  UniqueFactorizationMonoid.irreducible_iff_prime.mp hp⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem coeFn_nonneg (f : Lp.simpleFunc G p μ) : (0 : α → G) ≤ᵐ[μ] f ↔ 0 ≤ f

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝ : NormedLatticeAddCommGroup G
f : ↥(simpleFunc G p μ)
⊢ 0 ≤ᶠ[ae μ] ↑↑↑f ↔ 0 ≤ f

Tactic:
rw [← Subtype.coe_le_coe, Lp.coeFn_nonneg, AddSubmonoid.coe_zero]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem esymm_zero : esymm σ R 0 = 1

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ esymm σ R 0 = 1

Tactic:
simp only [esymm, powersetCard_zero, sum_singleton, prod_empty]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
/-- Swap matrices are self inverse. -/
lemma swap_mul_self (i j : n) : swap R i j * swap R i j = 1

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
⊢ Equiv.Perm.permMatrix R (Equiv.swap i j) * Equiv.Perm.permMatrix R (Equiv.swap i j) = 1

Tactic:
rw [← Equiv.swap_inv, Equiv.Perm.inv_def]

Result:
R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
⊢ Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) * Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) = 1

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
⊢ swap R i j * swap R i j = 1

Tactic:
simp only [swap]

Result:
R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
⊢ Equiv.Perm.permMatrix R (Equiv.swap i j) * Equiv.Perm.permMatrix R (Equiv.swap i j) = 1

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
⊢ Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) * Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) = 1

Tactic:
simp [← PEquiv.toMatrix_trans, ← Equiv.toPEquiv_trans]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_extract {as : Vector α n} {start stop : Nat}
    (h : i < min stop n - start) :
    (as.extract start stop)[i] = as[start + i]

Proof state:
α : Type u_1
n i : Nat
as : Vector α n
start stop : Nat
h : i < min stop n - start
⊢ (as.extract start stop)[i] = as[start + i]

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
i start stop : Nat
as : Array α
h : i < min stop as.size - start
⊢ ({ toArray := as, size_toArray := ⋯ }.extract start stop)[i] = { toArray := as, size_toArray := ⋯ }[start + i]

Proof state:
case mk
α : Type u_1
i start stop : Nat
as : Array α
h : i < min stop as.size - start
⊢ ({ toArray := as, size_toArray := ⋯ }.extract start stop)[i] = { toArray := as, size_toArray := ⋯ }[start + i]

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem borel_eq_generateFrom_Ioi_rat : borel ℝ = .generateFrom (⋃ a : ℚ, {Ioi (a : ℝ)})

Proof state:
⊢ ∀ t ∈ range Ioi, MeasurableSet t

Tactic:
rintro _ ⟨a, rfl⟩

Result:
case intro
a : ℝ
⊢ MeasurableSet (Ioi a)

Proof state:
a : ℝ
⊢ IsGLB (range Rat.cast ∩ Ioi a) a

Tactic:
simp [isGLB_iff_le_iff, mem_lowerBounds, ← le_iff_forall_lt_rat_imp_le]

Result:
no goals

Proof state:
case intro
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (Ioi a)

Tactic:
rw [← this.biUnion_Ioi_eq, ← image_univ, ← image_inter_preimage, univ_inter, biUnion_image]

Result:
case intro
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (⋃ y ∈ Rat.cast ⁻¹' Ioi a, Ioi ↑y)

Proof state:
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
b : ℚ
x✝ : b ∈ Rat.cast ⁻¹' Ioi a
⊢ Ioi ↑b ∈ ⋃ a, {Ioi ↑a}

Tactic:
simp

Result:
no goals

Proof state:
⊢ generateFrom (range Ioi) = generateFrom (⋃ a, {Ioi ↑a})

Tactic:
refine le_antisymm
  (generateFrom_le ?_)
  (generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)

Result:
⊢ ∀ t ∈ range Ioi, MeasurableSet t

Proof state:
case intro
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (⋃ y ∈ Rat.cast ⁻¹' Ioi a, Ioi ↑y)

Tactic:
exact MeasurableSet.biUnion (to_countable _)
  fun b _ => GenerateMeasurable.basic (Ioi (b : ℝ)) (by simp)

Result:
no goals

Proof state:
⊢ borel ℝ = generateFrom (⋃ a, {Ioi ↑a})

Tactic:
rw [borel_eq_generateFrom_Ioi]

Result:
⊢ generateFrom (range Ioi) = generateFrom (⋃ a, {Ioi ↑a})

Proof state:
case intro
a : ℝ
⊢ MeasurableSet (Ioi a)

Tactic:
have : IsGLB (range ((↑) : ℚ → ℝ) ∩ Ioi a) a := by
  simp [isGLB_iff_le_iff, mem_lowerBounds, ← le_iff_forall_lt_rat_imp_le]

Result:
case intro
a : ℝ
this : IsGLB (range Rat.cast ∩ Ioi a) a
⊢ MeasurableSet (Ioi a)
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem δ_comp_δ'' {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ Fin.castSucc j) :
    δ (i.castLT (Nat.lt_of_le_of_lt (Fin.le_iff_val_le_val.mp H) j.is_lt)) ≫ δ j.succ =
      δ j ≫ δ i

Proof state:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ i.castLT ⋯ ≤ j

Tactic:
exact H

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ δ (i.castLT ⋯) ≫ δ j.succ = δ j ≫ δ i

Tactic:
rw [δ_comp_δ]

Result:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ δ j ≫ δ (i.castLT ⋯).castSucc = δ j ≫ δ i

n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ i.castLT ⋯ ≤ j

Proof state:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ δ j ≫ δ (i.castLT ⋯).castSucc = δ j ≫ δ i

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffWithinAt_diff_singleton {y : E} :
    ContDiffWithinAt 𝕜 n f (s \ {y}) x ↔ ContDiffWithinAt 𝕜 n f s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
y : E
⊢ ContDiffWithinAt 𝕜 n f (s \ {y}) x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
rw [← contDiffWithinAt_insert, insert_diff_singleton, contDiffWithinAt_insert]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_X_pow_succ (n : ℕ) :
    derivative (X ^ (n + 1) : R[X]) = C (n + 1 : R) * X ^ n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ derivative (X ^ (n + 1)) = C (↑n + 1) * X ^ n

Tactic:
simp [derivative_X_pow]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem grundyValue_eq_sInf_moveLeft (G : PGame) :
    grundyValue G = sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ

Proof state:
G : PGame
⊢ G.grundyValue = sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ

Tactic:
rw [grundyValue]

Result:
G : PGame
⊢ sInf (Set.range fun i => (G.moveLeft i).grundyValue)ᶜ = sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ

Proof state:
G : PGame
⊢ sInf (Set.range fun i => (G.moveLeft i).grundyValue)ᶜ = sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem cons_inj_right (a : α) : ∀ {s t : Multiset α}, a ::ₘ s = a ::ₘ t ↔ s = t

Proof state:
α : Type u_1
a : α
⊢ ∀ {s t : Multiset α}, a ::ₘ s = a ::ₘ t ↔ s = t

Tactic:
rintro ⟨l₁⟩ ⟨l₂⟩

Result:
case mk.mk
α : Type u_1
a : α
s✝ : Multiset α
l₁ : List α
t✝ : Multiset α
l₂ : List α
⊢ a ::ₘ Quot.mk (⇑(isSetoid α)) l₁ = a ::ₘ Quot.mk (⇑(isSetoid α)) l₂ ↔
    Quot.mk (⇑(isSetoid α)) l₁ = Quot.mk (⇑(isSetoid α)) l₂

Proof state:
case mk.mk
α : Type u_1
a : α
s✝ : Multiset α
l₁ : List α
t✝ : Multiset α
l₂ : List α
⊢ a ::ₘ Quot.mk (⇑(isSetoid α)) l₁ = a ::ₘ Quot.mk (⇑(isSetoid α)) l₂ ↔
    Quot.mk (⇑(isSetoid α)) l₁ = Quot.mk (⇑(isSetoid α)) l₂

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem sym_inter (s t : Finset α) (n : ℕ) : (s ∩ t).sym n = s.sym n ∩ t.sym n

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
m : Sym α n
⊢ m ∈ (s ∩ t).sym n ↔ m ∈ s.sym n ∩ t.sym n

Tactic:
simp only [mem_inter, mem_sym_iff, imp_and, forall_and]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
⊢ (s ∩ t).sym n = s.sym n ∩ t.sym n

Tactic:
ext m

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
m : Sym α n
⊢ m ∈ (s ∩ t).sym n ↔ m ∈ s.sym n ∩ t.sym n
-- Mathlib/Data/Nat/Digits.lean
theorem dvd_iff_dvd_digits_sum (b b' : ℕ) (h : b' % b = 1) (n : ℕ) :
    b ∣ n ↔ b ∣ (digits b' n).sum

Proof state:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ ofDigits b' (b'.digits n) ↔ b ∣ ofDigits 1 (b'.digits n)

Tactic:
rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]

Result:
no goals

Proof state:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ ofDigits 1 (b'.digits n)

Tactic:
conv_lhs => rw [← ofDigits_digits b' n]

Result:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ ofDigits b' (b'.digits n) ↔ b ∣ ofDigits 1 (b'.digits n)

Proof state:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ (b'.digits n).sum

Tactic:
rw [← ofDigits_one]

Result:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ ofDigits 1 (b'.digits n)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem mergeSort_singleton (a : α) : [a].mergeSort r = [a]

Proof state:
α : Type u_1
r : α → α → Bool
a : α
⊢ [a].mergeSort r = [a]

Tactic:
rw [List.mergeSort]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem finset_inf_span_singleton {ι : Type*} (s : Finset ι) (I : ι → R)
    (hI : Set.Pairwise (↑s) (IsCoprime on I)) :
    (s.inf fun i => Ideal.span ({I i} : Set R)) = Ideal.span {∏ i ∈ s, I i}

Proof state:
case h
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s).Pairwise (IsCoprime on I)
x : R
⊢ (x ∈ s.inf fun i => span {I i}) ↔ x ∈ span {∏ i ∈ s, I i}

Tactic:
simp only [Submodule.mem_finset_inf, Ideal.mem_span_singleton]

Result:
case h
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s).Pairwise (IsCoprime on I)
x : R
⊢ (∀ i ∈ s, I i ∣ x) ↔ ∏ i ∈ s, I i ∣ x

Proof state:
case h
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s).Pairwise (IsCoprime on I)
x : R
⊢ (∀ i ∈ s, I i ∣ x) ↔ ∏ i ∈ s, I i ∣ x

Tactic:
exact ⟨Finset.prod_dvd_of_coprime hI, fun h i hi => (Finset.dvd_prod_of_mem _ hi).trans h⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s).Pairwise (IsCoprime on I)
⊢ (s.inf fun i => span {I i}) = span {∏ i ∈ s, I i}

Tactic:
ext x

Result:
case h
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s).Pairwise (IsCoprime on I)
x : R
⊢ (x ∈ s.inf fun i => span {I i}) ↔ x ∈ span {∏ i ∈ s, I i}
-- Mathlib/CategoryTheory/Galois/Decomposition.lean
theorem has_decomp_connected_components (X : C) :
    ∃ (ι : Type) (f : ι → C) (g : (i : ι) → f i ⟶ X) (_ : IsColimit (Cofan.mk X g)),
      (∀ i, IsConnected (f i)) ∧ Finite ι

Proof state:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
exact has_decomp_connected_components_aux F (Nat.card <| F.obj X) X rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
let F := GaloisCategory.getFiberFunctor C

Result:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
X : C
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_comp (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (x : E) (r : ℝ) :
    (p.comp f).closedBall x r = f ⁻¹' p.closedBall (f x) r

Proof state:
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
⊢ (p.comp f).closedBall x r = ⇑f ⁻¹' p.closedBall (f x) r

Tactic:
ext

Result:
case h
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ x✝ ∈ (p.comp f).closedBall x r ↔ x✝ ∈ ⇑f ⁻¹' p.closedBall (f x) r

Proof state:
case h
𝕜 : Type u_3
𝕜₂ : Type u_4
E : Type u_7
E₂ : Type u_8
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜₂ E₂
f : E →ₛₗ[σ₁₂] E₂
x : E
r : ℝ
x✝ : E
⊢ x✝ ∈ (p.comp f).closedBall x r ↔ x✝ ∈ ⇑f ⁻¹' p.closedBall (f x) r

Tactic:
simp_rw [closedBall, mem_preimage, comp_apply, Set.mem_setOf_eq, map_sub]

Result:
no goals
-- Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean
theorem Int.erdos_ginzburg_ziv_multiset (s : Multiset ℤ) (hs : 2 * n - 1 ≤ Multiset.card s) :
    ∃ t ≤ s, Multiset.card t = n ∧ ↑n ∣ t.sum

Proof state:
case intro.intro
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
t : Finset (ℤ × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ↑n ∣ ∑ i ∈ t, i.1
⊢ ∃ t ≤ s, t.card = n ∧ ↑n ∣ t.sum

Tactic:
exact ⟨t.1.map Prod.fst, Multiset.map_fst_le_of_subset_toEnumFinset hts, by simpa using ht⟩

Result:
no goals

Proof state:
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
t : Finset (ℤ × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ↑n ∣ ∑ i ∈ t, i.1
⊢ (Multiset.map Prod.fst t.val).card = n ∧ ↑n ∣ (Multiset.map Prod.fst t.val).sum

Tactic:
simpa using ht

Result:
no goals

Proof state:
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
⊢ ∃ t ≤ s, t.card = n ∧ ↑n ∣ t.sum

Tactic:
obtain ⟨t, hts, ht⟩ := Int.erdos_ginzburg_ziv (s := s.toEnumFinset) Prod.fst (by simpa using hs)

Result:
case intro.intro
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
t : Finset (ℤ × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ ↑n ∣ ∑ i ∈ t, i.1
⊢ ∃ t ≤ s, t.card = n ∧ ↑n ∣ t.sum

Proof state:
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
⊢ 2 * ?m.101950 - 1 ≤ #s.toEnumFinset

Tactic:
simpa using hs

Result:
no goals