harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Grade.lean
protected lemma isCoatom_iff : IsCoatom s ↔ ∃ a, s = {a}ᶜ

Proof state:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ IsCoatom s ↔ ∃ a, s = {a}ᶜ

Tactic:
simp_rw [← isAtom_compl, Finset.isAtom_iff, compl_eq_iff_isCompl, eq_compl_iff_isCompl]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem ball_eq_empty : ball x ε = ∅ ↔ ε ≤ 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ball x ε = ∅ ↔ ε ≤ 0

Tactic:
rw [← not_nonempty_iff_eq_empty, nonempty_ball, not_lt]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem pi_eq_generateFrom :
    Pi.topologicalSpace =
      generateFrom
        { g | ∃ (s : ∀ a, Set (π a)) (i : Finset ι), (∀ a ∈ i, IsOpen (s a)) ∧ g = pi (↑i) s } :=
  calc Pi.topologicalSpace
  _ = @Pi.topologicalSpace ι π fun _ => generateFrom { s | IsOpen s }

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
⊢ Pi.topologicalSpace = Pi.topologicalSpace

Tactic:
simp only [generateFrom_setOf_isOpen]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem pi_univ : Measure.pi μ univ = ∏ i, μ i univ

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
⊢ (Measure.pi μ) univ = ∏ i : ι, (μ i) univ

Tactic:
rw [← pi_univ, pi_pi μ]

Result:
no goals
-- Mathlib/Topology/Exterior.lean
theorem mem_exterior_iff_specializes : x ∈ exterior s ↔ ∃ y ∈ s, x ⤳ y := calc
  x ∈ exterior s ↔ x ∈ exterior (⋃ y ∈ s, {y})

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ exterior s ↔ x ∈ exterior (⋃ y ∈ s, {y})

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ exterior (⋃ y ∈ s, {y}) ↔ ∃ y ∈ s, x ⤳ y

Tactic:
simp only [exterior_iUnion, mem_exterior_singleton, mem_iUnion₂, exists_prop]

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem mem_support_iff (x : X) (a : FreeAbelianGroup X) : x ∈ a.support ↔ coeff x a ≠ 0

Proof state:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ (toFinsupp a) x ≠ 0 ↔ (coeff x) a ≠ 0

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∈ a.support ↔ (coeff x) a ≠ 0

Tactic:
rw [support, Finsupp.mem_support_iff]

Result:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ (toFinsupp a) x ≠ 0 ↔ (coeff x) a ≠ 0
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
@[simp] lemma support_pow (f : ι → M₀) (hn : n ≠ 0) : support (fun a ↦ f a ^ n) = support f

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
⊢ (support fun a => f a ^ n) = support f

Tactic:
ext

Result:
case h
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
x✝ : ι
⊢ (x✝ ∈ support fun a => f a ^ n) ↔ x✝ ∈ support f

Proof state:
case h
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MonoidWithZero M₀
inst✝ : NoZeroDivisors M₀
n : ℕ
f : ι → M₀
hn : n ≠ 0
x✝ : ι
⊢ (x✝ ∈ support fun a => f a ^ n) ↔ x✝ ∈ support f

Tactic:
exact (pow_eq_zero_iff hn).not

Result:
no goals
-- Mathlib/Data/Multiset/Dedup.lean
theorem dedup_map_of_injective [DecidableEq β] {f : α → β} (hf : Function.Injective f)
    (s : Multiset α) :
    (s.map f).dedup = s.dedup.map f :=
  Quot.induction_on s fun l => by simp [List.dedup_map_of_injective hf l]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
s : Multiset α
l : List α
⊢ (map f (Quot.mk (⇑(isSetoid α)) l)).dedup = map f (dedup (Quot.mk (⇑(isSetoid α)) l))

Tactic:
simp [List.dedup_map_of_injective hf l]

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_nat_pow_near_of_lt_one (xpos : 0 < x) (hx : x ≤ 1) (ypos : 0 < y) (hy : y < 1) :
    ∃ n : ℕ, y ^ (n + 1) < x ∧ x ≤ y ^ n

Proof state:
case intro.intro.refine_1
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ y ^ (n + 1) < x

Tactic:
rwa [inv_pow, inv_lt_inv₀ xpos (pow_pos ypos _)] at h'n

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n

Tactic:
refine ⟨n, ?_, ?_⟩

Result:
case intro.intro.refine_1
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ y ^ (n + 1) < x

case intro.intro.refine_2
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ x ≤ y ^ n

