awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ :
  Finite.{u_2 + 1}
    (S ⧸
      (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯) : Ideal S))
⊢ ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)
have this : ∀ (Q' : (↑(P.primesOver S) : Type u_2)), ∃ (σ : G), (↑Q' : Ideal S) = σ • Q
Tactic: have (Q' : Ideal.primesOver P S) : ∃ σ : G, Q'.1 = σ • Q :=
    Algebra.IsInvariant.exists_smul_of_under_eq R S G _ _ (hQ₂.over.symm.trans Q'.2.2.over)
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ :
  Finite.{u_2 + 1}
    (S ⧸
      (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯) : Ideal S))
this : ∀ (Q' : (↑(P.primesOver S) : Type u_2)), ∃ (σ : G), (↑Q' : Ideal S) = σ • Q
⊢ ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)
have choose : ∀ (τ : (Q' : (↑(P.primesOver S) : Type u_2)) → G)
  (hτ : ∀ (Q' : (↑(P.primesOver S) : Type u_2)), (↑Q' : Ideal S) = τ Q' • Q),
  ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)
Tactic: choose τ hτ using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
P : Ideal R
Q : Ideal S
hQ₁ : Q.IsPrime
hQ₂ : Q.LiesOver P
hQ₃ :
  Finite.{u_2 + 1}
    (S ⧸
      (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯) : Ideal S))
τ : (Q' : (↑(P.primesOver S) : Type u_2)) → G
hτ : ∀ (Q' : (↑(P.primesOver S) : Type u_2)), (↑Q' : Ideal S) = τ Q' • Q
⊢ ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)
have obtain : ∀ (σ : G) (hσ : IsArithFrobAt R σ Q),
  ∃ (σ : (↑(P.primesOver S) : Type u_2) → G),
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂)
Tactic: obtain ⟨σ, hσ⟩ := exists_of_isInvariant R G Q
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
⊢ IsConj (arithFrobAt R G Q) (arithFrobAt R G Q')
have obtain : ∀ (P : Ideal R) (hP : P.IsPrime) (h₁ : P = Ideal.under R Q) (h₂ : P = Ideal.under R Q'),
  IsConj (arithFrobAt R G Q) (arithFrobAt R G Q')
Tactic: obtain ⟨P, hP, h₁, h₂⟩ : ∃ P : Ideal R, P.IsPrime ∧ P = Q.under R ∧ P = Q'.under R :=
    ⟨Q.under R, inferInstance, rfl, H⟩
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
P : Ideal R
hP : P.IsPrime
h₁ : P = Ideal.under R Q
h₂ : P = Ideal.under R Q'
⊢ IsConj (arithFrobAt R G Q) (arithFrobAt R G Q')
have h : arithFrobAt R G Q =
  Exists.choose (p := fun (σ : (↑(P.primesOver S) : Type u_2) → G) ↦
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
    sorry (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q sorry)
Tactic: convert!
    (exists_primesOver_isConj S G P ⟨⟨Q, ‹_›, ⟨h₁⟩⟩, ‹Finite (S ⧸ Q)›⟩).choose_spec.2 ⟨Q, ‹_›, ⟨h₁⟩⟩
      ⟨Q', ‹_›, ⟨h₂⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
P : Ideal R
hP : P.IsPrime
h₁ : P = Ideal.under R Q
h₂ : P = Ideal.under R Q'
h :
  arithFrobAt R G Q =
    Exists.choose (p := fun (σ : (↑(P.primesOver S) : Type u_2) → G) ↦
      (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
      ⋯ (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯)
⊢ IsConj (arithFrobAt R G Q) (arithFrobAt R G Q')
have h₃ : arithFrobAt R G Q' =
  Exists.choose (p := fun (σ : (↑(P.primesOver S) : Type u_2) → G) ↦
    (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
      ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
    sorry (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q' sorry)
Tactic: convert!
    (exists_primesOver_isConj S G P ⟨⟨Q, ‹_›, ⟨h₁⟩⟩, ‹Finite (S ⧸ Q)›⟩).choose_spec.2 ⟨Q, ‹_›, ⟨h₁⟩⟩
      ⟨Q', ‹_›, ⟨h₂⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
P : Ideal R
hP : P.IsPrime
h₁ : P = Ideal.under R Q
h₂ : P = Ideal.under R Q'
⊢ arithFrobAt R G Q =
    Exists.choose (p := fun (σ : (↑(P.primesOver S) : Type u_2) → G) ↦
      (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
      ⋯ (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯)
have h : ∀ (hP : Ideal.IsPrime (Ideal.under R Q)) (h₂ : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')),
  arithFrobAt R G Q =
    Exists.choose (p := fun (σ : (↑(Ideal.primesOver (Ideal.under R Q) S) : Type u_2) → G) ↦
      (∀ (Q_1 : (↑(Ideal.primesOver (Ideal.under R Q) S) : Type u_2)), IsArithFrobAt R (σ Q_1) (↑Q_1 : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(Ideal.primesOver (Ideal.under R Q) S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
      sorry
      (Subtype.mk (p := fun (x : Ideal S) ↦
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) x) Q sorry)
Tactic: subst h₁
Cleared hypotheses: P, hP, h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.Frobenius (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
G : Type u_3
inst_3 : Group G
inst_4 : MulSemiringAction G S
inst_5 : SMulCommClass G R S
Q : Ideal S
inst_6 : Finite G
inst_7 : Algebra.IsInvariant R S G
inst_8 : Q.IsPrime
inst_9 : Finite.{u_2 + 1} (S ⧸ Q)
Q' : Ideal S
inst_10 : Q'.IsPrime
inst_11 : Finite.{u_2 + 1} (S ⧸ Q')
H : Eq (α := Ideal R) (Ideal.under R Q) (Ideal.under R Q')
P : Ideal R
hP : P.IsPrime
h₁ : P = Ideal.under R Q
h₂ : P = Ideal.under R Q'
⊢ arithFrobAt R G Q' =
    Exists.choose (p := fun (σ : (↑(P.primesOver S) : Type u_2) → G) ↦
      (∀ (Q : (↑(P.primesOver S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(P.primesOver S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
      ⋯ (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q' ⋯)
have h : ∀ (hP : Ideal.IsPrime (Ideal.under R Q')) (h₁ : Eq (α := Ideal R) (Ideal.under R Q') (Ideal.under R Q)),
  arithFrobAt R G Q' =
    Exists.choose (p := fun (σ : (↑(Ideal.primesOver (Ideal.under R Q') S) : Type u_2) → G) ↦
      (∀ (Q : (↑(Ideal.primesOver (Ideal.under R Q') S) : Type u_2)), IsArithFrobAt R (σ Q) (↑Q : Ideal S)) ∧
        ∀ (Q₁ Q₂ : (↑(Ideal.primesOver (Ideal.under R Q') S) : Type u_2)), IsConj (σ Q₁) (σ Q₂))
      sorry
      (Subtype.mk (p := fun (x : Ideal S) ↦
        Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q') S) x) Q' sorry)
Tactic: subst h₂
Cleared hypotheses: P, hP, h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.AlgHom (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
V : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
𝒞 : ι → Submodule R C
𝒟 : ι → Submodule R D
inst_11 : GradedAlgebra 𝒜
inst_12 : GradedAlgebra ℬ
inst_13 : GradedAlgebra 𝒞
inst_14 : GradedAlgebra 𝒟
f g : 𝒜 →ₐᵍ[R] ℬ
h :
  Eq (α := (a : A) → B) ((fun (f : 𝒜 →ₐᵍ[R] ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) f)
    ((fun (f : 𝒜 →ₐᵍ[R] ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)
⊢ f = g
have rcases : ∀ (toFun : A → B) (map_one' : toFun 1 = 1)
  (map_mul' :
    ∀ (x y : A),
      { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun (x * y) =
        { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun x *
          { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun y)
  (map_zero' : (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun 0 = 0)
  (map_add' :
    ∀ (x y : A),
      (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun (x + y) =
        (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun x +
          (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun y)
  (commutes' :
    ∀ (r : R),
      (↑(↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' :
                      A →+* B } :
                  A →* B) :
              OneHom A B).toFun
          ((algebraMap R A : (a : R) → A) r) =
        (algebraMap R B : (a : R) → B) r)
  (map_mem :
    ∀ {i : ι} {x : A},
      x ∈ 𝒜 i →
        Membership.mem (α := B) (ℬ i)
          (({ toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
                    commutes' := commutes' : A →ₐ[R] B }.toRingHom :
                (a : A) → B)
              x :
            B))
  (h :
    Eq (α := (a : A) → B)
      ((fun (f : 𝒜 →ₐᵍ[R] ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
        { toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
          commutes' := commutes', map_mem := @map_mem })
      ((fun (f : 𝒜 →ₐᵍ[R] ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)),
  { toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
      commutes' := commutes', map_mem := @map_mem } =
    g
Tactic: rcases f with ⟨⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩, _⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.AlgHom (goal)
Goal:
R : Type u_1
A : Type u_6
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n : ℕ
⊢ Eq (α := (a : A) → A) (⇑(f ^ Nat.zero) : (a : A) → A) (⇑f : (a : A) → A)^[Nat.zero]
have h : ∀ (x : A), (f ^ Nat.zero : (a : A) → A) x = (⇑f : (a : A) → A)^[Nat.zero] x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.AlgHom (goal)
Goal:
R : Type u_1
A : Type u_6
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
𝒜 : ι → Submodule R A
inst_5 : GradedAlgebra 𝒜
f : 𝒜 →ₐᵍ[R] 𝒜
n x : ℕ
ih : Eq (α := (a : A) → A) (⇑(f ^ x) : (a : A) → A) (⇑f : (a : A) → A)^[x]
⊢ Eq (α := (a : A) → A) (⇑(f ^ x.succ) : (a : A) → A) (⇑f : (a : A) → A)^[x.succ]
have h : ∀ (x_1 : A), (f ^ x.succ : (a : A) → A) x_1 = (⇑f : (a : A) → A)^[x.succ] x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring A
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ Eq (α := A) ((proj 𝒜 i : (a : A) → A) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a : A) : A)
    ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
        (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            ((a : (a : ι) → ↥(𝒜 a)) i) :
          ⨁ (i : ι), ↥(𝒜 i)) :
      A)
have rw : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a) :
            ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        i) :
    A) =
  (Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
    (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
        ((a : (a : ι) → ↥(𝒜 a)) i) :
      ⨁ (i : ι), ↥(𝒜 i))
Tactic: rw [GradedRing.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring A
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
rw :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
      (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
          ((a : (a : ι) → ↥(𝒜 a)) i) :
        ⨁ (i : ι), ↥(𝒜 i))
⊢ Eq (α := A) ((proj 𝒜 i : (a : A) → A) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a : A) : A)
    ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
        (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            ((a : (a : ι) → ↥(𝒜 a)) i) :
          ⨁ (i : ι), ↥(𝒜 i)) :
      A)
have rw₁ : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a) :
            ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        i) :
    A) =
  (↑((a : (a : ι) → ↥(𝒜 a)) i) : A)
Tactic: rw [GradedRing.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring A
inst_3 : SetLike σ A
inst_4 : AddSubmonoidClass σ A
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
rw :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
      (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
          ((a : (a : ι) → ↥(𝒜 a)) i) :
        ⨁ (i : ι), ↥(𝒜 i))
rw₁ :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a) :
              ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          i) :
      A) =
    (↑((a : (a : ι) → ↥(𝒜 a)) i) : A)
⊢ Eq (α := A) ((proj 𝒜 i : (a : A) → A) ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A) a : A) : A)
    ((Equiv.symm (decompose 𝒜) : (a : ⨁ (i : ι), ↥(𝒜 i)) → A)
        (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
            ((a : (a : ι) → ↥(𝒜 a)) i) :
          ⨁ (i : ι), ↥(𝒜 i)) :
      A)
have rw₂ : (↑((a : (a : ι) → ↥(𝒜 a)) i) : A) = (↑((a : (a : ι) → ↥(𝒜 a)) i) : A)
Tactic: rw [GradedRing.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst_4 : AddLeftCancelMonoid ι
inst_5 : GradedRing 𝒜
a b : A
a_mem : a ∈ 𝒜 i
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) : A) =
    a * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
have lift : ∀ (a : ↥(𝒜 i)),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
Tactic: lift a to 𝒜 i using a_mem
Cleared hypotheses: a, a_mem
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst_4 : AddLeftCancelMonoid ι
inst_5 : GradedRing 𝒜
b : A
a : ↥(𝒜 i)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
have rw : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) : ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        (i + j)) :
    A) =
  (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
Tactic: rw [decompose_mul, decompose_coe, coe_of_mul_apply_add]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst_4 : AddLeftCancelMonoid ι
inst_5 : GradedRing 𝒜
b : A
a : ↥(𝒜 i)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (i + j)) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
have rw₁ : (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
            (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) : (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                a :
              ⨁ (i : ι), ↥(𝒜 i))
            ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
          (a : ι) → ↥(𝒜 a))
        (i + j)) :
    A) =
  (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
Tactic: rw [decompose_mul, decompose_coe, coe_of_mul_apply_add]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst_4 : AddLeftCancelMonoid ι
inst_5 : GradedRing 𝒜
b : A
a : ↥(𝒜 i)
rw :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (↑a : A) : ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (i + j)) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
rw₁ :
  (↑((HMul.hMul (α := ⨁ (i : ι), ↥(𝒜 i)) (β := ⨁ (i : ι), ↥(𝒜 i))
              (((of.{u_1, u_3} (fun (i : ι) ↦ ↥(𝒜 i)) i : ↥(𝒜 i) →+ ⨁ (i : ι), ↥(𝒜 i)) :
                    (a : ↥(𝒜 i)) → ⨁ (i : ι), ↥(𝒜 i))
                  a :
                ⨁ (i : ι), ↥(𝒜 i))
              ((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) :
            (a : ι) → ↥(𝒜 a))
          (i + j)) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) ((↑a : A) * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) :
      A) =
    (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
have rw₂ : (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A) =
  (↑a : A) * (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) b : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) j) : A)
Tactic: rw [decompose_mul, decompose_coe, coe_of_mul_apply_add]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.Basic (goal)
Goal:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst : DecidableEq ι
inst_1 : Semiring A
inst_2 : SetLike σ A
inst_3 : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst_4 : AddRightCancelMonoid ι
inst_5 : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 j
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * b) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * b
have lift : ∀ (b : ↥(𝒜 j)),
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) (a * (↑b : A)) : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) (i + j)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ι), ↥(𝒜 i)) a : ⨁ (i : ι), ↥(𝒜 i)) : (a : ι) → ↥(𝒜 a)) i) : A) * (↑b : A)
Tactic: lift b to 𝒜 j using b_mem
Cleared hypotheses: b, b_mem