harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem pow_norm_pow_one_div_tendsto_nhds_spectralRadius (a : A) :
    Tendsto (fun n : ℕ => ENNReal.ofReal (‖a ^ n‖ ^ (1 / n : ℝ))) atTop
      (𝓝 (spectralRadius ℂ a))

Proof state:
case h.e'_3
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
⊢ (fun n => ENNReal.ofReal (‖a ^ n‖ ^ (1 / ↑n))) = fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)

Tactic:
ext1

Result:
case h.e'_3.h
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
x✝ : ℕ
⊢ ENNReal.ofReal (‖a ^ x✝‖ ^ (1 / ↑x✝)) = ↑‖a ^ x✝‖₊ ^ (1 / ↑x✝)

Proof state:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
⊢ Tendsto (fun n => ENNReal.ofReal (‖a ^ n‖ ^ (1 / ↑n))) atTop (𝓝 (spectralRadius ℂ a))

Tactic:
convert pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius a using 1

Result:
case h.e'_3
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
⊢ (fun n => ENNReal.ofReal (‖a ^ n‖ ^ (1 / ↑n))) = fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)

Proof state:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
x✝ : ℕ
⊢ 0 ≤ 1 / ↑x✝

Tactic:
exact one_div_nonneg.mpr (mod_cast zero_le _)

Result:
no goals

Proof state:
case h.e'_3.h
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
x✝ : ℕ
⊢ ENNReal.ofReal (‖a ^ x✝‖ ^ (1 / ↑x✝)) = ↑‖a ^ x✝‖₊ ^ (1 / ↑x✝)

Tactic:
rw [← ofReal_rpow_of_nonneg (norm_nonneg _) _, ← coe_nnnorm, coe_nnreal_eq]

Result:
A : Type u_2
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
x✝ : ℕ
⊢ 0 ≤ 1 / ↑x✝
-- Mathlib/CategoryTheory/Sites/Canonical.lean
theorem sheaf_for_finestTopology (Ps : Set (Cᵒᵖ ⥤ Type v)) (h : P ∈ Ps) :
    Presieve.IsSheaf (finestTopology Ps) P := fun X S hS => by
  simpa using hS _ ⟨⟨_, _, ⟨_, h, rfl⟩, rfl⟩, rfl⟩ _ (𝟙 _)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type v
Ps : Set (Cᵒᵖ ⥤ Type v)
h : P ∈ Ps
X : C
S : Sieve X
hS : S ∈ (finestTopology Ps) X
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
simpa using hS _ ⟨⟨_, _, ⟨_, h, rfl⟩, rfl⟩, rfl⟩ _ (𝟙 _)

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.restrict (h : l.HasBasis p s) {q : ι → Prop}
    (hq : ∀ i, p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i) : l.HasBasis (fun i => p i ∧ q i) s

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
j : ι
hpj : p j
hqj : q j
hji : s j ⊆ s i
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t

Tactic:
exact ⟨j, ⟨hpj, hqj⟩, hji.trans hti⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
⊢ l.HasBasis (fun i => p i ∧ q i) s

Tactic:
refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i, hpi, hti⟩ => h.mem_iff.2 ⟨i, hpi.1, hti⟩⟩⟩

Result:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t

Tactic:
rcases h.mem_iff.1 ht with ⟨i, hpi, hti⟩

Result:
case intro.intro
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t

Proof state:
case intro.intro
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t

Tactic:
rcases hq i hpi with ⟨j, hpj, hqj, hji⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
q : ι → Prop
hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i
t : Set α
ht : t ∈ l
i : ι
hpi : p i
hti : s i ⊆ t
j : ι
hpj : p j
hqj : q j
hji : s j ⊆ s i
⊢ ∃ i, (p i ∧ q i) ∧ s i ⊆ t
-- Mathlib/Topology/DiscreteSubset.lean
lemma mem_codiscrete' {S : Set X} :
    S ∈ codiscrete X ↔ IsOpen S ∧ DiscreteTopology ↑Sᶜ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ S ∈ codiscrete X ↔ IsOpen S ∧ DiscreteTopology ↑Sᶜ

Tactic:
rw [mem_codiscrete, ← isClosed_compl_iff, isClosed_and_discrete_iff]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem cast_bijective {α β : Sort _} (h : α = β) : Function.Bijective (cast h)

Proof state:
α β : Sort u_3
h : α = β
⊢ Bijective (cast h)

