awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
h_1 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y _x →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p_1 : R[X]
h_2 : p_1 ≠ 0
h_3 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p_1 h_2) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
h_4 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p hp) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
⊢ LT.lt (α := WithBot ℕ)
    (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
    (↑p.natDegree : WithBot ℕ)

Tactic:
simp only [degree_eq_natDegree hp, degree_eq_natDegree hd0] at wf

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
h_1 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y _x →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p_1 : R[X]
h_2 : p_1 ≠ 0
h_3 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p_1 h_2) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
h_4 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p hp) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf :
  LT.lt (α := WithBot ℕ)
    (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
    (↑p.natDegree : WithBot ℕ)
⊢ LT.lt (α := WithBot ℕ)
    (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
    (↑p.natDegree : WithBot ℕ)

Tactic:
assumption
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
h_1 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y _x →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p_1 : R[X]
h_2 : p_1 ≠ 0
h_3 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p_1 h_2) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
h_4 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p hp) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
apply :
  LT.lt (α := WithBot ℕ)
    (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
    (↑p.natDegree : WithBot ℕ)
apply₁ :
  ∀
    (wf :
      LT.lt (α := WithBot ℕ)
        (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
        (↑p.natDegree : WithBot ℕ)),
    LT.lt (α := WithBot ℕ)
      (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
      (↑p.natDegree : WithBot ℕ)
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree < p.natDegree

Tactic:
{
  apply (Nat.cast_lt (α := WithBot ℕ)).mp
  simp only [degree_eq_natDegree hp, degree_eq_natDegree hd0] at wf
  assumption}

Premises used: Polynomial.degree_eq_natDegree, Iff.mp, Nat.cast_lt
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
h_1 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y _x →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p_1 : R[X]
h_2 : p_1 ≠ 0
h_3 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p_1 h_2) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
h_4 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p hp) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
decreasing_by :
  LT.lt (α := WithBot ℕ)
    (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
    (↑p.natDegree : WithBot ℕ)
decreasing_by₁ :
  ∀
    (wf :
      LT.lt (α := WithBot ℕ)
        (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
        (↑p.natDegree : WithBot ℕ)),
    LT.lt (α := WithBot ℕ)
      (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
      (↑p.natDegree : WithBot ℕ)
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree < p.natDegree

Tactic:
decreasing_by {
  apply (Nat.cast_lt (α := WithBot ℕ)).mp
  simp only [degree_eq_natDegree hp, degree_eq_natDegree hd0] at wf
  assumption}

Premises used: Polynomial.degree_eq_natDegree, Iff.mp, Nat.cast_lt
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommMonoid M
inst_3 : DecidableEq M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
t : Finset M
r : R
hr : r ≠ 0
rw : 0 ∈ (↑(r • t) : Set M) ↔ 0 ∈ t
rw₁ : 0 ∈ r • (↑t : Set M) ↔ 0 ∈ t
rw₂ : 0 ∈ (↑t : Set M) ↔ 0 ∈ t
rw₃ rw₄ : 0 ∈ t ↔ 0 ∈ t
⊢ 0 ∈ r • t ↔ 0 ∈ t

Tactic:
rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff hr, mem_coe]

Premises used: Set.zero_mem_smul_set_iff, Finset.coe_smul_finset, Finset.mem_coe
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommMonoid M
inst_3 : DecidableEq M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
s : Finset R
t : Finset M
rw :
  0 ∈ (↑s : Set R) ∧ (↑t : Set M).Nonempty ∨ 0 ∈ (↑t : Set M) ∧ (↑s : Set R).Nonempty ↔
    0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
⊢ 0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
rw [← mem_coe, coe_smul, Set.zero_mem_smul_iff]

Premises used: Set.zero_mem_smul_iff, Finset.coe_smul, Finset.mem_coe
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : IsDomain R
inst_2 : AddCommMonoid M
inst_3 : DecidableEq M
inst_4 : Module R M
inst_5 : IsTorsionFree R M
s : Finset R
t : Finset M
⊢ 0 ∈ (↑s : Set R) ∧ (↑t : Set M).Nonempty ∨ 0 ∈ (↑t : Set M) ∧ (↑s : Set R).Nonempty ↔
    0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset
Goal:
R : Type u_1
G : Type u_2
inst : Ring R
inst_1 : AddCommGroup G
inst_2 : Module R G
inst_3 : DecidableEq G
t : Finset G
a : R
⊢ -a • t = -(a • t)

Tactic:
simp only [← image_smul, ← image_neg_eq_neg, image_image, neg_smul, Function.comp_def]

Premises used: neg_smul, Finset.image_smul, Function.comp_def, Finset.image_neg_eq_neg, Finset.image_image
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset
Goal:
R : Type u_1
G : Type u_2
inst : Ring R
inst_1 : AddCommGroup G
inst_2 : Module R G
inst_3 : DecidableEq G
s : Finset R
t : Finset G
inst_4 : DecidableEq R
⊢ HSMul.hSMul (α := Finset R) (image (fun (x : R) ↦ -x) s) t = image (fun (x : G) ↦ -x) (s • t)

Tactic:
image₂_image_left_comm neg_smul

Premises used: neg_smul, Finset.image₂_image_left_comm
-- Module: Mathlib.Algebra.Ring.Action.Pointwise.Finset
Goal:
R : Type u_1
G : Type u_2
inst : Ring R
inst_1 : AddCommGroup G
inst_2 : Module R G
inst_3 : DecidableEq G
s : Finset R
t : Finset G
inst_4 : DecidableEq R
⊢ HSMul.hSMul (α := Finset R) (image (fun (x : R) ↦ -x) s) t = image (fun (x : G) ↦ -x) (s • t)

Tactic:
exact image₂_image_left_comm neg_smul

Premises used: neg_smul, Finset.image₂_image_left_comm
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f : Edge x y
⊢ HomotopicL f f

Tactic:
⟨compId f⟩

Premises used: SSet.Truncated.Edge.CompStruct.compId, Nonempty.intro
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
hfg : HomotopicL f g
rcases : ∀ (hfg : f.CompStruct (Edge.id y) g), HomotopicL g f
⊢ HomotopicL g f

Tactic:
rcases hfg with ⟨hfg⟩
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
hfg : f.CompStruct (Edge.id y) g
⊢ HomotopicL g f

Tactic:
Quasicategory₂.fill31 hfg (idComp (id y)) (compId f)

Premises used: SSet.Truncated.Edge.CompStruct.compId, SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.Quasicategory₂.fill31, SSet.Truncated.Edge.id
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
hfg : f.CompStruct (Edge.id y) g
⊢ HomotopicL g f

Tactic:
exact Quasicategory₂.fill31 hfg (idComp (id y)) (compId f)

Premises used: SSet.Truncated.Edge.CompStruct.compId, SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.Quasicategory₂.fill31, SSet.Truncated.Edge.id
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g h : Edge x y
hfg : HomotopicL f g
hgh : HomotopicL g h
rcases : ∀ (hfg : f.CompStruct (Edge.id y) g), HomotopicL f h
⊢ HomotopicL f h

Tactic:
rcases hfg with ⟨hfg⟩
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g h : Edge x y
hgh : HomotopicL g h
hfg : f.CompStruct (Edge.id y) g
rcases : ∀ (hgh : g.CompStruct (Edge.id y) h), HomotopicL f h
⊢ HomotopicL f h

Tactic:
rcases hgh with ⟨hgh⟩
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g h : Edge x y
hfg : f.CompStruct (Edge.id y) g
hgh : g.CompStruct (Edge.id y) h
⊢ HomotopicL f h

Tactic:
Quasicategory₂.fill32 hfg (idComp (id y)) hgh

Premises used: SSet.Truncated.Quasicategory₂.fill32, SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.Edge.id
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g h : Edge x y
hfg : f.CompStruct (Edge.id y) g
hgh : g.CompStruct (Edge.id y) h
⊢ HomotopicL f h

Tactic:
exact Quasicategory₂.fill32 hfg (idComp (id y)) hgh

Premises used: SSet.Truncated.Quasicategory₂.fill32, SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.Edge.id
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f : Edge x y
⊢ HomotopicR f f

Tactic:
⟨idComp f⟩

Premises used: Nonempty.intro, SSet.Truncated.Edge.CompStruct.idComp
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
hfg : HomotopicR f g
rcases : ∀ (hfg : (Edge.id x).CompStruct f g), HomotopicR g f
⊢ HomotopicR g f

Tactic:
rcases hfg with ⟨hfg⟩
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
hfg : (Edge.id x).CompStruct f g
⊢ HomotopicR g f

Tactic:
Quasicategory₂.fill32 (idComp (id x)) hfg (idComp f)

Premises used: SSet.Truncated.Quasicategory₂.fill32, SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.Edge.id
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
hfg : (Edge.id x).CompStruct f g
⊢ HomotopicR g f

Tactic:
exact Quasicategory₂.fill32 (idComp (id x)) hfg (idComp f)

Premises used: SSet.Truncated.Quasicategory₂.fill32, SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.Edge.id
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g h : Edge x y
hfg : HomotopicR f g
hgh : HomotopicR g h
rcases : ∀ (hfg : (Edge.id x).CompStruct f g), HomotopicR f h
⊢ HomotopicR f h

Tactic:
rcases hfg with ⟨hfg⟩
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g h : Edge x y
hgh : HomotopicR g h
hfg : (Edge.id x).CompStruct f g
rcases : ∀ (hgh : (Edge.id x).CompStruct g h), HomotopicR f h
⊢ HomotopicR f h

Tactic:
rcases hgh with ⟨hgh⟩
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g h : Edge x y
hfg : (Edge.id x).CompStruct f g
hgh : (Edge.id x).CompStruct g h
⊢ HomotopicR f h

Tactic:
Quasicategory₂.fill31 (idComp (id x)) hfg hgh

Premises used: SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.Quasicategory₂.fill31, SSet.Truncated.Edge.id
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g h : Edge x y
hfg : (Edge.id x).CompStruct f g
hgh : (Edge.id x).CompStruct g h
⊢ HomotopicR f h

Tactic:
exact Quasicategory₂.fill31 (idComp (id x)) hfg hgh

Premises used: SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.Quasicategory₂.fill31, SSet.Truncated.Edge.id
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
h : HomotopicL f g
rcases : ∀ (h : f.CompStruct (Edge.id y) g), HomotopicR f g
⊢ HomotopicR f g

Tactic:
rcases h with ⟨h⟩
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
h : f.CompStruct (Edge.id y) g
⊢ HomotopicR f g

Tactic:
Quasicategory₂.fill32 (idComp f) (compId f) h

Premises used: SSet.Truncated.Quasicategory₂.fill32, SSet.Truncated.Edge.CompStruct.compId, SSet.Truncated.Edge.CompStruct.idComp
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
h : f.CompStruct (Edge.id y) g
⊢ HomotopicR f g

Tactic:
exact Quasicategory₂.fill32 (idComp f) (compId f) h

Premises used: SSet.Truncated.Quasicategory₂.fill32, SSet.Truncated.Edge.CompStruct.compId, SSet.Truncated.Edge.CompStruct.idComp
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
h : HomotopicR f g
rcases : ∀ (h : (Edge.id x).CompStruct f g), HomotopicL f g
⊢ HomotopicL f g

Tactic:
rcases h with ⟨h⟩
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
h : (Edge.id x).CompStruct f g
⊢ HomotopicL f g

Tactic:
Quasicategory₂.fill31 (idComp f) (compId f) h

Premises used: SSet.Truncated.Edge.CompStruct.compId, SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.Quasicategory₂.fill31
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
h : (Edge.id x).CompStruct f g
⊢ HomotopicL f g

Tactic:
exact Quasicategory₂.fill31 (idComp f) (compId f) h

Premises used: SSet.Truncated.Edge.CompStruct.compId, SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.Quasicategory₂.fill31
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
X : Truncated 2
inst : X.Quasicategory₂
x y :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f g : Edge x y
⊢ HomotopicL f g ↔ HomotopicR f g

Tactic:
⟨HomotopicL.homotopicR, HomotopicR.homotopicL⟩

Premises used: SSet.Truncated.HomotopicL.homotopicR, Iff.intro, SSet.Truncated.HomotopicR.homotopicL
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hf : HomotopicL f f'
hg : HomotopicL g g'
rcases : ∀ (hg : (id y).CompStruct g g'), HomotopicL h h'
⊢ HomotopicL h h'

Tactic:
rcases hg.homotopicR with ⟨hg⟩

Premises used: SSet.Truncated.HomotopicL.homotopicR
-- Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
Goal:
A : Truncated 2
inst : A.Quasicategory₂
x y z :
  A.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) { len := 0 }
        Quasicategory₂._proof_1))
f f' : Edge x y
g g' : Edge y z
h h' : Edge x z
s : f.CompStruct g h
s' : f'.CompStruct g' h'
hf : HomotopicL f f'
hg_1 : HomotopicL g g'
hg : (id y).CompStruct g g'
rcases : ∀ (hf : f.CompStruct (id y) f'), HomotopicL h h'
⊢ HomotopicL h h'

Tactic:
rcases hf with ⟨hf⟩