[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
g : CentroidHom α
toAddMonoidHom✝ : α →+ α
map_mul_left'✝ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝) (a * b) = a * ZeroHom.toFun (↑toAddMonoidHom✝) b
map_mul_right'✝ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝) (a * b) = ZeroHom.toFun (↑toAddMonoidHom✝) a * b
h :
  (fun f => f.toFun)
      { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ } =
    (fun f => f.toFun) g
⊢ { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
toAddMonoidHom✝¹ : α →+ α
map_mul_left'✝¹ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝¹) (a * b) = a * ZeroHom.toFun (↑toAddMonoidHom✝¹) b
map_mul_right'✝¹ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝¹) (a * b) = ZeroHom.toFun (↑toAddMonoidHom✝¹) a * b
toAddMonoidHom✝ : α →+ α
map_mul_left'✝ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝) (a * b) = a * ZeroHom.toFun (↑toAddMonoidHom✝) b
map_mul_right'✝ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝) (a * b) = ZeroHom.toFun (↑toAddMonoidHom✝) a * b
h :
  (fun f => f.toFun)
      { toAddMonoidHom := toAddMonoidHom✝¹, map_mul_left' := map_mul_left'✝¹, map_mul_right' := map_mul_right'✝¹ } =
    (fun f => f.toFun)
      { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ }
⊢ { toAddMonoidHom := toAddMonoidHom✝¹, map_mul_left' := map_mul_left'✝¹, map_mul_right' := map_mul_right'✝¹ } =
    { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ }
[PROOFSTEP]
congr with x
[GOAL]
case mk.mk.e_toAddMonoidHom.h
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
toAddMonoidHom✝¹ : α →+ α
map_mul_left'✝¹ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝¹) (a * b) = a * ZeroHom.toFun (↑toAddMonoidHom✝¹) b
map_mul_right'✝¹ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝¹) (a * b) = ZeroHom.toFun (↑toAddMonoidHom✝¹) a * b
toAddMonoidHom✝ : α →+ α
map_mul_left'✝ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝) (a * b) = a * ZeroHom.toFun (↑toAddMonoidHom✝) b
map_mul_right'✝ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝) (a * b) = ZeroHom.toFun (↑toAddMonoidHom✝) a * b
h :
  (fun f => f.toFun)
      { toAddMonoidHom := toAddMonoidHom✝¹, map_mul_left' := map_mul_left'✝¹, map_mul_right' := map_mul_right'✝¹ } =
    (fun f => f.toFun)
      { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ }
x : α
⊢ ↑toAddMonoidHom✝¹ x = ↑toAddMonoidHom✝ x
[PROOFSTEP]
exact congrFun h x
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = ↑f
src✝ : α →+ α := AddMonoidHom.copy f.toAddMonoidHom f' h
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := { toFun := f', map_zero' := (_ : ZeroHom.toFun (↑src✝) 0 = 0) },
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := { toFun := f', map_zero' := (_ : ZeroHom.toFun (↑src✝) 0 = 0) },
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
simp_rw [h, map_mul_left]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = ↑f
src✝ : α →+ α := AddMonoidHom.copy f.toAddMonoidHom f' h
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := { toFun := f', map_zero' := (_ : ZeroHom.toFun (↑src✝) 0 = 0) },
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := { toFun := f', map_zero' := (_ : ZeroHom.toFun (↑src✝) 0 = 0) },
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
simp_rw [h, map_mul_right]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
g f₁ f₂ : CentroidHom α
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
src✝ : α →+ α := ↑f + ↑g
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
show f (a * b) + g (a * b) = a * (f b + g b)
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
src✝ : α →+ α := ↑f + ↑g
a b : α
⊢ ↑f (a * b) + ↑g (a * b) = a * (↑f b + ↑g b)
[PROOFSTEP]
simp [map_mul_left, mul_add]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
src✝ : α →+ α := ↑f + ↑g
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
show f (a * b) + g (a * b) = (f a + g a) * b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
src✝ : α →+ α := ↑f + ↑g
a b : α
⊢ ↑f (a * b) + ↑g (a * b) = (↑f a + ↑g a) * b
[PROOFSTEP]
simp [map_mul_right, add_mul]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
change n • f (a * b) = a * n • f b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ n • ↑f (a * b) = a * n • ↑f b
[PROOFSTEP]
rw [map_mul_left f, ← mul_smul_comm]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
change n • f (a * b) = n • f a * b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ n • ↑f (a * b) = n • ↑f a * b
[PROOFSTEP]
rw [map_mul_right f, ← smul_mul_assoc]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n : ℕ
src✝ : AddMonoid.End α := toEnd f ^ n
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n
a b : α
src✝ : AddMonoid.End α := toEnd f ^ Nat.zero
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
exact rfl
[GOAL]
case succ
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n✝ : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n✝
a b : α
n : ℕ
ih :
  let src := toEnd f ^ n;
  ZeroHom.toFun
      (↑{ toZeroHom := ↑src,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        b
src✝ : AddMonoid.End α := toEnd f ^ Nat.succ n
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
simp
[GOAL]
case succ
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n✝ : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n✝
a b : α
n : ℕ
ih :
  let src := toEnd f ^ n;
  ZeroHom.toFun
      (↑{ toZeroHom := ↑src,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        b
src✝ : AddMonoid.End α := toEnd f ^ Nat.succ n
⊢ ↑(toEnd f ^ Nat.succ n) (a * b) = a * ↑(toEnd f ^ Nat.succ n) b
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n✝ : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n✝
a b : α
n : ℕ
ih :
  let src := toEnd f ^ n;
  ZeroHom.toFun
      (↑{ toZeroHom := ↑src,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        b
src✝ : AddMonoid.End α := toEnd f ^ Nat.succ n
⊢ ↑(toEnd f * toEnd f ^ n) (a * b) = a * ↑(toEnd f * toEnd f ^ n) b
[PROOFSTEP]
exact (congr_arg f.toEnd ih).trans (f.map_mul_left' _ _)
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n : ℕ
src✝ : AddMonoid.End α := toEnd f ^ n
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n
a b : α
src✝ : AddMonoid.End α := toEnd f ^ Nat.zero
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
exact rfl
[GOAL]
case succ
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n✝ : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n✝
a b : α
n : ℕ
ih :
  let src := toEnd f ^ n;
  ZeroHom.toFun
      (↑{ toZeroHom := ↑src,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        a *
      b
src✝ : AddMonoid.End α := toEnd f ^ Nat.succ n
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
simp
[GOAL]
case succ
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n✝ : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n✝
a b : α
n : ℕ
ih :
  let src := toEnd f ^ n;
  ZeroHom.toFun
      (↑{ toZeroHom := ↑src,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        a *
      b
src✝ : AddMonoid.End α := toEnd f ^ Nat.succ n
⊢ ↑(toEnd f ^ Nat.succ n) (a * b) = ↑(toEnd f ^ Nat.succ n) a * b
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n✝ : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n✝
a b : α
n : ℕ
ih :
  let src := toEnd f ^ n;
  ZeroHom.toFun
      (↑{ toZeroHom := ↑src,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        a *
      b
src✝ : AddMonoid.End α := toEnd f ^ Nat.succ n
⊢ ↑(toEnd f * toEnd f ^ n) (a * b) = ↑(toEnd f * toEnd f ^ n) a * b
[PROOFSTEP]
exact (congr_arg f.toEnd ih).trans (f.map_mul_right' _ _)
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ (↑T ∘ ↑S) (a * b) = (↑S ∘ ↑T) (a * b)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ ↑T (↑S (a * b)) = ↑S (↑T (a * b))
[PROOFSTEP]
rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f : CentroidHom α
src✝ : α →+ α := -↑f
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
change -f (a * b) = a * (-f b)
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f : CentroidHom α
src✝ : α →+ α := -↑f
a b : α
⊢ -↑f (a * b) = a * -↑f b
[PROOFSTEP]
simp [map_mul_left]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f : CentroidHom α
src✝ : α →+ α := -↑f
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
change -f (a * b) = (-f a) * b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f : CentroidHom α
src✝ : α →+ α := -↑f
a b : α
⊢ -↑f (a * b) = -↑f a * b
[PROOFSTEP]
simp [map_mul_right]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f g : CentroidHom α
src✝ : α →+ α := ↑f - ↑g
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
change (FunLike.coe f - FunLike.coe g) (a * b) = a * (FunLike.coe f - FunLike.coe g) b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f g : CentroidHom α
src✝ : α →+ α := ↑f - ↑g
a b : α
⊢ (↑f - ↑g) (a * b) = a * (↑f - ↑g) b
[PROOFSTEP]
simp [map_mul_left, mul_sub]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f g : CentroidHom α
src✝ : α →+ α := ↑f - ↑g
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
change (FunLike.coe f - FunLike.coe g) (a * b) = ((FunLike.coe f - FunLike.coe g) a) * b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f g : CentroidHom α
src✝ : α →+ α := ↑f - ↑g
a b : α
⊢ (↑f - ↑g) (a * b) = (↑f - ↑g) a * b
[PROOFSTEP]
simp [map_mul_right, sub_mul]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
n : ℤ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
change n • f (a * b) = a * n • f b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
n : ℤ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ n • ↑f (a * b) = a * n • ↑f b
[PROOFSTEP]
rw [map_mul_left f, ← mul_smul_comm]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
n : ℤ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
change n • f (a * b) = n • f a * b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
n : ℤ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ n • ↑f (a * b) = n • ↑f a * b
[PROOFSTEP]
rw [map_mul_right f, ← smul_mul_assoc]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
src✝ : Ring (CentroidHom α) := instRing
f g : CentroidHom α
⊢ f * g = g * f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
src✝ : Ring (CentroidHom α) := instRing
f g : CentroidHom α
a✝ : α
⊢ ↑(f * g) a✝ = ↑(g * f) a✝
[PROOFSTEP]
refine' sub_eq_zero.1 ((or_self_iff _).1 <| (h _ _) fun r ↦ _)
[GOAL]
case h
F : Type u_1
α : Type u_2
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
src✝ : Ring (CentroidHom α) := instRing
f g : CentroidHom α
a✝ r : α
⊢ (↑(f * g) a✝ - ↑(g * f) a✝) * r * (↑(f * g) a✝ - ↑(g * f) a✝) = 0
[PROOFSTEP]
rw [mul_assoc, sub_mul, sub_eq_zero, ← map_mul_right, ← map_mul_right, coe_mul, coe_mul, comp_mul_comm]


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁶ : FunLike F α fun x => β
inst✝⁵ : CommMonoid α
inst✝⁴ : CommMonoid β
inst✝³ : CommMonoid γ
inst✝² : CommMonoid δ
inst✝¹ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
inst✝ : FreimanHomClass F A β 2
f : F
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : a * b = c * d
⊢ ↑f a * ↑f b = ↑f c * ↑f d
[PROOFSTEP]
simp_rw [← prod_pair] at h ⊢
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁶ : FunLike F α fun x => β
inst✝⁵ : CommMonoid α
inst✝⁴ : CommMonoid β
inst✝³ : CommMonoid γ
inst✝² : CommMonoid δ
inst✝¹ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
inst✝ : FreimanHomClass F A β 2
f : F
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : prod {a, b} = prod {c, d}
⊢ prod {↑f a, ↑f b} = prod {↑f c, ↑f d}
[PROOFSTEP]
refine' map_prod_eq_map_prod f _ _ (card_pair _ _) (card_pair _ _) h
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁶ : FunLike F α fun x => β
inst✝⁵ : CommMonoid α
inst✝⁴ : CommMonoid β
inst✝³ : CommMonoid γ
inst✝² : CommMonoid δ
inst✝¹ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
inst✝ : FreimanHomClass F A β 2
f : F
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : prod {a, b} = prod {c, d}
⊢ ∀ ⦃x : α⦄, x ∈ {a, b} → x ∈ A
[PROOFSTEP]
simp [ha, hb, hc, hd]
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁶ : FunLike F α fun x => β
inst✝⁵ : CommMonoid α
inst✝⁴ : CommMonoid β
inst✝³ : CommMonoid γ
inst✝² : CommMonoid δ
inst✝¹ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
inst✝ : FreimanHomClass F A β 2
f : F
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : prod {a, b} = prod {c, d}
⊢ ∀ ⦃x : α⦄, x ∈ {c, d} → x ∈ A
[PROOFSTEP]
simp [ha, hb, hc, hd]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f g : A →*[n] β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
g : A →*[n] β
toFun✝ : α → β
map_prod_eq_map_prod'✝ :
  ∀ {s t : Multiset α},
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
        ↑card s = n → ↑card t = n → prod s = prod t → prod (map toFun✝ s) = prod (map toFun✝ t)
h : { toFun := toFun✝, map_prod_eq_map_prod' := map_prod_eq_map_prod'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_prod_eq_map_prod' := map_prod_eq_map_prod'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
toFun✝¹ : α → β
map_prod_eq_map_prod'✝¹ :
  ∀ {s t : Multiset α},
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
        ↑card s = n → ↑card t = n → prod s = prod t → prod (map toFun✝¹ s) = prod (map toFun✝¹ t)
toFun✝ : α → β
map_prod_eq_map_prod'✝ :
  ∀ {s t : Multiset α},
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
        ↑card s = n → ↑card t = n → prod s = prod t → prod (map toFun✝ s) = prod (map toFun✝ t)
h :
  { toFun := toFun✝¹, map_prod_eq_map_prod' := map_prod_eq_map_prod'✝¹ }.toFun =
    { toFun := toFun✝, map_prod_eq_map_prod' := map_prod_eq_map_prod'✝ }.toFun
⊢ { toFun := toFun✝¹, map_prod_eq_map_prod' := map_prod_eq_map_prod'✝¹ } =
    { toFun := toFun✝, map_prod_eq_map_prod' := map_prod_eq_map_prod'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A✝ : Set α
B : Set β
C : Set γ
n✝ : ℕ
a b c d : α
A : Set α
n : ℕ
s✝ t✝ : Multiset α
x✝³ : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
x✝² : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
x✝¹ : ↑card s✝ = n
x✝ : ↑card t✝ = n
h : prod s✝ = prod t✝
⊢ prod (map (fun x => x) s✝) = prod (map (fun x => x) t✝)
[PROOFSTEP]
rw [map_id', map_id', h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f : B →*[n] γ
g : A →*[n] β
hAB : Set.MapsTo (↑g) A B
s✝ t✝ : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
hs : ↑card s✝ = n
ht : ↑card t✝ = n
h : prod s✝ = prod t✝
⊢ prod (map (↑f ∘ ↑g) s✝) = prod (map (↑f ∘ ↑g) t✝)
[PROOFSTEP]
rw [← map_map, ← map_map]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f : B →*[n] γ
g : A →*[n] β
hAB : Set.MapsTo (↑g) A B
s✝ t✝ : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
hs : ↑card s✝ = n
ht : ↑card t✝ = n
h : prod s✝ = prod t✝
⊢ prod (map (↑f) (map (↑g) s✝)) = prod (map (↑f) (map (↑g) t✝))
[PROOFSTEP]
apply map_prod_eq_map_prod f _ _ ((card_map _ _).trans hs)
[GOAL]
case ht
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f : B →*[n] γ
g : A →*[n] β
hAB : Set.MapsTo (↑g) A B
s✝ t✝ : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
hs : ↑card s✝ = n
ht : ↑card t✝ = n
h : prod s✝ = prod t✝
⊢ ↑card (map (↑g) t✝) = n
[PROOFSTEP]
rwa [card_map]
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f : B →*[n] γ
g : A →*[n] β
hAB : Set.MapsTo (↑g) A B
s✝ t✝ : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
hs : ↑card s✝ = n
ht : ↑card t✝ = n
h : prod s✝ = prod t✝
⊢ prod (map (↑g) s✝) = prod (map (↑g) t✝)
[PROOFSTEP]
apply (map_prod_eq_map_prod g hsA htA hs ht h)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f : B →*[n] γ
g : A →*[n] β
hAB : Set.MapsTo (↑g) A B
s✝ t✝ : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
hs : ↑card s✝ = n
ht : ↑card t✝ = n
h : prod s✝ = prod t✝
⊢ ∀ ⦃x : β⦄, x ∈ map (↑g) s✝ → x ∈ B
[PROOFSTEP]
simpa using fun a h => hAB (hsA h)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f : B →*[n] γ
g : A →*[n] β
hAB : Set.MapsTo (↑g) A B
s✝ t✝ : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
hs : ↑card s✝ = n
ht : ↑card t✝ = n
h : prod s✝ = prod t✝
⊢ ∀ ⦃x : β⦄, x ∈ map (↑g) t✝ → x ∈ B
[PROOFSTEP]
simpa using fun a h => hAB (htA h)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
g₁ g₂ : B →*[n] γ
f : A →*[n] β
hf : Set.SurjOn (↑f) A B
hf' : Set.MapsTo (↑f) A B
⊢ Set.EqOn (↑(FreimanHom.comp g₁ f hf')) (↑(FreimanHom.comp g₂ f hf')) A ↔ Set.EqOn (↑g₁) (↑g₂) B
[PROOFSTEP]
simp [hf.cancel_right hf']
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
g : B →*[n] γ
f₁ f₂ : A →*[n] β
hg : Set.InjOn (↑g) B
hf₁ : Set.MapsTo (↑f₁) A B
hf₂ : Set.MapsTo (↑f₂) A B
⊢ Set.EqOn (↑(FreimanHom.comp g f₁ hf₁)) (↑(FreimanHom.comp g f₂ hf₂)) A ↔ Set.EqOn (↑f₁) (↑f₂) A
[PROOFSTEP]
simp [hg.cancel_left hf₁ hf₂]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A✝ : Set α
B : Set β
C : Set γ
n✝ : ℕ
a b✝ c d : α
A : Set α
n : ℕ
b : β
s✝ t✝ : Multiset α
x✝² : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
x✝¹ : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
hs : ↑card s✝ = n
ht : ↑card t✝ = n
x✝ : prod s✝ = prod t✝
⊢ prod (map (fun x => b) s✝) = prod (map (fun x => b) t✝)
[PROOFSTEP]
simp only [map_const', hs, prod_replicate, ht]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f g : A →*[n] β
s✝ t✝ : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
hs : ↑card s✝ = n
ht : ↑card t✝ = n
h : prod s✝ = prod t✝
⊢ prod (map (fun x => ↑f x * ↑g x) s✝) = prod (map (fun x => ↑f x * ↑g x) t✝)
[PROOFSTEP]
rw [prod_map_mul, prod_map_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f g : A →*[n] β
s✝ t✝ : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
hs : ↑card s✝ = n
ht : ↑card t✝ = n
h : prod s✝ = prod t✝
⊢ prod (map (fun x => ↑f x) s✝) * prod (map (fun x => ↑g x) s✝) =
    prod (map (fun x => ↑f x) t✝) * prod (map (fun x => ↑g x) t✝)
[PROOFSTEP]
rw [map_prod_eq_map_prod f hsA htA hs ht h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f g : A →*[n] β
s✝ t✝ : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
hs : ↑card s✝ = n
ht : ↑card t✝ = n
h : prod s✝ = prod t✝
⊢ prod (map (↑f) t✝) * prod (map (fun x => ↑g x) s✝) = prod (map (fun x => ↑f x) t✝) * prod (map (fun x => ↑g x) t✝)
[PROOFSTEP]
rw [map_prod_eq_map_prod g hsA htA hs ht h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f : A →*[n] G
s✝ t✝ : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
hs : ↑card s✝ = n
ht : ↑card t✝ = n
h : prod s✝ = prod t✝
⊢ prod (map (fun x => (↑f x)⁻¹) s✝) = prod (map (fun x => (↑f x)⁻¹) t✝)
[PROOFSTEP]
rw [prod_map_inv, prod_map_inv, map_prod_eq_map_prod f hsA htA hs ht h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f g : A →*[n] G
s✝ t✝ : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s✝ → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t✝ → x ∈ A
hs : ↑card s✝ = n
ht : ↑card t✝ = n
h : prod s✝ = prod t✝
⊢ prod (map (fun x => ↑f x / ↑g x) s✝) = prod (map (fun x => ↑f x / ↑g x) t✝)
[PROOFSTEP]
rw [prod_map_div, prod_map_div, map_prod_eq_map_prod f hsA htA hs ht h, map_prod_eq_map_prod g hsA htA hs ht h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a✝ b✝ c✝ d : α
a b c : A →*[n] β
⊢ a * b * c = a * (b * c)
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a✝ b✝ c✝ d : α
a b c : A →*[n] β
x✝ : α
⊢ ↑(a * b * c) x✝ = ↑(a * (b * c)) x✝
[PROOFSTEP]
apply mul_assoc
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a✝ b c d : α
a : A →*[n] β
⊢ 1 * a = a
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a✝ b c d : α
a : A →*[n] β
x✝ : α
⊢ ↑(1 * a) x✝ = ↑a x✝
[PROOFSTEP]
apply one_mul
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a✝ b c d : α
a : A →*[n] β
⊢ a * 1 = a
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a✝ b c d : α
a : A →*[n] β
x✝ : α
⊢ ↑(a * 1) x✝ = ↑a x✝
[PROOFSTEP]
apply mul_one
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a✝ b✝ c d : α
a b : A →*[n] β
⊢ a * b = b * a
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a✝ b✝ c d : α
a b : A →*[n] β
x✝ : α
⊢ ↑(a * b) x✝ = ↑(b * a) x✝
[PROOFSTEP]
apply mul_comm
[GOAL]
F : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁶ : FunLike F α fun x => β✝
inst✝⁵ : CommMonoid α
inst✝⁴ : CommMonoid β✝
inst✝³ : CommMonoid γ
inst✝² : CommMonoid δ
inst✝¹ : CommGroup G
A : Set α
B : Set β✝
C : Set γ
n : ℕ
a b c d : α
β : Type ?u.68728
inst✝ : CommGroup β
src✝ : CommMonoid (A →*[n] β) := commMonoid
⊢ ∀ (a b : A →*[n] β), a / b = a * b⁻¹
[PROOFSTEP]
intros
[GOAL]
F : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁶ : FunLike F α fun x => β✝
inst✝⁵ : CommMonoid α
inst✝⁴ : CommMonoid β✝
inst✝³ : CommMonoid γ
inst✝² : CommMonoid δ
inst✝¹ : CommGroup G
A : Set α
B : Set β✝
C : Set γ
n : ℕ
a b c d : α
β : Type ?u.68728
inst✝ : CommGroup β
src✝ : CommMonoid (A →*[n] β) := commMonoid
a✝ b✝ : A →*[n] β
⊢ a✝ / b✝ = a✝ * b✝⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁶ : FunLike F α fun x => β✝
inst✝⁵ : CommMonoid α
inst✝⁴ : CommMonoid β✝
inst✝³ : CommMonoid γ
inst✝² : CommMonoid δ
inst✝¹ : CommGroup G
A : Set α
B : Set β✝
C : Set γ
n : ℕ
a b c d : α
β : Type ?u.68728
inst✝ : CommGroup β
src✝ : CommMonoid (A →*[n] β) := commMonoid
a✝ b✝ : A →*[n] β
x✝ : α
⊢ ↑(a✝ / b✝) x✝ = ↑(a✝ * b✝⁻¹) x✝
[PROOFSTEP]
apply div_eq_mul_inv
[GOAL]
F : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁶ : FunLike F α fun x => β✝
inst✝⁵ : CommMonoid α
inst✝⁴ : CommMonoid β✝
inst✝³ : CommMonoid γ
inst✝² : CommMonoid δ
inst✝¹ : CommGroup G
A : Set α
B : Set β✝
C : Set γ
n : ℕ
a b c d : α
β : Type ?u.68728
inst✝ : CommGroup β
src✝ : CommMonoid (A →*[n] β) := commMonoid
⊢ ∀ (a : A →*[n] β), a⁻¹ * a = 1
[PROOFSTEP]
intros
[GOAL]
F : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁶ : FunLike F α fun x => β✝
inst✝⁵ : CommMonoid α
inst✝⁴ : CommMonoid β✝
inst✝³ : CommMonoid γ
inst✝² : CommMonoid δ
inst✝¹ : CommGroup G
A : Set α
B : Set β✝
C : Set γ
n : ℕ
a b c d : α
β : Type ?u.68728
inst✝ : CommGroup β
src✝ : CommMonoid (A →*[n] β) := commMonoid
a✝ : A →*[n] β
⊢ a✝⁻¹ * a✝ = 1
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁶ : FunLike F α fun x => β✝
inst✝⁵ : CommMonoid α
inst✝⁴ : CommMonoid β✝
inst✝³ : CommMonoid γ
inst✝² : CommMonoid δ
inst✝¹ : CommGroup G
A : Set α
B : Set β✝
C : Set γ
n : ℕ
a b c d : α
β : Type ?u.68728
inst✝ : CommGroup β
src✝ : CommMonoid (A →*[n] β) := commMonoid
a✝ : A →*[n] β
x✝ : α
⊢ ↑(a✝⁻¹ * a✝) x✝ = ↑1 x✝
[PROOFSTEP]
apply mul_left_inv
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f : α →* β
s t : Multiset α
x✝³ : ∀ ⦃x : α⦄, x ∈ s → x ∈ Set.univ
x✝² : ∀ ⦃x : α⦄, x ∈ t → x ∈ Set.univ
x✝¹ : ↑card s = n
x✝ : ↑card t = n
h : prod s = prod t
⊢ prod (map (↑f) s) = prod (map (↑f) t)
[PROOFSTEP]
rw [← f.map_multiset_prod, h, f.map_multiset_prod]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f g : α →* β
h : toFreimanHom A n f = toFreimanHom A n g
⊢ f = g
[PROOFSTEP]
rwa [toFreimanHom, toFreimanHom, FreimanHom.mk.injEq, FunLike.coe_fn_eq] at h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
⊢ prod (map (↑f) s) = prod (map (↑f) t)
[PROOFSTEP]
obtain rfl | hm := m.eq_zero_or_pos
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hst : prod s = prod t
hs : ↑card s = 0
ht : ↑card t = 0
h : 0 ≤ n
⊢ prod (map (↑f) s) = prod (map (↑f) t)
[PROOFSTEP]
rw [card_eq_zero] at hs ht
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hst : prod s = prod t
hs : s = 0
ht : t = 0
h : 0 ≤ n
⊢ prod (map (↑f) s) = prod (map (↑f) t)
[PROOFSTEP]
rw [hs, ht]
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
hm : m > 0
⊢ prod (map (↑f) s) = prod (map (↑f) t)
[PROOFSTEP]
simp [← hs, card_pos_iff_exists_mem] at hm
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
hm : ∃ a, a ∈ s
⊢ prod (map (↑f) s) = prod (map (↑f) t)
[PROOFSTEP]
obtain ⟨a, ha⟩ := hm
[GOAL]
case inr.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ s
⊢ prod (map (↑f) s) = prod (map (↑f) t)
[PROOFSTEP]
suffices ((s + Multiset.replicate (n - m) a).map f).prod = ((t + Multiset.replicate (n - m) a).map f).prod
  by
  simp_rw [Multiset.map_add, prod_add] at this
  exact mul_right_cancel this
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ s
this : prod (map (↑f) (s + replicate (n - m) a)) = prod (map (↑f) (t + replicate (n - m) a))
⊢ prod (map (↑f) s) = prod (map (↑f) t)
[PROOFSTEP]
simp_rw [Multiset.map_add, prod_add] at this
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ s
this :
  prod (map (fun x => ↑f x) s) * prod (map (fun x => ↑f x) (replicate (n - m) a)) =
    prod (map (fun x => ↑f x) t) * prod (map (fun x => ↑f x) (replicate (n - m) a))
⊢ prod (map (↑f) s) = prod (map (↑f) t)
[PROOFSTEP]
exact mul_right_cancel this
[GOAL]
case inr.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ s
⊢ prod (map (↑f) (s + replicate (n - m) a)) = prod (map (↑f) (t + replicate (n - m) a))
[PROOFSTEP]
replace ha := hsA _ ha
[GOAL]
case inr.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ prod (map (↑f) (s + replicate (n - m) a)) = prod (map (↑f) (t + replicate (n - m) a))
[PROOFSTEP]
apply
  map_prod_eq_map_prod f (A := A) (β := β) (n := n) (fun x hx => _) (fun x hx => _) _ _
    _
      -- porting note: below could be golfed when wlog is available
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ ∀ (x : α), x ∈ s + replicate (n - m) a → x ∈ A
[PROOFSTEP]
intro x hx
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ s + replicate (n - m) a
⊢ x ∈ A
[PROOFSTEP]
rw [mem_add] at hx
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ s ∨ x ∈ replicate (n - m) a
⊢ x ∈ A
[PROOFSTEP]
cases' hx with hx hx
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ s
⊢ x ∈ A
[PROOFSTEP]
exact hsA x hx
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ replicate (n - m) a
⊢ x ∈ A
[PROOFSTEP]
rwa [eq_of_mem_replicate hx]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ ∀ (x : α), x ∈ t + replicate (n - m) a → x ∈ A
[PROOFSTEP]
intro x hx
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ t + replicate (n - m) a
⊢ x ∈ A
[PROOFSTEP]
rw [mem_add] at hx
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ t ∨ x ∈ replicate (n - m) a
⊢ x ∈ A
[PROOFSTEP]
cases' hx with hx hx
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ t
⊢ x ∈ A
[PROOFSTEP]
exact htA x hx
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
x : α
hx : x ∈ replicate (n - m) a
⊢ x ∈ A
[PROOFSTEP]
rwa [eq_of_mem_replicate hx]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ ↑card (s + replicate (n - m) a) = n
[PROOFSTEP]
rw [_root_.map_add, card_replicate, hs]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ m + (n - m) = n
[PROOFSTEP]
simp [h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ ↑card (t + replicate (n - m) a) = n
[PROOFSTEP]
rw [_root_.map_add, card_replicate, ht]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ m + (n - m) = n
[PROOFSTEP]
simp [h]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝³ : FunLike F α fun x => β
inst✝² : CommMonoid α
inst✝¹ : CancelCommMonoid β
A : Set α
m n : ℕ
inst✝ : FreimanHomClass F A β n
f : F
s t : Multiset α
hsA : ∀ (x : α), x ∈ s → x ∈ A
htA : ∀ (x : α), x ∈ t → x ∈ A
hs : ↑card s = m
ht : ↑card t = m
hst : prod s = prod t
h : m ≤ n
a : α
ha : a ∈ A
⊢ prod (s + replicate (n - m) a) = prod (t + replicate (n - m) a)
[PROOFSTEP]
rw [prod_add, prod_add, hst]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
inst✝² : FunLike F α fun x => β
inst✝¹ : CommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
m n : ℕ
h : m ≤ n
f g : A →*[n] β
hfg : toFreimanHom h f = toFreimanHom h g
⊢ ∀ (x : α), ↑f x = ↑g x
[PROOFSTEP]
convert FunLike.ext_iff.1 hfg using 0