harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/PrimeIdeal.lean
theorem isPrime_of_mem_or_compl_mem [IsProper I] (h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I) : IsPrime I

Proof state:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ ∀ {x y : P}, x ⊓ y ∈ I → x ∉ I → y ∈ I

Tactic:
intro x y hxy hxI

Result:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
⊢ y ∈ I

Proof state:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ I.IsPrime

Tactic:
simp only [isPrime_iff_mem_or_mem, or_iff_not_imp_left]

Result:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ ∀ {x y : P}, x ⊓ y ∈ I → x ∉ I → y ∈ I

Proof state:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
hxcI : xᶜ ∈ I
⊢ y ∈ I

Tactic:
have ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I := sup_mem hxy (I.lower inf_le_right hxcI)

Result:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
hxcI : xᶜ ∈ I
ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I
⊢ y ∈ I

Proof state:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
hxcI : xᶜ ∈ I
ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I
⊢ y ∈ I

Tactic:
rwa [inf_comm, sup_inf_inf_compl] at ass

Result:
no goals

Proof state:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
⊢ y ∈ I

Tactic:
have hxcI : xᶜ ∈ I := h.resolve_left hxI

Result:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
hxcI : xᶜ ∈ I
⊢ y ∈ I
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
@[simp]
lemma diam_bot : (⊥ : SimpleGraph α).diam = 0

Proof state:
case inr
α : Type u_1
h✝ : Nontrivial α
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤

Tactic:
exact Or.inr ediam_bot

Result:
no goals

Proof state:
α : Type u_1
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤

Tactic:
cases subsingleton_or_nontrivial α

Result:
case inl
α : Type u_1
h✝ : Subsingleton α
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤

case inr
α : Type u_1
h✝ : Nontrivial α
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤

Proof state:
α : Type u_1
⊢ ⊥.diam = 0

Tactic:
rw [diam, ENat.toNat_eq_zero]

Result:
α : Type u_1
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤

Proof state:
case inl
α : Type u_1
h✝ : Subsingleton α
⊢ ⊥.ediam = 0 ∨ ⊥.ediam = ⊤

Tactic:
exact Or.inl ediam_eq_zero_of_subsingleton

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
theorem exists_finsupp_eq_lexOrder_of_ne_zero {φ : MvPowerSeries σ R} (hφ : φ ≠ 0) :
    ∃ (d : σ →₀ ℕ), lexOrder φ = toLex d

Proof state:
case intro
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
p : Lex (σ →₀ ℕ)
hp : ↑p = φ.lexOrder
⊢ ∃ d, φ.lexOrder = ↑(toLex d)

Tactic:
exact ⟨ofLex p, by simp only [toLex_ofLex, hp]⟩

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
p : Lex (σ →₀ ℕ)
hp : ↑p = φ.lexOrder
⊢ φ.lexOrder = ↑(toLex (ofLex p))

Tactic:
simp only [toLex_ofLex, hp]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ ∃ d, φ.lexOrder = ↑(toLex d)

Tactic:
simp only [ne_eq, ← lexOrder_eq_top_iff_eq_zero, WithTop.ne_top_iff_exists] at hφ

Result:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : ∃ a, ↑a = φ.lexOrder
⊢ ∃ d, φ.lexOrder = ↑(toLex d)

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : ∃ a, ↑a = φ.lexOrder
⊢ ∃ d, φ.lexOrder = ↑(toLex d)

Tactic:
obtain ⟨p, hp⟩ := hφ

Result:
case intro
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
p : Lex (σ →₀ ℕ)
hp : ↑p = φ.lexOrder
⊢ ∃ d, φ.lexOrder = ↑(toLex d)
-- Mathlib/Topology/Algebra/Module/ModuleTopology.lean
theorem iso (e : A ≃L[R] B) : IsModuleTopology R B where
  eq_moduleTopology'

Proof state:
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
⊢ τB = moduleTopology R B

Tactic:
let h : A →+ B := e

Result:
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
⊢ τB = moduleTopology R B

