-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
/-- A property is true for every morphism iff it holds for generators and is multiplicative. -/
lemma multiplicativeClosure_isGenerator_eq_top : generators.multiplicativeClosure = ⊤

Proof state:
⊢ generators.multiplicativeClosure = ⊤

Tactic:
apply le_antisymm (by simp)

Result:
⊢ ⊤ ≤ generators.multiplicativeClosure

Proof state:
x y : SimplexCategoryGenRel
f : x ⟶ y
a✝ : ⊤ f
⊢ generators.multiplicativeClosure f

Tactic:
apply CategoryTheory.Quotient.induction

Result:
case h
x y : SimplexCategoryGenRel
f : x ⟶ y
a✝ : ⊤ f
⊢ ∀ {x y : Paths FreeSimplexQuiver} (f : x ⟶ y),
    generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map f)

Proof state:
⊢ ⊤ ≤ generators.multiplicativeClosure

Tactic:
intro x y f _

Result:
x y : SimplexCategoryGenRel
f : x ⟶ y
a✝ : ⊤ f
⊢ generators.multiplicativeClosure f

Proof state:
case h.id
x y : SimplexCategoryGenRel
f : x ⟶ y
a✝ : ⊤ f
⊢ ∀ {v : FreeSimplexQuiver},
    generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map (𝟙 (Paths.of.obj v)))

Tactic:
exact generators.multiplicativeClosure.id_mem _

Result:
no goals

Proof state:
case h.comp
x y : SimplexCategoryGenRel
f : x ⟶ y
a✝ : ⊤ f
⊢ ∀ {u v w : FreeSimplexQuiver} (p : Paths.of.obj u ⟶ Paths.of.obj v) (q : v ⟶ w),
    generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p) →
      generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map (p ≫ Paths.of.map q))

Tactic:
rintro _ _ _ _ ⟨⟩ h

Result:
case h.comp.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
a✝ : ⊤ f
u✝ : FreeSimplexQuiver
n✝ : ℕ
i✝ : Fin (n✝ + 2)
p✝ : Paths.of.obj u✝ ⟶ Paths.of.obj (FreeSimplexQuiver.mk n✝)
h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p✝)
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map (p✝ ≫ Paths.of.map (FreeSimplexQuiver.Hom.δ i✝)))

case h.comp.σ
x y : SimplexCategoryGenRel
f : x ⟶ y
a✝ : ⊤ f
u✝ : FreeSimplexQuiver
n✝ : ℕ
i✝ : Fin (n✝ + 1)
p✝ : Paths.of.obj u✝ ⟶ Paths.of.obj (FreeSimplexQuiver.mk (n✝ + 1))
h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p✝)
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map (p✝ ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ i✝)))

Proof state:
case h.comp.σ
x y : SimplexCategoryGenRel
f : x ⟶ y
a✝ : ⊤ f
u✝ : FreeSimplexQuiver
n✝ : ℕ
i✝ : Fin (n✝ + 1)
p✝ : Paths.of.obj u✝ ⟶ Paths.of.obj (FreeSimplexQuiver.mk (n✝ + 1))
h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p✝)
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map (p✝ ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ i✝)))

Tactic:
exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .σ _

Result:
no goals

Proof state:
case h.comp.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
a✝ : ⊤ f
u✝ : FreeSimplexQuiver
n✝ : ℕ
i✝ : Fin (n✝ + 2)
p✝ : Paths.of.obj u✝ ⟶ Paths.of.obj (FreeSimplexQuiver.mk n✝)
h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p✝)
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map (p✝ ≫ Paths.of.map (FreeSimplexQuiver.Hom.δ i✝)))

Tactic:
exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .δ _

Result:
no goals

Proof state:
case h
x y : SimplexCategoryGenRel
f : x ⟶ y
a✝ : ⊤ f
⊢ ∀ {x y : Paths FreeSimplexQuiver} (f : x ⟶ y),
    generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map f)

Tactic:
apply Paths.induction

Result:
case h.id
x y : SimplexCategoryGenRel
f : x ⟶ y
a✝ : ⊤ f
⊢ ∀ {v : FreeSimplexQuiver},
    generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map (𝟙 (Paths.of.obj v)))

case h.comp
x y : SimplexCategoryGenRel
f : x ⟶ y
a✝ : ⊤ f
⊢ ∀ {u v w : FreeSimplexQuiver} (p : Paths.of.obj u ⟶ Paths.of.obj v) (q : v ⟶ w),
    generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p) →
      generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map (p ≫ Paths.of.map q))

Proof state:
⊢ generators.multiplicativeClosure ≤ ⊤

Tactic:
simp

Result:
no goals