awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p : R
ψ θ : HasQuotient.Quotient R (B := AddSubgroup R) (AddSubgroup.zmultiples p)
z : ℤ
hz : z ≠ 0
h :
  ∀ (a : R),
    z • ⟦a⟧ = z • θ ↔ ∃ (k : Fin z.natAbs), ⟦a⟧ = θ + (↑((↑k : ℕ) • (p / (↑z : R))) : R ⧸ AddSubgroup.zmultiples p)
⊢ z • ψ = z • θ ↔ ∃ (k : Fin z.natAbs), ψ = θ + (↑((↑k : ℕ) • (p / (↑z : R))) : R ⧸ AddSubgroup.zmultiples p)

Tactic:
induction ψ using Quotient.inductionOn
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p : R
θ : HasQuotient.Quotient R (B := AddSubgroup R) (AddSubgroup.zmultiples p)
z : ℤ
hz : z ≠ 0
a : R
h :
  ∀ (a_1 : R),
    z • ⟦a⟧ = z • ⟦a_1⟧ ↔
      ∃ (k : Fin z.natAbs), ⟦a⟧ = ⟦a_1⟧ + (↑((↑k : ℕ) • (p / (↑z : R))) : R ⧸ AddSubgroup.zmultiples p)
⊢ z • ⟦a⟧ = z • θ ↔ ∃ (k : Fin z.natAbs), ⟦a⟧ = θ + (↑((↑k : ℕ) • (p / (↑z : R))) : R ⧸ AddSubgroup.zmultiples p)

Tactic:
induction θ using Quotient.inductionOn
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a a_1 : R
h :
  Membership.mem (γ := AddSubgroup R) (AddSubgroup.zmultiples p) (z • (a - a_1)) ↔
    ∃ (k : Fin z.natAbs),
      Membership.mem (γ := AddSubgroup R) (AddSubgroup.zmultiples p) (a - a_1 - (↑k : ℕ) • (p / (↑z : R)))
⊢ z • ⟦a⟧ = z • ⟦a_1⟧ ↔
    ∃ (k : Fin z.natAbs), ⟦a⟧ = ⟦a_1⟧ + (↑((↑k : ℕ) • (p / (↑z : R))) : R ⧸ AddSubgroup.zmultiples p)

Tactic:
simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add,
    QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]

Premises used: QuotientAddGroup.eq_iff_sub_mem, QuotientAddGroup.mk_add, sub_sub, smul_sub, QuotientAddGroup.mk_zsmul
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a a_1 : R
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.zmultiples p) (z • (a - a_1)) ↔
    ∃ (k : Fin z.natAbs),
      Membership.mem (γ := AddSubgroup R) (AddSubgroup.zmultiples p) (a - a_1 - (↑k : ℕ) • (p / (↑z : R)))

Tactic:
AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div hz

Premises used: Set.Mem, AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a a_1 : R
⊢ Membership.mem (γ := AddSubgroup R) (AddSubgroup.zmultiples p) (z • (a - a_1)) ↔
    ∃ (k : Fin z.natAbs),
      Membership.mem (γ := AddSubgroup R) (AddSubgroup.zmultiples p) (a - a_1 - (↑k : ℕ) • (p / (↑z : R)))

Tactic:
exact AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div hz

Premises used: AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p : R
ψ θ : HasQuotient.Quotient R (B := AddSubgroup R) (AddSubgroup.zmultiples p)
n : ℕ
hz : n ≠ 0
rw :
  (∃ (k : Fin (Int.natAbs (↑n : ℤ))), ψ = θ + (↑((↑k : ℕ) • (p / (↑n : R))) : R ⧸ AddSubgroup.zmultiples p)) ↔
    ∃ (k : Fin n),
      ψ =
        θ +
          HSMul.hSMul (β := HasQuotient.Quotient R (B := AddSubgroup R) (AddSubgroup.zmultiples p)) (↑k : ℕ)
            (↑(p / (↑n : R)) : R ⧸ AddSubgroup.zmultiples p)
⊢ n • ψ = n • θ ↔
    ∃ (k : Fin n),
      ψ =
        θ +
          HSMul.hSMul (β := HasQuotient.Quotient R (B := AddSubgroup R) (AddSubgroup.zmultiples p)) (↑k : ℕ)
            (↑(p / (↑n : R)) : R ⧸ AddSubgroup.zmultiples p)

