awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
inst_1 : HasReverse.{v, u_2} V
a b c : V
p : Path.{v, u_2} a b
q : Path.{v, u_2} b c
nil : (p.comp Path.nil).reverse = comp (reverse Path.nil) p.reverse
⊢ (p.comp q).reverse = q.reverse.comp p.reverse
have cons : ∀ {b_1 c : V} (a_1 : Path.{v, u_2} b b_1) (a_2 : b_1 ⟶ c) (h : (p.comp a_1).reverse = a_1.reverse.comp p.reverse),
  (p.comp (a_1.cons a_2)).reverse = (a_1.cons a_2).reverse.comp p.reverse
Tactic: induction q with
  | nil => simp
  | cons _ _ h => simp [h]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h_1 : HasInvolutiveReverse.{v, u_2} V
a b b_1 c : V
a_1 : Path.{v, u_2} a b_1
a_2 : b_1 ⟶ c
h : a_1.reverse.reverse = a_1
⊢ (a_1.cons a_2).reverse.reverse = a_1.cons a_2
have cons : a_1.comp a_2.toPath = a_1.cons a_2
Tactic: rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h : HasInvolutiveReverse.{v, u_2} V
a b : V
p : Path.{v, u_2} a b
⊢ p.reverse.reverse = p
have nil : Eq (α := Path.{v, u_2} a a) (reverse (reverse nil)) nil
Tactic: induction p with
  | nil => simp
  | cons _ _ h =>
    rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]
    rfl
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h : HasInvolutiveReverse.{v, u_2} V
a b : V
p : Path.{v, u_2} a b
nil : Eq (α := Path.{v, u_2} a a) (reverse (reverse Path.nil)) Path.nil
⊢ p.reverse.reverse = p
have cons : ∀ {b c : V} (a_1 : Path.{v, u_2} a b) (a_2 : b ⟶ c) (h_1 : a_1.reverse.reverse = a_1),
  (a_1.cons a_2).reverse.reverse = a_1.cons a_2
