-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem IsNormal.generatedNormal_le {S : Subgroupoid C} (Sn : S.IsNormal) :
    generatedNormal X ≤ S ↔ ∀ c d, X c d ⊆ S.arrows c d

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : ∀ {c d : C}, (generatedNormal X).arrows c d ⊆ S.arrows c d
c d : C
h' : ∀ {c d : C}, (generated X).arrows c d ⊆ (generatedNormal X).arrows c d
⊢ X c d ⊆ S.arrows c d

Tactic:
exact ((subset_generated X c d).trans (@h' c d)).trans (@h c d)

Result:
no goals

Proof state:
case mpr.a
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : ∀ (c d : C), X c d ⊆ S.arrows c d
⊢ S ∈ {S | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal}

Tactic:
exact ⟨h, Sn⟩

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ (∀ (c d : C), X c d ⊆ S.arrows c d) → generatedNormal X ≤ S

Tactic:
rintro h

Result:
case mpr
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : ∀ (c d : C), X c d ⊆ S.arrows c d
⊢ generatedNormal X ≤ S

Proof state:
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ generatedNormal X ≤ S ↔ ∀ (c d : C), X c d ⊆ S.arrows c d

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ generatedNormal X ≤ S → ∀ (c d : C), X c d ⊆ S.arrows c d

case mpr
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ (∀ (c d : C), X c d ⊆ S.arrows c d) → generatedNormal X ≤ S

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : generatedNormal X ≤ S
c d : C
h' : generated X ≤ generatedNormal X
⊢ X c d ⊆ S.arrows c d

Tactic:
rw [le_iff] at h h'

Result:
case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : ∀ {c d : C}, (generatedNormal X).arrows c d ⊆ S.arrows c d
c d : C
h' : ∀ {c d : C}, (generated X).arrows c d ⊆ (generatedNormal X).arrows c d
⊢ X c d ⊆ S.arrows c d

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : generatedNormal X ≤ S
c d : C
⊢ X c d ⊆ S.arrows c d

Tactic:
have h' := generated_le_generatedNormal X

Result:
case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : generatedNormal X ≤ S
c d : C
h' : generated X ≤ generatedNormal X
⊢ X c d ⊆ S.arrows c d

Proof state:
case mpr
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : ∀ (c d : C), X c d ⊆ S.arrows c d
⊢ generatedNormal X ≤ S

Tactic:
apply @sInf_le (Subgroupoid C) _

Result:
case mpr.a
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : ∀ (c d : C), X c d ⊆ S.arrows c d
⊢ S ∈ {S | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal}

Proof state:
case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ generatedNormal X ≤ S → ∀ (c d : C), X c d ⊆ S.arrows c d

Tactic:
rintro h c d

Result:
case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : generatedNormal X ≤ S
c d : C
⊢ X c d ⊆ S.arrows c d