awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
inl : ∀ (h : IsEmpty ((i : ι) → α i)), WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2
inr : ∀ (x : (i : ι) → α i), WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2
⊢ WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2

Tactic:
obtain h | ⟨⟨x⟩⟩ := isEmpty_or_nonempty (∀ i, α i)

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
h : IsEmpty ((i : ι) → α i)
⊢ WellFounded (α := (i : ι) → α i) WellFoundedRelation.rel

Tactic:
emptyWf.wf

Premises used: WellFoundedRelation.wf
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
h : IsEmpty ((i : ι) → α i)
⊢ WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2

Tactic:
convert! emptyWf.wf

Premises used: WellFoundedRelation.wf
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
x : (i : ι) → α i
this : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := WellFounded.min (r := fun (x1 x2 : α i) ↦ x1 < x2) ⋯ ⊤ ⋯ }
inr : ∀ (this : Fintype ι), WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2
⊢ WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
x : (i : ι) → α i
this_1 : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := WellFounded.min (r := fun (x1 x2 : α i) ↦ x1 < x2) ⋯ ⊤ ⋯ }
this : Fintype ι
⊢ WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2

Tactic:
InvImage.wf equivFunOnFintype.symm (DFinsupp.wellFoundedLT fun i a => ?_).wf

Premises used: InvImage, DFinsupp.equivFunOnFintype, IsWellFounded.wf, InvImage.wf, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
x : (i : ι) → α i
this_1 : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := WellFounded.min (r := fun (x1 x2 : α i) ↦ x1 < x2) ⋯ ⊤ ⋯ }
this : Fintype ι
inr : ∀ (i : ι) (a : α i), ¬a < 0
⊢ WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2

Tactic:
refine InvImage.wf equivFunOnFintype.symm (DFinsupp.wellFoundedLT fun i a => ?_).wf

Premises used: DFinsupp.equivFunOnFintype, IsWellFounded.wf, InvImage.wf, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
x : (i : ι) → α i
this_1 : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := WellFounded.min (r := fun (x1 x2 : α i) ↦ x1 < x2) ⋯ ⊤ ⋯ }
this : Fintype ι
i : ι
a : α i
⊢ ¬a < 0

Tactic:
(hw i).wf.not_lt_min ⊤ trivial

Premises used: trivial, IsWellFounded.wf, WellFounded.not_lt_min, Top.top
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
x : (i : ι) → α i
this_1 : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := WellFounded.min (r := fun (x1 x2 : α i) ↦ x1 < x2) ⋯ ⊤ ⋯ }
this : Fintype ι
i : ι
a : α i
⊢ ¬a < 0

Tactic:
exact (hw i).wf.not_lt_min ⊤ trivial

Premises used: trivial, IsWellFounded.wf, WellFounded.not_lt_min, Top.top
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α_1 : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α_1 i → α_1 i → Prop
α : Type u_3
inst : Finite ι
inst_1 : Preorder α
inst_2 : WellFoundedLT α
⊢ WellFoundedLT (ι → α)

Tactic:
Pi.wellFoundedLT

Premises used: Pi.wellFoundedLT
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Zero (α i)
inst_2 : (i : ι) → Preorder (α i)
inst_3 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
⊢ WellFoundedLT (Π₀ (i : ι), α i)

Tactic:
have := Fintype.ofFinite ι
  ⟨InvImage.wf equivFunOnFintype Pi.wellFoundedLT.wf⟩

Premises used: Fintype.ofFinite, IsWellFounded.mk, DFinsupp.equivFunOnFintype, IsWellFounded.wf, InvImage.wf, DFunLike.coe
-- Module: Mathlib.Data.DList.Instances
Goal:
α : Type u_1
⊢ LawfulTraversable DList

Tactic:
Equiv.isLawfulTraversable DList.listEquivDList

