case h.e'_1
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a :: m) = of a * FreeAbelianGroup.of m
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ C (FreeAbelianGroup.of (a :: m))
convert hm _ _ (hb a) ih
case h.e'_1
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a :: m) = FreeAbelianGroup.of (FreeMonoid.of a * m)
case h.e'_1
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a :: m) = of a * FreeAbelianGroup.of m
rw [of, ← FreeAbelianGroup.of_mul]
no goals
case h.e'_1
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a :: m) = FreeAbelianGroup.of (FreeMonoid.of a * m)
rfl