harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Log.lean
private lemma logC_spec {b m : ℕ} (hb : 1 < b) (hm : 0 < m) :
    b ^ logC b m ≤ m ∧ m < b ^ (logC b m + 1)

Proof state:
b m : ℕ
hb : 1 < b
hm : 0 < m
x✝ : ℕ × ℕ
q e : ℕ
heq : logC.step m b hb = (q, e)
⊢ b ^ e ≤ m ∧ m < b ^ (e + 1)

Tactic:
obtain ⟨h₁, h₂, h₃, h₄⟩ := logC_step hb heq

Result:
case intro.intro.intro
b m : ℕ
hb : 1 < b
hm : 0 < m
x✝ : ℕ × ℕ
q e : ℕ
heq : logC.step m b hb = (q, e)
h₁ : b ^ e * q ≤ m
h₂ : q < b
h₃ : m < b ^ e * (q + 1)
h₄ : 0 < m → 0 < q
⊢ b ^ e ≤ m ∧ m < b ^ (e + 1)

Proof state:
case intro.intro.intro
b m : ℕ
hb : 1 < b
hm : 0 < m
x✝ : ℕ × ℕ
q e : ℕ
heq : logC.step m b hb = (q, e)
h₁ : b ^ e * q ≤ m
h₂ : q < b
h₃ : m < b ^ e * (q + 1)
h₄ : 0 < m → 0 < q
⊢ b ^ e ≤ m ∧ m < b ^ (e + 1)

Tactic:
exact ⟨h₁.trans' (Nat.le_mul_of_pos_right _ (h₄ hm)), h₃.trans_le (Nat.mul_le_mul_left _ h₂)⟩

Result:
no goals

Proof state:
b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b ^ logC b m ≤ m ∧ m < b ^ (logC b m + 1)

Tactic:
rw [logC, dif_pos hb]

Result:
b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ (b ^
        match logC.step m b hb with
        | (fst, e) => e) ≤
      m ∧
    m <
      b ^
        ((match logC.step m b hb with
          | (fst, e) => e) +
          1)

Proof state:
b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ (b ^
        match logC.step m b hb with
        | (fst, e) => e) ≤
      m ∧
    m <
      b ^
        ((match logC.step m b hb with
          | (fst, e) => e) +
          1)

Tactic:
split

Result:
b m : ℕ
hb : 1 < b
hm : 0 < m
x✝ : ℕ × ℕ
q✝ e✝ : ℕ
heq✝ : logC.step m b hb = (q✝, e✝)
⊢ b ^ e✝ ≤ m ∧ m < b ^ (e✝ + 1)

Proof state:
b m : ℕ
hb : 1 < b
hm : 0 < m
x✝ : ℕ × ℕ
q✝ e✝ : ℕ
heq✝ : logC.step m b hb = (q✝, e✝)
⊢ b ^ e✝ ≤ m ∧ m < b ^ (e✝ + 1)