Tactic:
cases h

Result:
case refl
α : Sort u_3
⊢ Bijective (cast ⋯)

Proof state:
case refl
α : Sort u_3
⊢ Bijective (cast ⋯)

Tactic:
exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IndYoneda.lean
@[reassoc (attr := simp)]
lemma coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π (i : I) :
    (coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ limit.π (F.op.comp coyoneda) ⟨i⟩
      = coyoneda.map (colimit.ι F i).op

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : I ⥤ C
inst✝ : HasColimit F
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ limit.π (F.op ⋙ coyoneda) (op i) = coyoneda.map (colimit.ι F i).op

Tactic:
simp only [coyonedaOpColimitIsoLimitCoyoneda, Functor.mapIso_symm,
  Iso.trans_hom, Iso.symm_hom, Functor.mapIso_inv, Category.assoc, preservesLimitIso_hom_π,
  ← Functor.map_comp, limitOpIsoOpColimit_inv_comp_π]

Result:
no goals
-- Mathlib/Dynamics/BirkhoffSum/Average.lean
theorem Function.IsFixedPt.birkhoffAverage_eq [CharZero R] {f : α → α} {x : α} (h : IsFixedPt f x)
    (g : α → M) {n : ℕ} (hn : n ≠ 0) : birkhoffAverage R f g n x = g x

Proof state:
R : Type u_1
α : Type u_2
M : Type u_3
inst✝³ : DivisionSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CharZero R
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : n ≠ 0
⊢ birkhoffAverage R f g n x = g x

Tactic:
rw [birkhoffAverage, h.birkhoffSum_eq, ← Nat.cast_smul_eq_nsmul R, inv_smul_smul₀]

Result:
case ha
R : Type u_1
α : Type u_2
M : Type u_3
inst✝³ : DivisionSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CharZero R
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Proof state:
case ha
R : Type u_1
α : Type u_2
M : Type u_3
inst✝³ : DivisionSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CharZero R
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
rwa [Nat.cast_ne_zero]

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
lemma absorbs_iff_eventually_cobounded_mapsTo :
    Absorbs G₀ s t ↔ ∀ᶠ c in cobounded G₀, MapsTo (c⁻¹ • ·) t s :=
  eventually_congr <| (eventually_ne_cobounded 0).mono fun c hc ↦ by
    rw [← preimage_smul_inv₀ hc]; rfl

Proof state:
G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s t : Set α
c : G₀
hc : c ≠ 0
⊢ t ⊆ c • s ↔ MapsTo (fun x => c⁻¹ • x) t s

Tactic:
rw [← preimage_smul_inv₀ hc]

Result:
G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s t : Set α
c : G₀
hc : c ≠ 0
⊢ t ⊆ (fun x => c⁻¹ • x) ⁻¹' s ↔ MapsTo (fun x => c⁻¹ • x) t s

Proof state:
G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s t : Set α
c : G₀
hc : c ≠ 0
⊢ t ⊆ (fun x => c⁻¹ • x) ⁻¹' s ↔ MapsTo (fun x => c⁻¹ • x) t s

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
@[simp]
lemma localized₀_bot : (⊥ : Submodule R M).localized₀ p f = ⊥

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
s : ↥p
⊢ IsLocalizedModule.mk' f 0 s ∈ ⊥

Tactic:
simp only [IsLocalizedModule.mk'_zero, mem_bot]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ localized₀ p f ⊥ = ⊥

Tactic:
rw [← le_bot_iff]

Result:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ localized₀ p f ⊥ ≤ ⊥

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ localized₀ p f ⊥ ≤ ⊥

Tactic:
rintro _ ⟨_, rfl, s, rfl⟩

Result:
case intro.intro.intro
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
s : ↥p
⊢ IsLocalizedModule.mk' f 0 s ∈ ⊥
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
lemma mem_of_adj_spanningCoe {v w : V} {s : Set V} (G : SimpleGraph s)
    (hadj : G.spanningCoe.Adj v w) : v ∈ s

Proof state:
V : Type u
v w : V
s : Set V
G : SimpleGraph ↑s
hadj : G.spanningCoe.Adj v w
⊢ v ∈ s

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem exists_lt (f : CauSeq α abs) : ∃ a : α, const a < f :=
  let ⟨a, h⟩ := (-f).exists_gt
  ⟨-a, show Pos _ by rwa [const_neg, sub_neg_eq_add, add_comm, ← sub_neg_eq_add]⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
a : α
h : -f < const a
⊢ (f - const (-a)).Pos

Tactic:
rwa [const_neg, sub_neg_eq_add, add_comm, ← sub_neg_eq_add]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Action/Prod.lean
theorem smul_mk_zero {β : Type*} [Monoid M] [AddMonoid β] [DistribMulAction M β] (a : M) (b : α) :
    a • (b, (0 : β)) = (a • b, 0)

Proof state:
M : Type u_1
α : Type u_3
inst✝³ : SMul M α
β : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction M β
a : M
b : α
⊢ a • (b, 0) = (a • b, 0)

Tactic:
rw [Prod.smul_mk, smul_zero]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma zero_mul_subset (s : Finset α) : 0 * s ⊆ 0

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
s : Finset α
⊢ 0 * s ⊆ 0

Tactic:
simp [subset_iff, mem_mul]

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Basic.lean
theorem zero_oreDiv (s : S) : (0 : X) /ₒ s = 0

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
s : ↥S
⊢ s • 0 = 1 • 0 ∧ ↑s * ↑1 = 1 * ↑s

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
s : ↥S
⊢ ∃ u v, u • 0 = v • 0 ∧ ↑u * ↑1 = v * ↑s

Tactic:
exact ⟨s, 1, by simp⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
s : ↥S
⊢ 0 /ₒ s = 0

Tactic:
rw [OreLocalization.zero_def, oreDiv_eq_iff]

Result:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
s : ↥S
⊢ ∃ u v, u • 0 = v • 0 ∧ ↑u * ↑1 = v * ↑s
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem AbsolutelyContinuous.prod [SFinite ν'] (h1 : μ ≪ μ') (h2 : ν ≪ ν') :
    μ.prod ν ≪ μ'.prod ν'

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ'.prod ν') s = 0
⊢ (μ.prod ν) s = 0

Tactic:
rw [measure_prod_null hs] at h2s ⊢

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (fun x => ν' (Prod.mk x ⁻¹' s)) =ᶠ[ae μ'] 0
⊢ (fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
⊢ μ.prod ν ≪ μ'.prod ν'

Tactic:
refine AbsolutelyContinuous.mk fun s hs h2s => ?_

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ'.prod ν') s = 0
⊢ (μ.prod ν) s = 0

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (fun x => ν' (Prod.mk x ⁻¹' s)) =ᶠ[ae μ'] 0
⊢ (fun x => ν (Prod.mk x ⁻¹' s)) =ᶠ[ae μ] 0

Tactic:
exact (h2s.filter_mono h1.ae_le).mono fun _ h => h2 h

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem mem_conjugatesOfSet_iff {x : G} : x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x

Proof state:
G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ (∃ i, ∃ (_ : i ∈ s), x ∈ conjugatesOf i) ↔ ∃ a ∈ s, IsConj a x

Tactic:
simp only [conjugatesOf, isConj_iff, Set.mem_setOf_eq, exists_prop]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x

Tactic:
rw [conjugatesOfSet, Set.mem_iUnion₂]

Result:
G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ (∃ i, ∃ (_ : i ∈ s), x ∈ conjugatesOf i) ↔ ∃ a ∈ s, IsConj a x
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem le_iff_mem_closure (x y : PrimeSpectrum R) :
    x ≤ y ↔ y ∈ closure ({x} : Set (PrimeSpectrum R))

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : PrimeSpectrum R
⊢ x ≤ y ↔ y ∈ closure {x}

Tactic:
rw [← asIdeal_le_asIdeal, ← zeroLocus_vanishingIdeal_eq_closure, mem_zeroLocus,
  vanishingIdeal_singleton, SetLike.coe_subset_coe]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem find?_insert_of_ne [@TransCmp α cmp] (t : RBMap α β cmp) (h : cmp k' k ≠ .eq) :
    (t.insert k v).find? k' = t.find? k'

Proof state:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k ≠ Ordering.eq
⊢ (t.insert k v).find? k' = t.find? k'

Tactic:
simp [find?, findEntry?_insert_of_ne _ h]

Result:
no goals
-- Mathlib/Algebra/FreeMonoid/Basic.lean
theorem map_map {α₁ : Type*} {g : α₁ → α} {x : FreeMonoid α₁} :
    map f (map g x) = map (f ∘ g) x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
α₁ : Type u_6
g : α₁ → α
x : FreeMonoid α₁
⊢ { toFun := fun l => ofList (List.map f (toList l)), map_one' := ⋯, map_mul' := ⋯ }
      ({ toFun := fun l => ofList (List.map g (toList l)), map_one' := ⋯, map_mul' := ⋯ } x) =
    { toFun := fun l => ofList (List.map (f ∘ g) (toList l)), map_one' := ⋯, map_mul' := ⋯ } x

Tactic:
simp only [MonoidHom.coe_mk, OneHom.coe_mk, toList_ofList, List.map_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
α₁ : Type u_6
g : α₁ → α
x : FreeMonoid α₁
⊢ (map f) ((map g) x) = (map (f ∘ g)) x

Tactic:
unfold map

Result:
α : Type u_1
β : Type u_2
f : α → β
α₁ : Type u_6
g : α₁ → α
x : FreeMonoid α₁
⊢ { toFun := fun l => ofList (List.map f (toList l)), map_one' := ⋯, map_mul' := ⋯ }
      ({ toFun := fun l => ofList (List.map g (toList l)), map_one' := ⋯, map_mul' := ⋯ } x) =
    { toFun := fun l => ofList (List.map (f ∘ g) (toList l)), map_one' := ⋯, map_mul' := ⋯ } x
-- Mathlib/Algebra/Order/Floor.lean
theorem lt_floor_add_one (a : α) : a < ⌊a⌋ + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ a < ↑⌊a⌋ + 1

Tactic:
simpa only [Int.succ, Int.cast_add, Int.cast_one] using lt_succ_floor a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_succ (s n step) : range' s (n + 1) step = #[s] ++ range' (s + step) n step

Proof state:
s n step : Nat
⊢ (range' s (n + 1) step).toList = (#[s] ++ range' (s + step) n step).toList

Tactic:
simp [List.range'_succ]

Result:
no goals

Proof state:
s n step : Nat
⊢ range' s (n + 1) step = #[s] ++ range' (s + step) n step

Tactic:
rw [← toList_inj]

Result:
s n step : Nat
⊢ (range' s (n + 1) step).toList = (#[s] ++ range' (s + step) n step).toList
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem map_drop (f : α → β) :
    ∀ (L : List α) (i : Nat), (L.drop i).map f = (L.map f).drop i
  | [], i => by simp
  | L, 0 => by simp
  | h :: t, n + 1 => by
    dsimp
    rw [map_drop f t]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
L : List α
⊢ map f (drop 0 L) = drop 0 (map f L)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
h : α
t : List α
n : Nat
⊢ map f (drop n t) = drop n (map f t)

Tactic:
rw [map_drop f t]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
h : α
t : List α
n : Nat
⊢ map f (drop (n + 1) (h :: t)) = drop (n + 1) (map f (h :: t))

Tactic:
dsimp

Result:
α : Type u_1
β : Type u_2
f : α → β
h : α
t : List α
n : Nat
⊢ map f (drop n t) = drop n (map f t)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
i : Nat
⊢ map f (drop i []) = drop i (map f [])

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem support_extendDomain_subset (f : Subtype P →₀ M) :
    ↑(f.extendDomain).support ⊆ {x | P x}

Proof state:
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
x : α
⊢ x ∈ ↑f.extendDomain.support → x ∈ {x | P x}

Tactic:
rw [extendDomain_support, mem_coe, mem_map, Embedding.coe_subtype]

Result:
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
x : α
⊢ (∃ a ∈ f.support, ↑a = x) → x ∈ {x | P x}

Proof state:
case intro.intro
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
x : Subtype P
⊢ ↑x ∈ {x | P x}

Tactic:
exact x.prop

Result:
no goals

Proof state:
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
⊢ ↑f.extendDomain.support ⊆ {x | P x}

Tactic:
intro x

Result:
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
x : α
⊢ x ∈ ↑f.extendDomain.support → x ∈ {x | P x}

Proof state:
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
x : α
⊢ (∃ a ∈ f.support, ↑a = x) → x ∈ {x | P x}

Tactic:
rintro ⟨x, -, rfl⟩

Result:
case intro.intro
α : Type u_1
M : Type u_13
inst✝¹ : Zero M
P : α → Prop
inst✝ : DecidablePred P
f : Subtype P →₀ M
x : Subtype P
⊢ ↑x ∈ {x | P x}
-- Mathlib/Topology/Order/Monotone.lean
theorem Monotone.map_ciSup_of_continuousAt {ι : Sort*} [Nonempty ι] {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f)
    (bdd : BddAbove (range g)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
bdd : autoParam (BddAbove (range g)) _auto✝
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
rw [iSup, Monotone.map_csSup_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iSup,
  comp_def]

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
theorem cancel_natIso_hom_right {X : D} {Y : C} (f f' : X ⟶ F.obj Y) :
    f ≫ α.hom.app Y = f' ≫ α.hom.app Y ↔ f = f'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
X : D
Y : C
f f' : X ⟶ F.obj Y
⊢ f ≫ α.hom.app Y = f' ≫ α.hom.app Y ↔ f = f'

Tactic:
simp only [cancel_mono, refl]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Multiset.lean
@[ext]
lemma addHom_ext [AddZeroClass β] ⦃f g : Multiset α →+ β⦄ (h : ∀ x, f {x} = g {x}) : f = g

Proof state:
case h.cons
α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
a : α
s : Multiset α
ih : f s = g s
⊢ f (a ::ₘ s) = g (a ::ₘ s)

Tactic:
simp only [← singleton_add, _root_.map_add, ih, h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
⊢ f = g

Tactic:
ext s

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
s : Multiset α
⊢ f s = g s

Proof state:
case h.empty
α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
⊢ f 0 = g 0

Tactic:
simp only [_root_.map_zero]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
s : Multiset α
⊢ f s = g s

Tactic:
induction' s using Multiset.induction_on with a s ih

Result:
case h.empty
α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
⊢ f 0 = g 0

case h.cons
α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
a : α
s : Multiset α
ih : f s = g s
⊢ f (a ::ₘ s) = g (a ::ₘ s)
-- Mathlib/Data/Real/Basic.lean
theorem mk_pos {f : CauSeq ℚ abs} : 0 < mk f ↔ Pos f

Proof state:
f : CauSeq ℚ abs
⊢ 0 < f ↔ f.Pos

Tactic:
exact iff_of_eq (congr_arg Pos (sub_zero f))

Result:
no goals

Proof state:
f : CauSeq ℚ abs
⊢ 0 < mk f ↔ f.Pos

Tactic:
rw [← mk_zero, mk_lt]

Result:
f : CauSeq ℚ abs
⊢ 0 < f ↔ f.Pos
-- Mathlib/Data/Finset/Basic.lean
theorem erase_insert {a : α} {s : Finset α} (h : a ∉ s) : erase (insert a s) a = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ (insert a s).erase a = s

Tactic:
rw [erase_insert_eq_erase, erase_eq_of_not_mem h]

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem finRange_map_get (l : List α) : (finRange l.length).map l.get = l :=
  List.ext_get (by simp) (by simp)

Proof state:
α : Type u
l : List α
⊢ ∀ (n : ℕ) (h₁ : n < (map l.get (finRange l.length)).length) (h₂ : n < l.length),
    (map l.get (finRange l.length)).get ⟨n, h₁⟩ = l.get ⟨n, h₂⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
⊢ (map l.get (finRange l.length)).length = l.length

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem not_isReal_of_mk_isComplex {φ : K →+* ℂ} (h : IsComplex (mk φ)) :
    ¬ ComplexEmbedding.IsReal φ

Proof state:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
h : (mk φ).IsComplex
⊢ ¬ComplexEmbedding.IsReal φ

Tactic:
rwa [← isComplex_mk_iff]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem simple_induction {p : W → Prop} (w : W) (simple : ∀ i : B, p (s i)) (one : p 1)
    (mul : ∀ w w' : W, p w → p w' → p (w * w')) : p w

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
simple : ∀ (i : B), p (cs.simple i)
one : p 1
mul : ∀ (w w' : W), p w → p w' → p (w * w')
⊢ p w

Tactic:
have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
simple : ∀ (i : B), p (cs.simple i)
one : p 1
mul : ∀ (w w' : W), p w → p w' → p (w * w')
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ p w

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
simple : ∀ (i : B), p (cs.simple i)
one : p 1
mul : ∀ (w w' : W), p w → p w' → p (w * w')
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ p w

Tactic:
exact Submonoid.closure_induction (fun x ⟨i, hi⟩ ↦ hi ▸ simple i) one (fun _ _ _ _ ↦ mul _ _)
  this

Result:
no goals