internlm/Lean-Github huggingface dataset:
Theorem: cmtr_pow_mul_unfix
Proof state before:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), y q ≠ q
Tactic:
exact hy
Proof state after:
no goals
Theorem: cmtr_pow_mul_unfix
Proof state before:
case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ 1 * y) q ≠ q
Tactic:
rw [pow_one]
Proof state after:
case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ * y) q ≠ q
Theorem: cmtr_pow_mul_unfix
Proof state before:
case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ * y) q ≠ q
Tactic:
exact cmtr_mul_unfix_of_unfix hy
Proof state after:
no goals
Theorem: cmtr_pow_mul_unfix
Proof state before:
case H3
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
_IH2✝ : ∀ (q : α), (⁅x, y⁆ ^ k.succ * y) q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ k.succ.succ * y) q ≠ q
Tactic:
intros q h
Proof state after:
case H3
α : Type u
x y : Perm α
q✝ : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
_IH2✝ : ∀ (q : α), (⁅x, y⁆ ^ k.succ * y) q ≠ q
q : α
h : (⁅x, y⁆ ^ k.succ.succ * y) q = q
⊢ False
Theorem: cmtr_pow_mul_unfix
Proof state before:
case H3
α : Type u
x y : Perm α
q✝ : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
_IH2✝ : ∀ (q : α), (⁅x, y⁆ ^ k.succ * y) q ≠ q
q : α
h : (⁅x, y⁆ ^ k.succ.succ * y) q = q
⊢ False
Tactic:
simp_rw [pow_succ (n := k.succ), pow_succ' (n := k), mul_assoc,
  cmtr_mul_eq_mul_inv_cmtr_inv, hxy, Perm.mul_apply,
  ← Perm.eq_inv_iff_eq (f := ⁅x, y⁆)] at h
Proof state after:
case H3
α : Type u
x y : Perm α
q✝ : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
_IH2✝ : ∀ (q : α), (⁅x, y⁆ ^ k.succ * y) q ≠ q
q : α
h : (⁅x, y⁆ ^ k) (y (⁅x, y⁆⁻¹ q)) = ⁅x, y⁆⁻¹ q
⊢ False
Theorem: cmtr_pow_mul_unfix
Proof state before:
case H3
α : Type u
x y : Perm α
q✝ : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
_IH2✝ : ∀ (q : α), (⁅x, y⁆ ^ k.succ * y) q ≠ q
q : α
h : (⁅x, y⁆ ^ k) (y (⁅x, y⁆⁻¹ q)) = ⁅x, y⁆⁻¹ q
⊢ False
Tactic:
exact IH (⁅x, y⁆⁻¹ q) h
Proof state after:
no goals
Theorem: cmtr_pow_inv_apply_ne_apply
Proof state before:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (⁅x, y⁆ ^ k)⁻¹ q ≠ y q
Tactic:
simp_rw [Perm.inv_eq_iff_eq.not]
Proof state after:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ¬q = (⁅x, y⁆ ^ k) (y q)
Theorem: cmtr_pow_inv_apply_ne_apply
Proof state before:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ¬q = (⁅x, y⁆ ^ k) (y q)
Tactic:
exact Ne.symm (cmtr_pow_mul_unfix hxy hy _)
Proof state after:
no goals
Theorem: cmtr_zpow_apply_ne_apply
Proof state before:
α : Type u
x y : Perm α
q : α
k : ℤ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (⁅x, y⁆ ^ k) q ≠ y q
Tactic:
cases k
Proof state after:
case ofNat
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.ofNat a✝) q ≠ y q

case negSucc
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.negSucc a✝) q ≠ y q
Theorem: cmtr_zpow_apply_ne_apply
Proof state before:
case ofNat
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.ofNat a✝) q ≠ y q
Tactic:
simp only [Int.ofNat_eq_coe, zpow_natCast, ne_eq, hxy, hy, not_false_eq_true, implies_true,
  cmtr_pow_apply_ne_apply]
Proof state after:
no goals
Theorem: cmtr_zpow_apply_ne_apply
Proof state before:
case negSucc
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
a✝ : ℕ
⊢ (⁅x, y⁆ ^ Int.negSucc a✝) q ≠ y q
Tactic:
simp only [zpow_negSucc, ne_eq, hxy, hy, not_false_eq_true, implies_true,
  cmtr_pow_inv_apply_ne_apply]