Premises used: Batteries.DList.listEquivDList, Equiv.isLawfulTraversable
-- Module: Mathlib.Data.ENNReal.Action
Goal:
M : Type u_1
inst : MulAction ℝ≥0∞ M
c : ℝ≥0
x : M
⊢ c • x = (↑c : ℝ≥0∞) • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ENNReal.Action
Goal:
c : ℝ≥0
⊢ HSMul.hSMul (β := ℝ≥0∞) c 1 = (↑c : ℝ≥0∞)

Tactic:
simp [smul_def]

Premises used: ENNReal.smul_def
-- Module: Mathlib.Data.ENNReal.Action
Goal:
a b c d : ℝ≥0∞
r_1 p q : ℝ≥0
A : Type u_1
inst : Semiring A
inst_1 : Algebra ℝ≥0∞ A
r : ℝ≥0
x : A
⊢ HMul.hMul (α := A) ((RingHom.comp (algebraMap ℝ≥0∞ A) ofNNRealHom : (a : ℝ≥0) → A) r : A) x =
    HMul.hMul (β := A) x ((RingHom.comp (algebraMap ℝ≥0∞ A) ofNNRealHom : (a : ℝ≥0) → A) r : A)

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- Module: Mathlib.Data.ENNReal.Action
Goal:
a b c d : ℝ≥0∞
r_1 p q : ℝ≥0
A : Type u_1
inst : Semiring A
inst_1 : Algebra ℝ≥0∞ A
r : ℝ≥0
x : A
⊢ r • x = HMul.hMul (α := A) ((RingHom.comp (algebraMap ℝ≥0∞ A) ofNNRealHom : (a : ℝ≥0) → A) r : A) x

Tactic:
simp [← Algebra.smul_def (r : ℝ≥0∞) x, smul_def]

Premises used: ENNReal.ofNNReal, ENNReal.smul_def, Algebra.smul_def
-- Module: Mathlib.Data.ENNReal.Action
Goal:
R : Type u_1
r : R
s : ℝ≥0
inst : SMul R ℝ≥0
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0 ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
rw : (↑(r • s) : ℝ≥0∞) = HSMul.hSMul (β := ℝ≥0) r 1 • (↑s : ℝ≥0∞)
rw₁ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ≥0∞) • (↑s : ℝ≥0∞)
rw₂ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ≥0∞) * (↑s : ℝ≥0∞)
rw₃ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1 * s) : ℝ≥0∞)
rw₄ : (↑(r • s) : ℝ≥0∞) = (↑(r • (1 * s)) : ℝ≥0∞)
rw₅ rw₆ : (↑(r • s) : ℝ≥0∞) = (↑(r • s) : ℝ≥0∞)
⊢ (↑(r • s) : ℝ≥0∞) = r • (↑s : ℝ≥0∞)

Tactic:
rw [← smul_one_smul ℝ≥0 r (s : ℝ≥0∞), smul_def, smul_eq_mul, ← ENNReal.coe_mul, smul_mul_assoc,
    one_mul]

Premises used: ENNReal.ofNNReal, ENNReal.smul_def, smul_mul_assoc, NNReal, ENNReal.coe_mul, smul_one_smul, smul_eq_mul, one_mul
-- Module: Mathlib.Data.ENNReal.Action
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
inst_5 : DecidableEq R
c : R
rw : Eq (α := ℝ≥0∞) (if HSMul.hSMul (β := ℝ≥0∞) c 1 = 0 then 0 else ∞) (if c = 0 then 0 else ∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) c ∞ = if c = 0 then 0 else ∞

