harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem max_eq_right {a b : Int} (h : a ≤ b) : max a b = b

Proof state:
a b : Int
h : a ≤ b
⊢ max a b = b

Tactic:
simp [Int.max_def, h, Int.not_lt.2 h]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive (attr := simp)]
lemma one_prod_one [One β] : (1 ×ˢ 1 : Set (α × β)) = 1

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
⊢ 1 ×ˢ 1 = 1

Tactic:
ext

Result:
case h
α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
x✝ : α × β
⊢ x✝ ∈ 1 ×ˢ 1 ↔ x✝ ∈ 1

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
x✝ : α × β
⊢ x✝ ∈ 1 ×ˢ 1 ↔ x✝ ∈ 1

Tactic:
simp [Prod.ext_iff]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem rel_zero_right {a : Multiset α} : Rel r a 0 ↔ a = 0

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ Rel r a 0 ↔ a = 0

Tactic:
rw [rel_iff]

Result:
α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ (a = 0 ∧ 0 = 0 ∨ ∃ a_1 b as bs, r a_1 b ∧ Rel r as bs ∧ a = a_1 ::ₘ as ∧ 0 = b ::ₘ bs) ↔ a = 0

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ (a = 0 ∧ 0 = 0 ∨ ∃ a_1 b as bs, r a_1 b ∧ Rel r as bs ∧ a = a_1 ::ₘ as ∧ 0 = b ::ₘ bs) ↔ a = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma add_pos_iff_pos_or_pos : 0 < m + n ↔ 0 < m ∨ 0 < n

Proof state:
m n : ℕ
⊢ 0 < m + n ↔ 0 < m ∨ 0 < n

Tactic:
omega

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem succ_lt_iSup_of_ne_iSup {ι} {f : ι → Ordinal.{u}} [Small.{u} ι]
    (hf : ∀ i, f i ≠ iSup f) {a} (hao : a < iSup f) : succ a < iSup f

Proof state:
ι : Type u_4
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_4} ι
hf : ∀ (i : ι), f i ≠ iSup f
a : Ordinal.{u}
hao : a < iSup f
hoa : iSup f ≤ succ a
⊢ False

Tactic:
exact hao.not_le (Ordinal.iSup_le fun i => le_of_lt_succ <|
  (lt_of_le_of_ne (Ordinal.le_iSup _ _) (hf i)).trans_le hoa)

Result:
no goals

Proof state:
ι : Type u_4
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_4} ι
hf : ∀ (i : ι), f i ≠ iSup f
a : Ordinal.{u}
hao : a < iSup f
⊢ succ a < iSup f

Tactic:
by_contra! hoa

Result:
ι : Type u_4
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_4} ι
hf : ∀ (i : ι), f i ≠ iSup f
a : Ordinal.{u}
hao : a < iSup f
hoa : iSup f ≤ succ a
⊢ False
-- Mathlib/Order/Minimal.lean
theorem inter_preimage_setOf_minimal_eq_of_subset (hts : t ⊆ f '' s) :
    x ∈ s ∩ f ⁻¹' {y | Minimal (· ∈ t) y} ↔ Minimal (· ∈ s ∩ f ⁻¹' t) x

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ ⇑f '' s
⊢ x ∈ s ∩ ⇑f ⁻¹' {y | Minimal (fun x => x ∈ t) y} ↔ Minimal (fun x => x ∈ s ∩ ⇑f ⁻¹' t) x

Tactic:
simp_rw [mem_inter_iff, preimage_setOf_eq, mem_setOf_eq, mem_preimage,
  f.minimal_apply_mem_iff (hts.trans (image_subset_range _ _)),
  minimal_and_iff_left_of_imp (fun _ hx ↦ f.injective.mem_set_image.1 <| hts hx)]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma not_nil_of_isCycle_cons {p : G.Walk u v} {h : G.Adj v u} (hc : (Walk.cons h p).IsCycle) :
    ¬ p.Nil

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
hc : (cons h p).IsCycle
this : 3 ≤ p.length + 1
⊢ 0 < p.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
hc : (cons h p).IsCycle
this : 3 ≤ p.length + 1
⊢ ¬p.Nil

Tactic:
rw [Walk.not_nil_iff_lt_length]

Result:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
hc : (cons h p).IsCycle
this : 3 ≤ p.length + 1
⊢ 0 < p.length

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
hc : (cons h p).IsCycle
⊢ ¬p.Nil

Tactic:
have := Walk.length_cons _ _ ▸ Walk.IsCycle.three_le_length hc

