harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Cycle.lean
theorem lists_nil : lists (@nil α) = [([] : List α)]

Proof state:
α : Type u_1
⊢ nil.lists = ↑[[]]

Tactic:
rw [nil, lists_coe, cyclicPermutations_nil]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma biUnion_supp_eq_supp {G G' : SimpleGraph V} (h : G ≤ G') (c' : ConnectedComponent G') :
    ⋃ (c : ConnectedComponent G) (_ : c.supp ⊆ c'.supp), c.supp = c'.supp

Proof state:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ v ∈ c'.supp → ∃ i, ∃ (_ : i.supp ⊆ c'.supp), v ∈ i.supp

Tactic:
intro hv

Result:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
⊢ ∃ i, ∃ (_ : i.supp ⊆ c'.supp), v ∈ i.supp

Proof state:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
⊢ v ∈ (G.connectedComponentMk v).supp

Tactic:
simp only [mem_supp_iff]

Result:
no goals

Proof state:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
⊢ ∃ i, ∃ (_ : i.supp ⊆ c'.supp), v ∈ i.supp

Tactic:
use G.connectedComponentMk v

Result:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
⊢ ∃ (_ : (G.connectedComponentMk v).supp ⊆ c'.supp), v ∈ (G.connectedComponentMk v).supp

Proof state:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
⊢ ∃ (_ : (G.connectedComponentMk v).supp ⊆ c'.supp), v ∈ (G.connectedComponentMk v).supp

Tactic:
use c'.connectedComponentMk_supp_subset_supp h hv

Result:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
⊢ v ∈ (G.connectedComponentMk v).supp

Proof state:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
⊢ ⋃ c, ⋃ (_ : c.supp ⊆ c'.supp), c.supp = c'.supp

Tactic:
ext v

Result:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ v ∈ ⋃ c, ⋃ (_ : c.supp ⊆ c'.supp), c.supp ↔ v ∈ c'.supp

Proof state:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ v ∈ ⋃ c, ⋃ (_ : c.supp ⊆ c'.supp), c.supp ↔ v ∈ c'.supp

Tactic:
simp_rw [Set.mem_iUnion]

Result:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ (∃ i, ∃ (_ : i.supp ⊆ c'.supp), v ∈ i.supp) ↔ v ∈ c'.supp

Proof state:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ (∃ i, ∃ (_ : i.supp ⊆ c'.supp), v ∈ i.supp) ↔ v ∈ c'.supp

Tactic:
refine ⟨fun ⟨_, ⟨hi, hi'⟩⟩ ↦ hi hi', ?_⟩

Result:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ v ∈ c'.supp → ∃ i, ∃ (_ : i.supp ⊆ c'.supp), v ∈ i.supp
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem prod_pow_factorization_eq_self {f : ℕ →₀ ℕ} (hf : ∀ p : ℕ, p ∈ f.support → Prime p) :
    (f.prod (· ^ ·)).factorization = f

Proof state:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
h : ∀ x ∈ f.support, x ^ f x ≠ 0
⊢ (f.prod fun x1 x2 => x1 ^ x2).factorization = f

Tactic:
simp only [Finsupp.prod, factorization_prod h]

Result:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
h : ∀ x ∈ f.support, x ^ f x ≠ 0
⊢ ∑ x ∈ f.support, (x ^ f x).factorization = f

Proof state:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
h : ∀ x ∈ f.support, x ^ f x ≠ 0
⊢ ∑ x ∈ f.support, (x ^ f x).factorization = f.sum single

Tactic:
exact sum_congr rfl fun p hp => Prime.factorization_pow (hf p hp)

Result:
no goals

Proof state:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ (f.prod fun x1 x2 => x1 ^ x2).factorization = f

Tactic:
have h : ∀ x : ℕ, x ∈ f.support → x ^ f x ≠ 0 := fun p hp =>
  pow_ne_zero _ (Prime.ne_zero (hf p hp))

Result:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
h : ∀ x ∈ f.support, x ^ f x ≠ 0
⊢ (f.prod fun x1 x2 => x1 ^ x2).factorization = f

Proof state:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
h : ∀ x ∈ f.support, x ^ f x ≠ 0
⊢ ∑ x ∈ f.support, (x ^ f x).factorization = f

Tactic:
conv =>
  rhs
  rw [(sum_single f).symm]

Result:
f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
h : ∀ x ∈ f.support, x ^ f x ≠ 0
⊢ ∑ x ∈ f.support, (x ^ f x).factorization = f.sum single
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive nsmul_add] lemma mul_pow (a b : M) : ∀ n, (a * b) ^ n = a ^ n * b ^ n
  | 0 => by rw [pow_zero, pow_zero, pow_zero, one_mul]
  | n + 1 => by rw [pow_succ', pow_succ', pow_succ', mul_pow, mul_mul_mul_comm]

Proof state:
M : Type u_4
inst✝ : CommMonoid M
a b : M
⊢ (a * b) ^ 0 = a ^ 0 * b ^ 0

Tactic:
rw [pow_zero, pow_zero, pow_zero, one_mul]

Result:
no goals

Proof state:
M : Type u_4
inst✝ : CommMonoid M
a b : M
n : ℕ
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)

Tactic:
rw [pow_succ', pow_succ', pow_succ', mul_pow, mul_mul_mul_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem MeasurePreserving.lintegral_comp {mb : MeasurableSpace β} {ν : Measure β} {g : α → β}
    (hg : MeasurePreserving g μ ν) {f : β → ℝ≥0∞} (hf : Measurable f) :
    ∫⁻ a, f (g a) ∂μ = ∫⁻ b, f b ∂ν

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mb : MeasurableSpace β
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
f : β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν

Tactic:
rw [← hg.map_eq, lintegral_map hf hg.measurable]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem norm_pos {x : ℤ[i]} : 0 < norm x ↔ x ≠ 0

Proof state:
x : ℤ[i]
⊢ 0 ≤ norm x ∧ ¬x = 0 ↔ x ≠ 0

Tactic:
simp [norm_nonneg]

Result:
no goals

Proof state:
x : ℤ[i]
⊢ 0 < norm x ↔ x ≠ 0

Tactic:
rw [lt_iff_le_and_ne, Ne, eq_comm, norm_eq_zero]

Result:
x : ℤ[i]
⊢ 0 ≤ norm x ∧ ¬x = 0 ↔ x ≠ 0
-- Mathlib/Data/Fin/Rev.lean
lemma succAbove_rev_left (p : Fin (n + 1)) (i : Fin n) :
    p.rev.succAbove i = (p.succAbove i.rev).rev

Proof state:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
obtain h | h := (rev p).succ_le_or_le_castSucc i

Result:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Proof state:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
rw [succAbove_of_le_castSucc _ _ h,
  succAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), rev_castSucc, rev_rev]

Result:
no goals

Proof state:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
rw [succAbove_of_succ_le _ _ h,
  succAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), rev_succ, rev_rev]

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Basic.lean
theorem smul {α M : Type*} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) (a : α)
    {w x : M} (h : c w x) : c (a • w) (a • x)

Proof state:
α : Type u_4
M : Type u_5
inst✝² : MulOneClass M
inst✝¹ : SMul α M
inst✝ : IsScalarTower α M M
c : Con M
a : α
w x : M
h : c w x
⊢ c (a • w) (a • x)

Tactic:
simpa only [smul_one_mul] using c.mul (c.refl' (a • (1 : M) : M)) h

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem measurableSet_of_differentiableWithinAt_Ici :
    MeasurableSet { x | DifferentiableWithinAt ℝ f (Ici x) x }

Proof state:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
inst✝ : CompleteSpace F
this : IsComplete univ
⊢ MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x}

Tactic:
convert measurableSet_of_differentiableWithinAt_Ici_of_isComplete f this

Result:
case h.e'_3.h.e'_2.h.a
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
inst✝ : CompleteSpace F
this : IsComplete univ
x✝ : ℝ
⊢ DifferentiableWithinAt ℝ f (Ici x✝) x✝ ↔ DifferentiableWithinAt ℝ f (Ici x✝) x✝ ∧ derivWithin f (Ici x✝) x✝ ∈ univ

Proof state:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
inst✝ : CompleteSpace F
⊢ MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x}

Tactic:
have : IsComplete (univ : Set F) := complete_univ

Result:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
inst✝ : CompleteSpace F
this : IsComplete univ
⊢ MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x}

Proof state:
case h.e'_3.h.e'_2.h.a
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
inst✝ : CompleteSpace F
this : IsComplete univ
x✝ : ℝ
⊢ DifferentiableWithinAt ℝ f (Ici x✝) x✝ ↔ DifferentiableWithinAt ℝ f (Ici x✝) x✝ ∧ derivWithin f (Ici x✝) x✝ ∈ univ

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem equivFunOnFinite_symm_eq_sum [Fintype α] [AddCommMonoid M] (f : α → M) :
    equivFunOnFinite.symm f = ∑ a, Finsupp.single a (f a)

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α → M
⊢ equivFunOnFinite.symm f = ∑ a : α, single a (f a)

Tactic:
rw [← univ_sum_single (equivFunOnFinite.symm f)]

Result:
α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α → M
⊢ ∑ a : α, single a ((equivFunOnFinite.symm f) a) = ∑ a : α, single a (f a)

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α → M
⊢ ∑ a : α, single a ((equivFunOnFinite.symm f) a) = ∑ a : α, single a (f a)

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α → M
a✝ : α
⊢ (∑ a : α, single a ((equivFunOnFinite.symm f) a)) a✝ = (∑ a : α, single a (f a)) a✝

Proof state:
case h
α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α → M
a✝ : α
⊢ (∑ a : α, single a ((equivFunOnFinite.symm f) a)) a✝ = (∑ a : α, single a (f a)) a✝

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem subset_countable_closure_of_compact {s : Set α} (hs : IsCompact s) :
    ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t

Proof state:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
t : Set α
htf : t.Finite
hst : s ⊆ ⋃ y ∈ t, ball y ε
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε

Tactic:
exact ⟨t, htf.countable, hst.trans <| iUnion₂_mono fun _ _ => ball_subset_closedBall⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε

Tactic:
rcases totallyBounded_iff'.1 hs.totallyBounded ε hε with ⟨t, -, htf, hst⟩

Result:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
t : Set α
htf : t.Finite
hst : s ⊆ ⋃ y ∈ t, ball y ε
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

Tactic:
refine subset_countable_closure_of_almost_dense_set s fun ε hε => ?_

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem rescale_rescale (f : R⟦X⟧) (a b : R) :
    rescale b (rescale a f) = rescale (a * b) f

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
⊢ (rescale b) ((rescale a) f) = (rescale (a * b)) f

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
n : ℕ
⊢ (coeff R n) ((rescale b) ((rescale a) f)) = (coeff R n) ((rescale (a * b)) f)

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
n : ℕ
⊢ (coeff R n) ((rescale b) ((rescale a) f)) = (coeff R n) ((rescale (a * b)) f)

Tactic:
simp_rw [coeff_rescale]

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
n : ℕ
⊢ b ^ n * (a ^ n * (coeff R n) f) = (a * b) ^ n * (coeff R n) f

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
n : ℕ
⊢ b ^ n * (a ^ n * (coeff R n) f) = (a * b) ^ n * (coeff R n) f

Tactic:
rw [mul_pow, mul_comm _ (b ^ n), mul_assoc]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem adjunction_counit_app_self {X : TopCat} (U : Opens X) :
    U.isOpenEmbedding.isOpenMap.adjunction.counit.app U = eqToHom (by simp) := Subsingleton.elim _ _

Proof state:
X : TopCat
U : Opens ↑X
⊢ (map U.inclusion' ⋙ ⋯.functor).obj U = (𝟭 (Opens ↑X)).obj U

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinaryHeap.lean
theorem size_pos_of_max {self : BinaryHeap α lt} (h : self.max = some x) : 0 < self.size

Proof state:
case isTrue
α : Type u_1
lt : α → α → Bool
x : α
self : BinaryHeap α lt
h✝ : 0 < self.arr.size
h : some self.arr[0] = some x
⊢ 0 < self.size

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
lt : α → α → Bool
x : α
self : BinaryHeap α lt
h : self.max = some x
⊢ 0 < self.size

Tactic:
simp only [max, getElem?_def] at h

Result:
α : Type u_1
lt : α → α → Bool
x : α
self : BinaryHeap α lt
h : (if h : 0 < self.arr.size then some self.arr[0] else none) = some x
⊢ 0 < self.size

Proof state:
case isFalse
α : Type u_1
lt : α → α → Bool
x : α
self : BinaryHeap α lt
h✝ : ¬0 < self.arr.size
h : none = some x
⊢ 0 < self.size

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
lt : α → α → Bool
x : α
self : BinaryHeap α lt
h : (if h : 0 < self.arr.size then some self.arr[0] else none) = some x
⊢ 0 < self.size

Tactic:
split at h

Result:
case isTrue
α : Type u_1
lt : α → α → Bool
x : α
self : BinaryHeap α lt
h✝ : 0 < self.arr.size
h : some self.arr[0] = some x
⊢ 0 < self.size

case isFalse
α : Type u_1
lt : α → α → Bool
x : α
self : BinaryHeap α lt
h✝ : ¬0 < self.arr.size
h : none = some x
⊢ 0 < self.size
-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
lemma exists_image_comap_of_monic (f g : R[X]) (hg : g.Monic) :
    ∃ t : Finset R, comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus t)ᶜ

Proof state:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ ∃ t, ⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ

Tactic:
apply (config := { allowSynthFailures := true }) exists_image_comap_of_finite_of_free

Result:
case inst
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Finite R (R[X] ⧸ Ideal.span {g})

case inst
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Free R (R[X] ⧸ Ideal.span {g})

Proof state:
case inst
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Free R (R[X] ⧸ Ideal.span {g})

Tactic:
exact .of_basis (AdjoinRoot.powerBasis' hg).basis

Result:
no goals

Proof state:
case inst
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Finite R (R[X] ⧸ Ideal.span {g})

Tactic:
exact .of_basis (AdjoinRoot.powerBasis' hg).basis

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_congr (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} :
    f =O[𝓝 b] g ↔ (f ∘ e) =O[𝓝 (e.symm b)] (g ∘ e)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ f =O[𝓝 b] g ↔ (f ∘ ⇑e) =O[𝓝 (e.symm b)] (g ∘ ⇑e)

Tactic:
simp only [IsBigO_def]

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ (∃ c, IsBigOWith c (𝓝 b) f g) ↔ ∃ c, IsBigOWith c (𝓝 (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : α ≃ₜ β
b : β
f : β → E
g : β → F
⊢ (∃ c, IsBigOWith c (𝓝 b) f g) ↔ ∃ c, IsBigOWith c (𝓝 (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)

Tactic:
exact exists_congr fun C => e.isBigOWith_congr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.count_toArray [BEq α] (l : List α) (a : α) : count a l.toArray = l.count a

Proof state:
α : Type u_1
inst✝ : BEq α
l : List α
a : α
⊢ count a l.toArray = List.count a l

Tactic:
simp [count, List.count_eq_countP]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma zeroLocus_minimalPrimes :
    zeroLocus ∘ (↑) '' minimalPrimes R =
    irreducibleComponents (PrimeSpectrum R)

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ zeroLocus ∘ SetLike.coe '' minimalPrimes R = irreducibleComponents (PrimeSpectrum R)

Tactic:
rw [← vanishingIdeal_irreducibleComponents, ← Set.image_comp, Set.EqOn.image_eq_self]

Result:
R : Type u
inst✝ : CommSemiring R
⊢ Set.EqOn ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) id (irreducibleComponents (PrimeSpectrum R))

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ Set.EqOn ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) id (irreducibleComponents (PrimeSpectrum R))

Tactic:
intros s hs

Result:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : s ∈ irreducibleComponents (PrimeSpectrum R)
⊢ ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) s = id s

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : s ∈ irreducibleComponents (PrimeSpectrum R)
⊢ ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) s = id s

Tactic:
simpa [zeroLocus_vanishingIdeal_eq_closure, closure_eq_iff_isClosed]
  using isClosed_of_mem_irreducibleComponents s hs

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem of_irreducible_expand_pow {p : ℕ} (hp : p ≠ 0) {f : R[X]} {n : ℕ} :
    Irreducible (expand R (p ^ n) f) → Irreducible f :=
  Nat.recOn n (fun hf => by rwa [pow_zero, expand_one] at hf) fun n ih hf =>
    ih <| of_irreducible_expand hp <| by
      rw [pow_succ'] at hf
      rwa [expand_expand]

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f
hf : Irreducible ((expand R (p * p ^ n)) f)
⊢ Irreducible ((expand R p) ((expand R (p ^ n)) f))

Tactic:
rwa [expand_expand]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f
hf : Irreducible ((expand R (p ^ n.succ)) f)
⊢ Irreducible ((expand R p) ((expand R (p ^ n)) f))

Tactic:
rw [pow_succ'] at hf

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible ((expand R (p ^ n)) f) → Irreducible f
hf : Irreducible ((expand R (p * p ^ n)) f)
⊢ Irreducible ((expand R p) ((expand R (p ^ n)) f))

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hf : Irreducible ((expand R (p ^ Nat.zero)) f)
⊢ Irreducible f

Tactic:
rwa [pow_zero, expand_one] at hf

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem toList_sorted (s : CompositionSeries X) : s.toList.Sorted (· < ·) :=
  List.pairwise_iff_get.2 fun i j h => by
    dsimp only [RelSeries.toList]
    rw [List.get_ofFn, List.get_ofFn]
    exact s.strictMono h

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (toList s).length
h : i < j
⊢ (toList s).get i < (toList s).get j

Tactic:
dsimp only [RelSeries.toList]

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (toList s).length
h : i < j
⊢ (List.ofFn s.toFun).get i < (List.ofFn s.toFun).get j

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (toList s).length
h : i < j
⊢ (List.ofFn s.toFun).get i < (List.ofFn s.toFun).get j

Tactic:
rw [List.get_ofFn, List.get_ofFn]

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (toList s).length
h : i < j
⊢ s.toFun (Fin.cast ⋯ i) < s.toFun (Fin.cast ⋯ j)

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (toList s).length
h : i < j
⊢ s.toFun (Fin.cast ⋯ i) < s.toFun (Fin.cast ⋯ j)

Tactic:
exact s.strictMono h

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem card_eq_card_quotient_mul_card (S : Submodule R M) :
    Nat.card M = Nat.card S * Nat.card (M ⧸ S)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
⊢ Nat.card M = Nat.card ↥S * Nat.card (M ⧸ S)

Tactic:
rw [mul_comm, ← Nat.card_prod]

Result:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
⊢ Nat.card M = Nat.card ((M ⧸ S) × ↥S)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
⊢ Nat.card M = Nat.card ((M ⧸ S) × ↥S)

Tactic:
exact Nat.card_congr AddSubgroup.addGroupEquivQuotientProdAddSubgroup

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean
theorem gaugeSeminormFamily_ball (s : AbsConvexOpenSets 𝕜 E) :
    (gaugeSeminormFamily 𝕜 E s).ball 0 1 = (s : Set E)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ {y | gauge (↑s) y < 1} = ↑s

Tactic:
exact gauge_lt_one_eq_self_of_isOpen s.coe_convex s.coe_zero_mem s.coe_isOpen

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ {y | (gaugeSeminorm ⋯ ⋯ ⋯) y < 1} = ↑s

Tactic:
simp_rw [gaugeSeminorm_toFun]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ {y | gauge (↑s) y < 1} = ↑s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ (gaugeSeminorm ⋯ ⋯ ⋯).ball 0 1 = ↑s

Tactic:
rw [Seminorm.ball_zero_eq]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ {y | (gaugeSeminorm ⋯ ⋯ ⋯) y < 1} = ↑s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ (gaugeSeminormFamily 𝕜 E s).ball 0 1 = ↑s

Tactic:
dsimp only [gaugeSeminormFamily]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ (gaugeSeminorm ⋯ ⋯ ⋯).ball 0 1 = ↑s
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem HeapNode.WF.toHeap {s : HeapNode α} (h : s.WF le a n) : s.toHeap.WF le 0 :=
  go h trivial
where
  go {res} : ∀ {n s}, s.WF le a n → res.WF le s.rank → (HeapNode.toHeap.go s s.rank res).WF le 0
  | _, .nil, _, hr => hr
  | _, .node a c s, ⟨n, rfl, _, h, h'⟩, hr =>
    go (s := s) h' ⟨Nat.le_refl _, by rw [← h'.rank_eq] at h; exact h, hr⟩

Proof state:
α : Type u_1
le : α → α → Bool
a✝ : α
n✝ : Nat
s✝ : HeapNode α
h✝ : WF le a✝ s✝ n✝
res : Heap α
a : α
c s : HeapNode α
n : Nat
left✝ : ∀ [inst : TotalBLE le], le a✝ a = true
h : WF le a c s.rank
h' : WF le a✝ s n
hr : Heap.WF le (node a c s).rank res
⊢ WF le a c ((node a c s).rank - 1)

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
a✝ : α
n✝ : Nat
s✝ : HeapNode α
h✝ : WF le a✝ s✝ n✝
res : Heap α
a : α
c s : HeapNode α
n : Nat
left✝ : ∀ [inst : TotalBLE le], le a✝ a = true
h : WF le a c n
h' : WF le a✝ s n
hr : Heap.WF le (node a c s).rank res
⊢ WF le a c ((node a c s).rank - 1)

Tactic:
rw [← h'.rank_eq] at h

Result:
α : Type u_1
le : α → α → Bool
a✝ : α
n✝ : Nat
s✝ : HeapNode α
h✝ : WF le a✝ s✝ n✝
res : Heap α
a : α
c s : HeapNode α
n : Nat
left✝ : ∀ [inst : TotalBLE le], le a✝ a = true
h : WF le a c s.rank
h' : WF le a✝ s n
hr : Heap.WF le (node a c s).rank res
⊢ WF le a c ((node a c s).rank - 1)