Proof state:
case h
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
⊢ TopologicalSpace.induced ⇑e.toHomeomorph.symm '' {t | ContinuousSMul R A ∧ ContinuousAdd A} =
    {t | ContinuousSMul R B ∧ ContinuousAdd B}

Tactic:
ext τ

Result:
case h.h
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
τ : TopologicalSpace B
⊢ τ ∈ TopologicalSpace.induced ⇑e.toHomeomorph.symm '' {t | ContinuousSMul R A ∧ ContinuousAdd A} ↔
    τ ∈ {t | ContinuousSMul R B ∧ ContinuousAdd B}

Proof state:
case h.h.mp.intro.intro.intro
R : Type u_1
τR : TopologicalSpace R
inst✝⁵ : Semiring R
A : Type u_2
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
g : A →ₗ[R] B := ↑↑e
g' : B →ₗ[R] A := ↑↑e.symm
h : A →+ B := ↑e
h' : B →+ A := ↑e.symm
σ : TopologicalSpace A
hσ1 : ContinuousSMul R A
hσ2 : ContinuousAdd A
⊢ TopologicalSpace.induced (⇑e.toHomeomorph.symm) σ ∈ {t | ContinuousSMul R B ∧ ContinuousAdd B}

Tactic:
exact ⟨continuousSMul_induced g'.toMulActionHom, continuousAdd_induced h'⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Defs.lean
theorem mk_surjective : Function.Surjective (@mk _ _ _ _ _ p)

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
b✝ : M ⧸ p
x : M
⊢ ∃ a, mk a = Quot.mk (⇑p.quotientRel) x

Tactic:
exact ⟨x, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ Function.Surjective mk

Tactic:
rintro ⟨x⟩

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
b✝ : M ⧸ p
x : M
⊢ ∃ a, mk a = Quot.mk (⇑p.quotientRel) x
-- Mathlib/Data/QPF/Multivariate/Basic.lean
theorem has_good_supp_iff {α : TypeVec n} (x : F α) :
    (∀ p, LiftP p x ↔ ∀ (i), ∀ u ∈ supp x i, p i u) ↔
      ∃ a f, abs ⟨a, f⟩ = x ∧ ∀ i a' f', abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ

Proof state:
case mpr.intro.intro.intro.mpr.a
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs ⟨a, f⟩ = x
h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
j : Fin2 n
y : (P F).B a j
a' : (P F).A
f' : (P F).B a' ⟹ α
xeq' : abs ⟨a', f'⟩ = x
⊢ f j y ∈ f' j '' univ

Tactic:
apply h _ a' f' xeq'

Result:
case mpr.intro.intro.intro.mpr.a.a
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs ⟨a, f⟩ = x
h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
j : Fin2 n
y : (P F).B a j
a' : (P F).A
f' : (P F).B a' ⟹ α
xeq' : abs ⟨a', f'⟩ = x
⊢ f j y ∈ f j '' univ

Proof state:
case mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
hu : abs ⟨f', h''⟩ = x
u : α a'
j : (P F).B a a'
_h₂ : j ∈ univ
hfi : f a' j = u
⊢ u ∈ h'' a' '' univ

Tactic:
have hh : u ∈ supp x a' := by rw [← hfi]; apply h'

Result:
case mp.intro.intro.intro.intro.intro
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
h : ∀ (p : (i : Fin2 n) → α i → Prop), LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
a : (P F).A
f : (P F).B a ⟹ α
xeq : x = abs ⟨a, f⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a i), supp x i (f i j)
a' : Fin2 n
f' : (P F).A
h'' : (P F).B f' ⟹ α
hu : abs ⟨f', h''⟩ = x
u : α a'
j : (P F).B a a'
_h₂ : j ∈ univ
hfi : f a' j = u
hh : u ∈ supp x a'
⊢ u ∈ h'' a' '' univ
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
theorem degree_map_eq_of_leadingCoeff_ne_zero (f : R →+* S) (hf : f (leadingCoeff p) ≠ 0) :
    degree (p.map f) = degree p

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
⊢ (map f p).degree = p.degree

Tactic:
refine degree_map_le.antisymm ?_

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
⊢ p.degree ≤ (map f p).degree

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
⊢ p.degree ≤ (map f p).degree

