awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
Goal:
Γ : Type u_5
Γ' : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
R : Type u_7
inst_2 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_3 : AddCommGroup U
inst_4 : Module R U
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : AddCommGroup W
inst_8 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
x : Γ'
x_1 : Γ
⊢ (HSMul.hSMul (β := HahnModule Γ R W) r
          ((A : (a : V) → HahnModule Γ R W)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))
              x))).coeff
      x_1 =
    HSMul.hSMul (β := W) r
      (HahnSeries.coeff
        ((A : (a : V) → HahnModule Γ R W)
          (HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u)) x))
        x_1)
have coeff : (HSMul.hSMul (β := HahnModule Γ R W) r
        ((A : (a : V) → HahnModule Γ R W)
          (HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))
            x))).coeff
    x_1 =
  (HSMul.hSMul (β := HahnSeries Γ W) r
        ((A : (a : V) → HahnModule Γ R W)
          (HahnSeries.coeff
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → HahnSeries Γ' V) ((B : (a : U) → HahnModule Γ' R V) u))
            x))).coeff
    x_1
Tactic: rw [← HahnSeries.coeff_smul]
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
Goal:
Γ_1 : Type u_1
inst : PartialOrder Γ_1
R_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
inst_1 : CommRing R_1
inst_2 : AddCommGroup V_1
inst_3 : Module R_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module R_1 W_1
Γ : Type u_5
Γ' : Type u_6
inst_6 : PartialOrder Γ
inst_7 : PartialOrder Γ'
R : Type u_7
inst_8 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_9 : AddCommGroup U
inst_10 : Module R U
inst_11 : AddCommGroup V
inst_12 : Module R V
inst_13 : AddCommGroup W
inst_14 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
⊢ (of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B (u + v)).ofIterate =
    HAdd.hAdd (α := HahnModule (Lex (Γ' × Γ)) R W) (β := HahnModule (Lex (Γ' × Γ)) R W)
      ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B u).ofIterate :
        HahnModule (Lex (Γ' × Γ)) R W)
      ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B v).ofIterate :
        HahnModule (Lex (Γ' × Γ)) R W)
have h : ∀ (g : Lex (Γ' × Γ)),
  Eq.{u_10 + 1} (α := W)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule (Lex (Γ' × Γ)) R W) → HahnSeries (Lex (Γ' × Γ)) W)
        ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W)
          (A.compHahnSeries B (u + v)).ofIterate))
      g)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule (Lex (Γ' × Γ)) R W) → HahnSeries (Lex (Γ' × Γ)) W)
        (HAdd.hAdd (α := HahnModule (Lex (Γ' × Γ)) R W) (β := HahnModule (Lex (Γ' × Γ)) R W)
          ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B u).ofIterate :
            HahnModule (Lex (Γ' × Γ)) R W)
          ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B v).ofIterate :
            HahnModule (Lex (Γ' × Γ)) R W)))
      g)
Tactic: ext g
-- Lean 4 proof step from Mathlib.Algebra.Vertex.HVertexOperator (goal)
Goal:
Γ_1 : Type u_1
inst : PartialOrder Γ_1
R_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
inst_1 : CommRing R_1
inst_2 : AddCommGroup V_1
inst_3 : Module R_1 V_1
inst_4 : AddCommGroup W_1
inst_5 : Module R_1 W_1
Γ : Type u_5
Γ' : Type u_6
inst_6 : PartialOrder Γ
inst_7 : PartialOrder Γ'
R : Type u_7
inst_8 : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst_9 : AddCommGroup U
inst_10 : Module R U
inst_11 : AddCommGroup V
inst_12 : Module R V
inst_13 : AddCommGroup W
inst_14 : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
x : U
⊢ (of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B (r • x)).ofIterate =
    HSMul.hSMul (α := R) (β := HahnModule (Lex (Γ' × Γ)) R W) ((RingHom.id R : (a : R) → R) r : R)
      ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B x).ofIterate :
        HahnModule (Lex (Γ' × Γ)) R W)
have h : ∀ (g : Lex (Γ' × Γ)),
  Eq.{u_10 + 1} (α := W)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule (Lex (Γ' × Γ)) R W) → HahnSeries (Lex (Γ' × Γ)) W)
        ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W)
          (A.compHahnSeries B (r • x)).ofIterate))
      g)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule (Lex (Γ' × Γ)) R W) → HahnSeries (Lex (Γ' × Γ)) W)
        (HSMul.hSMul (α := R) (β := HahnModule (Lex (Γ' × Γ)) R W) ((RingHom.id R : (a : R) → R) r : R)
          ((of R : (a : HahnSeries (Lex (Γ' × Γ)) W) → HahnModule (Lex (Γ' × Γ)) R W) (A.compHahnSeries B x).ofIterate :
            HahnModule (Lex (Γ' × Γ)) R W)))
      g)
Tactic: ext g
-- Lean 4 proof step from Mathlib.Algebra.Vertex.VertexOperator (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
x x_1 : VertexOperator R V
⊢ (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (x + x_1) (-n - 1)) =
    HAdd.hAdd (α := ℤ → Module.End R V)
      (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x (-n - 1)) fun (n : ℤ) ↦
      (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x_1 (-n - 1)
have h : ∀ (x_2 : ℤ) (x_3 : V),
  Eq (α := V)
    ((((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (x + x_1) (-x_2 - 1) : V →ₗ[R] V) : (a : V) → V) x_3 : V)
    ((HAdd.hAdd (α := ℤ → Module.End R V) (β := ℤ → Module.End R V)
            (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x (-n - 1))
            (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x_1 (-n - 1)) x_2 :
          (a : V) → V)
        x_3 :
      V)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Vertex.VertexOperator (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
x : R
x_1 : VertexOperator R V
⊢ (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (x • x_1) (-n - 1)) =
    HSMul.hSMul (α := R) (β := ℤ → Module.End R V) ((RingHom.id R : (a : R) → R) x : R) fun (n : ℤ) ↦
      (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x_1 (-n - 1)
have h : ∀ (x_2 : ℤ) (x_3 : V),
  Eq (α := V)
    ((((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (x • x_1) (-x_2 - 1) : V →ₗ[R] V) : (a : V) → V) x_3 : V)
    ((HSMul.hSMul (α := R) (β := ℤ → Module.End R V) ((RingHom.id R : (a : R) → R) x : R)
            (fun (n : ℤ) ↦ (coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) x_1 (-n - 1)) x_2 :
          (a : V) → V)
        x_3 :
      V)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Vertex.VertexOperator (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
⊢ Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) A (-n - 1) : Module.End R V)
have rw : Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
  ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (-(-n - 1) - 1) : V →ₗ[R] V)
Tactic: rw [ncoeff_apply, neg_sub, Int.sub_neg, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Vertex.VertexOperator (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
rw :
  Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (-(-n - 1) - 1) : V →ₗ[R] V)
⊢ Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) A (-n - 1) : Module.End R V)
have rw₁ : Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
  ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (1 - -n - 1) : V →ₗ[R] V)
Tactic: rw [ncoeff_apply, neg_sub, Int.sub_neg, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Vertex.VertexOperator (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
rw :
  Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (-(-n - 1) - 1) : V →ₗ[R] V)
rw₁ :
  Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (1 - -n - 1) : V →ₗ[R] V)
⊢ Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) A (-n - 1) : Module.End R V)
have rw₂ : Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
  ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (1 + n - 1) : V →ₗ[R] V)
Tactic: rw [ncoeff_apply, neg_sub, Int.sub_neg, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Vertex.VertexOperator (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
rw :
  Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (-(-n - 1) - 1) : V →ₗ[R] V)
rw₁ :
  Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (1 - -n - 1) : V →ₗ[R] V)
rw₂ :
  Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A (1 + n - 1) : V →ₗ[R] V)
⊢ Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
    ((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) A (-n - 1) : Module.End R V)
have rw₃ : Eq (α := V →ₗ[R] V) ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
  ((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V)
Tactic: rw [ncoeff_apply, neg_sub, Int.sub_neg, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Vertex.VertexOperator (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
x : V
h :
  -n - 1 <
    HahnSeries.order.{0, u_2} (R := V)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
⊢ Eq (α := V) ((((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) A n : Module.End R V) : (a : V) → V) x : V)
    (0 : V)
have simp : Eq.{u_2 + 1} (α := V)
  (HahnSeries.coeff
    ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
    (-n - 1))
  0
Tactic: simp only [ncoeff, HVertexOperator.coeff, LinearMap.coe_mk, AddHom.coe_mk]
-- Lean 4 proof step from Mathlib.Algebra.Vertex.VertexOperator (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : VertexOperator R V
n : ℤ
x : V
h :
  n <
    HahnSeries.order.{0, u_2} (R := V)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
⊢ Eq (α := V) ((((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) A n : V →ₗ[R] V) : (a : V) → V) x : V) (0 : V)
have rw : -(-n - 1) - 1 <
  HahnSeries.order.{0, u_2} (R := V)
    ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V) ((A : (a : V) → HahnModule ℤ R V) x))
Tactic: rw [coeff_eq_ncoeff, ncoeff_eq_zero_of_lt_order A (-n - 1) x]
-- Lean 4 proof step from Mathlib.Algebra.Vertex.VertexOperator (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (α := ℤ) (Function.support.{0, u_2} (M := V) fun (y : ℤ) ↦ (f y : (a : V) → V) x)
n : ℤ
⊢ (ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) (of_coeff f hf) n = f (-n - 1)
have h : ∀ (v : V),
  Eq (α := V)
    ((((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) (of_coeff f hf) n : Module.End R V) : (a : V) → V) v :
      V)
    ((f (-n - 1) : (a : V) → V) v : V)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Algebra.Vertex.VertexOperator (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (α := ℤ) (Function.support.{0, u_2} (M := V) fun (y : ℤ) ↦ (f y : (a : V) → V) x)
n : ℤ
v : V
⊢ Eq (α := V)
    ((((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) (of_coeff f hf) n : Module.End R V) : (a : V) → V) v :
      V)
    ((f (-n - 1) : (a : V) → V) v : V)
have h : Eq (α := V)
  ((((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (of_coeff f hf) (-n - 1) : V →ₗ[R] V) : (a : V) → V) v : V)
  ((f (-n - 1) : (a : V) → V) v : V)
Tactic: rw [ncoeff_apply, coeff_apply_apply, of_coeff_apply_coeff]
-- Lean 4 proof step from Mathlib.Algebra.Vertex.VertexOperator (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (α := ℤ) (Function.support.{0, u_2} (M := V) fun (y : ℤ) ↦ (f y : (a : V) → V) x)
n : ℤ
v : V
h :
  Eq (α := V)
    ((((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (of_coeff f hf) (-n - 1) : V →ₗ[R] V) : (a : V) → V) v :
      V)
    ((f (-n - 1) : (a : V) → V) v : V)
⊢ Eq (α := V)
    ((((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) (of_coeff f hf) n : Module.End R V) : (a : V) → V) v :
      V)
    ((f (-n - 1) : (a : V) → V) v : V)
have h₁ : Eq (α := V)
  (HahnSeries.coeff
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V)
        ((of_coeff f hf : (a : V) → HahnModule ℤ R V) v))
      (-n - 1) :
    V)
  ((f (-n - 1) : (a : V) → V) v : V)
Tactic: rw [ncoeff_apply, coeff_apply_apply, of_coeff_apply_coeff]
-- Lean 4 proof step from Mathlib.Algebra.Vertex.VertexOperator (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (α := ℤ) (Function.support.{0, u_2} (M := V) fun (y : ℤ) ↦ (f y : (a : V) → V) x)
n : ℤ
v : V
h :
  Eq (α := V)
    ((((coeff : (a : HVertexOperator ℤ R V V) → ℤ → V →ₗ[R] V) (of_coeff f hf) (-n - 1) : V →ₗ[R] V) : (a : V) → V) v :
      V)
    ((f (-n - 1) : (a : V) → V) v : V)
h₁ :
  Eq (α := V)
    (HahnSeries.coeff
        ((Equiv.symm (HahnModule.of R) : (a : HahnModule ℤ R V) → HahnSeries ℤ V)
          ((of_coeff f hf : (a : V) → HahnModule ℤ R V) v))
        (-n - 1) :
      V)
    ((f (-n - 1) : (a : V) → V) v : V)
⊢ Eq (α := V)
    ((((ncoeff : (a : VertexOperator R V) → ℤ → Module.End R V) (of_coeff f hf) n : Module.End R V) : (a : V) → V) v :
      V)
    ((f (-n - 1) : (a : V) → V) v : V)
have h₂ : Eq (α := V) ((f (-n - 1) : (a : V) → V) v : V) ((f (-n - 1) : (a : V) → V) v : V)
Tactic: rw [ncoeff_apply, coeff_apply_apply, of_coeff_apply_coeff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
⊢ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f
have rw : X.isoSpec.hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
Tactic: rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
    asIso_inv, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
rw : X.isoSpec.hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
⊢ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f
have rw₁ : (asIso X.toSpecΓ).hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
Tactic: rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
    asIso_inv, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
rw : X.isoSpec.hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₁ : (asIso X.toSpecΓ).hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
⊢ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f
have rw₂ : X.toSpecΓ ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
Tactic: rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
    asIso_inv, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
rw : X.isoSpec.hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₁ : (asIso X.toSpecΓ).hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₂ : X.toSpecΓ ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
⊢ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f
have rw₃ : f ≫ Y.toSpecΓ ≫ Y.isoSpec.inv = f
Tactic: rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
    asIso_inv, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
rw : X.isoSpec.hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₁ : (asIso X.toSpecΓ).hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₂ : X.toSpecΓ ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₃ : f ≫ Y.toSpecΓ ≫ Y.isoSpec.inv = f
⊢ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f
have rw₄ : f ≫ Y.toSpecΓ ≫ (asIso Y.toSpecΓ).inv = f
Tactic: rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
    asIso_inv, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
rw : X.isoSpec.hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₁ : (asIso X.toSpecΓ).hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₂ : X.toSpecΓ ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₃ : f ≫ Y.toSpecΓ ≫ Y.isoSpec.inv = f
rw₄ : f ≫ Y.toSpecΓ ≫ (asIso Y.toSpecΓ).inv = f
⊢ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f
have rw₅ : f ≫ Y.toSpecΓ ≫ inv Y.toSpecΓ = f
Tactic: rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
    asIso_inv, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
rw : X.isoSpec.hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₁ : (asIso X.toSpecΓ).hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₂ : X.toSpecΓ ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₃ : f ≫ Y.toSpecΓ ≫ Y.isoSpec.inv = f
rw₄ : f ≫ Y.toSpecΓ ≫ (asIso Y.toSpecΓ).inv = f
rw₅ : f ≫ Y.toSpecΓ ≫ inv Y.toSpecΓ = f
⊢ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f
have rw₆ : f ≫ 𝟙 Y = f
Tactic: rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
    asIso_inv, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
f : X ⟶ Y
rw : X.isoSpec.hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₁ : (asIso X.toSpecΓ).hom ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₂ : X.toSpecΓ ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f
rw₃ : f ≫ Y.toSpecΓ ≫ Y.isoSpec.inv = f
rw₄ : f ≫ Y.toSpecΓ ≫ (asIso Y.toSpecΓ).inv = f
rw₅ : f ≫ Y.toSpecΓ ≫ inv Y.toSpecΓ = f
rw₆ : f ≫ 𝟙 Y = f
⊢ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f
have rw₇ : f = f
Tactic: rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
    asIso_inv, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
h : IsAffine Y
⊢ IsAffine X
have rw : ∀ (h : Scheme.Spec.essImage Y), Scheme.Spec.essImage X
Tactic: rw [← essImage_Spec] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine Y
f g : X ⟶ Y
e : Scheme.Hom.appTop f = Scheme.Hom.appTop g
⊢ f = g
have rw : f ≫ Y.toSpecΓ = g ≫ Y.toSpecΓ
Tactic: rw [← cancel_mono Y.toSpecΓ, Scheme.toSpecΓ_naturality, Scheme.toSpecΓ_naturality, e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine Y
f g : X ⟶ Y
e : Scheme.Hom.appTop f = Scheme.Hom.appTop g
rw : f ≫ Y.toSpecΓ = g ≫ Y.toSpecΓ
⊢ f = g
have rw₁ : X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f) = g ≫ Y.toSpecΓ
Tactic: rw [← cancel_mono Y.toSpecΓ, Scheme.toSpecΓ_naturality, Scheme.toSpecΓ_naturality, e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine Y
f g : X ⟶ Y
e : Scheme.Hom.appTop f = Scheme.Hom.appTop g
rw : f ≫ Y.toSpecΓ = g ≫ Y.toSpecΓ
rw₁ : X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f) = g ≫ Y.toSpecΓ
⊢ f = g
have rw₂ : X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f) = X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop g)
Tactic: rw [← cancel_mono Y.toSpecΓ, Scheme.toSpecΓ_naturality, Scheme.toSpecΓ_naturality, e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine Y
f g : X ⟶ Y
e : Scheme.Hom.appTop f = Scheme.Hom.appTop g
rw : f ≫ Y.toSpecΓ = g ≫ Y.toSpecΓ
rw₁ : X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f) = g ≫ Y.toSpecΓ
rw₂ : X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f) = X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop g)
⊢ f = g
have rw₃ : X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop g) = X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop g)
Tactic: rw [← cancel_mono Y.toSpecΓ, Scheme.toSpecΓ_naturality, Scheme.toSpecΓ_naturality, e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Scheme
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
⊢ PreservesLimit D Scheme.Γ.rightOp
have this : ∀ (i : I), IsIso (α.app i)
Tactic: have (i : _) : IsIso (α.app i) := IsAffine.affine
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Scheme
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this : ∀ (i : I), IsIso (α.app i)
⊢ PreservesLimit D Scheme.Γ.rightOp
have this₁ : IsIso α
Tactic: have : IsIso α := NatIso.isIso_of_isIso_app α
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Scheme
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this_1 : ∀ (i : I), IsIso (α.app i)
this : IsIso α
⊢ PreservesLimit D Scheme.Γ.rightOp
have suffices : PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp
Tactic: suffices PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp from
    preservesLimit_of_iso_diagram _ (asIso α).symm