Tactic: induction p with
  | nil => simp
  | cons _ _ h =>
    rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]
    rfl
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
V' : Type u_4
inst_1 : Quiver.{v', u_4} V'
inst_2 : HasReverse.{v', u_4} V'
φ : Prefunctor.{v, v', u_2, u_4} V V'
⊢ of ⋙q lift φ = φ
have h_obj : ∀ (X : V), (of ⋙q lift φ).obj X = φ.obj X
Tactic: fapply Prefunctor.ext
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
V' : Type u_4
inst_1 : Quiver.{v', u_4} V'
inst_2 : HasReverse.{v', u_4} V'
φ : Prefunctor.{v, v', u_2, u_4} V V'
h_obj : ∀ (X : V), (of ⋙q lift φ).obj X = φ.obj X
⊢ of ⋙q lift φ = φ
have h_map : ∀ (X Y : V) (f : X ⟶ Y),
  (of ⋙q lift φ).map f =
    Eq.recOn (motive := fun (x : V') (x_1 : φ.obj Y = x) ↦ (of ⋙q lift φ).obj X ⟶ x) sorry
      (Eq.recOn (motive := fun (x : V') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) sorry (φ.map f))
Tactic: fapply Prefunctor.ext
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
V' : Type u_4
inst_1 : Quiver.{v', u_4} V'
h : HasInvolutiveReverse.{v', u_4} V'
φ : Prefunctor.{v, v', u_2, u_4} V V'
X Y : Symmetrify V
f : X ⟶ Y
⊢ (lift φ).map (reverse f) = reverse ((lift φ).map f)
have dsimp : Eq.{v' + 1} (α := φ.obj Y ⟶ φ.obj X)
  (match (motive := (Y ⟶ X) → (φ.obj Y ⟶ φ.obj X)) Sum.swap f with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g) :
    φ.obj Y ⟶ φ.obj X)
  (reverse
      (match (motive := (X ⟶ Y) → (φ.obj X ⟶ φ.obj Y)) f with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g)) :
    φ.obj Y ⟶ φ.obj X)
Tactic: dsimp [Symmetrify.lift]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
V' : Type u_4
inst_1 : Quiver.{v', u_4} V'
h : HasInvolutiveReverse.{v', u_4} V'
φ : Prefunctor.{v, v', u_2, u_4} V V'
X Y : Symmetrify V
f : X ⟶ Y
⊢ Eq.{v' + 1} (α := φ.obj Y ⟶ φ.obj X)
    (match (motive := (Y ⟶ X) → (φ.obj Y ⟶ φ.obj X)) Sum.swap f with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g) :
      φ.obj Y ⟶ φ.obj X)
    (reverse
        (match (motive := (X ⟶ Y) → (φ.obj X ⟶ φ.obj Y)) f with
        | Sum.inl g => φ.map g
        | Sum.inr g => reverse (φ.map g)) :
      φ.obj Y ⟶ φ.obj X)
have inl : ∀ (val : X ⟶ Y),
  Eq.{v' + 1} (α := φ.obj Y ⟶ φ.obj X)
    (match (motive := (Y ⟶ X) → (φ.obj Y ⟶ φ.obj X)) Sum.swap (Sum.inl val) with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g) :
      φ.obj Y ⟶ φ.obj X)
    (reverse
        (match (motive := (X ⟶ Y) → (φ.obj X ⟶ φ.obj Y)) Sum.inl val with
        | Sum.inl g => φ.map g
        | Sum.inr g => reverse (φ.map g)) :
      φ.obj Y ⟶ φ.obj X)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
V' : Type u_4
inst_1 : Quiver.{v', u_4} V'
h : HasInvolutiveReverse.{v', u_4} V'
φ : Prefunctor.{v, v', u_2, u_4} V V'
X Y : Symmetrify V
f : X ⟶ Y
inl :
  ∀ (val : X ⟶ Y),
    Eq.{v' + 1} (α := φ.obj Y ⟶ φ.obj X)
      (match (motive := (Y ⟶ X) → (φ.obj Y ⟶ φ.obj X)) Sum.swap (Sum.inl val) with
        | Sum.inl g => φ.map g
        | Sum.inr g => reverse (φ.map g) :
        φ.obj Y ⟶ φ.obj X)
      (reverse
          (match (motive := (X ⟶ Y) → (φ.obj X ⟶ φ.obj Y)) Sum.inl val with
          | Sum.inl g => φ.map g
          | Sum.inr g => reverse (φ.map g)) :
        φ.obj Y ⟶ φ.obj X)
⊢ Eq.{v' + 1} (α := φ.obj Y ⟶ φ.obj X)
    (match (motive := (Y ⟶ X) → (φ.obj Y ⟶ φ.obj X)) Sum.swap f with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g) :
      φ.obj Y ⟶ φ.obj X)
    (reverse
        (match (motive := (X ⟶ Y) → (φ.obj X ⟶ φ.obj Y)) f with
        | Sum.inl g => φ.map g
        | Sum.inr g => reverse (φ.map g)) :
      φ.obj Y ⟶ φ.obj X)
have inr : ∀ (val : Y ⟶ X),
  Eq.{v' + 1} (α := φ.obj Y ⟶ φ.obj X)
    (match (motive := (Y ⟶ X) → (φ.obj Y ⟶ φ.obj X)) Sum.swap (Sum.inr val) with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g) :
      φ.obj Y ⟶ φ.obj X)
    (reverse
        (match (motive := (X ⟶ Y) → (φ.obj X ⟶ φ.obj Y)) Sum.inr val with
        | Sum.inl g => φ.map g
        | Sum.inr g => reverse (φ.map g)) :
      φ.obj Y ⟶ φ.obj X)
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
V' : Type u_4
inst_1 : Quiver.{v', u_4} V'
h : HasInvolutiveReverse.{v', u_4} V'
φ : Prefunctor.{v, v', u_2, u_4} V V'
X Y : Symmetrify V
val : Y ⟶ X
⊢ Eq.{v' + 1} (α := φ.obj Y ⟶ φ.obj X)
    (match (motive := (Y ⟶ X) → (φ.obj Y ⟶ φ.obj X)) Sum.swap (Sum.inr val) with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g) :
      φ.obj Y ⟶ φ.obj X)
    (reverse
        (match (motive := (X ⟶ Y) → (φ.obj X ⟶ φ.obj Y)) Sum.inr val with
        | Sum.inl g => φ.map g
        | Sum.inr g => reverse (φ.map g)) :
      φ.obj Y ⟶ φ.obj X)
have inr : (match (motive := (Y ⟶ X) → (φ.obj Y ⟶ φ.obj X)) Sum.swap (Sum.inr val) with
  | Sum.inl g => φ.map g
  | Sum.inr g => reverse (φ.map g)) =
  φ.map val
Tactic: simp only [reverse_reverse]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
V' : Type u_4
inst_1 : Quiver.{v', u_4} V'
inst_2 : HasReverse.{v', u_4} V'
φ : Prefunctor.{v, v', u_2, u_4} V V'
Φ : Prefunctor.{v, v', u_2, u_4} (Symmetrify V) V'
hΦ : of ⋙q Φ = φ
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ Φ = lift φ
have subst_vars : Φ = lift (of ⋙q Φ)
Tactic: subst_vars
Cleared hypotheses: φ, hΦ
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
V' : Type u_4
inst_1 : Quiver.{v', u_4} V'
inst_2 : HasReverse.{v', u_4} V'
Φ : Prefunctor.{v, v', u_2, u_4} (Symmetrify V) V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ Φ = lift (of ⋙q Φ)
have h_obj : ∀ (X : Symmetrify V), Φ.obj X = (lift (of ⋙q Φ)).obj X
Tactic: fapply Prefunctor.ext
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
V' : Type u_4
inst_1 : Quiver.{v', u_4} V'
inst_2 : HasReverse.{v', u_4} V'
Φ : Prefunctor.{v, v', u_2, u_4} (Symmetrify V) V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
h_obj : ∀ (X : Symmetrify V), Φ.obj X = (lift (of ⋙q Φ)).obj X
⊢ Φ = lift (of ⋙q Φ)
have h_map : ∀ (X Y : Symmetrify V) (f : X ⟶ Y),
  Φ.map f =
    Eq.recOn (motive := fun (x : V') (x_1 : (lift (of ⋙q Φ)).obj Y = x) ↦ Φ.obj X ⟶ x) sorry
      (Eq.recOn (motive := fun (x : V') (x_1 : (lift (of ⋙q Φ)).obj X = x) ↦ x ⟶ (lift (of ⋙q Φ)).obj Y) sorry
        ((lift (of ⋙q Φ)).map f))
Tactic: fapply Prefunctor.ext
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
V' : Type u_4
inst_1 : Quiver.{v', u_4} V'
inst_2 : HasReverse.{v', u_4} V'
Φ : Prefunctor.{v, v', u_2, u_4} (Symmetrify V) V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
f : X ⟶ Y
⊢ Φ.map f =
    Eq.recOn (motive := fun (x : V') (x_1 : (lift (of ⋙q Φ)).obj Y = x) ↦ Φ.obj X ⟶ x) ⋯
      (Eq.recOn (motive := fun (x : V') (x_1 : (lift (of ⋙q Φ)).obj X = x) ↦ x ⟶ (lift (of ⋙q Φ)).obj Y) ⋯
        ((lift (of ⋙q Φ)).map f))
have h_map : ∀ (val : X ⟶ Y),
  Φ.map (Sum.inl val) =
    Eq.recOn (motive := fun (x : V') (x_1 : (lift (of ⋙q Φ)).obj Y = x) ↦ Φ.obj X ⟶ x) sorry
      (Eq.recOn (motive := fun (x : V') (x_1 : (lift (of ⋙q Φ)).obj X = x) ↦ x ⟶ (lift (of ⋙q Φ)).obj Y) sorry
        ((lift (of ⋙q Φ)).map (Sum.inl val)))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
V' : Type u_4
inst_1 : Quiver.{v', u_4} V'
inst_2 : HasReverse.{v', u_4} V'
Φ : Prefunctor.{v, v', u_2, u_4} (Symmetrify V) V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
f : X ⟶ Y
h_map :
  ∀ (val : X ⟶ Y),
    Φ.map (Sum.inl val) =
      Eq.recOn (motive := fun (x : V') (x_1 : (lift (of ⋙q Φ)).obj Y = x) ↦ Φ.obj X ⟶ x) ⋯
        (Eq.recOn (motive := fun (x : V') (x_1 : (lift (of ⋙q Φ)).obj X = x) ↦ x ⟶ (lift (of ⋙q Φ)).obj Y) ⋯
          ((lift (of ⋙q Φ)).map (Sum.inl val)))
⊢ Φ.map f =
    Eq.recOn (motive := fun (x : V') (x_1 : (lift (of ⋙q Φ)).obj Y = x) ↦ Φ.obj X ⟶ x) ⋯
      (Eq.recOn (motive := fun (x : V') (x_1 : (lift (of ⋙q Φ)).obj X = x) ↦ x ⟶ (lift (of ⋙q Φ)).obj Y) ⋯
        ((lift (of ⋙q Φ)).map f))
have h_map₁ : ∀ (val : Y ⟶ X),
  Φ.map (Sum.inr val) =
    Eq.recOn (motive := fun (x : V') (x_1 : (lift (of ⋙q Φ)).obj Y = x) ↦ Φ.obj X ⟶ x) sorry
      (Eq.recOn (motive := fun (x : V') (x_1 : (lift (of ⋙q Φ)).obj X = x) ↦ x ⟶ (lift (of ⋙q Φ)).obj Y) sorry
        ((lift (of ⋙q Φ)).map (Sum.inr val)))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
U : Type u_1
V : Type u_2
W : Type u_3
inst : Quiver.{u, u_1} U
inst_1 : Quiver.{v, u_2} V
inst_2 : Quiver.{w, u_3} W
V' : Type u_4
inst_3 : Quiver.{v', u_4} V'
φ : Prefunctor.{u, v, u_1, u_2} U V
u v : Symmetrify U
e : u ⟶ v
⊢ φ.symmetrify.map (reverse e) = reverse (φ.symmetrify.map e)
have inl : ∀ (val : u ⟶ v), φ.symmetrify.map (reverse (Sum.inl val)) = reverse (φ.symmetrify.map (Sum.inl val))
Tactic: cases e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
U : Type u_1
V : Type u_2
W : Type u_3
inst : Quiver.{u, u_1} U
inst_1 : Quiver.{v, u_2} V
inst_2 : Quiver.{w, u_3} W
V' : Type u_4
inst_3 : Quiver.{v', u_4} V'
φ : Prefunctor.{u, v, u_1, u_2} U V
u v : Symmetrify U
e : u ⟶ v
inl : ∀ (val : u ⟶ v), φ.symmetrify.map (reverse (Sum.inl val)) = reverse (φ.symmetrify.map (Sum.inl val))
⊢ φ.symmetrify.map (reverse e) = reverse (φ.symmetrify.map e)
have inr : ∀ (val : v ⟶ u), φ.symmetrify.map (reverse (Sum.inr val)) = reverse (φ.symmetrify.map (Sum.inr val))
Tactic: cases e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
U : Type u_1
V : Type u_2
W : Type u_3
inst : Quiver.{u, u_1} U
inst_1 : Quiver.{v, u_2} V
inst_2 : Quiver.{w, u_3} W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse.{v, u_2} V
a b : Push σ
X Y : V
f : X ⟶ Y
⊢ Eq (α := σ X ⟶ σ Y) (reverse (reverse (PushQuiver.arrow f))) (PushQuiver.arrow f)
have dsimp : Eq (α := σ X ⟶ σ Y) (PushQuiver.arrow (HasReverse.reverse' (HasReverse.reverse' f))) (PushQuiver.arrow f)
Tactic: dsimp [reverse]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Symmetric (goal)
Goal:
U : Type u_1
V : Type u_2
W : Type u_3
inst : Quiver.{u, u_1} U
inst_1 : Quiver.{v, u_2} V
inst_2 : Quiver.{w, u_3} W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse.{v, u_2} V
a b : Push σ
X Y : V
f : X ⟶ Y
⊢ Eq (α := σ X ⟶ σ Y) (PushQuiver.arrow (HasReverse.reverse' (HasReverse.reverse' f))) (PushQuiver.arrow f)
have e_f : HasReverse.reverse' (HasReverse.reverse' f) = f
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
n : ℕ
⊢ schnirelmannDensity A * (↑n : ℝ) ≤ (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ)
have inl : schnirelmannDensity A * (↑0 : ℝ) ≤ (↑(card (α := ℕ) ({a ∈ Ioc 0 0 | a ∈ A})) : ℝ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
n : ℕ
inl : schnirelmannDensity A * (↑0 : ℝ) ≤ (↑(card (α := ℕ) ({a ∈ Ioc 0 0 | a ∈ A})) : ℝ)
⊢ schnirelmannDensity A * (↑n : ℝ) ≤ (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ)
have inr : ∀ (hn : n ≠ 0), schnirelmannDensity A * (↑n : ℝ) ≤ (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
⊢ HDiv.hDiv (α := ℝ) (↑(card (α := ℕ) ({a ∈ Ioc 0 1 | a ∈ A})) : ℝ) (↑1 : ℝ) ≤ 1
have rw : card (α := ℕ) ({a ∈ Ioc 0 1 | a ∈ A}) ≤ 1
Tactic: rw [Nat.cast_one, div_one, Nat.cast_le_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
⊢ schnirelmannDensity A ≤ HSub.hSub (α := ℝ) 1 (↑k : ℝ)⁻¹
have inl : ∀ (hk : 0 ∉ A), schnirelmannDensity A ≤ HSub.hSub (α := ℝ) 1 (↑0 : ℝ)⁻¹
Tactic: rcases k.eq_zero_or_pos with rfl | hk'
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
inl : ∀ (hk : 0 ∉ A), schnirelmannDensity A ≤ HSub.hSub (α := ℝ) 1 (↑0 : ℝ)⁻¹
⊢ schnirelmannDensity A ≤ HSub.hSub (α := ℝ) 1 (↑k : ℝ)⁻¹
have inr : ∀ (hk' : k > 0), schnirelmannDensity A ≤ HSub.hSub (α := ℝ) 1 (↑k : ℝ)⁻¹
Tactic: rcases k.eq_zero_or_pos with rfl | hk'
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ schnirelmannDensity A ≤ HSub.hSub (α := ℝ) 1 (↑k : ℝ)⁻¹
have inr : HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 k | a ∈ A})) : ℝ) (↑k : ℝ) ≤ HSub.hSub (α := ℝ) 1 (↑k : ℝ)⁻¹
Tactic: apply schnirelmannDensity_le_of_le k hk'.ne'
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 k | a ∈ A})) : ℝ) (↑k : ℝ) ≤ HSub.hSub (α := ℝ) 1 (↑k : ℝ)⁻¹
have inr : HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 k | a ∈ A})) : ℝ) (↑k : ℝ) ≤ HSub.hSub (α := ℝ) (↑k : ℝ) 1 / (↑k : ℝ)
Tactic: rw [← one_div, one_sub_div (Nat.cast_pos.2 hk').ne']
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 k | a ∈ A})) : ℝ) (↑k : ℝ) ≤ HSub.hSub (α := ℝ) (↑k : ℝ) 1 / (↑k : ℝ)
have inr : (↑(#({a ∈ Ioc 0 k | a ∈ A})) : ℝ) ≤ HSub.hSub (α := ℝ) (↑k : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ (↑(#({a ∈ Ioc 0 k | a ∈ A})) : ℝ) ≤ HSub.hSub (α := ℝ) (↑k : ℝ) 1
have inr : #({a ∈ Ioc 0 k | a ∈ A}) ≤ k - 1
Tactic: rw [← Nat.cast_pred hk', Nat.cast_le]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ #({a ∈ Ioc 0 k | a ∈ A}) ≤ k - 1
have inr : {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k
Tactic: suffices {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k from (card_le_card this).trans_eq (by simp)
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k
have inr : {a ∈ Ioo 0 k | a ∈ A} ⊆ Ioo 0 k
Tactic: rw [← Ioo_insert_right hk', filter_insert, if_neg hk]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
B : Set ℕ
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
h : A ⊆ B
x : { n : ℕ // 0 < n }
⊢ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑x : ℕ) | a ∈ A})) : ℝ) (↑(↑x : ℕ) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑x : ℕ) | a ∈ B})) : ℝ) (↑(↑x : ℕ) : ℝ)
have hc : LE.le (α := ℝ) 0 (↑(↑x : ℕ) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
⊢ schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A
have rw : 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A
Tactic: rw [le_antisymm_iff, and_iff_right schnirelmannDensity_le_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
⊢ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A
have mp : 1 ≤ schnirelmannDensity A → {0}ᶜ ⊆ A
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
mp : 1 ≤ schnirelmannDensity A → {0}ᶜ ⊆ A
⊢ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A
have mpr : {0}ᶜ ⊆ A → 1 ≤ schnirelmannDensity A
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
⊢ 1 ≤ schnirelmannDensity A → {0}ᶜ ⊆ A
have mp : ¬{0}ᶜ ⊆ A → schnirelmannDensity A < 1
Tactic: rw [← not_imp_not, not_le]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
⊢ ¬{0}ᶜ ⊆ A → schnirelmannDensity A < 1
have mp : ∀ (x : ℕ), Membership.mem (γ := Set ℕ) {0}ᶜ x → x ∉ A → schnirelmannDensity A < 1
Tactic: simp only [Set.not_subset, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
x : ℕ
hx : Membership.mem (γ := Set ℕ) {0}ᶜ x
hx' : x ∉ A
⊢ schnirelmannDensity A < 1
have mp : HSub.hSub (α := ℝ) 1 (↑x : ℝ)⁻¹ < 1
Tactic: apply (schnirelmannDensity_le_of_notMem hx').trans_lt
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
h : {0}ᶜ ⊆ A
⊢ 1 ≤ schnirelmannDensity A
have mpr : ∀ (x : { n : ℕ // 0 < n }) (n : ℕ) (hn : 0 < n),
  1 ≤
    HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ A})) : ℝ)
      (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) : ℝ)
Tactic: refine le_ciInf fun ⟨n, hn⟩ => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
h : {0}ᶜ ⊆ A
x : { n : ℕ // 0 < n }
n : ℕ
hn : 0 < n
⊢ 1 ≤
    HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ A})) : ℝ)
      (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) : ℝ)
have mpr : ∀ x ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ), x ∈ A
Tactic: rw [one_le_div (Nat.cast_pos.2 hn), Nat.cast_le, filter_true_of_mem, Nat.card_Ioc, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
⊢ schnirelmannDensity A = 1 ↔ A = Set.univ
have rw : {0}ᶜ ⊆ A ↔ A = Set.univ
Tactic: rw [schnirelmannDensity_eq_one_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A ↔ A = Set.univ
have mp : {0}ᶜ ⊆ A → A = Set.univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
mp : {0}ᶜ ⊆ A → A = Set.univ
⊢ {0}ᶜ ⊆ A ↔ A = Set.univ
have mpr : A = Set.univ → {0}ᶜ ⊆ A
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A → A = Set.univ
have mp : ∀ (h : {0}ᶜ ⊆ A) (x : ℕ), x ∈ A
Tactic: refine fun h => Set.eq_univ_of_forall fun x => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
x : ℕ
mp : 0 ∈ A
⊢ x ∈ A
have mp₁ : ∀ (hx : x ≠ 0), x ∈ A
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
x : ℝ
⊢ schnirelmannDensity A < x ↔ ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) < x
have rw : (¬∀ (n : ℕ), 0 < n → x ≤ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ)) ↔
  ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) < x
Tactic: rw [← not_le, le_schnirelmannDensity_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
x : ℝ
⊢ schnirelmannDensity A ≤ x ↔
    ∀ (ε : ℝ), 0 < ε → ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) < x + ε
have rw : (∀ (ε : ℝ), 0 < ε → schnirelmannDensity A < x + ε) ↔
  ∀ (ε : ℝ), 0 < ε → ∃ (n : ℕ), 0 < n ∧ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ) (↑n : ℝ) < x + ε
Tactic: rw [le_iff_forall_pos_lt_add]
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
B : Set ℕ
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ Eq (α := ℝ) (⨅ (n : { n : ℕ // 0 < n }), HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ))
    (⨅ (n : { n : ℕ // 0 < n }), HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ B})) : ℝ) (↑(↑n : ℕ) : ℝ))
have e_s : Eq (α := { n : ℕ // 0 < n } → ℝ)
  (fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ))
  fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ B})) : ℝ) (↑(↑n : ℕ) : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
B : Set ℕ
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ Eq (α := { n : ℕ // 0 < n } → ℝ)
    (fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ))
    fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ B})) : ℝ) (↑(↑n : ℕ) : ℝ)
have e_s : ∀ (n : ℕ) (hn : 0 < n),
  HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ A})) : ℝ)
      (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) | a ∈ B})) : ℝ)
      (↑(↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn) : ℕ) : ℝ)
Tactic: ext ⟨n, hn⟩