Tactic:
rw [← natCast_zsmul ψ, ← natCast_zsmul θ,
    zmultiples_zsmul_eq_zsmul_iff (Int.natCast_ne_zero.mpr hz), Int.cast_natCast]

Premises used: Iff.mpr, Int.cast_natCast, Int.natCast_ne_zero, QuotientAddGroup.zmultiples_zsmul_eq_zsmul_iff, natCast_zsmul
-- Module: Mathlib.Algebra.CharZero.Quotient
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p : R
ψ θ : HasQuotient.Quotient R (B := AddSubgroup R) (AddSubgroup.zmultiples p)
n : ℕ
hz : n ≠ 0
⊢ (∃ (k : Fin (Int.natAbs (↑n : ℤ))), ψ = θ + (↑((↑k : ℕ) • (p / (↑n : R))) : R ⧸ AddSubgroup.zmultiples p)) ↔
    ∃ (k : Fin n),
      ψ =
        θ +
          HSMul.hSMul (β := HasQuotient.Quotient R (B := AddSubgroup R) (AddSubgroup.zmultiples p)) (↑k : ℕ)
            (↑(p / (↑n : R)) : R ⧸ AddSubgroup.zmultiples p)

Tactic:
rfl
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : Nonempty ι
inst_5 : (i : ι) → One (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), OneHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
⊢ Eq (α := DirectLimit G (T := T) f) 1 ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 1⟧

Tactic:
map₀_def _ _ (fun _ _ _ ↦ map_one _) _

Premises used: map_one, DirectLimit.map₀_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : Nonempty ι
inst_5 : (i : ι) → One (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), OneHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
x : (i : ι) × G i
rw :
  (setoid f : (i : ι) × G i → (i : ι) × G i → Prop) x
      (Sigma.mk (β := fun (i : ι) ↦ G i) (x.fst (β := fun (i : ι) ↦ G i)) 1) ↔
    ∃ (i : ι) (h : x.fst (β := fun (i : ι) ↦ G i) ≤ i),
      Eq (α := G i)
        ((f (x.fst (β := fun (i : ι) ↦ G i)) i h : (a : G x.fst) → G i) (x.snd (β := fun (i : ι) ↦ G i)) : G i)
        (1 : G i)
⊢ Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f)) ⟦x⟧ 1 ↔
    ∃ (i : ι) (h : x.fst (β := fun (i : ι) ↦ G i) ≤ i),
      Eq (α := G i)
        ((f (x.fst (β := fun (i : ι) ↦ G i)) i h : (a : G x.fst) → G i) (x.snd (β := fun (i : ι) ↦ G i)) : G i)
        (1 : G i)

Tactic:
rw [one_def x.1, Quotient.eq]

Premises used: Sigma.fst, DirectLimit.one_def, Quotient.eq
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : Nonempty ι
inst_5 : (i : ι) → One (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), OneHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
x : (i : ι) × G i
⊢ (setoid f : (i : ι) × G i → (i : ι) × G i → Prop) x
      (Sigma.mk (β := fun (i : ι) ↦ G i) (x.fst (β := fun (i : ι) ↦ G i)) 1) ↔
    ∃ (i : ι) (h : x.fst (β := fun (i : ι) ↦ G i) ≤ i),
      Eq (α := G i)
        ((f (x.fst (β := fun (i : ι) ↦ G i)) i h : (a : G x.fst) → G i) (x.snd (β := fun (i : ι) ↦ G i)) : G i)
        (1 : G i)

Tactic:
⟨fun ⟨i, h, _, eq⟩ ↦ ⟨i, h, eq.trans (map_one _)⟩,
    fun ⟨i, h, eq⟩ ↦ ⟨i, h, h, eq.trans (map_one _).symm⟩⟩

Premises used: Exists, Sigma.fst, _private.0.DirectLimit.exists_eq_one.match_1, map_one, Iff.intro, Exists.intro, _private.0.DirectLimit.exists_eq_one.match_2, Sigma.mk, OfNat.ofNat, Eq.symm, Sigma.snd, Eq, DFunLike.coe, Setoid.r, Eq.trans
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : Nonempty ι
inst_5 : (i : ι) → One (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), OneHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
x : (i : ι) × G i
⊢ (setoid f : (i : ι) × G i → (i : ι) × G i → Prop) x
      (Sigma.mk (β := fun (i : ι) ↦ G i) (x.fst (β := fun (i : ι) ↦ G i)) 1) ↔
    ∃ (i : ι) (h : x.fst (β := fun (i : ι) ↦ G i) ≤ i),
      Eq (α := G i)
        ((f (x.fst (β := fun (i : ι) ↦ G i)) i h : (a : G x.fst) → G i) (x.snd (β := fun (i : ι) ↦ G i)) : G i)
        (1 : G i)

