awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : CharZero R
n : ℕ
rw : Eq.{u_1 + 1} (α := R) (↑n : R) (↑1 : R) ↔ n = 1
⊢ Eq.{u_1 + 1} (α := R) (↑n : R) 1 ↔ n = 1
have rw₁ : n = 1 ↔ n = 1
Tactic: rw [← cast_one, cast_inj]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddMonoidWithOne M
inst_1 : CharZero M
⊢ Ne.{u_2 + 1} (α := M) 1 0
have rw : Ne (α := ℕ) 1 0
Tactic: rw [← Nat.cast_one, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ (k : ℤ), k • p = z • r) ↔
    ∃ (k : Fin z.natAbs), Membership.mem (γ := AddSubgroup R) (zmultiples p) (r - (↑k : ℕ) • (p / (↑z : R)))
have simp_rw : (∃ (k : ℤ), k • p = z • r) ↔ ∃ (k : Fin z.natAbs) (k_1 : ℤ), k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹ = r
Tactic: simp_rw [AddSubgroup.mem_zmultiples_iff, div_eq_mul_inv, ← smul_mul_assoc, eq_sub_iff_add_eq]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (hypothesis)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ (k : ℤ), k • p = z • r) ↔ ∃ (k : Fin z.natAbs) (k_1 : ℤ), k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹ = r
have hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
Tactic: have hz' : (z : R) ≠ 0 := Int.cast_ne_zero.mpr hz
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
| ∃ (k : Fin z.natAbs) (k_1 : ℤ), k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹ = r
have simp : ∃ (k : Fin z.natAbs) (k_1 : ℤ), (↑z : R) * (k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹) = (↑z : R) * r
Tactic: simp +singlePass only [← (mul_right_injective₀ hz').eq_iff]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
⊢ (∃ (k : ℤ), k • p = z • r) ↔ ∃ (k : Fin z.natAbs) (k_1 : ℤ), k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹ = r
have conv_rhs : (∃ (k : ℤ), k • p = z • r) ↔
  ∃ (k : Fin z.natAbs) (k_1 : ℤ), (↑z : R) * (k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹) = (↑z : R) * r
Tactic: conv_rhs => simp +singlePass only [← (mul_right_injective₀ hz').eq_iff]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
⊢ (∃ (k : ℤ), k • p = z • r) ↔
    ∃ (k : Fin z.natAbs) (k_1 : ℤ), (↑z : R) * (k_1 • p + (↑k : ℕ) • p * (↑z : R)⁻¹) = (↑z : R) * r
have simp_rw : (∃ (k : ℤ), k • p = z • r) ↔ ∃ (k : Fin z.natAbs) (k_1 : ℤ), (z * k_1 + (↑(↑k : ℕ) : ℤ)) • p = z • r
Tactic: simp_rw [← zsmul_eq_mul, smul_add, ← mul_smul_comm, zsmul_eq_mul (z : R)⁻¹, mul_inv_cancel₀ hz',
    mul_one, ← natCast_zsmul, smul_smul, ← add_smul]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
⊢ (∃ (k : ℤ), k • p = z • r) ↔ ∃ (k : Fin z.natAbs) (k_1 : ℤ), (z * k_1 + (↑(↑k : ℕ) : ℤ)) • p = z • r
have mp : (∃ (k : ℤ), k • p = z • r) → ∃ (k : Fin z.natAbs) (k_1 : ℤ), (z * k_1 + (↑(↑k : ℕ) : ℤ)) • p = z • r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
mp : (∃ (k : ℤ), k • p = z • r) → ∃ (k : Fin z.natAbs) (k_1 : ℤ), (z * k_1 + (↑(↑k : ℕ) : ℤ)) • p = z • r
⊢ (∃ (k : ℤ), k • p = z • r) ↔ ∃ (k : Fin z.natAbs) (k_1 : ℤ), (z * k_1 + (↑(↑k : ℕ) : ℤ)) • p = z • r
have mpr : (∃ (k : Fin z.natAbs) (k_1 : ℤ), (z * k_1 + (↑(↑k : ℕ) : ℤ)) • p = z • r) → ∃ (k : ℤ), k • p = z • r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
⊢ ∃ (k : Fin z.natAbs) (k_1 : ℤ), (z * k_1 + (↑(↑k : ℕ) : ℤ)) • p = z • r
have mp : ∃ (k_1 : Fin z.natAbs) (k_2 : ℤ), (z * k_2 + (↑(↑k_1 : ℕ) : ℤ)) • p = k • p
Tactic: simp_rw [← h]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
⊢ ∃ (k_1 : Fin z.natAbs) (k_2 : ℤ), (z * k_2 + (↑(↑k_1 : ℕ) : ℤ)) • p = k • p
have mp : (k % z).toNat < z.natAbs
Tactic: refine ⟨⟨(k % z).toNat, ?_⟩, k / z, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
mp : (k % z).toNat < z.natAbs
⊢ ∃ (k_1 : Fin z.natAbs) (k_2 : ℤ), (z * k_2 + (↑(↑k_1 : ℕ) : ℤ)) • p = k • p
have mp₁ : (z * (k / z) + (↑(↑(⟨(k % z).toNat, sorry⟩ : Fin z.natAbs) : ℕ) : ℤ)) • p = k • p
Tactic: refine ⟨⟨(k % z).toNat, ?_⟩, k / z, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
⊢ (k % z).toNat < z.natAbs
have mp : k % z < (↑z.natAbs : ℤ)
Tactic: rw [← Int.ofNat_lt, Int.toNat_of_nonneg (Int.emod_nonneg _ hz)]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + (↑(↑(⟨(k % z).toNat, ⋯⟩ : Fin z.natAbs) : ℕ) : ℤ)) • p = k • p
have mp : (z * (k / z) + k % z) • p = k • p
Tactic: rw [Fin.val_mk, Int.toNat_of_nonneg (Int.emod_nonneg _ hz)]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : Ne.{u_1 + 1} (α := R) (↑z : R) 0
k : ℤ
h : k • p = z • r
⊢ (z * (k / z) + k % z) • p = k • p
have mp : (z * (k / z) + k % z) • p = (z * (k / z) + k % z) • p
Tactic: nth_rewrite 3 [← Int.mul_ediv_add_emod k z]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ Membership.mem (γ := AddSubgroup R) (zmultiples p) (n • r) ↔
    ∃ (k : Fin n), Membership.mem (γ := AddSubgroup R) (zmultiples p) (r - (↑k : ℕ) • (p / (↑n : R)))
have rw : (∃ (k : Fin (Int.natAbs (↑n : ℤ))),
    Membership.mem (γ := AddSubgroup R) (zmultiples p) (r - (↑k : ℕ) • (p / (↑n : R)))) ↔
  ∃ (k : Fin n), Membership.mem (γ := AddSubgroup R) (zmultiples p) (r - (↑k : ℕ) • (p / (↑n : R)))
Tactic: rw [← natCast_zsmul r, zsmul_mem_zmultiples_iff_exists_sub_div (Int.natCast_ne_zero.mpr hn),
    Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
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
⊢ z • ψ = z • θ ↔ ∃ (k : Fin z.natAbs), ψ = θ + (↑((↑k : ℕ) • (p / (↑z : R))) : R ⧸ AddSubgroup.zmultiples p)
have h : ∀ (a : R),
  z • ⟦a⟧ = z • θ ↔ ∃ (k : Fin z.natAbs), ⟦a⟧ = θ + (↑((↑k : ℕ) • (p / (↑z : R))) : R ⧸ AddSubgroup.zmultiples p)
Tactic: induction ψ using Quotient.inductionOn
Cleared hypotheses: ψ
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
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
⊢ z • ⟦a⟧ = z • θ ↔ ∃ (k : Fin z.natAbs), ⟦a⟧ = θ + (↑((↑k : ℕ) • (p / (↑z : R))) : R ⧸ AddSubgroup.zmultiples p)
have h : ∀ (a_1 : R),
  z • ⟦a⟧ = z • ⟦a_1⟧ ↔
    ∃ (k : Fin z.natAbs), ⟦a⟧ = ⟦a_1⟧ + (↑((↑k : ℕ) • (p / (↑z : R))) : R ⧸ AddSubgroup.zmultiples p)
Tactic: induction θ using Quotient.inductionOn
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a a_1 : R
⊢ z • ⟦a⟧ = z • ⟦a_1⟧ ↔
    ∃ (k : Fin z.natAbs), ⟦a⟧ = ⟦a_1⟧ + (↑((↑k : ℕ) • (p / (↑z : R))) : R ⧸ AddSubgroup.zmultiples p)
have 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)))
Tactic: simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add,
    QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.CharZero.Quotient (goal)
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
⊢ n • ψ = n • θ ↔
    ∃ (k : Fin n),
      ψ =
        θ +
          HSMul.hSMul (β := HasQuotient.Quotient R (B := AddSubgroup R) (AddSubgroup.zmultiples p)) (↑k : ℕ)
            (↑(p / (↑n : R)) : R ⧸ AddSubgroup.zmultiples p)
have 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)
Tactic: rw [← natCast_zsmul ψ, ← natCast_zsmul θ,
    zmultiples_zsmul_eq_zsmul_iff (Int.natCast_ne_zero.mpr hz), Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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
⊢ 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)
have 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)
Tactic: rw [one_def x.1, Quotient.eq]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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))
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h 1 = 1
have let : ∀ (i : ι), DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h 1 = 1
Tactic: let ⟨i⟩ := ‹Nonempty ι›
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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 : ι
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h 1 = 1
have 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
Tactic: rw [one_def, lift_def, map_one (g i)]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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₁ : ι
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h 1 = 1
have 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)
Tactic: rw [one_def, lift_def, map_one (g i)]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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₃ : ι
⊢ DirectLimit.lift (F := G) (T := T) f (fun (x : ι) ↦ (⇑(g x) : (a : G x) → C)) h 1 = 1
have rw₄ : Eq.{u_5 + 1} (α := C) 1 1
Tactic: rw [one_def, lift_def, map_one (g i)]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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)
⊢ Eq (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f 1) 1
have rw : Eq (α := DirectLimit G (T := T) f)
  ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) (1 (Classical.arbitrary ι))⟧ 1
Tactic: rw [map₀, Pi.one_apply, one_def]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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
⊢ Eq (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f 1) 1
have rw₁ : Eq (α := DirectLimit G (T := T) f) ⟦Sigma.mk (β := fun (i : ι) ↦ G i) (Classical.arbitrary ι) 1⟧ 1
Tactic: rw [map₀, Pi.one_apply, one_def]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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
⊢ Eq (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f 1) 1
have 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⟧
Tactic: rw [map₀, Pi.one_apply, one_def]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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⟧
⊢ Eq (α := DirectLimit G (T := T) f) (map₀ (F := G) (T := T) f 1) 1
have rw₃ : ι
Tactic: rw [map₀, Pi.one_apply, one_def]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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
⊢ 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⟧)
have 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⟧)
Tactic: simp_rw [star_def, lift_def, map_star (g i)]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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⟧)
⊢ 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⟧)
have 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)
Tactic: simp_rw [star_def, lift_def, map_star (g i)]
-- Lean 4 proof step from Mathlib.Algebra.Colimit.DirectLimit (goal)
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)
⊢ Function.Involutive (α := DirectLimit G (T := T) f) star
have 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⟧
Tactic: apply DirectLimit.induction