Proof state after:
no goals
Theorem: cmtr_zpow_apply_ne_apply_cmtr_pow_apply
Proof state before:
α : Type u
x y : Perm α
q : α
j k : ℤ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (⁅x, y⁆ ^ j) q ≠ y ((⁅x, y⁆ ^ k) q)
Tactic:
rw [← sub_add_cancel j k, zpow_add, Perm.mul_apply]
Proof state after:
α : Type u
x y : Perm α
q : α
j k : ℤ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (⁅x, y⁆ ^ (j - k)) ((⁅x, y⁆ ^ k) q) ≠ y ((⁅x, y⁆ ^ k) q)
Theorem: cmtr_zpow_apply_ne_apply_cmtr_pow_apply
Proof state before:
α : Type u
x y : Perm α
q : α
j k : ℤ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (⁅x, y⁆ ^ (j - k)) ((⁅x, y⁆ ^ k) q) ≠ y ((⁅x, y⁆ ^ k) q)
Tactic:
exact cmtr_zpow_apply_ne_apply hxy hy
Proof state after:
no goals
Theorem: Fin.perm_fin_two
Proof state before:
π : Equiv.Perm (Fin 2)
⊢ π = if π 0 = 1 then Equiv.swap 0 1 else 1
Tactic:
rw [Equiv.ext_iff, forall_fin_two]
Proof state after:
π : Equiv.Perm (Fin 2)
⊢ π 0 = (if π 0 = 1 then Equiv.swap 0 1 else 1) 0 ∧ π 1 = (if π 0 = 1 then Equiv.swap 0 1 else 1) 1
Theorem: Fin.perm_fin_two
Proof state before:
π : Equiv.Perm (Fin 2)
⊢ π 0 = (if π 0 = 1 then Equiv.swap 0 1 else 1) 0 ∧ π 1 = (if π 0 = 1 then Equiv.swap 0 1 else 1) 1
Tactic:
rcases (exists_fin_two.mp ⟨π 0, rfl⟩) with (h0 | h0) <;>
rcases (exists_fin_two.mp ⟨π 1, rfl⟩) with (h1 | h1) <;>
simp only [h0, ite_true, Equiv.swap_apply_left, h1, Equiv.swap_apply_right, one_eq_zero_iff, id_eq,
  OfNat.ofNat_ne_one, and_false, zero_eq_one_iff, ite_false, Equiv.Perm.coe_one,  and_self] <;>
exact (zero_ne_one ((EmbeddingLike.apply_eq_iff_eq _).mp (h0.trans (h1.symm)))).elim
Proof state after:
no goals
Theorem: Fin.perm_fin_two_mul_self
Proof state before:
π : Equiv.Perm (Fin 2)
⊢ π * π = 1
Tactic:
rw [perm_fin_two π]
Proof state after:
π : Equiv.Perm (Fin 2)
⊢ ((if π 0 = 1 then Equiv.swap 0 1 else 1) * if π 0 = 1 then Equiv.swap 0 1 else 1) = 1
Theorem: Fin.perm_fin_two_mul_self
Proof state before:
π : Equiv.Perm (Fin 2)
⊢ ((if π 0 = 1 then Equiv.swap 0 1 else 1) * if π 0 = 1 then Equiv.swap 0 1 else 1) = 1
Tactic:
split_ifs
Proof state after:
case pos
π : Equiv.Perm (Fin 2)
h✝ : π 0 = 1
⊢ Equiv.swap 0 1 * Equiv.swap 0 1 = 1