Tactic:
exact ⟨fun ⟨i, h, _, eq⟩ ↦ ⟨i, h, eq.trans (map_one _)⟩,
    fun ⟨i, h, eq⟩ ↦ ⟨i, h, h, eq.trans (map_one _).symm⟩⟩
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → One (G i)
inst_7 : One C
inst_8 : ∀ (i : ι), OneHomClass.{u_4, u_3, u_5} (H i) (G i) C
inst_9 : ∀ (i j : ι) (h : i ≤ j), OneHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
g : (i : ι) → H i
h :
  ∀ (i j : ι) (h : i ≤ j) (x : G i),
    Eq.{u_5 + 1} (α := C) ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) i x)
      ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) j ((f i j h : (a : G i) → G j) x))
let : ∀ (i : ι), DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h 1 = 1
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h 1 = 1

Tactic:
let ⟨i⟩ := ‹Nonempty ι›
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
inst_6 : (i : ι) → One (G i)
inst_7 : One C
inst_8 : ∀ (i : ι), OneHomClass.{u_4, u_3, u_5} (H i) (G i) C
inst_9 : ∀ (i j : ι) (h : i ≤ j), OneHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
g : (i : ι) → H i
h :
  ∀ (i j : ι) (h : i ≤ j) (x : G i),
    Eq.{u_5 + 1} (α := C) ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) i x)
      ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) j ((f i j h : (a : G i) → G j) x))
i : ι
rw :
  DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i 1⟧ =
    1
rw₁ : ι
rw₂ :
  Eq.{u_5 + 1} (α := C)
    ((g (Sigma.fst (β := fun (i : ι) ↦ G i) (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) : (a : G ⟨i, 1⟩.fst) → C)
        (Sigma.snd (β := fun (i : ι) ↦ G i) (Sigma.mk (β := fun (i : ι) ↦ G i) i 1)) :
      C)
    (1 : C)
rw₃ : ι
rw₄ rw₅ : Eq.{u_5 + 1} (α := C) 1 1
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h 1 = 1

Tactic:
rw [one_def, lift_def, map_one (g i)]

Premises used: DirectLimit.lift_def, DirectLimit.one_def, map_one
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : Nonempty ι
inst_5 : (i : ι) → One (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), OneHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
rw :
  Eq (α := DirectLimit G (T := T) f)
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (1 (Classical.arbitrary ι))⟧ 1
rw₁ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) 1⟧ 1
rw₂ :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) 1⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) 1⟧
rw₃ : ι
rw₄ :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) 1⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) 1⟧
rw₅ : ι
⊢ Eq (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f 1) 1

Tactic:
rw [map₀, Pi.one_apply, one_def]

Premises used: Pi.one_apply, DirectLimit.map₀, DirectLimit.one_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : (i : ι) → Star (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x : G i
⊢ Eq (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f)) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x)⟧

Tactic:
rfl
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → Star (G i)
inst_6 : Star C
inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : ∀ (i : ι), StarHomClass.{u_4, u_3, u_5} (H i) (G i) C
g : (i : ι) → H i
h :
  ∀ (i j : ι) (h : i ≤ j) (x : G i),
    Eq.{u_5 + 1} (α := C) ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) i x)
      ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) j ((f i j h : (a : G i) → G j) x))
x_1 : DirectLimit G (T := T) f
i : ι
x : G i
simp_rw :
  DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x)⟧ =
    star
      (DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)
simp_rw₁ : Eq.{u_5 + 1} (α := C) ((g i : (a : G i) → C) (star x) : C) (star ((g i : (a : G i) → C) x) : C)
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧) =
    star
      (DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧)

Tactic:
simp_rw [star_def, lift_def, map_star (g i)]