Proof state:
case intro.intro.refine_2
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ x ≤ y ^ n

Tactic:
rwa [inv_pow, inv_le_inv₀ (pow_pos ypos _) xpos] at hn

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
⊢ ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n

Tactic:
rcases exists_nat_pow_near (one_le_inv_iff₀.2 ⟨xpos, hx⟩) (one_lt_inv_iff₀.2 ⟨ypos, hy⟩) with
  ⟨n, hn, h'n⟩

Result:
case intro.intro
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n
-- Mathlib/Algebra/Module/LinearMap/End.lean
theorem _root_.Module.End_isUnit_apply_inv_apply_of_isUnit
    {f : Module.End R M} (h : IsUnit f) (x : M) :
    f (h.unit.inv x) = x :=
  show (f * h.unit.inv) x = x by simp

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : Module.End R M
h : IsUnit f
x : M
⊢ (f * h.unit.inv) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isTheta_cpow_const_rpow {b : ℂ} (hl : b.re = 0 → b ≠ 0 → ∀ᶠ x in l, f x ≠ 0) :
    (fun x => f x ^ b) =Θ[l] fun x => ‖f x‖ ^ b.re :=
  isTheta_cpow_rpow isBoundedUnder_const <| by
    simpa only [eventually_imp_distrib_right, not_imp_not, Imp.swap (a := b.re = 0)] using hl

Proof state:
α : Type u_1
l : Filter α
f : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ ∀ᶠ (x : α) in l, f x = 0 → b.re = 0 → b = 0

Tactic:
simpa only [eventually_imp_distrib_right, not_imp_not, Imp.swap (a := b.re = 0)] using hl

Result:
no goals
-- Mathlib/Data/Finsupp/Multiset.lean
theorem count_toMultiset [DecidableEq α] (f : α →₀ ℕ) (a : α) : (toMultiset f).count a = f a :=
  calc
    (toMultiset f).count a = Finsupp.sum f (fun x n => (n • {x} : Multiset α).count a)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ (f.sum fun x n => Multiset.count a (n • {x})) = f.sum fun x n => n * Multiset.count a {x}

Tactic:
simp only [Multiset.count_nsmul]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (toMultiset f) = f.sum fun x n => Multiset.count a (n • {x})

Tactic:
rw [toMultiset_apply]

Result:
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (f.sum fun a n => n • {a}) = f.sum fun x n => Multiset.count a (n • {x})

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ f a * Multiset.count a {a} = f a

Tactic:
rw [Multiset.count_singleton_self, mul_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a a' : α
x✝ : f a' ≠ 0
H : a' ≠ a
⊢ f a' * Multiset.count a {a'} = 0