Tactic:
have hp0 : p ≠ 0 :=
  leadingCoeff_ne_zero.mp fun hp0 => hf (_root_.trans (congr_arg _ hp0) f.map_zero)

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ p.degree ≤ (map f p).degree

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ p.degree ≤ (map f p).degree

Tactic:
rw [degree_eq_natDegree hp0]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ ↑p.natDegree ≤ (map f p).degree

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ f (p.coeff p.natDegree) ≠ 0

Tactic:
exact hf

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ (map f p).coeff p.natDegree ≠ 0

Tactic:
rw [coeff_map]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ f (p.coeff p.natDegree) ≠ 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ ↑p.natDegree ≤ (map f p).degree

Tactic:
refine le_degree_of_ne_zero ?_

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ (map f p).coeff p.natDegree ≠ 0
-- Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean
theorem isColimit_rep_eq_of_exists {D : Cocone F} {i j : J} (x : ToType (F.obj i))
    (y : ToType (F.obj j))
    (h : ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y) :
    D.ι.app i x = D.ι.app j y

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
J : Type w
inst✝ : Category.{r, w} J
F : J ⥤ C
D : Cocone F
i j : J
x : ToType (F.obj i)
y : ToType (F.obj j)
h : ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
⊢ (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y

Tactic:
obtain ⟨k, f, g, (hfg : (F ⋙ forget C).map f x = F.map g y)⟩ := h

Result:
case intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
J : Type w
inst✝ : Category.{r, w} J
F : J ⥤ C
D : Cocone F
i j : J
x : ToType (F.obj i)
y : ToType (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
k : J
f : i ⟶ k
g : j ⟶ k
hfg : (F ⋙ forget C).map f x = (ConcreteCategory.hom (F.map g)) y
⊢ (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
private lemma tendsto_log_one_sub_sub_log_nhdsLT_one_atBot :
    Tendsto (fun p ↦ log (1 - p) - log p) (𝓝[<] 1) atBot

Proof state:
this : Tendsto log (𝓝[>] 0) atBot
contF : Continuous fun x => 1 - x
⊢ MapsTo (fun x => 1 - x) (Iio 1) (Ioi 0)

Tactic:
intro p hx

Result:
this : Tendsto log (𝓝[>] 0) atBot
contF : Continuous fun x => 1 - x
p : ℝ
hx : p ∈ Iio 1
⊢ (fun x => 1 - x) p ∈ Ioi 0

Proof state:
case h
h₁ : 1 - 2⁻¹ < 1
p : ℝ
hx : p ∈ Ico (1 - 2⁻¹) 1
⊢ -log p ≤ -log (1 - 2⁻¹)

Tactic:
gcongr

Result:
case h.a.hxy
h₁ : 1 - 2⁻¹ < 1
p : ℝ
hx : p ∈ Ico (1 - 2⁻¹) 1
⊢ 1 - 2⁻¹ ≤ p

Proof state:
case hg
h₁ : 1 - 2⁻¹ < 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, -log x ≤ -log (1 - 2⁻¹)

Tactic:
filter_upwards [Ico_mem_nhdsLT h₁] with p hx

Result:
case h
h₁ : 1 - 2⁻¹ < 1
p : ℝ
hx : p ∈ Ico (1 - 2⁻¹) 1
⊢ -log p ≤ -log (1 - 2⁻¹)

Proof state:
case hg

⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, -log x ≤ -log (1 - 2⁻¹)

Tactic:
have h₁ : (1 : ℝ) - (2 : ℝ)⁻¹ < 1 := by norm_num

Result:
case hg
h₁ : 1 - 2⁻¹ < 1
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, -log x ≤ -log (1 - 2⁻¹)

Proof state:
case h.e'_5.h.e'_3
this✝ : Tendsto log (𝓝[>] 0) atBot
contF : Continuous fun x => 1 - x
this : MapsTo (fun x => 1 - x) (Iio 1) (Ioi 0)
⊢ 0 = 1 - 1

Tactic:
exact Eq.symm (sub_eq_zero_of_eq rfl)

Result:
no goals

Proof state:
case hf
this✝ : Tendsto log (𝓝[>] 0) atBot
contF : Continuous fun x => 1 - x
this : MapsTo (fun x => 1 - x) (Iio 1) (Ioi 0)
⊢ Tendsto (fun x => 1 - x) (𝓝[<] 1) (𝓝[>] 0)

Tactic:
convert ContinuousWithinAt.tendsto_nhdsWithin (x :=(1 : ℝ)) contF.continuousWithinAt this

Result:
case h.e'_5.h.e'_3
this✝ : Tendsto log (𝓝[>] 0) atBot
contF : Continuous fun x => 1 - x
this : MapsTo (fun x => 1 - x) (Iio 1) (Ioi 0)
⊢ 0 = 1 - 1

Proof state:
⊢ Tendsto (fun p => log (1 - p) - log p) (𝓝[<] 1) atBot

Tactic:
apply Filter.tendsto_atBot_add_right_of_ge' (𝓝[<] 1) (-log (1 - 2⁻¹))

Result:
case hf

⊢ Tendsto (fun x => log (1 - x)) (𝓝[<] 1) atBot

case hg

⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, -log x ≤ -log (1 - 2⁻¹)

Proof state:
case hf

⊢ Tendsto (fun x => log (1 - x)) (𝓝[<] 1) atBot

Tactic:
have : Tendsto log (𝓝[>] 0) atBot := Real.tendsto_log_nhdsWithin_zero_right

Result:
case hf
this : Tendsto log (𝓝[>] 0) atBot
⊢ Tendsto (fun x => log (1 - x)) (𝓝[<] 1) atBot

Proof state:
this : Tendsto log (𝓝[>] 0) atBot
contF : Continuous fun x => 1 - x
p : ℝ
hx : p ∈ Iio 1
⊢ (fun x => 1 - x) p ∈ Ioi 0

Tactic:
simp_all only [mem_Iio, mem_Ioi, sub_pos]

Result:
no goals

Proof state:
⊢ 1 - 2⁻¹ < 1

Tactic:
norm_num

Result:
no goals

Proof state:
case h.a.hxy
h₁ : 1 - 2⁻¹ < 1
p : ℝ
hx : p ∈ Ico (1 - 2⁻¹) 1
⊢ 1 - 2⁻¹ ≤ p

Tactic:
exact hx.1

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem ae_map_mem_range {m0 : MeasurableSpace α} (f : α → β) (hf : MeasurableSet (range f))
    (μ : Measure α) : ∀ᵐ x ∂μ.map f, x ∈ range f

Proof state:
case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ f ⁻¹' range f ∈ ae μ

Tactic:
filter_upwards using mem_range_self

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f

Tactic:
by_cases h : AEMeasurable f μ

Result:
case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f

case neg
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : ¬AEMeasurable f μ
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f

Proof state:
case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ range f ∈ ae (map f μ)

Tactic:
rw [mem_ae_map_iff h hf]

Result:
case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ f ⁻¹' range f ∈ ae μ

Proof state:
case neg
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : ¬AEMeasurable f μ
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f

Tactic:
simp [map_of_not_aemeasurable h]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ ∀ᵐ (x : β) ∂map f μ, x ∈ range f

Tactic:
change range f ∈ ae (μ.map f)

Result:
case pos
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m0 : MeasurableSpace α
f : α → β
hf : MeasurableSet (range f)
μ : Measure α
h : AEMeasurable f μ
⊢ range f ∈ ae (map f μ)
-- Mathlib/Algebra/ModEq.lean
theorem modEq_iff_eq_add_zsmul : a ≡ b [PMOD p] ↔ ∃ z : ℤ, b = a + z • p

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
⊢ a ≡ b [PMOD p] ↔ ∃ z, b = a + z • p

Tactic:
simp_rw [ModEq, sub_eq_iff_eq_add']

Result:
no goals
-- Mathlib/Topology/ApproximateUnit.lean
/-- In a topological unital magma, `𝓝 1` is the largest approximate unit. -/
lemma iff_le_nhds_one [ContinuousMul α] {l : Filter α} [l.NeBot] :
    IsApproximateUnit l ↔ l ≤ 𝓝 1

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MulOneClass α
inst✝¹ : ContinuousMul α
l : Filter α
inst✝ : l.NeBot
⊢ l.IsApproximateUnit ↔ l ≤ 𝓝 1

Tactic:
simpa [iff_neBot_and_le_nhds_one] using fun _ ↦ ‹_›

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_sub_div (hc : c ≠ 0) (d) :
    (∫ x in a..b, f (d - x / c)) = c • ∫ x in d - b / c..d - a / c, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d - x / c) = c • ∫ (x : ℝ) in d - b / c..d - a / c, f x

Tactic:
simpa only [div_eq_inv_mul, inv_inv] using integral_comp_sub_mul f (inv_ne_zero hc) d

Result:
no goals
-- Mathlib/LinearAlgebra/Semisimple.lean
lemma eq_zero_of_isNilpotent_of_isFinitelySemisimple
    (hn : IsNilpotent f) (hs : IsFinitelySemisimple f) : f = 0

Proof state:
case intro.intro.a.inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
i : ℕ
hk : f ^ i = 0
p : Submodule R M := Submodule.span R {x_1 | ∃ i_1, ∃ (_ : i_1 ≤ i), (f ^ i_1) x = x_1}
hi : i ≤ i
⊢ f ((f ^ i) x) ∈ {x_1 | ∃ i_1, ∃ (_ : i_1 ≤ i), (f ^ i_1) x = x_1}

Tactic:
exact ⟨i, by simp [hk]⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
i : ℕ
hk : f ^ i = 0
p : Submodule R M := Submodule.span R {x_1 | ∃ i_1, ∃ (_ : i_1 ≤ i), (f ^ i_1) x = x_1}
hi : i ≤ i
⊢ ∃ (_ : i ≤ i), (f ^ i) x = f ((f ^ i) x)

Tactic:
simp [hk]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem exists_pow_neg_lt {ε : ℝ} (hε : 0 < ε) : ∃ k : ℕ, (p : ℝ) ^ (-(k : ℤ)) < ε

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
⊢ ∃ k, ↑p ^ (-↑k) < ε

Tactic:
obtain ⟨k, hk⟩ := exists_nat_gt ε⁻¹

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ∃ k, ↑p ^ (-↑k) < ε

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ∃ k, ↑p ^ (-↑k) < ε

Tactic:
use k

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ↑p ^ (-↑k) < ε

Proof state:
case h.hab.convert_3
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 1 < p

Tactic:
exact hp.1.one_lt

Result:
no goals

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < ↑p ^ k

Tactic:
apply lt_of_lt_of_le hk

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ↑k ≤ ↑p ^ k

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 0 < ↑p

Tactic:
exact mod_cast hp.1.pos

Result:
no goals

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ↑k ≤ ↑p ^ k

Tactic:
norm_cast

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ k ≤ p ^ k

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ k ≤ p ^ k

Tactic:
apply le_of_lt

Result:
case h.hab
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ k < p ^ k

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < (↑p ^ (-↑k))⁻¹

Tactic:
rw [zpow_neg, inv_inv, zpow_natCast]

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < ↑p ^ k

Proof state:
case h.hab
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ k < p ^ k

Tactic:
convert Nat.lt_pow_self _ using 1

Result:
case h.hab.convert_3
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 1 < p

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ↑p ^ (-↑k) < ε

Tactic:
rw [← inv_lt_inv₀ hε (zpow_pos _ _)]

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < (↑p ^ (-↑k))⁻¹

p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 0 < ↑p
-- Mathlib/Data/Finite/Prod.lean
lemma finite_image2 (hfs : ∀ b ∈ t, InjOn (f · b) s) (hft : ∀ a ∈ s, InjOn (f a) t) :
    (image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun x => f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅) ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun x => f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

Tactic:
rw [← not_infinite, infinite_image2 hfs hft]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun x => f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ ¬(s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty) ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun x => f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ ¬(s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty) ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

Tactic:
simp [not_or, -not_and, not_and_or, not_nonempty_iff_eq_empty]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun x => f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅) ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