case neg
π : Equiv.Perm (Fin 2)
h✝ : ¬π 0 = 1
⊢ 1 * 1 = 1
Theorem: Fin.perm_fin_two_mul_self
Proof state before:
case pos
π : Equiv.Perm (Fin 2)
h✝ : π 0 = 1
⊢ Equiv.swap 0 1 * Equiv.swap 0 1 = 1
Tactic:
rw [Equiv.swap_mul_self]
Proof state after:
no goals
Theorem: Fin.perm_fin_two_mul_self
Proof state before:
case neg
π : Equiv.Perm (Fin 2)
h✝ : ¬π 0 = 1
⊢ 1 * 1 = 1
Tactic:
rw [mul_one]
Proof state after:
no goals
Theorem: Fin.perm_fin_two_apply_apply
Proof state before:
q : Fin 2
π : Equiv.Perm (Fin 2)
⊢ π (π q) = q
Tactic:
rw [← Equiv.Perm.mul_apply, perm_fin_two_mul_self, Equiv.Perm.one_apply]
Proof state after:
no goals
Theorem: Fin.perm_fin_two_of_fix_zero
Proof state before:
π : Equiv.Perm (Fin 2)
h : π 0 = 0
⊢ π = 1
Tactic:
rw [perm_fin_two π]
Proof state after:
π : Equiv.Perm (Fin 2)
h : π 0 = 0
⊢ (if π 0 = 1 then Equiv.swap 0 1 else 1) = 1
Theorem: Fin.perm_fin_two_of_fix_zero
Proof state before:
π : Equiv.Perm (Fin 2)
h : π 0 = 0
⊢ (if π 0 = 1 then Equiv.swap 0 1 else 1) = 1
Tactic:
simp_rw [h, zero_eq_one_iff, OfNat.ofNat_ne_one, ite_false]
Proof state after:
no goals
Theorem: Fin.perm_fin_two_of_fix_one
Proof state before:
π : Equiv.Perm (Fin 2)
h : π 1 = 1
⊢ π = 1
Tactic:
rw [perm_fin_two π, ← h]
Proof state after:
π : Equiv.Perm (Fin 2)
h : π 1 = 1
⊢ (if π 0 = π 1 then Equiv.swap 0 (π 1) else 1) = 1
Theorem: Fin.perm_fin_two_of_fix_one
Proof state before:
π : Equiv.Perm (Fin 2)
h : π 1 = 1
⊢ (if π 0 = π 1 then Equiv.swap 0 (π 1) else 1) = 1
Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq, zero_eq_one_iff, OfNat.ofNat_ne_one, ite_false]
Proof state after:
no goals
Theorem: Fin.perm_fin_two_of_unfix_zero
Proof state before:
π : Equiv.Perm (Fin 2)
h : π 0 = 1
⊢ π = Equiv.swap 0 1
Tactic:
rw [perm_fin_two π]
Proof state after:
π : Equiv.Perm (Fin 2)
h : π 0 = 1
⊢ (if π 0 = 1 then Equiv.swap 0 1 else 1) = Equiv.swap 0 1
Theorem: Fin.perm_fin_two_of_unfix_zero
Proof state before:
π : Equiv.Perm (Fin 2)
h : π 0 = 1
⊢ (if π 0 = 1 then Equiv.swap 0 1 else 1) = Equiv.swap 0 1
Tactic:
simp_rw [h, ite_true]
Proof state after:
no goals
Theorem: Fin.perm_fin_two_of_unfix_one
Proof state before:
π : Equiv.Perm (Fin 2)
h : π 1 = 0
⊢ π = Equiv.swap 0 1
Tactic:
rw [perm_fin_two π, ← perm_fin_two_apply_apply (π := π) (q := 1)]
Proof state after:
π : Equiv.Perm (Fin 2)
h : π 1 = 0
⊢ (if π 0 = π (π 1) then Equiv.swap 0 (π (π 1)) else 1) = Equiv.swap 0 (π (π 1))
Theorem: Fin.perm_fin_two_of_unfix_one
Proof state before:
π : Equiv.Perm (Fin 2)
h : π 1 = 0
⊢ (if π 0 = π (π 1) then Equiv.swap 0 (π (π 1)) else 1) = Equiv.swap 0 (π (π 1))
Tactic:
simp_rw [h, ite_true]
Proof state after:
no goals
Theorem: Fin.cmtr_fin_two
Proof state before:
x y : Equiv.Perm (Fin 2)
⊢ ⁅x, y⁆ = 1
Tactic:
rw [perm_fin_two x, perm_fin_two y]
Proof state after:
x y : Equiv.Perm (Fin 2)
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Theorem: Fin.cmtr_fin_two
Proof state before:
x y : Equiv.Perm (Fin 2)
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Tactic:
by_cases h : (x 0 = 1)
Proof state after:
case pos
x y : Equiv.Perm (Fin 2)
h : x 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1