Result:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
hc : (cons h p).IsCycle
this : 3 ≤ p.length + 1
⊢ ¬p.Nil
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_sub : cosh (x - y) = cosh x * cosh y - sinh x * sinh y

Proof state:
x y : ℝ
⊢ cosh (x - y) = cosh x * cosh y - sinh x * sinh y

Tactic:
simp [sub_eq_add_neg, cosh_add, sinh_neg, cosh_neg]

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
protected lemma TendstoUniformly.im {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ}
    (hf : TendstoUniformly f g p) :
    TendstoUniformly (fun n x => (f n x).im) (fun y => (g y).im) p

Proof state:
α : Type u_1
ι : Type u_2
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformly f g p
⊢ TendstoUniformly (fun n x => (f n x).im) (fun y => (g y).im) p

Tactic:
apply UniformContinuous.comp_tendstoUniformly uniformlyContinuous_im hf

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
lemma inf'_univ_eq_ciInf (f : ι → α) : univ.inf' univ_nonempty f = ⨅ i, f i

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
f : ι → α
⊢ univ.inf' ⋯ f = ⨅ i, f i

Tactic:
simp [inf'_eq_csInf_image, iInf]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Metric.emetric_closedBall {x : α} {ε : ℝ} (h : 0 ≤ ε) :
    EMetric.closedBall x (ENNReal.ofReal ε) = closedBall x ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
⊢ EMetric.closedBall x (ENNReal.ofReal ε) = closedBall x ε

Tactic:
ext y

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
y : α
⊢ y ∈ EMetric.closedBall x (ENNReal.ofReal ε) ↔ y ∈ closedBall x ε

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
y : α
⊢ y ∈ EMetric.closedBall x (ENNReal.ofReal ε) ↔ y ∈ closedBall x ε

Tactic:
simp [edist_le_ofReal h]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.linearIndependentSingleton {I} [LinearOrder I] :
    LinearIndependent ℤ (eval ({fun _ ↦ false} : Set (I → Bool)))

Proof state:
I : Type u_1
inst✝ : LinearOrder I
⊢ LinearIndependent ℤ (eval {fun x => false})

Tactic:
refine linearIndependent_unique (eval ({fun _ ↦ false} : Set (I → Bool))) ?_

Result:
I : Type u_1
inst✝ : LinearOrder I
⊢ eval {fun x => false} default ≠ 0

Proof state:
I : Type u_1
inst✝ : LinearOrder I
⊢ eval {fun x => false} default ≠ 0

Tactic:
simp [eval, Products.eval, Products.nil, default]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean
lemma exists_inter_eq_singleton (hrep : Represents s C) (h : c ∈ C) : ∃ x, s ∩ c.supp = {x}

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃ x, s ∩ c.supp = {x}

Tactic:
obtain ⟨a, ha⟩ := existsUnique_rep hrep h

Result:
case intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
a : V
ha : (fun x => x ∈ s ∩ c.supp) a ∧ ∀ (y : V), (fun x => x ∈ s ∩ c.supp) y → y = a
⊢ ∃ x, s ∩ c.supp = {x}

Proof state:
case intro
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
a : V
ha : (fun x => x ∈ s ∩ c.supp) a ∧ ∀ (y : V), (fun x => x ∈ s ∩ c.supp) y → y = a
⊢ ∃ x, s ∩ c.supp = {x}

Tactic:
aesop

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean
@[ext]
lemma ext (β : BasedNatTrans F G) (h : α.toNatTrans = β.toNatTrans) : α = β

Proof state:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α β : BasedNatTrans F G
h : α.toNatTrans = β.toNatTrans
⊢ α = β

Tactic:
cases α

Result:
case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
β : BasedNatTrans F G
toNatTrans✝ : NatTrans F.toFunctor G.toFunctor
isHomLift'✝ : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (toNatTrans✝.app a)
h : { toNatTrans := toNatTrans✝, isHomLift' := isHomLift'✝ }.toNatTrans = β.toNatTrans
⊢ { toNatTrans := toNatTrans✝, isHomLift' := isHomLift'✝ } = β

Proof state:
case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
β : BasedNatTrans F G
toNatTrans✝ : NatTrans F.toFunctor G.toFunctor
isHomLift'✝ : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (toNatTrans✝.app a)
h : { toNatTrans := toNatTrans✝, isHomLift' := isHomLift'✝ }.toNatTrans = β.toNatTrans
⊢ { toNatTrans := toNatTrans✝, isHomLift' := isHomLift'✝ } = β

Tactic:
subst h

Result:
case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
β : BasedNatTrans F G
isHomLift'✝ : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (β.app a)
⊢ { toNatTrans := β.toNatTrans, isHomLift' := isHomLift'✝ } = β

Proof state:
case mk
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
β : BasedNatTrans F G
isHomLift'✝ : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (β.app a)
⊢ { toNatTrans := β.toNatTrans, isHomLift' := isHomLift'✝ } = β

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
@[simp]
lemma cfc_zero : cfc (0 : R → R) a = 0

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
ha : p a
⊢ cfc 0 a = 0

Tactic:
exact cfc_apply (0 : R → R) a ▸ map_zero (cfcHom ha)

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
⊢ cfc 0 a = 0

Tactic:
by_cases ha : p a

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
ha : p a
⊢ cfc 0 a = 0

case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
ha : ¬p a
⊢ cfc 0 a = 0

Proof state:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
ha : ¬p a
⊢ cfc 0 a = 0

Tactic:
rw [cfc_apply_of_not_predicate a ha]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem leadingCoeff_mul_prod_normalizedFactors [DecidableEq R] (a : R[X]) :
    C a.leadingCoeff * (normalizedFactors a).prod = a

Proof state:
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
⊢ C a.leadingCoeff * (normalizedFactors a).prod = a

Tactic:
by_cases ha : a = 0

Result:
case pos
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : a = 0
⊢ C a.leadingCoeff * (normalizedFactors a).prod = a

case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ C a.leadingCoeff * (normalizedFactors a).prod = a

Proof state:
case pos
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : a = 0
⊢ C a.leadingCoeff * (normalizedFactors a).prod = a

Tactic:
simp [ha]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : Field R
inst✝ : DecidableEq R
a : R[X]
ha : ¬a = 0
⊢ C a.leadingCoeff * (normalizedFactors a).prod = a

Tactic:
rw [prod_normalizedFactors_eq, normalize_apply, coe_normUnit, CommGroupWithZero.coe_normUnit,
  mul_comm, mul_assoc, ← map_mul, inv_mul_cancel₀] <;>
simp_all

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsTopologicalGroup.of_nhds_one' {G : Type u} [Group G] [TopologicalSpace G]
    (hmul : Tendsto (uncurry ((· * ·) : G → G → G)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
    (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1))
    (hleft : ∀ x₀ : G, 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1))
    (hright : ∀ x₀ : G, 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)) : IsTopologicalGroup G :=
  { toContinuousMul := ContinuousMul.of_nhds_one hmul hleft hright
    toContinuousInv :=
      ContinuousInv.of_nhds_one hinv hleft fun x₀ =>
        le_of_eq
          (by
            rw [show (fun x => x₀ * x * x₀⁻¹) = (fun x => x * x₀⁻¹) ∘ fun x => x₀ * x from rfl, ←
              map_map, ← hleft, hright, map_map]
            simp [(· ∘ ·)]) }

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ : G
⊢ map (fun x => x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1

Tactic:
rw [show (fun x => x₀ * x * x₀⁻¹) = (fun x => x * x₀⁻¹) ∘ fun x => x₀ * x from rfl, ←
  map_map, ← hleft, hright, map_map]

Result:
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ : G
⊢ map ((fun x => x * x₀⁻¹) ∘ fun x => x * x₀) (𝓝 1) = 𝓝 1
-- Mathlib/Order/Sublattice.lean
@[simp] lemma mem_iInf {f : ι → Sublattice α} : a ∈ ⨅ i, f i ↔ ∀ i, a ∈ f i

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : Lattice α
a : α
f : ι → Sublattice α
⊢ a ∈ ⨅ i, f i ↔ ∀ (i : ι), a ∈ f i

Tactic:
rw [← SetLike.mem_coe]

Result:
ι : Sort u_1
α : Type u_2
inst✝ : Lattice α
a : α
f : ι → Sublattice α
⊢ a ∈ ↑(⨅ i, f i) ↔ ∀ (i : ι), a ∈ f i

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : Lattice α
a : α
f : ι → Sublattice α
⊢ a ∈ ↑(⨅ i, f i) ↔ ∀ (i : ι), a ∈ f i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma IsNonZero.neg (h : α.IsNonZero) : (-α).IsNonZero := fun e ↦ h (by simpa using e.neg)

Proof state:
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsNonZero
e : (-α).IsZero
⊢ α.IsZero

Tactic:
simpa using e.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Log2.lean
theorem log2_le_self (n : Nat) : Nat.log2 n ≤ n

Proof state:
n : Nat
a✝ : ∀ (y : Nat), (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y n → y.log2 ≤ y
h✝ : n ≥ 2
⊢ n / 2 < n

Tactic:
exact Nat.log2_terminates _ ‹_›

Result:
no goals

Proof state:
n : Nat
⊢ (if n ≥ 2 then (n / 2).log2 + 1 else 0) ≤ n

Tactic:
split

Result:
case isTrue
n : Nat
h✝ : n ≥ 2
⊢ (n / 2).log2 + 1 ≤ n

case isFalse
n : Nat
h✝ : ¬n ≥ 2
⊢ 0 ≤ n

Proof state:
case isFalse
n : Nat
h✝ : ¬n ≥ 2
⊢ 0 ≤ n

Tactic:
apply Nat.zero_le

Result:
no goals

Proof state:
n : Nat
h : n ≥ 2
this : (n / 2).log2 ≤ n / 2
⊢ (n / 2).log2 + 1 ≤ n

Tactic:
exact Nat.lt_of_le_of_lt this (Nat.div_lt_self (Nat.le_of_lt h) (by decide))

Result:
no goals

Proof state:
case isTrue
n : Nat
h✝ : n ≥ 2
⊢ (n / 2).log2 + 1 ≤ n

Tactic:
next h =>
have := log2_le_self (n / 2)
exact Nat.lt_of_le_of_lt this (Nat.div_lt_self (Nat.le_of_lt h) (by decide))

Result:
no goals

Proof state:
n : Nat
h : n ≥ 2
⊢ (n / 2).log2 + 1 ≤ n

Tactic:
have := log2_le_self (n / 2)

Result:
n : Nat
h : n ≥ 2
this : (n / 2).log2 ≤ n / 2
⊢ (n / 2).log2 + 1 ≤ n

Proof state:
n : Nat
h : n ≥ 2
this : (n / 2).log2 ≤ n / 2
⊢ 1 < 2

Tactic:
decide

Result:
no goals

Proof state:
n : Nat
⊢ n.log2 ≤ n

Tactic:
unfold Nat.log2

Result:
n : Nat
⊢ (if n ≥ 2 then (n / 2).log2 + 1 else 0) ≤ n
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_add_le_iff_right {n : ℕ} (p q : R[X]) (pn : p.natDegree ≤ n) :
    (p + q).natDegree ≤ n ↔ q.natDegree ≤ n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
pn : p.natDegree ≤ n
⊢ (q + p).natDegree ≤ n ↔ q.natDegree ≤ n

Tactic:
exact natDegree_add_le_iff_left _ _ pn

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
pn : p.natDegree ≤ n
⊢ (p + q).natDegree ≤ n ↔ q.natDegree ≤ n

Tactic:
rw [add_comm]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
pn : p.natDegree ≤ n
⊢ (q + p).natDegree ≤ n ↔ q.natDegree ≤ n
-- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
theorem integrable_comp_mul_right_iff (g : ℝ → F) {R : ℝ} (hR : R ≠ 0) :
    (Integrable fun x => g (x * R)) ↔ Integrable g

Proof state:
F : Type u_1
inst✝ : NormedAddCommGroup F
g : ℝ → F
R : ℝ
hR : R ≠ 0
⊢ Integrable (fun x => g (x * R)) volume ↔ Integrable g volume

Tactic:
simpa only [mul_comm] using integrable_comp_mul_left_iff g hR

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasStrictDerivAt.scomp_of_eq
    (hg : HasStrictDerivAt g₁ g₁' y) (hh : HasStrictDerivAt h h' x) (hy : y = h x) :
    HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasStrictDerivAt g₁ g₁' (h x)
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
exact hg.scomp x hh

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasStrictDerivAt g₁ g₁' y
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
rw [hy] at hg

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasStrictDerivAt g₁ g₁' (h x)
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem LinearIndependent.span_eq_top_of_card_eq_finrank' {ι : Type*}
    [Fintype ι] [FiniteDimensional K V] {b : ι → V} (lin_ind : LinearIndependent K b)
    (card_eq : Fintype.card ι = finrank K V) : span K (Set.range b) = ⊤

Proof state:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : finrank K ↥(span K (Set.range b)) = finrank K V
ne_top : ¬span K (Set.range b) = ⊤
⊢ False

Tactic:
exact ne_of_lt (Submodule.finrank_lt <| lt_top_iff_ne_top.2 ne_top) card_eq

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
⊢ span K (Set.range b) = ⊤

Tactic:
by_contra ne_top

Result:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
ne_top : ¬span K (Set.range b) = ⊤
⊢ False

Proof state:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
ne_top : ¬span K (Set.range b) = ⊤
⊢ False

Tactic:
rw [← finrank_span_eq_card lin_ind] at card_eq

Result:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : finrank K ↥(span K (Set.range b)) = finrank K V
ne_top : ¬span K (Set.range b) = ⊤
⊢ False
-- Mathlib/Data/PFunctor/Univariate/Basic.lean
theorem W.dest_mk (p : P (W P)) : W.dest (W.mk p) = p

Proof state:
case mk
P : PFunctor.{u}
fst✝ : P.A
snd✝ : P.B fst✝ → P.W
⊢ (mk ⟨fst✝, snd✝⟩).dest = ⟨fst✝, snd✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
P : PFunctor.{u}
p : ↑P P.W
⊢ (mk p).dest = p

Tactic:
cases p

Result:
case mk
P : PFunctor.{u}
fst✝ : P.A
snd✝ : P.B fst✝ → P.W
⊢ (mk ⟨fst✝, snd✝⟩).dest = ⟨fst✝, snd✝⟩
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem card_multiples (n p : ℕ) : #{e ∈ range n | p ∣ e + 1} = n / p

Proof state:
case zero
p : ℕ
⊢ #(Finset.filter (fun e => p ∣ e + 1) (Finset.range 0)) = 0 / p

Tactic:
simp

Result:
no goals

Proof state:
case succ
p n : ℕ
hn : #(Finset.filter (fun e => p ∣ e + 1) (Finset.range n)) = n / p
⊢ #(Finset.filter (fun e => p ∣ e + 1) (Finset.range (n + 1))) = (n + 1) / p

Tactic:
simp [Nat.succ_div, add_ite, add_zero, Finset.range_succ, filter_insert, apply_ite card,
  card_insert_of_not_mem, hn]

Result:
no goals

Proof state:
n p : ℕ
⊢ #(Finset.filter (fun e => p ∣ e + 1) (Finset.range n)) = n / p

Tactic:
induction' n with n hn

Result:
case zero
p : ℕ
⊢ #(Finset.filter (fun e => p ∣ e + 1) (Finset.range 0)) = 0 / p

case succ
p n : ℕ
hn : #(Finset.filter (fun e => p ∣ e + 1) (Finset.range n)) = n / p
⊢ #(Finset.filter (fun e => p ∣ e + 1) (Finset.range (n + 1))) = (n + 1) / p
-- Mathlib/Analysis/Normed/Group/HomCompletion.lean
theorem NormedAddGroupHom.ker_le_ker_completion (f : NormedAddGroupHom G H) :
    (toCompl.comp <| incl f.ker).range ≤ f.completion.ker

Proof state:
case intro.mk
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
g : G
h₀ : f g = 0
⊢ (toCompl.comp (incl f.ker)).toAddMonoidHom ⟨g, h₀⟩ ∈ f.completion.ker

Tactic:
simp [h₀, mem_ker, Completion.coe_zero]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
⊢ (toCompl.comp (incl f.ker)).range ≤ f.completion.ker

Tactic:
rintro _ ⟨⟨g, h₀ : f g = 0⟩, rfl⟩

Result:
case intro.mk
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
g : G
h₀ : f g = 0
⊢ (toCompl.comp (incl f.ker)).toAddMonoidHom ⟨g, h₀⟩ ∈ f.completion.ker
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
lemma range_fst_comp :
    Set.range (pullback.fst f g ≫ f).base = Set.range f.base ∩ Set.range g.base

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g ≫ f).base) =
    Set.range ⇑(ConcreteCategory.hom f.base) ∩ Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
simp [Set.range_comp, range_fst, Set.image_preimage_eq_range_inter]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
/-- A closed ball in a product space is a product of closed balls. See also `closedBall_pi`
for a version assuming `0 ≤ r` instead of `Nonempty β`. -/
lemma closedBall_pi' [Nonempty β] (x : ∀ b, π b) (r : ℝ) :
    closedBall x r = Set.pi univ fun b => closedBall (x b) r :=
  (le_or_lt 0 r).elim (closedBall_pi x) fun hr => by simp [closedBall_eq_empty.2 hr]

Proof state:
β : Type u_2
π : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
x : (b : β) → π b
r : ℝ
hr : r < 0
⊢ closedBall x r = Set.univ.pi fun b => closedBall (x b) r

Tactic:
simp [closedBall_eq_empty.2 hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_mul_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : a / b * b = a

Proof state:
a b : Int
H : a % b = 0
⊢ a / b * b = a

Tactic:
rw [Int.mul_comm, mul_ediv_cancel_of_emod_eq_zero H]

Result:
no goals