awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
x b c : SingleObj α
a : Path (star α) b
a_1 : b ⟶ c
ih : listToPath (pathToList a) = Path.cast ⋯ ⋯ a
cons : (listToPath (pathToList a)).cons a_1 = a.cons a_1
⊢ listToPath (pathToList (a.cons a_1)) = Path.cast ⋯ ⋯ (a.cons a_1)

Tactic:
dsimp [pathToList] at *

Premises used: Quiver.SingleObj.pathToList
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
x b c : SingleObj α
a : Path (star α) b
a_1 : b ⟶ c
ih : listToPath (pathToList a) = a
cons cons₁ : a.cons a_1 = a.cons a_1
⊢ (listToPath (pathToList a)).cons a_1 = a.cons a_1

Tactic:
rw [ih]
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
x : SingleObj α
p : Path (star α) x
nil : Eq.{u_1 + 1} (α := Path (star α) (star α)) (listToPath (pathToList Path.nil)) (Path.cast ⋯ ⋯ Path.nil)
cons :
  ∀ {b c : SingleObj α} (a : Path (star α) b) (a_1 : b ⟶ c) (ih : listToPath (pathToList a) = Path.cast ⋯ ⋯ a),
    listToPath (pathToList (a.cons a_1)) = Path.cast ⋯ ⋯ (a.cons a_1)
⊢ listToPath (pathToList p) = Path.cast ⋯ ⋯ p

Tactic:
induction p with
  | nil => rfl
  | cons _ _ ih => dsimp [pathToList] at *; rw [ih]

Premises used: Quiver.SingleObj.pathToList
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α) (pathToList (listToPath [])) []

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
a : α
l : List α
ih : pathToList (listToPath l) = l
cons cons₁ : a :: l = a :: l
⊢ a :: pathToList (listToPath l) = a :: l

Tactic:
rw [ih]
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
l : List α
nil : Eq.{u_1 + 1} (α := List α) (pathToList (listToPath [])) []
cons : ∀ (a : α) (l : List α) (ih : pathToList (listToPath l) = l), pathToList (listToPath (a :: l)) = a :: l
⊢ pathToList (listToPath l) = l

Tactic:
induction l with
  | nil => rfl
  | cons a l ih => change a :: pathToList (listToPath l) = a :: l; rw [ih]

Premises used: Quiver.SingleObj.pathToList, Quiver.SingleObj.listToPath
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α) ((pathEquivList : (a : Path (star α) (star α)) → List α) Path.nil : List α) ([] : List α)

Tactic:
rfl

Premises used: Quiver.SingleObj.pathToList, rfl
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
p : Path (star α) (star α)
a : star α ⟶ star α
⊢ (pathEquivList : (a : Path (star α) (star α)) → List α) (p.cons a) = a :: pathToList p

Tactic:
rfl

Premises used: Quiver.SingleObj.pathToList, rfl
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
⊢ Eq (α := Path (star α) (star α))
    ((Equiv.symm pathEquivList : (a : List α) → Path (star α) (star α)) [] : Path (star α) (star α))
    (Path.nil : Path (star α) (star α))

Tactic:
rfl

Premises used: Quiver.SingleObj.listToPath, rfl
-- Module: Mathlib.Combinatorics.Quiver.SingleObj
Goal:
α : Type u_1
l : List α
a : α
⊢ Eq (α := Path (star α) (star α))
    ((Equiv.symm pathEquivList : (a : List α) → Path (star α) (star α)) (a :: l) : Path (star α) (star α))
    (Path.cons (b := star α) ((Equiv.symm pathEquivList : (a : List α) → Path (star α) (star α)) l) a :
      Path (star α) (star α))

Tactic:
rfl

Premises used: Quiver.SingleObj.listToPath, rfl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h : HasInvolutiveReverse.{v, u_2} V
a b : V
f : a ⟶ b
⊢ reverse (reverse f) = f

Tactic:
apply h.inv'

Premises used: Quiver.HasInvolutiveReverse.inv'
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h : HasInvolutiveReverse.{v, u_2} V
a b : V
f g : a ⟶ b
mp : reverse f = reverse g → f = g
mpr : f = g → reverse f = reverse g
⊢ reverse f = reverse g ↔ f = g

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h_1 : HasInvolutiveReverse.{v, u_2} V
a b : V
f g : a ⟶ b
h : reverse f = reverse g
⊢ f = g

Tactic:
simpa using congr_arg Quiver.reverse h

Premises used: congr_arg, Quiver.reverse
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h_1 : HasInvolutiveReverse.{v, u_2} V
a b : V
f g : a ⟶ b
h : f = g
⊢ reverse f = reverse g