case neg
x y : Equiv.Perm (Fin 2)
h : ¬x 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Theorem: Fin.cmtr_fin_two
Proof state before:
case pos
x y : Equiv.Perm (Fin 2)
h : x 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Tactic:
by_cases h₂ : (y 0 = 1)
Proof state after:
case pos
x y : Equiv.Perm (Fin 2)
h : x 0 = 1
h₂ : y 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1

case neg
x y : Equiv.Perm (Fin 2)
h : x 0 = 1
h₂ : ¬y 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Theorem: Fin.cmtr_fin_two
Proof state before:
case pos
x y : Equiv.Perm (Fin 2)
h : x 0 = 1
h₂ : y 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Tactic:
rw [if_pos h, if_pos h₂, commutatorElement_self]
Proof state after:
no goals
Theorem: Fin.cmtr_fin_two
Proof state before:
case neg
x y : Equiv.Perm (Fin 2)
h : x 0 = 1
h₂ : ¬y 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Tactic:
rw [if_neg h₂, commutatorElement_one_right]
Proof state after:
no goals
Theorem: Fin.cmtr_fin_two
Proof state before:
case neg
x y : Equiv.Perm (Fin 2)
h : ¬x 0 = 1
⊢ ⁅if x 0 = 1 then Equiv.swap 0 1 else 1, if y 0 = 1 then Equiv.swap 0 1 else 1⁆ = 1
Tactic:
rw [if_neg h, commutatorElement_one_left]
Proof state after:
no goals
Theorem: Category.imageQuotientFunctor_faithful
Proof state before:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
⊢ Faithful (imageQuotientFunctor F)
Tactic:
intro A B f g
Proof state after:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f g : A ⟶ B
⊢ Functor.map (imageQuotientFunctor F) f = Functor.map (imageQuotientFunctor F) g → f = g
Theorem: Category.imageQuotientFunctor_faithful
Proof state before:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f g : A ⟶ B
⊢ Functor.map (imageQuotientFunctor F) f = Functor.map (imageQuotientFunctor F) g → f = g
Tactic:
refine HomQuotient.inductionOn f ?_
Proof state after:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f g : A ⟶ B
⊢ ∀ (f : A.unquot ⟶ B.unquot),
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f) =
        Functor.map (imageQuotientFunctor F) g →
      HomQuotient.quotHom (imageCongruence F) f = g
Theorem: Category.imageQuotientFunctor_faithful
Proof state before:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f g : A ⟶ B
⊢ ∀ (f : A.unquot ⟶ B.unquot),
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f) =
        Functor.map (imageQuotientFunctor F) g →
      HomQuotient.quotHom (imageCongruence F) f = g
Tactic:
refine HomQuotient.inductionOn g ?_
Proof state after:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f g : A ⟶ B
⊢ ∀ (f f_1 : A.unquot ⟶ B.unquot),
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f_1) =
        Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f) →
      HomQuotient.quotHom (imageCongruence F) f_1 = HomQuotient.quotHom (imageCongruence F) f
Theorem: Category.imageQuotientFunctor_faithful
Proof state before:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f g : A ⟶ B
⊢ ∀ (f f_1 : A.unquot ⟶ B.unquot),
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f_1) =
        Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f) →
      HomQuotient.quotHom (imageCongruence F) f_1 = HomQuotient.quotHom (imageCongruence F) f
Tactic:
intro f g h
Proof state after:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f✝ g✝ : A ⟶ B
f g : A.unquot ⟶ B.unquot
h :
  Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) g) =
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f)
⊢ HomQuotient.quotHom (imageCongruence F) g = HomQuotient.quotHom (imageCongruence F) f
Theorem: Category.imageQuotientFunctor_faithful
Proof state before:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f✝ g✝ : A ⟶ B
f g : A.unquot ⟶ B.unquot
h :
  Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) g) =
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f)
⊢ HomQuotient.quotHom (imageCongruence F) g = HomQuotient.quotHom (imageCongruence F) f
Tactic:
rw [HomQuotient.quotHom_eq_iff]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f✝ g✝ : A ⟶ B
f g : A.unquot ⟶ B.unquot
h :
  Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) g) =
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f)
⊢ Congruence.rel (imageCongruence F) A.unquot B.unquot g f
Theorem: Category.imageQuotientFunctor_faithful
Proof state before:
α : Type u_1
β : Type u_2
γ : Type ?u.1282
δ : Type ?u.1285
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
A B : ImageQuotient F
f✝ g✝ : A ⟶ B
f g : A.unquot ⟶ B.unquot
h :
  Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) g) =
    Functor.map (imageQuotientFunctor F) (HomQuotient.quotHom (imageCongruence F) f)