Tactic:
next q e heq =>
obtain ⟨h₁, h₂, h₃, h₄⟩ := logC_step hb heq
exact ⟨h₁.trans' (Nat.le_mul_of_pos_right _ (h₄ hm)), h₃.trans_le (Nat.mul_le_mul_left _ h₂)⟩

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma rootSpan_dualAnnihilator_map_eq :
    P.rootSpan.dualAnnihilator.map P.toDualRight.symm =
      (span R (range P.root')).dualCoannihilator

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ Submodule.map P.toDualRight.symm P.rootSpan.dualAnnihilator = (span R (range P.root')).dualCoannihilator

Tactic:
apply SetLike.coe_injective

Result:
case a
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ ↑(Submodule.map P.toDualRight.symm P.rootSpan.dualAnnihilator) = ↑(span R (range P.root')).dualCoannihilator

Proof state:
case a
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ ↑(Submodule.map P.toDualRight.symm P.rootSpan.dualAnnihilator) = ↑(span R (range P.root')).dualCoannihilator

Tactic:
rw [Submodule.coe_dualCoannihilator_span, coe_rootSpan_dualAnnihilator_map]

Result:
case a
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ {x | ∀ (i : ι), (P.root' i) x = 0} = {x | ∀ f ∈ range P.root', f x = 0}

Proof state:
case a
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ {x | ∀ (i : ι), (P.root' i) x = 0} = {x | ∀ f ∈ range P.root', f x = 0}

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
lemma interior_extend_target_subset_interior_range :
    interior (f.extend I).target ⊆ interior (range I)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ interior (f.extend I).target ⊆ interior (range ↑I)

Tactic:
rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ↑I.symm ⁻¹' f.target ∩ interior (range ↑I) ⊆ interior (range ↑I)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ↑I.symm ⁻¹' f.target ∩ interior (range ↑I) ⊆ interior (range ↑I)

Tactic:
exact inter_subset_right

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem mrange_inl_sup_mrange_inr : mrange (inl M N) ⊔ mrange (inr M N) = ⊤

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mrange (inl M N) ⊔ mrange (inr M N) = ⊤

Tactic:
simp only [mrange_inl, mrange_inr, prod_bot_sup_bot_prod, top_prod_top]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma sups_eq_self : s ⊻ s = s ↔ SupClosed (s : Set α)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : SemilatticeSup α
s : Finset α
⊢ s ⊻ s = s ↔ SupClosed ↑s

Tactic:
simp [← coe_inj]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem preimage_div_preimage_subset {s t : Set β} : m ⁻¹' s / m ⁻¹' t ⊆ m ⁻¹' (s / t)

Proof state:
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
s t : Set β
w✝¹ : α
left✝¹ : w✝¹ ∈ ⇑m ⁻¹' s
w✝ : α
left✝ : w✝ ∈ ⇑m ⁻¹' t
⊢ (fun x1 x2 => x1 / x2) w✝¹ w✝ ∈ ⇑m ⁻¹' (s / t)

Tactic:
exact ⟨_, ‹_›, _, ‹_›, (map_div m ..).symm⟩

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
s t : Set β
⊢ ⇑m ⁻¹' s / ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s / t)

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

Result:
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
s t : Set β
w✝¹ : α
left✝¹ : w✝¹ ∈ ⇑m ⁻¹' s
w✝ : α
left✝ : w✝ ∈ ⇑m ⁻¹' t
⊢ (fun x1 x2 => x1 / x2) w✝¹ w✝ ∈ ⇑m ⁻¹' (s / t)
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem exists_isCompact_not_null [InnerRegular μ] : (∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.InnerRegular
⊢ (∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0

Tactic:
simp_rw [Ne, ← measure_univ_eq_zero, MeasurableSet.univ.measure_eq_iSup_isCompact,
  ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cmp_to_nat : ∀ m n, (Ordering.casesOn (cmp m n) ((m : ℕ) < n) (m = n) ((n : ℕ) < m) : Prop)
  | 1, 1 => rfl
  | bit0 a, 1 =>
    let h : (1 : ℕ) ≤ a := to_nat_pos a
    Nat.add_le_add h h
  | bit1 a, 1 => Nat.succ_lt_succ <| to_nat_pos <| bit0 a
  | 1, bit0 b =>
    let h : (1 : ℕ) ≤ b := to_nat_pos b
    Nat.add_le_add h h
  | 1, bit1 b => Nat.succ_lt_succ <| to_nat_pos <| bit0 b
  | bit0 a, bit0 b => by
    dsimp [cmp]
    have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
    · exact Nat.add_lt_add this this
    · rw [this]
    · exact Nat.add_lt_add this this
  | bit0 a, bit1 b => by
    dsimp [cmp]
    have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
    · exact Nat.le_succ_of_le (Nat.add_lt_add this this)
    · rw [this]
      apply Nat.lt_succ_self
    · exact cmp_to_nat_lemma this
  | bit1 a, bit0 b => by
    dsimp [cmp]
    have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
    · exact cmp_to_nat_lemma this
    · rw [this]
      apply Nat.lt_succ_self
    · exact Nat.le_succ_of_le (Nat.add_lt_add this this)
  | bit1 a, bit1 b => by
    dsimp [cmp]
    have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
    · exact Nat.succ_lt_succ (Nat.add_lt_add this this)
    · rw [this]
    · exact Nat.succ_lt_succ (Nat.add_lt_add this this)

Proof state:
a b : PosNum
this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) (a.cmp b)

Tactic:
revert this

Result:
a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) (a.cmp b)

Proof state:
case eq
a b : PosNum
this : a = b
⊢ a.bit0 = b.bit0

Tactic:
rw [this]

Result:
no goals

Proof state:
a b : PosNum
⊢ Ordering.casesOn (a.bit1.cmp b.bit1) (↑a.bit1 < ↑b.bit1) (a.bit1 = b.bit1) (↑b.bit1 < ↑a.bit1)

Tactic:
dsimp [cmp]

Result:
a b : PosNum
⊢ Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) (a.cmp b)

Proof state:
case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑b + ↑b + 1

Tactic:
apply Nat.lt_succ_self

Result:
no goals

Proof state:
a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) (a.cmp b)

Tactic:
cases cmp a b <;> dsimp <;> intro this

Result:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a < ↑b + ↑b

case eq
a b : PosNum
this : a = b
⊢ a.bit0 = b.bit0

case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a

Proof state:
case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑a + ↑a + 1

Tactic:
rw [this]

Result:
case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑b + ↑b + 1

Proof state:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a + 1 < ↑b + ↑b

Tactic:
exact cmp_to_nat_lemma this

Result:
no goals
-- Mathlib/Data/Fin/Tuple/BubbleSortInduction.lean
theorem bubble_sort_induction' {n : ℕ} {α : Type*} [LinearOrder α] {f : Fin n → α}
    {P : (Fin n → α) → Prop} (hf : P f)
    (h : ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
      i < j → (f ∘ σ) j < (f ∘ σ) i → P (f ∘ σ) → P (f ∘ σ ∘ Equiv.swap i j)) :
    P (f ∘ sort f)

Proof state:
case intro.intro.intro
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ => toLex (f ∘ ⇑σ)
σ : Fin n ≃ Fin n
hσ : (fun σ => f ∘ ⇑σ) σ ≠ (fun σ => f ∘ ⇑σ) (sort f)
hfσ : P ((fun σ => f ∘ ⇑σ) σ)
i j : Fin n
hij₁ : i < j
hij₂ : (f ∘ ⇑σ) j < (f ∘ ⇑σ) i
⊢ ∃ c < σ, P ((fun σ => f ∘ ⇑σ) c)

Tactic:
exact ⟨σ * Equiv.swap i j, Pi.lex_desc hij₁.le hij₂, h σ i j hij₁ hij₂ hfσ⟩

Result:
no goals

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))
⊢ P (f ∘ ⇑(sort f))

Tactic:
letI := @Preorder.lift _ (Lex (Fin n → α)) _ fun σ : Equiv.Perm (Fin n) => toLex (f ∘ σ)

Result:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ => toLex (f ∘ ⇑σ)
⊢ P (f ∘ ⇑(sort f))

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ => toLex (f ∘ ⇑σ)
σ : Fin n ≃ Fin n
hσ : (fun σ => f ∘ ⇑σ) σ ≠ (fun σ => f ∘ ⇑σ) (sort f)
hfσ : P ((fun σ => f ∘ ⇑σ) σ)
⊢ ∃ c < σ, P ((fun σ => f ∘ ⇑σ) c)

Tactic:
obtain ⟨i, j, hij₁, hij₂⟩ := antitone_pair_of_not_sorted' hσ

Result:
case intro.intro.intro
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
P : (Fin n → α) → Prop
hf : P f
h :
  ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
    i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))
this : Preorder (Equiv.Perm (Fin n)) := Preorder.lift fun σ => toLex (f ∘ ⇑σ)
σ : Fin n ≃ Fin n
hσ : (fun σ => f ∘ ⇑σ) σ ≠ (fun σ => f ∘ ⇑σ) (sort f)
hfσ : P ((fun σ => f ∘ ⇑σ) σ)
i j : Fin n
hij₁ : i < j
hij₂ : (f ∘ ⇑σ) j < (f ∘ ⇑σ) i
⊢ ∃ c < σ, P ((fun σ => f ∘ ⇑σ) c)
-- Mathlib/Data/Complex/Basic.lean
theorem ofReal_pow (r : ℝ) (n : ℕ) : ((r ^ n : ℝ) : ℂ) = (r : ℂ) ^ n

Proof state:
r : ℝ
n : ℕ
⊢ ↑(r ^ n) = ↑r ^ n

Tactic:
induction n <;> simp [*, ofReal_mul, pow_succ]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem _root_.IsClosed.not_mem_iff_infDist_pos (h : IsClosed s) (hs : s.Nonempty) :
    x ∉ s ↔ 0 < infDist x s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : IsClosed s
hs : s.Nonempty
⊢ x ∉ s ↔ 0 < infDist x s

Tactic:
simp [h.mem_iff_infDist_zero hs, infDist_nonneg.gt_iff_ne]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_true : (countP fun (_ : α) => true) = (fun (_ : Vector α n) => n)

Proof state:
case h
α : Type u_1
n : Nat
l : Vector α n
⊢ Array.countP (fun x => true) l.toArray = n

Tactic:
simp only [Array.countP_true, l.2]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
⊢ (countP fun x => true) = fun x => n

Tactic:
funext l

Result:
case h
α : Type u_1
n : Nat
l : Vector α n
⊢ countP (fun x => true) l = n

Proof state:
case h
α : Type u_1
n : Nat
l : Vector α n
⊢ countP (fun x => true) l = n

Tactic:
rw [countP]

Result:
case h
α : Type u_1
n : Nat
l : Vector α n
⊢ Array.countP (fun x => true) l.toArray = n
-- Mathlib/NumberTheory/Divisors.lean
theorem insert_self_properDivisors (h : n ≠ 0) : insert n (properDivisors n) = divisors n

Proof state:
n : ℕ
h : n ≠ 0
⊢ insert n n.properDivisors = n.divisors

Tactic:
rw [divisors, properDivisors, Ico_succ_right_eq_insert_Ico (one_le_iff_ne_zero.2 h),
  Finset.filter_insert, if_pos (dvd_refl n)]

Result:
no goals
-- Mathlib/Algebra/Tropical/Basic.lean
theorem mul_eq_zero_iff {R : Type*} [LinearOrderedAddCommMonoid R] {a b : Tropical (WithTop R)} :
    a * b = 0 ↔ a = 0 ∨ b = 0

Proof state:
R : Type u_1
inst✝ : LinearOrderedAddCommMonoid R
a b : Tropical (WithTop R)
⊢ a * b = 0 ↔ a = 0 ∨ b = 0

Tactic:
simp [← untrop_inj_iff, WithTop.add_eq_top]

Result:
no goals
-- Mathlib/Data/Real/Sign.lean
theorem sign_mul_nonneg (r : ℝ) : 0 ≤ sign r * r

Proof state:
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r

Tactic:
exact hp.le

Result:
no goals

Proof state:
r : ℝ
hn : r < 0
⊢ -1 ≤ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case inr.inl

⊢ 0 ≤ sign 0 * 0

Tactic:
rw [mul_zero]

Result:
no goals

Proof state:
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r.sign * r

Tactic:
rw [sign_of_pos hp, one_mul]

Result:
case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r

Proof state:
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ -1 * r

Tactic:
exact mul_nonneg_of_nonpos_of_nonpos (by norm_num) hn.le

Result:
no goals

Proof state:
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ r.sign * r

Tactic:
rw [sign_of_neg hn]

Result:
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ -1 * r

Proof state:
r : ℝ
⊢ 0 ≤ r.sign * r

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)

Result:
case inl
r : ℝ
hn : r < 0
⊢ 0 ≤ r.sign * r

case inr.inl

⊢ 0 ≤ sign 0 * 0

case inr.inr
r : ℝ
hp : 0 < r
⊢ 0 ≤ r.sign * r
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_subset_ge_of_subset_image_lift {α : Type u} {β : Type v} (f : α → β) {s : Set α}
    {t : Set β} (h : t ⊆ f '' s) : lift.{u} #t ≤ lift.{v} #({ x ∈ s | f x ∈ t } : Set α)

Proof state:
case h.e'_4
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ lift.{v, u} #↑{x | f ↑x ∈ t} = lift.{v, u} #↑((fun x => f ↑x) ⁻¹' t)

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_4
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t} = lift.{v, u} #↑((fun x => f ↑x) ⁻¹' t)

Tactic:
rw [mk_sep]

Result:
case h.e'_4
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ lift.{v, u} #↑{x | f ↑x ∈ t} = lift.{v, u} #↑((fun x => f ↑x) ⁻¹' t)

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ lift.{u, v} #↑t ≤ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t}

Tactic:
rw [image_eq_range] at h

Result:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ lift.{u, v} #↑t ≤ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t}

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ lift.{u, v} #↑t ≤ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t}

Tactic:
convert mk_preimage_of_subset_range_lift _ _ h using 1

Result:
case h.e'_4
α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t} = lift.{v, u} #↑((fun x => f ↑x) ⁻¹' t)
-- Mathlib/Order/SuccPred/Basic.lean
theorem le_of_lt_succ {a b : α} : a < succ b → a ≤ b := fun h ↦ by
  by_contra! nh
  exact (h.trans_le (succ_le_of_lt nh)).false

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < succ b
nh : b < a
⊢ False

Tactic:
exact (h.trans_le (succ_le_of_lt nh)).false

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < succ b
⊢ a ≤ b

Tactic:
by_contra! nh

Result:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a < succ b
nh : b < a
⊢ False
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem normalizedFactors_prod_of_prime [Subsingleton αˣ] {m : Multiset α}
    (h : ∀ p ∈ m, Prime p) : normalizedFactors m.prod = m

Proof state:
case inl
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Subsingleton α
⊢ normalizedFactors m.prod = m

Tactic:
obtain rfl : m = 0 := by
  refine Multiset.eq_zero_of_forall_not_mem fun x hx ↦ ?_
  simpa [Subsingleton.elim x 0] using h x hx

Result:
case inl
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
h✝ : Subsingleton α
h : ∀ p ∈ 0, Prime p
⊢ normalizedFactors (Multiset.prod 0) = 0

Proof state:
case inr
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Nontrivial α
⊢ normalizedFactors m.prod = m

Tactic:
simpa only [← Multiset.rel_eq, ← associated_eq_eq] using
  prime_factors_unique prime_of_normalized_factor h
    (prod_normalizedFactors (m.prod_ne_zero_of_prime h))

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
h✝ : Subsingleton α
h : ∀ p ∈ 0, Prime p
⊢ normalizedFactors (Multiset.prod 0) = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Subsingleton α
x : α
hx : x ∈ m
⊢ False

Tactic:
simpa [Subsingleton.elim x 0] using h x hx

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
⊢ normalizedFactors m.prod = m

Tactic:
cases subsingleton_or_nontrivial α

Result:
case inl
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Subsingleton α
⊢ normalizedFactors m.prod = m

case inr
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Nontrivial α
⊢ normalizedFactors m.prod = m

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Subsingleton α
⊢ m = 0

Tactic:
refine Multiset.eq_zero_of_forall_not_mem fun x hx ↦ ?_

Result:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Subsingleton α
x : α
hx : x ∈ m
⊢ False
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem Filter.HasBasis.isUniformEmbedding_iff' {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'}
    (h : (𝓤 α).HasBasis p s) (h' : (𝓤 β).HasBasis p' s') {f : α → β} :
    IsUniformEmbedding f ↔ Injective f ∧
      (∀ i, p' i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        (∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j)

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
⊢ IsUniformEmbedding f ↔
    Injective f ∧
      (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j

Tactic:
rw [isUniformEmbedding_iff, and_comm, h.isUniformInducing_iff h']

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Finset.lean
lemma tendsto_toRight_atTop :
    Tendsto (Finset.toRight (α := α) (β := β)) atTop atTop

Proof state:
α : Type u_3
β : Type u_4
s : Set (Finset β)
hs : ∃ a, ∀ b ≥ a, b ∈ s
⊢ ∃ a, ∀ b ≥ a, b.toRight ∈ s

Tactic:
obtain ⟨t, H⟩ := hs

Result:
case intro
α : Type u_3
β : Type u_4
s : Set (Finset β)
t : Finset β
H : ∀ b ≥ t, b ∈ s
⊢ ∃ a, ∀ b ≥ a, b.toRight ∈ s

Proof state:
α : Type u_3
β : Type u_4
s : Set (Finset β)
t : Finset β
H : ∀ b ≥ t, b ∈ s
b : Finset (α ⊕ β)
hb : b ≥ ∅.disjSum t
⊢ b.toRight ≥ t

Tactic:
simpa [← Finset.coe_subset, Set.subset_def] using hb

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
⊢ Tendsto Finset.toRight atTop atTop

Tactic:
intro s hs

Result:
α : Type u_3
β : Type u_4
s : Set (Finset β)
hs : s ∈ atTop
⊢ s ∈ map Finset.toRight atTop

Proof state:
α : Type u_3
β : Type u_4
s : Set (Finset β)
hs : s ∈ atTop
⊢ s ∈ map Finset.toRight atTop

Tactic:
simp only [mem_atTop_sets, Finset.le_eq_subset, Filter.mem_map, Set.mem_preimage] at hs ⊢

Result:
α : Type u_3
β : Type u_4
s : Set (Finset β)
hs : ∃ a, ∀ b ≥ a, b ∈ s
⊢ ∃ a, ∀ b ≥ a, b.toRight ∈ s

Proof state:
case intro
α : Type u_3
β : Type u_4
s : Set (Finset β)
t : Finset β
H : ∀ b ≥ t, b ∈ s
⊢ ∃ a, ∀ b ≥ a, b.toRight ∈ s

Tactic:
exact ⟨.disjSum ∅ t, fun b hb ↦ H _ (by simpa [← Finset.coe_subset, Set.subset_def] using hb)⟩

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem prime_generator_of_isPrime (S : Ideal R) [S.IsPrincipal] [is_prime : S.IsPrime]
    (ne_bot : S ≠ ⊥) : Prime (generator S) :=
  ⟨fun h => ne_bot ((eq_bot_iff_generator_eq_zero S).2 h), fun h =>
    is_prime.ne_top (S.eq_top_of_isUnit_mem (generator_mem S) h), fun _ _ => by
    simpa only [← mem_iff_generator_dvd S] using is_prime.2⟩

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Ideal R
inst✝ : IsPrincipal S
is_prime : S.IsPrime
ne_bot : S ≠ ⊥
x✝¹ x✝ : R
⊢ generator S ∣ x✝¹ * x✝ → generator S ∣ x✝¹ ∨ generator S ∣ x✝

Tactic:
simpa only [← mem_iff_generator_dvd S] using is_prime.2

Result:
no goals