Tactic:
rw [← smul_one_mul, mul_top']

Premises used: ENNReal.mul_top', smul_one_mul
-- Module: Mathlib.Data.ENNReal.Action
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
inst_5 : DecidableEq R
c : R
simp_rw : Eq (α := ℝ≥0∞) (if c = 0 ∨ Eq (α := ℝ≥0∞) 1 0 then 0 else ∞) (if c = 0 then 0 else ∞)
⊢ Eq (α := ℝ≥0∞) (if HSMul.hSMul (β := ℝ≥0∞) c 1 = 0 then 0 else ∞) (if c = 0 then 0 else ∞)

Tactic:
simp_rw [smul_eq_zero, or_iff_left one_ne_zero]

Premises used: or_iff_left, one_ne_zero, smul_eq_zero
-- Module: Mathlib.Data.ENNReal.Action
Goal:
x : ℝ≥0
y : ℝ≥0∞
hy : y < ∞
⊢ (↑x : ℝ≥0∞) < ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Action
Goal:
x : ℝ≥0
y : ℝ≥0∞
hy : y ≠ ∞
⊢ (↑x : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Action
Goal:
x : ℝ≥0
hx : x ≠ 0
h : HSMul.hSMul (β := ℝ≥0∞) x ∞ ≠ ∞
⊢ False

Tactic:
simp [smul_top (R := ℝ≥0), hx] at h

Premises used: ENNReal.smul_top
-- Module: Mathlib.Data.ENNReal.Action
Goal:
x : ℝ≥0
y : ℝ≥0∞
hx : x ≠ 0
rw : x • y ≠ ∞ ↔ y < ∞
rw₁ : x • y ≠ ∞ ↔ y ≠ ∞
rw₂ rw₃ : y ≠ ∞ ↔ y ≠ ∞
⊢ x • y < ∞ ↔ y < ∞

Tactic:
rw [lt_top_iff_ne_top, lt_top_iff_ne_top, nnreal_smul_ne_top_iff hx]

Premises used: lt_top_iff_ne_top, ENNReal.nnreal_smul_ne_top_iff
-- Module: Mathlib.Data.ENNReal.Action
Goal:
a : ℝ≥0
b : ℝ≥0∞
⊢ ((↑a : ℝ≥0∞) * b).toNNReal = a * b.toNNReal

Tactic:
simp only [ENNReal.toNNReal_mul, ENNReal.toNNReal_coe]

Premises used: ENNReal.toNNReal_coe, ENNReal.toNNReal_mul
-- Module: Mathlib.Data.ENNReal.Action
Goal:
r : ℝ≥0
s : ℝ≥0∞
rw : (↑r : ℝ) * s.toReal = r • s.toReal
⊢ (r • s).toReal = r • s.toReal

Tactic:
rw [ENNReal.smul_def, smul_eq_mul, toReal_mul, coe_toReal]

Premises used: ENNReal.smul_def, ENNReal.coe_toReal, ENNReal.toReal_mul, smul_eq_mul
-- Module: Mathlib.Data.ENNReal.Action
Goal:
r : ℝ≥0
s : ℝ≥0∞
⊢ (↑r : ℝ) * s.toReal = r • s.toReal

Tactic:
rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
⊢ Eq (α := ℝ≥0∞) 0 ⊥

Tactic:
rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
⊢ Eq (α := ℝ≥0∞) 0 ⊥

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
⊢ CharZero ℝ≥0∞

Tactic:
inferInstanceAs (CharZero (WithTop ℝ≥0))

Premises used: _private.0.ENNReal.instCharZero._proof_1
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
⊢ IsOrderedRing ℝ≥0∞

Tactic:
inferInstanceAs (IsOrderedRing (WithTop ℝ≥0))

Premises used: _private.0.ENNReal.instIsOrderedRing._proof_1
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
⊢ CanonicallyOrderedAdd ℝ≥0∞

Tactic:
inferInstanceAs (CanonicallyOrderedAdd (WithTop ℝ≥0))

Premises used: _private.0.ENNReal.instCanonicallyOrderedAdd._proof_1
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
⊢ NoZeroDivisors ℝ≥0∞

Tactic:
inferInstanceAs (NoZeroDivisors (WithTop ℝ≥0))

Premises used: _private.0.ENNReal.instNoZeroDivisors._proof_1
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
⊢ DenselyOrdered ℝ≥0∞

Tactic:
inferInstanceAs (DenselyOrdered (WithTop ℝ≥0))

Premises used: _private.0.ENNReal.instDenselyOrdered._proof_1
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
⊢ IsOrderedAddMonoid ℝ≥0∞

Tactic:
inferInstanceAs (IsOrderedAddMonoid (WithTop ℝ≥0))

Premises used: _private.0.ENNReal.instIsOrderedAddMonoid._proof_1
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
⊢ OrderedSub ℝ≥0∞

Tactic:
inferInstanceAs (OrderedSub (WithTop ℝ≥0))

Premises used: _private.0.ENNReal.instOrderedSub._proof_1
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
a : AddUnits ℝ≥0∞
rw : (↑a : ℝ≥0∞) ≤ (↑a : ℝ≥0∞) + (↑(-a) : ℝ≥0∞)
⊢ (↑a : ℝ≥0∞) ≤ 0

Tactic:
rw [← a.add_neg]

Premises used: AddUnits.add_neg
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
a : AddUnits ℝ≥0∞
⊢ (↑a : ℝ≥0∞) ≤ (↑a : ℝ≥0∞) + (↑(-a) : ℝ≥0∞)

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
a_1 b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
a : AddUnits ℝ≥0∞
⊢ (↑a : ℝ≥0∞) ≤ (↑a : ℝ≥0∞) + (↑(-a) : ℝ≥0∞)

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
α : Type u_1
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ CanLift ℝ≥0∞ ℝ≥0 ofNNReal fun (x : ℝ≥0∞) ↦ x ≠ ∞

Tactic:
WithTop.canLift

Premises used: ENNReal.ofNNReal, WithTop.canLift, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ Eq (α := Option ℝ≥0) none ∞

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0
⊢ some a = (↑a : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.some, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0
⊢ (↑a : WithTop ℝ≥0) = (↑a : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ Injective ofNNReal

Tactic:
WithTop.coe_injective

Premises used: ENNReal.ofNNReal, WithTop.coe_injective, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
p q : ℝ≥0
⊢ (↑p : ℝ≥0∞) = (↑q : ℝ≥0∞) ↔ p = q

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, ENNReal.coe_injective
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
p q : ℝ≥0
⊢ (↑p : ℝ≥0∞) ≠ (↑q : ℝ≥0∞) ↔ p ≠ q

Tactic:
coe_inj.not

Premises used: ENNReal.coe_inj, Iff.not
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ range ofNNReal = Iio ∞

Tactic:
WithTop.range_coe

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.range_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ range ofNNReal = {∞}ᶜ

Tactic:
(isCompl_range_some_none ℝ≥0).symm.compl_eq.symm

Premises used: ENNReal.ofNNReal, Set.isCompl_range_some_none, Set.Mem, setOf, NNReal, IsCompl.compl_eq, WithTop.some, ENNReal, Eq.symm, WithTop, IsCompl.symm
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
q : ℚ≥0
⊢ (↑(↑q : ℝ≥0) : ℝ≥0∞) = (↑q : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ (↑r : ℝ≥0∞).toNNReal = r

Tactic:
rfl

Premises used: ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
ι : Type u_2
f : ι → ℝ≥0∞
hf : ∀ (x : ι), f x ≠ ∞
h : ∀ (x : ι), ((fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f) x = f x
⊢ (fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f = f

Tactic:
ext x
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
ι : Type u_2
f : ι → ℝ≥0∞
hf : ∀ (x : ι), f x ≠ ∞
x : ι
⊢ ((fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f) x = f x

Tactic:
simp [coe_toNNReal (hf x)]

Premises used: ENNReal.coe_toNNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
h : a ≠ ∞
⊢ ENNReal.ofReal a.toReal = a

Tactic:
simp [ENNReal.toReal, ENNReal.ofReal, h]

Premises used: ENNReal.ofReal, ENNReal.toReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ
h : 0 ≤ r
⊢ (ENNReal.ofReal r).toReal = r

Tactic:
max_eq_left h

Premises used: max_eq_left, ENNReal.toReal, NNReal.toReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ
⊢ (ENNReal.ofReal r).toReal = max r 0

Tactic:
rfl

Premises used: ENNReal.toReal, NNReal.toReal, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
rw rw₁ : (↑r : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)
⊢ (↑(↑r : ℝ≥0∞).toNNReal : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)

Tactic:
rw [toNNReal_coe]

Premises used: ENNReal.toNNReal_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
rw : (↑r : ℝ≥0∞) = (↑(↑r : ℝ).toNNReal : ℝ≥0∞)
rw₁ rw₂ : (↑r : ℝ≥0∞) = (↑r : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) = ENNReal.ofReal (↑r : ℝ)

Tactic:
rw [ENNReal.ofReal, Real.toNNReal_coe]

Premises used: ENNReal.ofReal, Real.toNNReal_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x : ℝ
h : 0 ≤ x
⊢ ENNReal.ofReal x = (↑(NNReal.mk x h) : ℝ≥0∞)

Tactic:
(coe_nnreal_eq ⟨x, h⟩).symm

Premises used: NNReal.mk, Subtype.mk, ENNReal.coe_nnreal_eq, Eq.symm, NNReal.toReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x : ℝ
⊢ (↑x.toNNReal : ℝ≥0∞) = ENNReal.ofReal x

Tactic:
rfl

Premises used: ENNReal.ofReal, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
p : ℝ≥0
⊢ ENNReal.ofReal (↑p : ℝ) = (↑p : ℝ≥0∞)

Tactic:
(coe_nnreal_eq p).symm

Premises used: ENNReal.coe_nnreal_eq, Eq.symm
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ (↑0 : ℝ≥0∞) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ (↑1 : ℝ≥0∞) = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
⊢ 0 ≤ a.toReal

Tactic:
a.toNNReal.2

Premises used: ENNReal.toNNReal, ENNReal.toReal, NNReal.toReal, Subtype.property
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
z : ℝ≥0∞
⊢ (↑z.toNNReal : ℝ) = z.toReal

Tactic:
rfl

Premises used: ENNReal.toReal, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
z : ℝ≥0∞
a : (↑z.toReal.toNNReal : ℝ) = (↑z.toNNReal : ℝ)
⊢ z.toReal.toNNReal = z.toNNReal

Tactic:
ext
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
z : ℝ≥0∞
⊢ (↑z.toReal.toNNReal : ℝ) = (↑z.toNNReal : ℝ)

Tactic:
simp [coe_toNNReal_eq_toReal]

Premises used: ENNReal.coe_toNNReal_eq_toReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ ENNReal.toNNReal ∞ = 0

Tactic:
rfl

Premises used: ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ ENNReal.toReal ∞ = 0

Tactic:
rfl

Premises used: ENNReal.toReal, NNReal.toReal, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ ENNReal.toReal 1 = 1

Tactic:
rfl

Premises used: ENNReal.toReal, NNReal.toReal, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ ENNReal.toNNReal 1 = 1

Tactic:
rfl

Premises used: ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ (↑r : ℝ≥0∞).toReal = (↑r : ℝ)

Tactic:
rfl

Premises used: ENNReal.toNNReal, ENNReal.toReal, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ ENNReal.toNNReal 0 = 0

Tactic:
rfl

Premises used: ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ ENNReal.toReal 0 = 0

Tactic:
rfl

Premises used: ENNReal.toReal, NNReal.toReal, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ ENNReal.ofReal 0 = 0

Tactic:
simp [ENNReal.ofReal]

Premises used: ENNReal.ofReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ ENNReal.ofReal 1 = 1

Tactic:
simp [ENNReal.ofReal]

Premises used: ENNReal.ofReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
⊢ ENNReal.ofReal a.toReal ≤ a

Tactic:
if ha : a = ∞ then ha.symm ▸ le_top else le_of_eq (ofReal_toReal ha)

Premises used: Eq.rec, ENNReal.ofReal_toReal, dite, le_top, le_of_eq, Eq.symm
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
p : ℝ≥0∞ → Prop
⊢ (∀ (a : ℝ≥0∞), p a) ↔ (∀ (r : ℝ≥0), p (↑r : ℝ≥0∞)) ∧ p ∞

Tactic:
WithTop.forall.trans and_comm

Premises used: WithTop.forall, and_comm, ENNReal, Iff.trans
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
p : ℝ≥0∞ → Prop
⊢ (∀ (x : ℝ≥0∞), x ≠ ∞ → p x) ↔ ∀ (x : ℝ≥0), p (↑x : ℝ≥0∞)

Tactic:
WithTop.forall_ne_top

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.forall_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
p : ℝ≥0∞ → Prop
⊢ (∃ (x : ℝ≥0∞), x ≠ ∞ ∧ p x) ↔ ∃ (x : ℝ≥0), p (↑x : ℝ≥0∞)

Tactic:
WithTop.exists_ne_top

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.exists_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x : ℝ≥0∞
⊢ x.toNNReal = 0 ↔ x = 0 ∨ x = ∞

Tactic:
WithTop.untopD_eq_self_iff

Premises used: ENNReal.ofNNReal, ENNReal.toNNReal, WithTop.some, ENNReal, WithTop.untopD_eq_self_iff
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x : ℝ≥0∞
⊢ x.toReal = 0 ↔ x = 0 ∨ x = ∞

Tactic:
simp [ENNReal.toReal, toNNReal_eq_zero_iff]

Premises used: ENNReal.toNNReal_eq_zero_iff, ENNReal.toReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
⊢ a.toNNReal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ∞

Tactic:
a.toNNReal_eq_zero_iff.not.trans not_or

Premises used: ENNReal.toNNReal_eq_zero_iff, Iff.not, not_or, Iff.trans
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
⊢ a.toReal ≠ 0 ↔ a ≠ 0 ∧ a ≠ ∞

Tactic:
a.toReal_eq_zero_iff.not.trans not_or

Premises used: Iff.not, not_or, Iff.trans, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x : ℝ≥0∞
⊢ x = (↑1 : WithTop ℝ≥0) ∨ x = ⊤ ∧ Eq (α := ℝ≥0) 1 0 ↔ x = 1

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x : ℝ≥0∞
rw : (↑x.toNNReal : ℝ) = 1 ↔ x = 1
rw₁ : x.toNNReal = 1 ↔ x = 1
rw₂ rw₃ : x = 1 ↔ x = 1
⊢ x.toReal = 1 ↔ x = 1

Tactic:
rw [ENNReal.toReal, NNReal.coe_eq_one, ENNReal.toNNReal_eq_one_iff]

Premises used: ENNReal.toNNReal_eq_one_iff, ENNReal.toReal, NNReal.coe_eq_one
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
⊢ a.toNNReal ≠ 1 ↔ a ≠ 1

Tactic:
a.toNNReal_eq_one_iff.not

Premises used: ENNReal.toNNReal_eq_one_iff, Iff.not
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
⊢ a.toReal ≠ 1 ↔ a ≠ 1

Tactic:
a.toReal_eq_one_iff.not

Premises used: Iff.not, ENNReal.toReal_eq_one_iff
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) ≠ ∞

Tactic:
WithTop.coe_ne_top

Premises used: ENNReal.ofNNReal, WithTop.coe_ne_top, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ ∞ ≠ (↑r : ℝ≥0∞)

Tactic:
WithTop.top_ne_coe

Premises used: ENNReal.ofNNReal, WithTop.top_ne_coe, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) < ∞

Tactic:
WithTop.coe_lt_top r

Premises used: ENNReal.ofNNReal, WithTop.coe_lt_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ
⊢ ENNReal.ofReal r ≠ ∞

Tactic:
coe_ne_top

Premises used: ENNReal.ofReal, ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ
⊢ ENNReal.ofReal r < ∞

Tactic:
coe_lt_top

Premises used: ENNReal.ofReal, ENNReal.coe_lt_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ
⊢ ∞ ≠ ENNReal.ofReal r

Tactic:
top_ne_coe

Premises used: ENNReal.top_ne_coe, ENNReal.ofReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
h : ENNReal.ofReal a.toReal = a
rw : ENNReal.ofReal a.toReal ≠ ∞
⊢ a ≠ ∞

Tactic:
rw [← h]
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
h : ENNReal.ofReal a.toReal = a
⊢ ENNReal.ofReal a.toReal ≠ ∞

Tactic:
ofReal_ne_top

Premises used: ENNReal.ofReal_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
h : ENNReal.ofReal a.toReal = a
⊢ ENNReal.ofReal a.toReal ≠ ∞

Tactic:
exact ofReal_ne_top

Premises used: ENNReal.ofReal_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ
h : (ENNReal.ofReal a).toReal = a
rw : 0 ≤ (ENNReal.ofReal a).toReal
⊢ 0 ≤ a

Tactic:
rw [← h]
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ
h : (ENNReal.ofReal a).toReal = a
⊢ 0 ≤ (ENNReal.ofReal a).toReal

Tactic:
toReal_nonneg

Premises used: ENNReal.toReal_nonneg
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ
h : (ENNReal.ofReal a).toReal = a
⊢ 0 ≤ (ENNReal.ofReal a).toReal

Tactic:
exact toReal_nonneg

Premises used: ENNReal.toReal_nonneg
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ Ne (α := ℝ≥0∞) 0 ∞

Tactic:
coe_ne_top

Premises used: ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ Ne (α := ℝ≥0∞) ∞ 0

Tactic:
top_ne_coe

Premises used: ENNReal.top_ne_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
coe_ne_top

Premises used: ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ Ne (α := ℝ≥0∞) ∞ 1

Tactic:
top_ne_coe

Premises used: ENNReal.top_ne_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
coe_lt_top

Premises used: ENNReal.coe_lt_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r q : ℝ≥0
⊢ (↑r : ℝ≥0∞) ≤ (↑q : ℝ≥0∞) ↔ r ≤ q

Tactic:
WithTop.coe_le_coe

Premises used: ENNReal.ofNNReal, WithTop.coe_le_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r q : ℝ≥0
⊢ (↑r : ℝ≥0∞) < (↑q : ℝ≥0∞) ↔ r < q

Tactic:
WithTop.coe_lt_coe

Premises used: ENNReal.ofNNReal, WithTop.coe_lt_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ Monotone ofNNReal

Tactic:
fun _ _ => coe_le_coe.2

Premises used: Iff.mpr, Monotone, ENNReal.coe_le_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ StrictMono ofNNReal

Tactic:
fun _ _ => coe_lt_coe.2

Premises used: Iff.mpr, StrictMono, ENNReal.coe_lt_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) = 0 ↔ r = 0

Tactic:
coe_inj

Premises used: ENNReal.coe_inj
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ 0 = (↑r : ℝ≥0∞) ↔ 0 = r

Tactic:
coe_inj

Premises used: ENNReal.coe_inj
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) = 1 ↔ r = 1

Tactic:
coe_inj

Premises used: ENNReal.coe_inj
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ 1 = (↑r : ℝ≥0∞) ↔ 1 = r

Tactic:
coe_inj

Premises used: ENNReal.coe_inj
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ 0 < (↑r : ℝ≥0∞) ↔ 0 < r

Tactic:
coe_lt_coe

Premises used: ENNReal.coe_lt_coe
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) ≠ 0 ↔ r ≠ 0

Tactic:
WithTop.coe_ne_zero

Premises used: ENNReal.ofNNReal, WithTop.coe_ne_zero, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) ≠ 1 ↔ r ≠ 1

Tactic:
WithTop.coe_ne_one

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.coe_ne_one
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x y : ℝ≥0
⊢ (↑(x + y) : ℝ≥0∞) = (↑x : ℝ≥0∞) + (↑y : ℝ≥0∞)

Tactic:
rfl

Premises used: ENNReal.ofNNReal, WithTop.map₂, WithTop.some, rfl, Option.map₂