⊢ Congruence.rel (imageCongruence F) A.unquot B.unquot g f
Tactic:
exact h
Proof state after:
no goals
Theorem: Category.whisker_eq
Proof state before:
α : Type u_2
β : Type ?u.23211
γ : Type ?u.23214
δ : Type ?u.23217
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
h : B ⟶ C
f g : A ⟶ B
w : f = g
⊢ h ∘ f = h ∘ g
Tactic:
rw [w]
Proof state after:
no goals
Theorem: Category.eq_whisker
Proof state before:
α : Type u_2
β : Type ?u.23648
γ : Type ?u.23651
δ : Type ?u.23654
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
f g : B ⟶ C
w : f = g
h : A ⟶ B
⊢ f ∘ h = g ∘ h
Tactic:
rw [w]
Proof state after:
no goals
Theorem: Category.Functor.id_comp
Proof state before:
α : Type u_1
β : Type u_2
γ : Type ?u.59997
δ : Type ?u.60000
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
⊢ 𝟭 β ◌ F = F
Tactic:
aesop
Proof state after:
no goals
Theorem: Category.Functor.comp_id
Proof state before:
α : Type u_1
β : Type u_2
γ : Type ?u.60194
δ : Type ?u.60197
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ β
⊢ F ◌ 𝟭 α = F
Tactic:
aesop
Proof state after:
no goals
Theorem: Category.Functor.comp_assoc
Proof state before:
α : Type u_7
β : Type u_5
γ : Type u_1
δ : Type u_2
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
H : γ ⥤ δ
G : β ⥤ γ
F : α ⥤ β
⊢ (H ◌ G) ◌ F = H ◌ G ◌ F
Tactic:
aesop
Proof state after:
no goals
Theorem: Category.HomQuotient.comp_rel
Proof state before:
α : Type u_1
β : Type ?u.68744
γ : Type ?u.68747
δ : Type ?u.68750
A✝ B✝ C✝ D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B C : HomQuotient r
f₁ : B.unquot ⟶ C.unquot
g₁ : A.unquot ⟶ B.unquot
f₂ : B.unquot ⟶ C.unquot
g₂ : A.unquot ⟶ B.unquot
hf : Congruence.rel r B.unquot C.unquot f₁ f₂
hg : Congruence.rel r A.unquot B.unquot g₁ g₂
⊢ Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₁ ∘ g₁) =
    Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₂ ∘ g₂)
Tactic:
have h₁ := r.whisker_rel f₁ g₁ g₂ hg
Proof state after:
α : Type u_1
β : Type ?u.68744
γ : Type ?u.68747
δ : Type ?u.68750
A✝ B✝ C✝ D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B C : HomQuotient r
f₁ : B.unquot ⟶ C.unquot
g₁ : A.unquot ⟶ B.unquot
f₂ : B.unquot ⟶ C.unquot
g₂ : A.unquot ⟶ B.unquot
hf : Congruence.rel r B.unquot C.unquot f₁ f₂
hg : Congruence.rel r A.unquot B.unquot g₁ g₂
h₁ : Congruence.rel r A.unquot C.unquot (f₁ ∘ g₁) (f₁ ∘ g₂)
⊢ Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₁ ∘ g₁) =
    Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₂ ∘ g₂)
Theorem: Category.HomQuotient.comp_rel
Proof state before:
α : Type u_1
β : Type ?u.68744
γ : Type ?u.68747
δ : Type ?u.68750
A✝ B✝ C✝ D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B C : HomQuotient r
f₁ : B.unquot ⟶ C.unquot
g₁ : A.unquot ⟶ B.unquot
f₂ : B.unquot ⟶ C.unquot
g₂ : A.unquot ⟶ B.unquot
hf : Congruence.rel r B.unquot C.unquot f₁ f₂
hg : Congruence.rel r A.unquot B.unquot g₁ g₂
h₁ : Congruence.rel r A.unquot C.unquot (f₁ ∘ g₁) (f₁ ∘ g₂)
⊢ Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₁ ∘ g₁) =
    Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₂ ∘ g₂)