Tactic:
congr
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h : HasInvolutiveReverse.{v, u_2} V
a b : V
f : a ⟶ b
g : b ⟶ a
rw : reverse f = reverse (reverse g) ↔ reverse f = g
rw₁ rw₂ : reverse f = g ↔ reverse f = g
⊢ f = reverse g ↔ reverse f = g

Tactic:
rw [← reverse_inj, reverse_reverse]

Premises used: Quiver.reverse_inj, Quiver.reverse_reverse
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
Goal:
U : Type u_1
V : Type u_2
inst : Quiver.{u, u_1} U
inst_1 : Quiver.{v, u_2} V
inst_2 : HasReverse.{u, u_1} U
inst_3 : HasReverse.{v, u_2} V
φ : Prefunctor.{u, v, u_1, u_2} U V
inst_4 : φ.MapReverse
u v : U
e : u ⟶ v
⊢ φ.map (reverse e) = reverse (φ.map e)

Tactic:
Prefunctor.MapReverse.map_reverse' e

Premises used: Prefunctor.MapReverse.map_reverse'
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
inst_3 : HasReverse.{u, u_1} U
inst_4 : HasReverse.{v, u_2} V
inst_5 : HasReverse.{w, u_3} W
φ : Prefunctor.{u, v, u_1, u_2} U V
ψ : Prefunctor.{v, w, u_2, u_3} V W
inst_6 : φ.MapReverse
inst_7 : ψ.MapReverse
u v : U
e : u ⟶ v
⊢ (φ ⋙q ψ).map (reverse e) = reverse ((φ ⋙q ψ).map e)

Tactic:
simp only [Prefunctor.comp_map, Prefunctor.MapReverse.map_reverse']

Premises used: Prefunctor.comp_map, Prefunctor.MapReverse.map_reverse'
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
a b : Symmetrify V
e : a ⟶ b
⊢ reverse e = Sum.swap e

Tactic:
rfl

Premises used: Sum.swap, rfl, Sum.elim
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
inst_1 : HasReverse.{v, u_2} V
a b : V
f : a ⟶ b
⊢ f.toPath.reverse = (Quiver.reverse f).toPath

Tactic:
rfl

Premises used: Quiver.Hom.toPath, Quiver.Path.reverse, Quiver.Path.comp, rfl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
⊢ (p.comp nil).reverse = comp (reverse nil) p.reverse

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
b_1 c_1 : V
a_1 : Path.{v, u_2} b b_1
a_2 : b_1 ⟶ c_1
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:
simp [h]
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
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
⊢ (p.comp q).reverse = q.reverse.comp p.reverse

Tactic:
induction q with
  | nil => simp
  | cons _ _ h => simp [h]

Premises used: Quiver.Path.nil, Quiver.Path.cons
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
h : HasInvolutiveReverse.{v, u_2} V
a b : V
⊢ Eq (α := Path.{v, u_2} a a) (reverse (reverse nil)) nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
cons : a_1.comp a_2.toPath = a_1.cons a_2
⊢ (a_1.cons a_2).reverse.reverse = a_1.cons a_2

Tactic:
rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]

Premises used: Quiver.reverse_reverse, Quiver.Path.reverse_comp, Quiver.Path.reverse, Quiver.Path.reverse_toPath
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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.comp a_2.toPath = a_1.cons a_2

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
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
⊢ p.reverse.reverse = p

Tactic:
induction p with
  | nil => simp
  | cons _ _ h =>
    rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]
    rfl

Premises used: Quiver.Path.nil, Quiver.reverse_reverse, Quiver.Path.reverse_comp, Quiver.Path.cons, Quiver.Path.reverse, Quiver.Path.reverse_toPath
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
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) ⋯
        (Eq.recOn (motive := fun (x : V') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) ⋯ (φ.map f))
⊢ of ⋙q lift φ = φ

Tactic:
fapply Prefunctor.ext

Premises used: Prefunctor.ext
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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'
X : V
⊢ (of ⋙q lift φ).obj X = φ.obj X

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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'
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) ⋯
      (Eq.recOn (motive := fun (x : V') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) ⋯ (φ.map f))

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
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)
⊢ (lift φ).map (reverse f) = reverse ((lift φ).map f)

Tactic:
dsimp [Symmetrify.lift]

Premises used: Quiver.Symmetrify.lift
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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)
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)
⊢ 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:
cases f
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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 : X ⟶ Y
⊢ (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)) =
    reverse (φ.map val)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
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
⊢ 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:
simp only [reverse_reverse]

Premises used: Quiver.reverse_reverse
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
⊢ (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:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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)
subst_vars : Φ = lift (of ⋙q Φ)
⊢ Φ = lift φ

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
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) ⋯
        (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))
⊢ Φ = lift (of ⋙q Φ)