Tactic:
simp only [Multiset.count_singleton, if_false, H.symm, mul_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (f.sum fun a n => n • {a}) = f.sum fun x n => Multiset.count a (n • {x})

Tactic:
exact map_sum (Multiset.countAddMonoidHom a) _ f.support

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_sub_two (n : ℤ) : T R (n - 2) = 2 * X * T R (n - 1) - T R n

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (n - 2) = 2 * X * T R (n - 1) - T R n

Tactic:
linear_combination (norm := ring_nf) T_add_two R (n - 2)

Result:
no goals
-- Mathlib/CategoryTheory/Category/Quiv.lean
lemma inv_map_hom_map_of_iso {V W : Quiv} (e : V ≅ W) {X Y : V} (f : X ⟶ Y) :
    e.inv.map (e.hom.map f) = Quiver.homOfEq f (by simp) (by simp) :=
  hom_map_inv_map_of_iso e.symm f

Proof state:
V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑V
f : X ⟶ Y
⊢ Y = e.inv.obj (e.hom.obj Y)

Tactic:
simp

Result:
no goals

Proof state:
V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑V
f : X ⟶ Y
⊢ X = e.inv.obj (e.hom.obj X)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem rotateRight_eq_rotateRightAux_of_lt {x : BitVec w} {r : Nat} (hr : r < w) :
    x.rotateRight r = x.rotateRightAux r

Proof state:
w : Nat
x : BitVec w
r : Nat
hr : r < w
⊢ x.rotateRight r = x.rotateRightAux r

Tactic:
simp only [rotateRight, Nat.mod_eq_of_lt hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem sub_sub_self (a b : Int) : a - (a - b) = b

Proof state:
a b : Int
⊢ a - (a - b) = b

Tactic:
simp [Int.sub_eq_add_neg, ← Int.add_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
lemma measurableAtom_subset {s : Set β} {x : β} (hs : MeasurableSet s) (hx : x ∈ s) :
    measurableAtom x ⊆ s :=
  iInter₂_subset_of_subset s hx fun ⦃a⦄ ↦ (by simp [hs])

Proof state:
β : Type u_2
inst✝ : MeasurableSpace β
s : Set β
x : β
hs : MeasurableSet s
hx : x ∈ s
a : β
⊢ a ∈ ⋂ (_ : MeasurableSet s), s → a ∈ s

Tactic:
simp [hs]

Result:
no goals
-- Mathlib/CategoryTheory/Elements.lean
lemma Functor.Elements.ext {F : C ⥤ Type w} (x y : F.Elements) (h₁ : x.fst = y.fst)
    (h₂ : F.map (eqToHom h₁) x.snd = y.snd) : x = y

Proof state:
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝ : C
snd✝¹ snd✝ : F.obj fst✝
h₂ : F.map (eqToHom ⋯) ⟨fst✝, snd✝¹⟩.snd = ⟨fst✝, snd✝⟩.snd
⊢ ⟨fst✝, snd✝¹⟩ = ⟨fst✝, snd✝⟩

Tactic:
simp only [eqToHom_refl, FunctorToTypes.map_id_apply] at h₂

Result:
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝ : C
snd✝¹ snd✝ : F.obj fst✝
h₂ : snd✝¹ = snd✝
⊢ ⟨fst✝, snd✝¹⟩ = ⟨fst✝, snd✝⟩

Proof state:
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝ : C
snd✝¹ snd✝ : F.obj fst✝
h₂ : snd✝¹ = snd✝
⊢ ⟨fst✝, snd✝¹⟩ = ⟨fst✝, snd✝⟩

Tactic:
simp [h₂]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
x y : F.Elements
h₁ : x.fst = y.fst
h₂ : F.map (eqToHom h₁) x.snd = y.snd
⊢ x = y

Tactic:
cases x

Result:
case mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
y : F.Elements
fst✝ : C
snd✝ : F.obj fst✝
h₁ : ⟨fst✝, snd✝⟩.fst = y.fst
h₂ : F.map (eqToHom h₁) ⟨fst✝, snd✝⟩.snd = y.snd
⊢ ⟨fst✝, snd✝⟩ = y

Proof state:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝¹ : C
snd✝¹ : F.obj fst✝¹
fst✝ : C
snd✝ : F.obj fst✝
h₁ : ⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fst
h₂ : F.map (eqToHom h₁) ⟨fst✝¹, snd✝¹⟩.snd = ⟨fst✝, snd✝⟩.snd
⊢ ⟨fst✝¹, snd✝¹⟩ = ⟨fst✝, snd✝⟩

Tactic:
cases h₁

Result:
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝ : C
snd✝¹ snd✝ : F.obj fst✝
h₂ : F.map (eqToHom ⋯) ⟨fst✝, snd✝¹⟩.snd = ⟨fst✝, snd✝⟩.snd
⊢ ⟨fst✝, snd✝¹⟩ = ⟨fst✝, snd✝⟩

Proof state:
case mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
y : F.Elements
fst✝ : C
snd✝ : F.obj fst✝
h₁ : ⟨fst✝, snd✝⟩.fst = y.fst
h₂ : F.map (eqToHom h₁) ⟨fst✝, snd✝⟩.snd = y.snd
⊢ ⟨fst✝, snd✝⟩ = y

Tactic:
cases y

Result:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝¹ : C
snd✝¹ : F.obj fst✝¹
fst✝ : C
snd✝ : F.obj fst✝
h₁ : ⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fst
h₂ : F.map (eqToHom h₁) ⟨fst✝¹, snd✝¹⟩.snd = ⟨fst✝, snd✝⟩.snd
⊢ ⟨fst✝¹, snd✝¹⟩ = ⟨fst✝, snd✝⟩
-- Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
theorem min_lexOrder_le {φ ψ : MvPowerSeries σ R} :
    min (lexOrder φ) (lexOrder ψ) ≤ lexOrder (φ + ψ)

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
⊢ φ.lexOrder ⊓ ψ.lexOrder ≤ (φ + ψ).lexOrder

Tactic:
rw [le_lexOrder_iff]

Result:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
⊢ ∀ (d : σ →₀ ℕ), ↑(toLex d) < φ.lexOrder ⊓ ψ.lexOrder → (coeff R d) (φ + ψ) = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
⊢ ∀ (d : σ →₀ ℕ), ↑(toLex d) < φ.lexOrder ⊓ ψ.lexOrder → (coeff R d) (φ + ψ) = 0

Tactic:
intro d hd

Result:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder ⊓ ψ.lexOrder
⊢ (coeff R d) (φ + ψ) = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder ∧ ↑(toLex d) < ψ.lexOrder
⊢ (coeff R d) (φ + ψ) = 0

Tactic:
rw [map_add, coeff_eq_zero_of_lt_lexOrder hd.1, coeff_eq_zero_of_lt_lexOrder hd.2, add_zero]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder ⊓ ψ.lexOrder
⊢ (coeff R d) (φ + ψ) = 0

Tactic:
simp only [lt_min_iff] at hd

Result:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder ∧ ↑(toLex d) < ψ.lexOrder
⊢ (coeff R d) (φ + ψ) = 0
-- Mathlib/Data/Set/Image.lean
theorem preimage_inl_range_inr : Sum.inl ⁻¹' range (Sum.inr : β → α ⊕ β) = ∅

Proof state:
α : Type u_1
β : Type u_2
⊢ Sum.inl ⁻¹' range Sum.inr = ∅

Tactic:
rw [← image_univ, preimage_inl_image_inr]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem coeff_mul_right_one_sub_of_lt_weightedOrder
    {d : σ →₀ ℕ} (h : (weight w d) < g.weightedOrder w) :
    coeff R d ((1 - g) * f) = coeff R d f

Proof state:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ ↑((weight w) d) < weightedOrder w (g * f)

Tactic:
apply lt_of_lt_of_le (lt_of_lt_of_le h le_self_add) (le_weightedOrder_mul w)

Result:
no goals

Proof state:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ (coeff R d) (g * f) = 0

Tactic:
apply coeff_eq_zero_of_lt_weightedOrder w

Result:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ ↑((weight w) d) < weightedOrder w (g * f)

Proof state:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ (coeff R d) ((1 - g) * f) = (coeff R d) f

Tactic:
simp only [sub_mul, one_mul, _root_.map_sub, sub_eq_self]

Result:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ (coeff R d) (g * f) = 0
-- Mathlib/Data/Nat/Choose/Central.lean
theorem four_pow_le_two_mul_self_mul_centralBinom :
    ∀ (n : ℕ) (_ : 0 < n), 4 ^ n ≤ 2 * n * centralBinom n
  | 0, pr => (Nat.not_lt_zero _ pr).elim
  | 1, _ => by norm_num [centralBinom, choose]
  | 2, _ => by norm_num [centralBinom, choose]
  | 3, _ => by norm_num [centralBinom, choose]
  | n + 4, _ =>
    calc
      4 ^ (n+4) ≤ (n+4) * centralBinom (n+4) := (four_pow_lt_mul_centralBinom _ le_add_self).le
      _ ≤ 2 * (n+4) * centralBinom (n+4)

Proof state:
x✝ : 0 < 1
⊢ 4 ^ 1 ≤ 2 * 1 * centralBinom 1

Tactic:
norm_num [centralBinom, choose]

Result:
no goals

Proof state:
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * ((n + 4) * (n + 4).centralBinom)

Tactic:
refine Nat.le_mul_of_pos_left _ zero_lt_two

Result:
no goals

Proof state:
x✝ : 0 < 3
⊢ 4 ^ 3 ≤ 2 * 3 * centralBinom 3

Tactic:
norm_num [centralBinom, choose]

Result:
no goals

Proof state:
x✝ : 0 < 2
⊢ 4 ^ 2 ≤ 2 * 2 * centralBinom 2

Tactic:
norm_num [centralBinom, choose]

Result:
no goals

Proof state:
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * (n + 4) * (n + 4).centralBinom

Tactic:
rw [mul_assoc]

Result:
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * ((n + 4) * (n + 4).centralBinom)
-- Mathlib/Analysis/Convex/Segment.lean
theorem mem_openSegment_of_ne_left_right (hx : x ≠ z) (hy : y ≠ z) (hz : z ∈ [x -[𝕜] y]) :
    z ∈ openSegment 𝕜 x y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ insert x (insert y (openSegment 𝕜 x y))
⊢ z ∈ openSegment 𝕜 x y

Tactic:
exact (hz.resolve_left hx.symm).resolve_left hy.symm

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ [x-[𝕜]y]
⊢ z ∈ openSegment 𝕜 x y

Tactic:
rw [← insert_endpoints_openSegment] at hz

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ insert x (insert y (openSegment 𝕜 x y))
⊢ z ∈ openSegment 𝕜 x y
-- Mathlib/Data/NNReal/Defs.lean
theorem _root_.Real.toNNReal_div {x y : ℝ} (hx : 0 ≤ x) :
    Real.toNNReal (x / y) = Real.toNNReal x / Real.toNNReal y

Proof state:
x y : ℝ
hx : 0 ≤ x
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ← Real.toNNReal_inv, ← Real.toNNReal_mul hx]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem cycleType_extendDomain {β : Type*} [Fintype β] [DecidableEq β] {p : β → Prop}
    [DecidablePred p] (f : α ≃ Subtype p) {g : Perm α} :
    cycleType (g.extendDomain f) = cycleType g

Proof state:
case induction_disjoint
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : (σ.extendDomain f).cycleType = σ.cycleType
hτ : (τ.extendDomain f).cycleType = τ.cycleType
⊢ ((σ * τ).extendDomain f).cycleType = (σ * τ).cycleType

Tactic:
rw [hd.cycleType, ← extendDomain_mul, (hd.extendDomain f).cycleType, hσ, hτ]

Result:
no goals

Proof state:
case base_cycles
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ : Perm α
hσ : σ.IsCycle
⊢ (σ.extendDomain f).cycleType = σ.cycleType

Tactic:
rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]

Result:
no goals

Proof state:
case base_one
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ (extendDomain 1 f).cycleType = cycleType 1

Tactic:
rw [extendDomain_one, cycleType_one, cycleType_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
β : Type u_2
inst✝² : Fintype β
inst✝¹ : DecidableEq β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ (g.extendDomain f).cycleType = g.cycleType

Tactic:
induction g using cycle_induction_on with
| base_one => rw [extendDomain_one, cycleType_one, cycleType_one]
| base_cycles σ hσ =>
  rw [(hσ.extendDomain f).cycleType, hσ.cycleType, card_support_extend_domain]
| induction_disjoint σ τ hd _ hσ hτ =>
  rw [hd.cycleType, ← extendDomain_mul, (hd.extendDomain f).cycleType, hσ, hτ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem rootSet_def (p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] [DecidableEq S] :
    p.rootSet S = (p.aroots S).toFinset

Proof state:
T : Type w
inst✝⁴ : CommRing T
p : T[X]
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : DecidableEq S
⊢ ↑(p.aroots S).toFinset = ↑(p.aroots S).toFinset

Tactic:
convert rfl

Result:
no goals

Proof state:
T : Type w
inst✝⁴ : CommRing T
p : T[X]
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : DecidableEq S
⊢ p.rootSet S = ↑(p.aroots S).toFinset

Tactic:
rw [rootSet]

Result:
T : Type w
inst✝⁴ : CommRing T
p : T[X]
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : DecidableEq S
⊢ ↑(p.aroots S).toFinset = ↑(p.aroots S).toFinset
-- Mathlib/Algebra/Homology/Single.lean
theorem single_map_f_self (j : ι) {A B : V} (f : A ⟶ B) :
    ((single V c j).map f).f j = (singleObjXSelf c j A).hom ≫
      f ≫ (singleObjXSelf c j B).inv

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : A ⟶ B
⊢ eqToHom ⋯ ≫ f ≫ eqToHom ⋯ = (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : A ⟶ B
⊢ (if h : j = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) = (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv

Tactic:
rw [dif_pos rfl]

Result:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : A ⟶ B
⊢ eqToHom ⋯ ≫ f ≫ eqToHom ⋯ = (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : A ⟶ B
⊢ ((single V c j).map f).f j = (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv

Tactic:
dsimp [single]

Result:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : A ⟶ B
⊢ (if h : j = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) = (singleObjXSelf c j A).hom ≫ f ≫ (singleObjXSelf c j B).inv
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem any_iff (s : String) (p : Char → Bool) : any s p ↔ ∃ c ∈ s.1, p c

Proof state:
s : String
p : Char → Bool
⊢ s.any p = true ↔ ∃ c, c ∈ s.data ∧ p c = true

Tactic:
simp [any_eq]

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Basic.lean
theorem tendsto_iff_ultrafilter (f : α → β) (l₁ : Filter α) (l₂ : Filter β) :
    Tendsto f l₁ l₂ ↔ ∀ g : Ultrafilter α, ↑g ≤ l₁ → Tendsto f g l₂

Proof state:
α : Type u
β : Type v
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ Tendsto f l₁ l₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ l₁ → Tendsto f (↑g) l₂

Tactic:
simpa only [tendsto_iff_comap] using le_iff_ultrafilter

Result:
no goals