Premises used: DirectLimit.lift_def, DirectLimit.star_def, StarHomClass.map_star
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → InvolutiveStar (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
ih :
  ∀ (i : ι) (x : G i),
    Eq (α := DirectLimit G (T := T) f) (star (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧))
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
⊢ Function.Involutive (α := DirectLimit G (T := T) f) star

Tactic:
apply DirectLimit.induction
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → InvolutiveStar (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), StarHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x : G i
ih :
  Eq (α := DirectLimit G (T := T) f) (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star x)⟧)
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
ih₁ :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (star (star x))⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
ih₂ ih₃ :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
⊢ Eq (α := DirectLimit G (T := T) f) (star (star ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧))
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧

Tactic:
rw [star_def, star_def, star_star]

Premises used: star_star, DirectLimit.star_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : (i : ι) → Mul (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x y : G i
⊢ HMul.hMul (α := Quotient (α := (i : ι) × G i) (setoid (F := G) (T := T) f)) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧ =
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)⟧

Tactic:
map₂_def ..

Premises used: DirectLimit.map₂_def
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → Mul (G i)
inst_6 : Mul C
inst_7 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_8 : ∀ (i : ι), MulHomClass.{u_4, u_3, u_5} (H i) (G i) C
g : (i : ι) → H i
h :
  ∀ (i j : ι) (h : i ≤ j) (x : G i),
    Eq.{u_5 + 1} (α := C) ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) i x)
      ((fun (x : ι) ↦ ((⇑(g x) : (a : G x) → C) : (a : G x) → C)) j ((f i j h : (a : G i) → G j) x))
x_1 y_1 : DirectLimit G (T := T) f
i : ι
x y : G i
simp_rw :
  DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * y)⟧ =
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧
simp_rw₁ :
  (g i : (a : G i) → C) (x * y) =
    HMul.hMul (α := C) (β := C) ((g i : (a : G i) → C) x : C) ((g i : (a : G i) → C) y : C)
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
      (HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧) =
    DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i y⟧

Tactic:
simp_rw [mul_def, lift_def, map_mul (g i)]

Premises used: DirectLimit.lift_def, DirectLimit.mul_def, map_mul
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_3 : IsDirectedOrder ι
inst_4 : (i : ι) → Mul (G i)
inst_5 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
inst_6 : Nonempty ι
r s : (i : ι) → G i
simp_rw :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) ((r * s) (Classical.arbitrary ι))⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (r (Classical.arbitrary ι))⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (s (Classical.arbitrary ι))⟧
simp_rw₁ :
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι)
        (HMul.hMul (α := G (Classical.arbitrary ι)) (r (Classical.arbitrary ι)) (s (Classical.arbitrary ι)))⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f)
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (r (Classical.arbitrary ι))⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (s (Classical.arbitrary ι))⟧
⊢ map₀ (F := G) (T := T) f (r * s) =
    HMul.hMul (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f r) (map₀ (F := G) (T := T) f s)

Tactic:
simp_rw [map₀, Pi.mul_apply, mul_def]

Premises used: Pi.mul_apply, DirectLimit.mul_def, DirectLimit.map₀
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_2 : ι) → (h : x ≤ x_2) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → CommMagma (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x x_1 : G i
simp_rw :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x_1 * x)⟧
⊢ HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧ =
    HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧

Tactic:
simp_rw [mul_def, mul_comm]

Premises used: DirectLimit.mul_def, mul_comm
-- Module: Mathlib.Algebra.Colimit.DirectLimit
Goal:
R : Type u_1
ι : Type u_2
inst : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_3 : ι) → (h : x ≤ x_3) → T h
inst_1 : (i j : ι) → (h : i ≤ j) → FunLike.{u_6 + 1, u_3 + 1, u_3 + 1} (T h) (G i) (G j)
inst_2 : (i : ι) → FunLike.{u_4 + 1, u_3 + 1, u_5 + 1} (H i) (G i) C
inst_3 : DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f x1 x2 x3) : (a : G x1) → G x2)
inst_4 : IsDirectedOrder ι
inst_5 : (i : ι) → Semigroup (G i)
inst_6 : ∀ (i j : ι) (h : i ≤ j), MulHomClass.{u_6, u_3, u_3} (T h) (G i) (G j)
i : ι
x x_1 x_2 : G i
simp_rw :
  Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * x_1 * x_2)⟧
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i (x * (x_1 * x_2))⟧
⊢ HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧ *
      ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧ =
    ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x⟧ *
      HMul.hMul (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_1⟧
        ⟦Sigma.mk (β := fun (i : ι) ↦ G i) i x_2⟧

Tactic:
simp_rw [mul_def, mul_assoc]

Premises used: mul_assoc, DirectLimit.mul_def