awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
f : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }
⊢ (fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
        (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
            ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
            (F.comp (mkAlgHom S s)) ⋯ :
          { f : A →ₐ[S] B //
            ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }))
      ((fun
            (f' :
              { f : A →ₐ[S] B //
                ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
          preLiftAlgHom S (s := s) ⋯)
        f) =
    f
have a : ∀ (x : A),
  Eq.{u₄ + 1} (α := B)
    (((↑((fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
                  (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                      ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
                      (F.comp (mkAlgHom S s)) sorry :
                    { f : A →ₐ[S] B //
                      ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }))
                ((fun
                      (f' :
                        { f : A →ₐ[S] B //
                          ∀ ⦃x y : A⦄,
                            s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
                    preLiftAlgHom S (s := s) sorry)
                  f)) :
            A →ₐ[S] B) :
          (a : A) → B)
        x :
      B)
    (((↑f : A →ₐ[S] B) : (a : A) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
inst_4 : Semiring T
B : Type u₄
inst_5 : Semiring B
inst_6 : Algebra S B
s : A → A → Prop
F : AlgHom.{uS, uA, u₄} S (RingQuot s) B
⊢ (fun
          (f' :
            { f : A →ₐ[S] B //
              ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
        preLiftAlgHom S (s := s) ⋯)
      ((fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
          (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
              ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
              (F.comp (mkAlgHom S s)) ⋯ :
            { f : A →ₐ[S] B //
              ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }))
        F) =
    F
have w : ∀ (x : A),
  Eq.{u₄ + 1} (α := B)
    ((AlgHom.comp
            ((fun
                  (f' :
                    { f : A →ₐ[S] B //
                      ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
                preLiftAlgHom S (s := s) sorry)
              ((fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
                  (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                      ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
                      (F.comp (mkAlgHom S s)) sorry :
                    { f : A →ₐ[S] B //
                      ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }))
                F))
            (mkAlgHom S s) :
          (a : A) → B)
        x :
      B)
    ((F.comp (mkAlgHom S s) : (a : A) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
x : A
⊢ Eq.{u₄ + 1} (α := B)
    ((((liftAlgHom S (s := s) :
                (a : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → (f : (a : A) → B) x = (f : (a : A) → B) y }) →
                  RingQuot s →ₐ[S] B)
              (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)) f w) :
            AlgHom.{uS, uA, u₄} S (RingQuot s) B) :
          (a : RingQuot s) → B)
        ((mkAlgHom S s : (a : A) → RingQuot s) x : RingQuot s) :
      B)
    ((f : (a : A) → B) x : B)
have simp_rw : Eq.{u₄ + 1} (α := B)
  (((({
                toFun :=
                  fun
                    (f' :
                      { f : A →ₐ[S] B //
                        ∀ ⦃x y : A⦄,
                          s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B) }) ↦
                  {
                    toFun := fun (x : RingQuot s) ↦
                      Quot.lift (r := Rel s) (⇑(↑f' : A →ₐ[S] B) : (a : A) → B) sorry (x.toQuot (r := s)),
                    map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry, commutes' := sorry },
                invFun := fun (F : AlgHom.{uS, uA, u₄} S (RingQuot s) B) ↦
                  Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                    ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B))
                    (F.comp
                      { toFun := fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x), map_one' := sorry, map_mul' := sorry,
                        map_zero' := sorry, map_add' := sorry, commutes' := sorry })
                    sorry,
                left_inv := sorry, right_inv := sorry } :
              (a : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → (f : (a : A) → B) x = (f : (a : A) → B) y }) →
                RingQuot s →ₐ[S] B)
            (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
              ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)) f w) :
          AlgHom.{uS, uA, u₄} S (RingQuot s) B) :
        (a : RingQuot s) → B)
      (({ toFun := fun (x : A) ↦ mk (r := s) (Quot.mk (Rel s) x), map_one' := sorry, map_mul' := sorry, map_zero' := sorry,
              map_add' := sorry, commutes' := sorry } :
            (a : A) → RingQuot s)
          x :
        RingQuot s) :
    B)
  ((f : (a : A) → B) x : B)
Tactic: simp_rw [liftAlgHom_def, preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
S : Type uS
inst : CommSemiring S
A : Type uA
inst_1 : Semiring A
inst_2 : Algebra S A
B : Type u₄
inst_3 : Semiring B
inst_4 : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
g : AlgHom.{uS, uA, u₄} S (RingQuot s) B
h : g.comp (mkAlgHom S s) = f
⊢ g =
    (liftAlgHom S (s := s) :
        (a : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → (f : (a : A) → B) x = (f : (a : A) → B) y }) → RingQuot s →ₐ[S] B)
      (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
        ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)) f w)
have w₁ : ∀ (x : A),
  Eq.{u₄ + 1} (α := B) ((g.comp (mkAlgHom S s) : (a : A) → B) x : B)
    ((AlgHom.comp
            ((liftAlgHom S (s := s) :
                (a : { f : A →ₐ[S] B // ∀ ⦃x y : A⦄, s x y → (f : (a : A) → B) x = (f : (a : A) → B) y }) →
                  RingQuot s →ₐ[S] B)
              (Subtype.mk (p := fun (f : A →ₐ[S] B) ↦
                ∀ ⦃x y : A⦄, s x y → Eq.{u₄ + 1} (α := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)) f w))
            (mkAlgHom S s) :
          (a : A) → B)
        x :
      B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a b : G →₀ k
⊢ { toFinsupp := a + b : SkewMonoidAlgebra k G } = { toFinsupp := a }.add { toFinsupp := b }
have rw : { toFinsupp := a + b : SkewMonoidAlgebra k G } = { toFinsupp := a + b }
Tactic: rw [add]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : SMulZeroClass S k
a : S
b : G →₀ k
⊢ { toFinsupp := a • b : SkewMonoidAlgebra k G } = smul a { toFinsupp := b }
have rw : { toFinsupp := a • b : SkewMonoidAlgebra k G } = { toFinsupp := a • b }
Tactic: rw [smul]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a b : SkewMonoidAlgebra k G
⊢ (a + b).toFinsupp = a.toFinsupp + b.toFinsupp
have rw : { toFinsupp := a.toFinsupp + b.toFinsupp : SkewMonoidAlgebra k G }.toFinsupp = a.toFinsupp + b.toFinsupp
Tactic: rw [← ofFinsupp_add]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : SMulZeroClass S k
a : S
b : SkewMonoidAlgebra k G
⊢ (a • b).toFinsupp = a • b.toFinsupp
have rw : { toFinsupp := a • b.toFinsupp : SkewMonoidAlgebra k G }.toFinsupp = a • b.toFinsupp
Tactic: rw [← ofFinsupp_smul]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p : G →₀ k
⊢ { toFinsupp := p : SkewMonoidAlgebra k G }.support = p.support
have rw : { toFinsupp := p : SkewMonoidAlgebra k G }.toFinsupp.support = p.support
Tactic: rw [support]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p : SkewMonoidAlgebra k G
⊢ p.toFinsupp.support = p.support
have rw : p.toFinsupp.support = p.toFinsupp.support
Tactic: rw [support]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p : SkewMonoidAlgebra k G
⊢ p.support = ∅ ↔ p = 0
have rcases : ∀ (toFinsupp : G →₀ k),
  { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.support = ∅ ↔
    { toFinsupp := toFinsupp : SkewMonoidAlgebra k G } = 0
Tactic: rcases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
f : SkewMonoidAlgebra k G
a : G
⊢ a ∈ f.support ↔ f.coeff a ≠ 0
have rcases : ∀ (toFinsupp : G →₀ k),
  a ∈ { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.support ↔
    { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.coeff a ≠ 0
Tactic: rcases f with ⟨⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p q : SkewMonoidAlgebra k G
⊢ p = q ↔ ∀ (n : G), p.coeff n = q.coeff n
have rcases : ∀ (f : G →₀ k),
  { toFinsupp := f : SkewMonoidAlgebra k G } = q ↔
    ∀ (n : G), { toFinsupp := f : SkewMonoidAlgebra k G }.coeff n = q.coeff n
Tactic: rcases p with ⟨f : G →₀ k⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
q : SkewMonoidAlgebra k G
f : G →₀ k
⊢ { toFinsupp := f : SkewMonoidAlgebra k G } = q ↔
    ∀ (n : G), { toFinsupp := f : SkewMonoidAlgebra k G }.coeff n = q.coeff n
have rcases : ∀ (g : G →₀ k),
  { toFinsupp := f : SkewMonoidAlgebra k G } = { toFinsupp := g } ↔
    ∀ (n : G), { toFinsupp := f : SkewMonoidAlgebra k G }.coeff n = { toFinsupp := g : SkewMonoidAlgebra k G }.coeff n
Tactic: rcases q with ⟨g : G →₀ k⟩
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
p q : SkewMonoidAlgebra k G
a : G
⊢ (p + q).coeff a = p.coeff a + q.coeff a
have rcases : ∀ (toFinsupp : G →₀ k),
  ({ toFinsupp := toFinsupp : SkewMonoidAlgebra k G } + q).coeff a =
    { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.coeff a + q.coeff a
Tactic: rcases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
q : SkewMonoidAlgebra k G
a : G
toFinsupp : G →₀ k
⊢ ({ toFinsupp := toFinsupp : SkewMonoidAlgebra k G } + q).coeff a =
    { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.coeff a + q.coeff a
have rcases : ∀ (toFinsupp_1 : G →₀ k),
  ({ toFinsupp := toFinsupp : SkewMonoidAlgebra k G } + { toFinsupp := toFinsupp_1 : SkewMonoidAlgebra k G }).coeff a =
    { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.coeff a +
      { toFinsupp := toFinsupp_1 : SkewMonoidAlgebra k G }.coeff a
Tactic: rcases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a : G
toFinsupp toFinsupp_1 : G →₀ k
⊢ ({ toFinsupp := toFinsupp : SkewMonoidAlgebra k G } + { toFinsupp := toFinsupp_1 : SkewMonoidAlgebra k G }).coeff a =
    { toFinsupp := toFinsupp : SkewMonoidAlgebra k G }.coeff a +
      { toFinsupp := toFinsupp_1 : SkewMonoidAlgebra k G }.coeff a
have simp_rw : (toFinsupp + toFinsupp_1 : (a : G) → k) a =
  HAdd.hAdd (α := k) (β := k) ((toFinsupp : (a : G) → k) a : k) ((toFinsupp_1 : (a : G) → k) a : k)
Tactic: simp_rw [← ofFinsupp_add, coeff]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
a a' : G
b : k
h : b ≠ 0
⊢ Eq (α := SkewMonoidAlgebra k G) (single a b) (single a' b) ↔ a = a'
have rw : Eq (α := G →₀ k) (toFinsupp (single a b)) (toFinsupp (single a' b)) ↔ a = a'
Tactic: rw [← toFinsupp_inj]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : Monoid S
inst_2 : DistribMulAction S k
a : S
inst_3 : Nonempty G
⊢ IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a
have inhabit : ∀ (inhabited_h : Inhabited G), IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a
Tactic: inhabit G
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : Monoid S
inst_2 : DistribMulAction S k
a : S
inst_3 : Nonempty G
inhabited_h : Inhabited G
⊢ IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a
have refine : ∀ (ha : IsSMulRegular (SkewMonoidAlgebra k G) a) (b₁ b₂ : k)
  (inj : Eq.{u_1 + 1} (α := k) ((fun (x : k) ↦ a • x) b₁) ((fun (x : k) ↦ a • x) b₂)), b₁ = b₂
Tactic: refine ⟨IsSMulRegular.skewMonoidAlgebra, fun ha b₁ b₂ inj ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddMonoid k
S : Type u_3
inst_1 : Monoid S
inst_2 : DistribMulAction S k
a : S
inst_3 : Nonempty G
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj : Eq.{u_1 + 1} (α := k) ((fun (x : k) ↦ a • x) b₁) ((fun (x : k) ↦ a • x) b₂)
⊢ b₁ = b₂
have rw : ∀
  (inj :
    HSMul.hSMul (β := SkewMonoidAlgebra k G) a (single default b₁) =
      HSMul.hSMul (β := SkewMonoidAlgebra k G) a (single default b₂)),
  b₁ = b₂
Tactic: rw [← (single_injective _).eq_iff, ← smul_single, ← smul_single] at inj
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
n : ℕ
⊢ Eq (α := SkewMonoidAlgebra k G) (↑n : SkewMonoidAlgebra k G) (single 1 (↑n : k))
have zero : Eq (α := SkewMonoidAlgebra k G) (↑0 : SkewMonoidAlgebra k G) (single 1 (↑0 : k))
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddMonoidWithOne k
n : ℕ
zero : Eq (α := SkewMonoidAlgebra k G) (↑0 : SkewMonoidAlgebra k G) (single 1 (↑0 : k))
⊢ Eq (α := SkewMonoidAlgebra k G) (↑n : SkewMonoidAlgebra k G) (single 1 (↑n : k))
have succ : ∀ (n : ℕ),
  Eq (α := SkewMonoidAlgebra k G) (↑n : SkewMonoidAlgebra k G) (single 1 (↑n : k)) →
    Eq (α := SkewMonoidAlgebra k G) (↑(n + 1) : SkewMonoidAlgebra k G) (single 1 (↑(n + 1) : k))
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst_1 : AddCommMonoid k'
f : G →₀ k
g : G → k → G' →₀ k'
⊢ { toFinsupp := f.sum g : SkewMonoidAlgebra k' G' } =
    { toFinsupp := f : SkewMonoidAlgebra k G }.sum fun (x1 : G) (x2 : k) ↦ { toFinsupp := g x1 x2 }
have a : { toFinsupp := f.sum g : SkewMonoidAlgebra k' G' }.toFinsupp =
  toFinsupp ({ toFinsupp := f : SkewMonoidAlgebra k G }.sum fun (x1 : G) (x2 : k) ↦ { toFinsupp := g x1 x2 })
Tactic: apply toFinsupp_injective
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
f : SkewMonoidAlgebra k G
⊢ f.sum single = f
have a : toFinsupp (f.sum single) = f.toFinsupp
Tactic: apply toFinsupp_injective
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ f + g = { toFinsupp := f.toFinsupp + g.toFinsupp }
have rw : f + g = { toFinsupp := f.toFinsupp : SkewMonoidAlgebra k G } + { toFinsupp := g.toFinsupp : SkewMonoidAlgebra k G }
Tactic: rw [ofFinsupp_add, eta]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f + g).sum h = f.sum h + g.sum h
have rw : { toFinsupp := f.toFinsupp + g.toFinsupp : SkewMonoidAlgebra k G }.sum h = f.sum h + g.sum h
Tactic: rw [show f + g = ⟨f.toFinsupp + g.toFinsupp⟩ by rw [ofFinsupp_add, eta]]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : DecidableEq G
inst_2 : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ f + g = { toFinsupp := f.toFinsupp + g.toFinsupp }
have rw : f + g = { toFinsupp := f.toFinsupp : SkewMonoidAlgebra k G } + { toFinsupp := g.toFinsupp : SkewMonoidAlgebra k G }
Tactic: rw [ofFinsupp_add, eta]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
S : Type u_3
inst_1 : DecidableEq G
inst_2 : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f + g).sum h = f.sum h + g.sum h
have rw : { toFinsupp := f.toFinsupp + g.toFinsupp : SkewMonoidAlgebra k G }.sum h = f.sum h + g.sum h
Tactic: rw [show f + g = ⟨f.toFinsupp + g.toFinsupp⟩ by rw [ofFinsupp_add, eta]]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.sum g).sum h = f.sum fun (a : α) (b : M) ↦ (g a b).sum h
have rw : Eq.{u_7 + 1} (α := P) (f.toFinsupp.sum fun (a : α) (b : M) ↦ (g a b).toFinsupp.sum h)
  (f.sum fun (a : α) (b : M) ↦ (g a b).sum h)
Tactic: rw [sum_def, toFinsupp_sum' f g, Finsupp.sum_sum_index h_zero h_add]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst_1 : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
a₂ : G'
⊢ (f.sum g).coeff a₂ = f.sum fun (a₁ : G) (b : k) ↦ (g a₁ b).coeff a₂
have simp_rw : Eq.{u_3 + 1} (α := k') (((f.sum g).toFinsupp : (a : G') → k') a₂ : k')
  (f.sum fun (a₁ : G) (b : k) ↦ ((g a₁ b).toFinsupp : (a : G') → k') a₂ : k')
Tactic: simp_rw [coeff, toFinsupp_sum', sum_def, Finsupp.sum_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst_1 : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
a₂ : G'
simp_rw :
  Eq.{u_3 + 1} (α := k') (((f.sum g).toFinsupp : (a : G') → k') a₂ : k')
    (f.sum fun (a₁ : G) (b : k) ↦ ((g a₁ b).toFinsupp : (a : G') → k') a₂ : k')
⊢ (f.sum g).coeff a₂ = f.sum fun (a₁ : G) (b : k) ↦ (g a₁ b).coeff a₂
have simp_rw₁ : Eq.{u_3 + 1} (α := k') ((f.toFinsupp.sum fun (x1 : G) (x2 : k) ↦ (g x1 x2).toFinsupp : (a : G') → k') a₂ : k')
  (f.sum fun (a₁ : G) (b : k) ↦ ((g a₁ b).toFinsupp : (a : G') → k') a₂ : k')
Tactic: simp_rw [coeff, toFinsupp_sum', sum_def, Finsupp.sum_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst_1 : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
a₂ : G'
simp_rw :
  Eq.{u_3 + 1} (α := k') (((f.sum g).toFinsupp : (a : G') → k') a₂ : k')
    (f.sum fun (a₁ : G) (b : k) ↦ ((g a₁ b).toFinsupp : (a : G') → k') a₂ : k')
simp_rw₁ :
  Eq.{u_3 + 1} (α := k') ((f.toFinsupp.sum fun (x1 : G) (x2 : k) ↦ (g x1 x2).toFinsupp : (a : G') → k') a₂ : k')
    (f.sum fun (a₁ : G) (b : k) ↦ ((g a₁ b).toFinsupp : (a : G') → k') a₂ : k')
⊢ (f.sum g).coeff a₂ = f.sum fun (a₁ : G) (b : k) ↦ (g a₁ b).coeff a₂
have simp_rw₂ : Eq.{u_3 + 1} (α := k') ((f.toFinsupp.sum fun (x1 : G) (x2 : k) ↦ (g x1 x2).toFinsupp : (a : G') → k') a₂ : k')
  (f.toFinsupp.sum fun (a₁ : G) (b : k) ↦ ((g a₁ b).toFinsupp : (a : G') → k') a₂ : k')
Tactic: simp_rw [coeff, toFinsupp_sum', sum_def, Finsupp.sum_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
p : SkewMonoidAlgebra k G → Prop
f : SkewMonoidAlgebra k G
zero : p 0
single : ∀ (g : G) (a : k), p (SkewMonoidAlgebra.single g a)
add : ∀ (f g : SkewMonoidAlgebra k G), p f → p g → p (f + g)
⊢ p f
have rw : p (∑ a ∈ f.support, SkewMonoidAlgebra.single a (f.coeff a))
Tactic: rw [← sum_single f, sum_def']
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
M : Type u_3
inst_1 : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h :
  ∀ (a : G) (b : k),
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
      ((g : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
⊢ f = g
have h₁ : ∀ (p : SkewMonoidAlgebra k G),
  Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) p : M) ((g : (a : SkewMonoidAlgebra k G) → M) p : M)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
M : Type u_3
inst_1 : AddZeroClass M
f g : SkewMonoidAlgebra k G →+ M
h :
  ∀ (a : G) (b : k),
    Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
      ((g : (a : SkewMonoidAlgebra k G) → M) (single a b) : M)
p : SkewMonoidAlgebra k G
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) p : M) ((g : (a : SkewMonoidAlgebra k G) → M) p : M)
have h₁ : Eq.{u_3 + 1} (α := M) ((f : (a : SkewMonoidAlgebra k G) → M) 0 : M) ((g : (a : SkewMonoidAlgebra k G) → M) 0 : M)
Tactic: induction p using SkewMonoidAlgebra.induction_on
Cleared hypotheses: p