Tactic:
fapply Prefunctor.ext

Premises used: Prefunctor.ext
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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 : Symmetrify V
⊢ Φ.obj X = (lift (of ⋙q Φ)).obj X

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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)))
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) ⋯
        (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.inr 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))

Tactic:
cases f
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
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)))

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
val : Y ⟶ X
⊢ Φ.map (Sum.inr 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.inr val)))

Tactic:
hΦinv (Sum.inl _)

Premises used: Sum.swap, Sum.inl, Quiver.Symmetrify, Quiver.reverse, Sum.elim
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
val : Y ⟶ X
⊢ Φ.map (Sum.inr 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.inr val)))

Tactic:
exact hΦinv (Sum.inl _)

Premises used: Sum.inl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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))
inr : ∀ (val : v ⟶ u), φ.symmetrify.map (reverse (Sum.inr val)) = reverse (φ.symmetrify.map (Sum.inr val))
⊢ φ.symmetrify.map (reverse e) = reverse (φ.symmetrify.map e)

Tactic:
cases e
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
val : u ⟶ v
⊢ φ.symmetrify.map (reverse (Sum.inl val)) = reverse (φ.symmetrify.map (Sum.inl val))

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
val : v ⟶ u
⊢ φ.symmetrify.map (reverse (Sum.inr val)) = reverse (φ.symmetrify.map (Sum.inr val))

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
dsimp : Eq (α := σ X ⟶ σ Y) (PushQuiver.arrow (HasReverse.reverse' (HasReverse.reverse' f))) (PushQuiver.arrow f)
⊢ Eq (α := σ X ⟶ σ Y) (reverse (reverse (PushQuiver.arrow f))) (PushQuiver.arrow f)

Tactic:
dsimp [reverse]

Premises used: Quiver.reverse
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
e_f : HasReverse.reverse' (HasReverse.reverse' f) = f
⊢ Eq (α := σ X ⟶ σ Y) (PushQuiver.arrow (HasReverse.reverse' (HasReverse.reverse' f))) (PushQuiver.arrow f)

Tactic:
congr
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
⊢ HasReverse.reverse' (HasReverse.reverse' f) = f

Tactic:
apply h.inv'

Premises used: Quiver.HasInvolutiveReverse.inv'
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
Goal:
V : Type u_2
inst : Quiver.{v, u_2} V
V' : Type u_4
σ : V → V'
inst_1 : HasInvolutiveReverse.{v, u_2} V
X Y : V
f : X ⟶ Y
⊢ Eq (α := Prefunctor.obj (of σ) Y ⟶ Prefunctor.obj (of σ) X) (reverse (Prefunctor.map (of σ) f))
    (Prefunctor.map (of σ) (reverse f))

Tactic:
rfl

Premises used: Quiver.reverse, rfl
-- Module: Mathlib.Combinatorics.Quiver.Symmetric
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
⊢ ∀ {u v : V} (e : u ⟶ v),
    Eq (α := Prefunctor.obj (of σ) v ⟶ Prefunctor.obj (of σ) u) (Prefunctor.map (of σ) (reverse e))
      (reverse (Prefunctor.map (of σ) e))

Tactic:
simp [of_reverse]

Premises used: Quiver.Push.of_reverse
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
x : { n : ℕ // 0 < n }
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑x : ℕ) | a ∈ A})) : ℝ) (↑(↑x : ℕ) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
n : ℕ
hn : n ≠ 0
x : ℝ
h :
  Membership.mem (γ := Set ℝ)
    (Set.range fun (n : { n : ℕ // 0 < n }) ↦
      HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ))
    x
w : { n : ℕ // 0 < n }
hx : (fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ)) w = x
⊢ LE.le (α := ℝ) 0
    ((fun (n : { n : ℕ // 0 < n }) ↦ HDiv.hDiv (α := ℝ) (↑(#({a ∈ Ioc 0 (↑n : ℕ) | a ∈ A})) : ℝ) (↑(↑n : ℕ) : ℝ)) w)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
n : ℕ
inl : schnirelmannDensity A * (↑0 : ℝ) ≤ (↑(card (α := ℕ) ({a ∈ Ioc 0 0 | a ∈ A})) : ℝ)
inr : ∀ (hn : n ≠ 0), schnirelmannDensity A * (↑n : ℝ) ≤ (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ)
⊢ schnirelmannDensity A * (↑n : ℝ) ≤ (↑(#({a ∈ Ioc 0 n | a ∈ A})) : ℝ)

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
⊢ schnirelmannDensity A * (↑0 : ℝ) ≤ (↑(card (α := ℕ) ({a ∈ Ioc 0 0 | a ∈ A})) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
n : ℕ
hn : n ≠ 0
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity