harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_mul_le {f g : MvPolynomial σ R} :
    m.degree (f * g) ≼[m] m.degree f + m.degree g

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn (d + m.degree g) ≤ m.toSyn (m.degree f + m.degree g)

Tactic:
simp only [map_add]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn d + m.toSyn (m.degree g) ≤ m.toSyn (m.degree f) + m.toSyn (m.degree g)

Proof state:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
⊢ m.toSyn (m.degree g) < m.toSyn e

Tactic:
simp only [not_lt] at hd

Result:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn (m.degree g) < m.toSyn e

Proof state:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
⊢ ∀ x ∈ Finset.antidiagonal c, coeff x.1 f * coeff x.2 g = 0

Tactic:
rintro ⟨d, e⟩ hde

Result:
case h.mk
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : (d, e) ∈ Finset.antidiagonal c
⊢ coeff (d, e).1 f * coeff (d, e).2 g = 0

Proof state:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f * coeff e g = 0

Tactic:
rw [m.coeff_eq_zero_of_lt hd, zero_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean
theorem not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter {f : ℝ → E} {g : ℝ → F}
    {a b : ℝ} (l : Filter ℝ) [NeBot l] [TendstoIxxClass Icc l l] (hl : [[a, b]] ∈ l)
    (hd : ∀ᶠ x in l, DifferentiableAt ℝ f x) (hf : Tendsto (fun x => ‖f x‖) l atTop)
    (hfg : deriv f =O[l] g) : ¬IntervalIntegrable g volume a b

Proof state:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
⊢ ¬IntervalIntegrable g volume a b

Tactic:
rw [intervalIntegrable_iff']

Result:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
⊢ ¬IntegrableOn g [[a, b]] volume

Proof state:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x => ‖f x‖) l atTop
hfg : deriv f =O[l] g
⊢ ¬IntegrableOn g [[a, b]] volume

Tactic:
exact not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter _ hl hd hf hfg

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem countable_meas_pos_of_disjoint_iUnion₀ {ι : Type*} {_ : MeasurableSpace α} {μ : Measure α}
    [SFinite μ] {As : ι → Set α} (As_mble : ∀ i : ι, NullMeasurableSet (As i) μ)
    (As_disj : Pairwise (AEDisjoint μ on As)) :
    Set.Countable { i : ι | 0 < μ (As i) }

Proof state:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : 0 < (sum (sfiniteSeq μ)) (As i)
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
⊢ False

Tactic:
rw [sum_apply₀] at hi

Result:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : 0 < ∑' (i_1 : ℕ), (sfiniteSeq μ i_1) (As i)
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
⊢ False

case hs
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : 0 < (sum (sfiniteSeq μ)) (As i)
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
⊢ NullMeasurableSet (As i) (sum (sfiniteSeq μ))

Proof state:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : i ∈ {i | 0 < (sum (sfiniteSeq μ)) (As i)}
con : i ∉ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
⊢ False

Tactic:
simp only [mem_iUnion, mem_setOf_eq, not_exists, not_lt, nonpos_iff_eq_zero] at *

Result:
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : 0 < (sum (sfiniteSeq μ)) (As i)
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
⊢ False

Proof state:
case As_disj
α : Type u_1
ι : Type u_5
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs : {i | 0 < (sum (sfiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sfiniteSeq μ n) (As i)}
n : ℕ
⊢ Pairwise (AEDisjoint (sfiniteSeq μ n) on As)

Tactic:
exact fun i j hij ↦ AEDisjoint.of_le (As_disj hij) (le_sum _ _)

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem uniformContinuous_iInf_rng {f : α → β} {u₁ : UniformSpace α} {u₂ : ι → UniformSpace β} :
    UniformContinuous[u₁, iInf u₂] f ↔ ∀ i, UniformContinuous[u₁, u₂ i] f

Proof state:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
⊢ UniformContinuous f ↔ ∀ (i : ι), UniformContinuous f

Tactic:
delta UniformContinuous

Result:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
⊢ Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔ ∀ (i : ι), Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Proof state:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
⊢ Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β) ↔ ∀ (i : ι), Tendsto (fun x => (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
rw [iInf_uniformity, tendsto_iInf]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem IsSelfAdjoint.conjugate_nonneg {a : R} (ha : 0 ≤ a) {c : R}
    (hc : IsSelfAdjoint c) : 0 ≤ c * a * c

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
hc : IsSelfAdjoint c
⊢ 0 ≤ c * a * star c

Tactic:
exact conjugate_nonneg' ha c

Result:
no goals

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
hc : IsSelfAdjoint c
⊢ 0 ≤ c * a * c

Tactic:
nth_rewrite 2 [← hc]

Result:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
hc : IsSelfAdjoint c
⊢ 0 ≤ c * a * star c
-- Mathlib/LinearAlgebra/Dual.lean
@[simp]
lemma LinearMap.range_dualMap_dual_eq_span_singleton (f : Dual R M₁) :
    range f.dualMap = R ∙ f

Proof state:
case h.refine_2.h
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝¹ : ∃ a, a • f = m
r : R
hr : r • f = m
x✝ : M₁
⊢ ((dualMap f) (r • id)) x✝ = m x✝

Tactic:
simp [dualMap_apply', ← hr]

Result:
no goals

Proof state:
case h
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
⊢ m ∈ range (dualMap f) ↔ m ∈ span R {f}

Tactic:
rw [Submodule.mem_span_singleton]

Result:
case h
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
⊢ m ∈ range (dualMap f) ↔ ∃ a, a • f = m

Proof state:
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : Dual R M₁
⊢ range (dualMap f) = span R {f}

Tactic:
ext m

Result:
case h
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
⊢ m ∈ range (dualMap f) ↔ m ∈ span R {f}

Proof state:
case h.refine_1.h
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝¹ : m ∈ range (dualMap f)
r : Dual R R
hr : (dualMap f) r = m
x✝ : M₁
⊢ (r 1 • f) x✝ = m x✝

Tactic:
simp [dualMap_apply', ← hr]

Result:
no goals

Proof state:
case h
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
⊢ m ∈ range (dualMap f) ↔ ∃ a, a • f = m

Tactic:
refine ⟨fun ⟨r, hr⟩ ↦ ⟨r 1, ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r • LinearMap.id, ?_⟩⟩

Result:
case h.refine_1
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝ : m ∈ range (dualMap f)
r : Dual R R
hr : (dualMap f) r = m
⊢ r 1 • f = m

case h.refine_2
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝ : ∃ a, a • f = m
r : R
hr : r • f = m
⊢ (dualMap f) (r • id) = m

Proof state:
case h.refine_1
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝ : m ∈ range (dualMap f)
r : Dual R R
hr : (dualMap f) r = m
⊢ r 1 • f = m

Tactic:
ext

Result:
case h.refine_1.h
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝¹ : m ∈ range (dualMap f)
r : Dual R R
hr : (dualMap f) r = m
x✝ : M₁
⊢ (r 1 • f) x✝ = m x✝

Proof state:
case h.refine_2
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝ : ∃ a, a • f = m
r : R
hr : r • f = m
⊢ (dualMap f) (r • id) = m

Tactic:
ext

Result:
case h.refine_2.h
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f m : Dual R M₁
x✝¹ : ∃ a, a • f = m
r : R
hr : r • f = m
x✝ : M₁
⊢ ((dualMap f) (r • id)) x✝ = m x✝
-- Mathlib/Data/List/Cycle.lean
theorem Nodup.nontrivial_iff {s : Cycle α} (h : Nodup s) : Nontrivial s ↔ ¬Subsingleton s

Proof state:
α : Type u_1
s : Cycle α
h : s.Nodup
⊢ s.Nontrivial ↔ ¬s.Subsingleton

Tactic:
rw [length_subsingleton_iff]

Result:
α : Type u_1
s : Cycle α
h : s.Nodup
⊢ s.Nontrivial ↔ ¬s.length ≤ 1

Proof state:
case h
α : Type u_1
a✝ : List α
h : a✝.Nodup
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1

Tactic:
simp [h, Nat.succ_le_iff]

Result:
no goals

Proof state:
α : Type u_1
s : Cycle α
h : s.Nodup
⊢ s.Nontrivial ↔ ¬s.length ≤ 1

Tactic:
induction s using Quotient.inductionOn'

Result:
case h
α : Type u_1
a✝ : List α
h : Nodup (Quotient.mk'' a✝)
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1

Proof state:
case h
α : Type u_1
a✝ : List α
h : Nodup (Quotient.mk'' a✝)
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1

Tactic:
simp only [mk''_eq_coe, nodup_coe_iff] at h

Result:
case h
α : Type u_1
a✝ : List α
h : a✝.Nodup
⊢ Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem coeFn_smul [IsScalarTower R ℝ≥0 ℝ≥0] (c : R) (μ : FiniteMeasure Ω) :
    (⇑(c • μ) : Set Ω → ℝ≥0) = c • (⇑μ : Set Ω → ℝ≥0)

Proof state:
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type u_2
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
⊢ ⇑(c • μ) = c • ⇑μ

Tactic:
funext

Result:
case h
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type u_2
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
x✝ : Set Ω
⊢ (c • μ) x✝ = (c • ⇑μ) x✝

Proof state:
case h
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type u_2
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
x✝ : Set Ω
⊢ (c • μ) x✝ = (c • ⇑μ) x✝

Tactic:
simp [← ENNReal.coe_inj, ENNReal.coe_smul]

Result:
no goals
-- Mathlib/NumberTheory/Modular.lean
theorem c_eq_zero (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : g 1 0 = 0

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
⊢ False

Tactic:
have had : T ^ (-a) * g' = S * T ^ d := by
  rw [g_eq_of_c_eq_one hc]
  dsimp [a, d]
  group

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
g' : SL(2, ℤ)
hg' : g' • z ∈ 𝒟ᵒ
hc : ↑g' 1 0 = 1
a : ℤ := ↑g' 0 0
d : ℤ := ↑g' 1 1
had : T ^ (-a) * g' = S * T ^ d
⊢ False
-- Mathlib/Data/Int/Log.lean
theorem zpow_pred_clog_lt_self {b : ℕ} {r : R} (hb : 1 < b) (hr : 0 < r) :
    (b : R) ^ (clog b r - 1) < r

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ r⁻¹ < ↑b ^ (log b r⁻¹ + 1)

Tactic:
exact lt_zpow_succ_log_self hb _

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ 0 < ↑b ^ (log b r⁻¹ + 1)

Tactic:
exact zpow_pos (Nat.cast_pos.mpr <| zero_le_one.trans_lt hb) _

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ ↑b ^ (clog b r - 1) < r

Tactic:
rw [← neg_log_inv_eq_clog, ← neg_add', zpow_neg, inv_lt_comm₀ _ hr]

Result:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ r⁻¹ < ↑b ^ (log b r⁻¹ + 1)

R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hb : 1 < b
hr : 0 < r
⊢ 0 < ↑b ^ (log b r⁻¹ + 1)
-- Mathlib/Order/Atoms/Finite.lean
theorem exists_covby_infinite_Ici_of_infinite_Ici [IsStronglyAtomic α]
    (ha : (Set.Ici a).Infinite) (hfin : {x | a ⋖ x}.Finite) :
    ∃ b, a ⋖ b ∧ (Set.Ici b).Infinite

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
h : ∀ (b : α), a ⋖ b → ¬(Set.Ici b).Infinite
b : α
hb : b ∈ Set.Ici a \ {a}
⊢ b ∈ ⋃ i ∈ {x | a ⋖ x}, Set.Ici i

Tactic:
obtain ⟨x, hax, hxb⟩ := ((show a ≤ b from hb.1).lt_of_ne (Ne.symm hb.2)).exists_covby_le

Result:
case intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
h : ∀ (b : α), a ⋖ b → ¬(Set.Ici b).Infinite
b : α
hb : b ∈ Set.Ici a \ {a}
x : α
hax : a ⋖ x
hxb : x ≤ b
⊢ b ∈ ⋃ i ∈ {x | a ⋖ x}, Set.Ici i

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
h : ∀ (b : α), a ⋖ b → ¬(Set.Ici b).Infinite
b : α
hb : b ∈ Set.Ici a \ {a}
x : α
hax : a ⋖ x
hxb : x ≤ b
⊢ b ∈ ⋃ i ∈ {x | a ⋖ x}, Set.Ici i

Tactic:
exact Set.mem_biUnion hax hxb

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
⊢ ∃ b, a ⋖ b ∧ (Set.Ici b).Infinite

Tactic:
by_contra! h

Result:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
h : ∀ (b : α), a ⋖ b → ¬(Set.Ici b).Infinite
⊢ False

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
h : ∀ (b : α), a ⋖ b → ¬(Set.Ici b).Infinite
⊢ ∀ i ∈ {x | a ⋖ x}, (Set.Ici i).Finite

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
h : ∀ (b : α), a ⋖ b → ¬(Set.Ici b).Infinite
⊢ False

Tactic:
refine ((hfin.biUnion (t := Set.Ici) (by simpa using h)).subset (fun b hb ↦ ?_)).not_infinite
  (ha.diff (Set.finite_singleton a))

Result:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
h : ∀ (b : α), a ⋖ b → ¬(Set.Ici b).Infinite
b : α
hb : b ∈ Set.Ici a \ {a}
⊢ b ∈ ⋃ i ∈ {x | a ⋖ x}, Set.Ici i
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem basicOpen_mul_le_left (f g : R) : basicOpen (f * g) ≤ basicOpen f

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen f ⊓ basicOpen g ≤ basicOpen f

Tactic:
exact inf_le_left

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen (f * g) ≤ basicOpen f

Tactic:
rw [basicOpen_mul f g]

Result:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen f ⊓ basicOpen g ≤ basicOpen f
-- Mathlib/MeasureTheory/Integral/Layercake.lean
theorem countable_meas_le_ne_meas_lt (g : α → R) :
    {t : R | μ {a : α | t ≤ g a} ≠ μ {a : α | t < g a}}.Countable

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder R
g : α → R
F : R → ℝ≥0∞ := fun t => μ {a | t ≤ g a}
⊢ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}} ⊆ {x | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z}

Tactic:
intro t ht

Result:
α : Type u_1
R : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder R
g : α → R
F : R → ℝ≥0∞ := fun t => μ {a | t ≤ g a}
t : R
ht : t ∈ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}}
⊢ t ∈ {x | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z}

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder R
g : α → R
F : R → ℝ≥0∞ := fun t => μ {a | t ≤ g a}
t : R
ht : t ∈ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}}
⊢ t ∈ {x | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z}

Tactic:
have : μ {a | t < g a} < μ {a | t ≤ g a} :=
  lt_of_le_of_ne (measure_mono (fun a ha ↦ le_of_lt ha)) (Ne.symm ht)

Result:
α : Type u_1
R : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder R
g : α → R
F : R → ℝ≥0∞ := fun t => μ {a | t ≤ g a}
t : R
ht : t ∈ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}}
this : μ {a | t < g a} < μ {a | t ≤ g a}
⊢ t ∈ {x | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z}

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder R
g : α → R
F : R → ℝ≥0∞ := fun t => μ {a | t ≤ g a}
t : R
ht : t ∈ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}}
this : μ {a | t < g a} < μ {a | t ≤ g a}
⊢ t ∈ {x | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z}

Tactic:
exact ⟨μ {a | t < g a}, this, fun s hs ↦ measure_mono (fun a ha ↦ hs.trans_le ha)⟩

Result:
no goals

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder R
g : α → R
F : R → ℝ≥0∞ := fun t => μ {a | t ≤ g a}
⊢ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}}.Countable

Tactic:
apply (countable_image_gt_image_Ioi F).mono

Result:
α : Type u_1
R : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder R
g : α → R
F : R → ℝ≥0∞ := fun t => μ {a | t ≤ g a}
⊢ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}} ⊆ {x | ∃ z < F x, ∀ (y : R), x < y → F y ≤ z}

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder R
g : α → R
⊢ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}}.Countable

Tactic:
let F : R → ℝ≥0∞ := fun t ↦ μ {a : α | t ≤ g a}

Result:
α : Type u_1
R : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : LinearOrder R
g : α → R
F : R → ℝ≥0∞ := fun t => μ {a | t ≤ g a}
⊢ {t | μ {a | t ≤ g a} ≠ μ {a | t < g a}}.Countable
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@[to_additive (attr := simp)]
lemma monoidHomOfForallMemZpowers_apply_gen :
    monoidHomOfForallMemZpowers hg hg' g = g'

Proof state:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g' ^ Classical.choose ⋯ = g' ^ 1

Tactic:
rw [zpow_eq_zpow_iff_modEq]

Result:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ Classical.choose ⋯ ≡ 1 [ZMOD ↑(orderOf g')]

Proof state:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ (monoidHomOfForallMemZpowers hg hg') g = g'

Tactic:
simp only [monoidHomOfForallMemZpowers, MonoidHom.coe_mk, OneHom.coe_mk]

Result:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g' ^ Classical.choose ⋯ = g'

Proof state:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ Classical.choose ⋯ ≡ 1 [ZMOD ↑(orderOf g)]

Tactic:
rw [← zpow_eq_zpow_iff_modEq, zpow_one]

Result:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g ^ Classical.choose ⋯ = g

Proof state:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g' ^ Classical.choose ⋯ = g'

Tactic:
nth_rw 2 [← zpow_one g']

Result:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g' ^ Classical.choose ⋯ = g' ^ 1

Proof state:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ Classical.choose ⋯ ≡ 1 [ZMOD ↑(orderOf g')]

Tactic:
apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr hg')

Result:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ Classical.choose ⋯ ≡ 1 [ZMOD ↑(orderOf g)]

Proof state:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g ^ Classical.choose ⋯ = g

Tactic:
exact Classical.choose_spec <| mem_zpowers_iff.mp <| hg g

Result:
no goals