Tactic:
have h₂ := r.rel_whisker f₁ f₂ g₂ hf
Proof state after:
α : Type u_1
β : Type ?u.68744
γ : Type ?u.68747
δ : Type ?u.68750
A✝ B✝ C✝ D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B C : HomQuotient r
f₁ : B.unquot ⟶ C.unquot
g₁ : A.unquot ⟶ B.unquot
f₂ : B.unquot ⟶ C.unquot
g₂ : A.unquot ⟶ B.unquot
hf : Congruence.rel r B.unquot C.unquot f₁ f₂
hg : Congruence.rel r A.unquot B.unquot g₁ g₂
h₁ : Congruence.rel r A.unquot C.unquot (f₁ ∘ g₁) (f₁ ∘ g₂)
h₂ : Congruence.rel r A.unquot C.unquot (f₁ ∘ g₂) (f₂ ∘ g₂)
⊢ Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₁ ∘ g₁) =
    Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₂ ∘ g₂)
Theorem: Category.HomQuotient.comp_rel
Proof state before:
α : Type u_1
β : Type ?u.68744
γ : Type ?u.68747
δ : Type ?u.68750
A✝ B✝ C✝ D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B C : HomQuotient r
f₁ : B.unquot ⟶ C.unquot
g₁ : A.unquot ⟶ B.unquot
f₂ : B.unquot ⟶ C.unquot
g₂ : A.unquot ⟶ B.unquot
hf : Congruence.rel r B.unquot C.unquot f₁ f₂
hg : Congruence.rel r A.unquot B.unquot g₁ g₂
h₁ : Congruence.rel r A.unquot C.unquot (f₁ ∘ g₁) (f₁ ∘ g₂)
h₂ : Congruence.rel r A.unquot C.unquot (f₁ ∘ g₂) (f₂ ∘ g₂)
⊢ Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₁ ∘ g₁) =
    Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₂ ∘ g₂)
Tactic:
exact Quotient.sound ((r.equivalence _ _).trans h₁ h₂)
Proof state after:
no goals
Theorem: Category.HomQuotient.quotHom_eq_iff
Proof state before:
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
⊢ quotHom r f = quotHom r g ↔ Congruence.rel r A B f g
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
⊢ quotHom r f = quotHom r g → Congruence.rel r A B f g

case mpr
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
⊢ Congruence.rel r A B f g → quotHom r f = quotHom r g
Theorem: Category.HomQuotient.quotHom_eq_iff
Proof state before:
case mp
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
⊢ quotHom r f = quotHom r g → Congruence.rel r A B f g
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
h : quotHom r f = quotHom r g
⊢ Congruence.rel r A B f g
Theorem: Category.HomQuotient.quotHom_eq_iff
Proof state before:
case mp
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
h : quotHom r f = quotHom r g
⊢ Congruence.rel r A B f g
Tactic:
exact Quotient.exact h
Proof state after:
no goals
Theorem: Category.HomQuotient.quotHom_eq_iff
Proof state before:
case mpr
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
⊢ Congruence.rel r A B f g → quotHom r f = quotHom r g
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
h : Congruence.rel r A B f g
⊢ quotHom r f = quotHom r g
Theorem: Category.HomQuotient.quotHom_eq_iff
Proof state before:
case mpr
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
h : Congruence.rel r A B f g
⊢ quotHom r f = quotHom r g
Tactic:
exact Quotient.sound h
Proof state after:
no goals
Theorem: Category.NatTrans.id_comp
Proof state before:
α : Type u_1
β : Type u_2
γ : Type ?u.76228
δ : Type ?u.76231
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G : α ⥤ β
η : NatTrans F G
⊢ comp (id G) η = η
Tactic:
ext
Proof state after:
case app.h
α : Type u_1
β : Type u_2
γ : Type ?u.76228
δ : Type ?u.76231
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G : α ⥤ β
η : NatTrans F G
x✝ : α
⊢ app (comp (id G) η) x✝ = app η x✝