awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y_1 : M
f_1 f : M →* P
x y : Con.Quotient (ker f)
a a_1 : M
h :
  Eq.{u_3 + 1} (α := ↥(MonoidHom.mrange (kerLift f)))
    (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f)))
        (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a) :
      ↥(MonoidHom.mrange (kerLift f)))
    (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f)))
        (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a_1) :
      ↥(MonoidHom.mrange (kerLift f)))
⊢ Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a) : P)
    ((kerLift f : (a : (ker f).Quotient) → P) (Quot.mk (⇑(ker f).toSetoid : M → M → Prop) a_1) : P)

Tactic:
injections
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x y : M
f_1 f : M →* P
x_1 : ↥(MonoidHom.mrange (kerLift f))
w : P
z : Con.Quotient (ker f)
hz : (kerLift f : (a : (ker f).Quotient) → P) z = w
rcases :
  Eq.{u_3 + 1} (α := ↥(MonoidHom.mrange (kerLift f)))
    (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f))) z :
      ↥(MonoidHom.mrange (kerLift f)))
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submonoid P) (MonoidHom.mrange (kerLift f)) x)
        ((kerLift f : (a : (ker f).Quotient) → P) z) ⋯ :
      ↥(MonoidHom.mrange (kerLift f)))
⊢ Eq.{u_3 + 1} (α := ↥(MonoidHom.mrange (kerLift f)))
    (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f))) z :
      ↥(MonoidHom.mrange (kerLift f)))
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submonoid P) (MonoidHom.mrange (kerLift f)) x) w ⋯ :
      ↥(MonoidHom.mrange (kerLift f)))

Tactic:
rcases hz with ⟨⟩
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x y : M
f_1 f : M →* P
x_1 : ↥(MonoidHom.mrange (kerLift f))
z : Con.Quotient (ker f)
⊢ Eq.{u_3 + 1} (α := ↥(MonoidHom.mrange (kerLift f)))
    (((kerLift f).mrangeRestrict : (a : (ker f).Quotient) → ↥(MonoidHom.mrange (kerLift f))) z :
      ↥(MonoidHom.mrange (kerLift f)))
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submonoid P) (MonoidHom.mrange (kerLift f)) x)
        ((kerLift f : (a : (ker f).Quotient) → P) z) ⋯ :
      ↥(MonoidHom.mrange (kerLift f)))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y : M
f_1 f : M →* P
g : P → M
hf : RightInverse g (⇑f : (a : M) → P)
x : Con.Quotient (ker f)
rw :
  Eq.{u_3 + 1} (α := P)
    ((kerLift f : (a : (ker f).Quotient) → P) (↑(g ((kerLift f : (a : (ker f).Quotient) → P) x)) : (ker f).Quotient) :
      P)
    ((kerLift f : (a : (ker f).Quotient) → P) x : P)
rw₁ :
  Eq.{u_3 + 1} (α := P) ((f : (a : M) → P) (g ((kerLift f : (a : (ker f).Quotient) → P) x)) : P)
    ((kerLift f : (a : (ker f).Quotient) → P) x : P)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) x : P)
    ((kerLift f : (a : (ker f).Quotient) → P) x : P)
⊢ Eq.{u_3 + 1} (α := P)
    ((kerLift f : (a : (ker f).Quotient) → P) ((toQuotient ∘ g) ((kerLift f : (a : (ker f).Quotient) → P) x)) : P)
    ((kerLift f : (a : (ker f).Quotient) → P) x : P)

Tactic:
rw [Function.comp_apply, kerLift_mk, hf]

Premises used: Con.kerLift_mk, Function.comp_apply
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y : M
f_1 f : M →* P
g : P → M
hf : RightInverse g (⇑f : (a : M) → P)
x : P
rw : ((f : (a : M) → P) (g x) : P)
| x

Tactic:
rw [← hf x]
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y : M
f_1 f : M →* P
g : P → M
hf : RightInverse g (⇑f : (a : M) → P)
x : P
conv_rhs :
  Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) ((toQuotient ∘ g) x) : P)
    ((f : (a : M) → P) (g x) : P)
⊢ (kerLift f : (a : (ker f).Quotient) → P) ((toQuotient ∘ g) x) = x

Tactic:
conv_rhs => rw [← hf x]
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c : Con M
x_1 y : M
f_1 f : M →* P
g : P → M
hf : RightInverse g (⇑f : (a : M) → P)
x : P
⊢ Eq.{u_3 + 1} (α := P) ((kerLift f : (a : (ker f).Quotient) → P) ((toQuotient ∘ g) x) : P)
    ((f : (a : M) → P) (g x) : P)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
c : Con M
f : N →* M
hf : Surjective.{u_2 + 1, u_1 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
x : N
⊢ Eq.{u_1 + 1} (α := c.Quotient)
    ((c.comapQuotientEquivOfSurj f hf : (a : (comap (⇑f : (a : N) → M) ⋯ c).Quotient) → c.Quotient)
        (↑x : (comap (⇑f : (a : N) → M) ⋯ c).Quotient) :
      c.Quotient)
    ((↑((f : (a : N) → M) x) : c.Quotient) : c.Quotient)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, Con.toQuotient, rfl
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
c : Con M
f : N →* M
hf : Surjective.{u_2 + 1, u_1 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
x : N
⊢ Eq.{u_2 + 1} (α := (comap (⇑f : (a : N) → M) ⋯ c).Quotient)
    (((c.comapQuotientEquivOfSurj f hf).symm : (a : c.Quotient) → (comap (⇑f : (a : N) → M) ⋯ c).Quotient)
        (↑((f : (a : N) → M) x) : c.Quotient) :
      (comap (⇑f : (a : N) → M) ⋯ c).Quotient)
    ((↑x : (comap (⇑f : (a : N) → M) ⋯ c).Quotient) : (comap (⇑f : (a : N) → M) ⋯ c).Quotient)

Tactic:
(MulEquiv.symm_apply_eq (c.comapQuotientEquivOfSurj f hf)).mpr rfl

Premises used: Iff.mpr, MulEquiv.symm_apply_eq, Con.comapQuotientEquivOfSurj, rfl
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
c : Con M
f : N ≃* M
x : N
⊢ Eq.{u_2 + 1} (α := Con.Quotient (comap (⇑f : (a : N) → M) ⋯ c))
    (((MulEquiv.symm (c.comapQuotientEquivOfSurj (↑f : N →* M) ⋯) :
            MulEquiv.{u_1, u_2} c.Quotient (Con.Quotient (comap (⇑f : (a : N) → M) ⋯ c))) :
          (a : c.Quotient) → (comap (⇑f : (a : N) → M) ⋯ c).Quotient)
        ⟦(f : (a : N) → M) x⟧ :
      Con.Quotient (comap (⇑f : (a : N) → M) ⋯ c))
    ((↑x : Con.Quotient (comap (⇑f : (a : N) → M) ⋯ c)) : Con.Quotient (comap (⇑f : (a : N) → M) ⋯ c))

Tactic:
(MulEquiv.symm_apply_eq (@comapQuotientEquivOfSurj M N _ _ c f _)).mpr rfl

Premises used: Iff.mpr, MonoidHomClass.toMonoidHom, MulEquiv.symm_apply_eq, Con.comapQuotientEquivOfSurj, rfl
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
c_1 : Con M
x_1 y_1 : M
f : M →* P
c d : Con M
h : c ≤ d
x y : Con.Quotient (ker (c.map d h))
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun
      (HMul.hMul (α := Con.Quotient (ker (c.map d h))) (↑(↑a : c.Quotient) : (ker (c.map d h)).Quotient)
        (↑(↑b : c.Quotient) : (ker (c.map d h)).Quotient)) =
    (d.mk' : (a : M) → d.Quotient) (a * b)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
α : Type u_4
M : Type u_5
inst : MulOneClass M
inst_1 : SMul α M
inst_2 : IsScalarTower α M M
c : Con M
a : α
w x : M
h : (c : (a : M) → M → Prop) w x
⊢ (c : (a : M) → M → Prop) (a • w) (a • x)

Tactic:
simpa only [smul_one_mul] using c.mul (c.refl' (a • (1 : M) : M)) h

Premises used: Con.mul, Setoid.refl', Con.toSetoid, smul_one_mul, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Congruence.Basic
Goal:
α : Type u_4
M : Type u_5
inst : MulOneClass M
inst_1 : SMul α M
inst_2 : IsScalarTower α M M
c : Con M
a : α
x : M
⊢ (↑(a • x) : c.Quotient) = HSMul.hSMul (β := c.Quotient) a (↑x : c.Quotient)

Tactic:
rfl

Premises used: Quot.map, Quotient.map', Con.toQuotient, rfl
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
c : Con M
f g : ι → M
h : ∀ (x : ι), Membership.mem (γ := List ι) [] x → (c : (a : M) → M → Prop) (f x) (g x)
⊢ (c : (a : M) → M → Prop) (List.map f []).prod (List.map g []).prod

Tactic:
simpa only [List.map_nil, List.prod_nil] using c.refl 1

Premises used: Con.refl, List.prod_nil, OfNat.ofNat, List.map_nil
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
c : Con M
f g : ι → M
x : ι
xs : List ι
ih :
  ∀ (h : ∀ x ∈ xs, (c : (a : M) → M → Prop) (f x) (g x)),
    (c : (a : M) → M → Prop) (List.map f xs).prod (List.map g xs).prod
h : ∀ x_1 ∈ x :: xs, (c : (a : M) → M → Prop) (f x_1) (g x_1)
cons : (c : (a : M) → M → Prop) (f x * (List.map f xs).prod) (g x * (List.map g xs).prod)
⊢ (c : (a : M) → M → Prop) (List.map f (x :: xs)).prod (List.map g (x :: xs)).prod

Tactic:
rw [List.map_cons, List.map_cons, List.prod_cons, List.prod_cons]

Premises used: List.map_cons, List.prod_cons
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
c : Con M
f g : ι → M
x : ι
xs : List ι
ih :
  ∀ (h : ∀ x ∈ xs, (c : (a : M) → M → Prop) (f x) (g x)),
    (c : (a : M) → M → Prop) (List.map f xs).prod (List.map g xs).prod
h : ∀ x_1 ∈ x :: xs, (c : (a : M) → M → Prop) (f x_1) (g x_1)
⊢ (c : (a : M) → M → Prop) (f x * (List.map f xs).prod) (g x * (List.map g xs).prod)

Tactic:
c.mul (h _ <| .head _) <| ih fun k hk ↦ h _ (.tail _ hk)

Premises used: Con.mul, List.Mem.tail, List.Mem.head
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
c : Con M
f g : ι → M
x : ι
xs : List ι
ih :
  ∀ (h : ∀ x ∈ xs, (c : (a : M) → M → Prop) (f x) (g x)),
    (c : (a : M) → M → Prop) (List.map f xs).prod (List.map g xs).prod
h : ∀ x_1 ∈ x :: xs, (c : (a : M) → M → Prop) (f x_1) (g x_1)
⊢ (c : (a : M) → M → Prop) (f x * (List.map f xs).prod) (g x * (List.map g xs).prod)

Tactic:
exact c.mul (h _ <| .head _) <| ih fun k hk ↦ h _ (.tail _ hk)

Premises used: Con.mul, List.Mem.tail, List.Mem.head
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
c : Con M
l : List ι
f g : ι → M
h : ∀ x ∈ l, (c : (a : M) → M → Prop) (f x) (g x)
nil :
  ∀ (h : ∀ (x : ι), Membership.mem (γ := List ι) [] x → (c : (a : M) → M → Prop) (f x) (g x)),
    (c : (a : M) → M → Prop) (List.map f []).prod (List.map g []).prod
cons :
  ∀ (x : ι) (xs : List ι)
    (ih :
      ∀ (h : ∀ x ∈ xs, (c : (a : M) → M → Prop) (f x) (g x)),
        (c : (a : M) → M → Prop) (List.map f xs).prod (List.map g xs).prod)
    (h : ∀ x_1 ∈ x :: xs, (c : (a : M) → M → Prop) (f x_1) (g x_1)),
    (c : (a : M) → M → Prop) (List.map f (x :: xs)).prod (List.map g (x :: xs)).prod
⊢ (c : (a : M) → M → Prop) (List.map f l).prod (List.map g l).prod

Tactic:
induction l with
  | nil =>
    simpa only [List.map_nil, List.prod_nil] using c.refl 1
  | cons x xs ih =>
    rw [List.map_cons, List.map_cons, List.prod_cons, List.prod_cons]
    exact c.mul (h _ <| .head _) <| ih fun k hk ↦ h _ (.tail _ hk)

Premises used: Con.mul, List.map_cons, Con.refl, List.prod_nil, OfNat.ofNat, List.prod_cons, List.map_nil
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : CommMonoid M
c : Con M
s : Multiset ι
f g : ι → M
h : ∀ x ∈ s, (c : (a : M) → M → Prop) (f x) (g x)
mk :
  ∀ (a : List ι)
    (h :
      ∀ (x : ι),
        Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) a) x →
          (c : (a : M) → M → Prop) (f x) (g x)),
    (c : (a : M) → M → Prop) (Multiset.map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) a)).prod
      (Multiset.map g (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) a)).prod
⊢ (c : (a : M) → M → Prop) (Multiset.map f s).prod (Multiset.map g s).prod

Tactic:
rcases s
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : CommMonoid M
c : Con M
s : Multiset ι
f g : ι → M
a : List ι
h :
  ∀ (x : ι),
    Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) a) x →
      (c : (a : M) → M → Prop) (f x) (g x)
⊢ (c : (a : M) → M → Prop) (Multiset.map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) a)).prod
    (Multiset.map g (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) a)).prod

Tactic:
simpa using c.list_prod h

Premises used: Con.list_prod
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : CommMonoid M
c : Con M
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, (c : (a : M) → M → Prop) (f i) (g i)
⊢ (c : (a : M) → M → Prop) (s.prod f) (s.prod g)

Tactic:
c.multiset_prod h

Premises used: Finset.prod, Con.multiset_prod
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
inst_1 : Zero β
c : Con M
h h' : ι → β → M
f g : ι →₀ β
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β) i)) (h' i ((g : (a : ι) → β) i))
⊢ (c : (a : M) → M → Prop) (f.prod h) (g.prod h')

Tactic:
Quotient.exact (show c.mk' _ = c.mk' _ from ?_)

Premises used: Quotient.exact
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
inst_1 : Zero β
c : Con M
h h' : ι → β → M
f g : ι →₀ β
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β) i)) (h' i ((g : (a : ι) → β) i))
refine :
  Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) (f.prod h) : c.Quotient)
    ((c.mk' : (a : M) → c.Quotient) (g.prod h') : c.Quotient)
⊢ (c : (a : M) → M → Prop) (f.prod h) (g.prod h')

Tactic:
refine Quotient.exact (show c.mk' _ = c.mk' _ from ?_)

Premises used: Quotient.exact
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
inst_1 : Zero β
c : Con M
h h' : ι → β → M
f g : ι →₀ β
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β) i)) (h' i ((g : (a : ι) → β) i))
rw :
  Eq.{u_3 + 1} (α := c.Quotient) (f.prod fun (a : ι) (b : β) ↦ (c.mk' : (a : M) → c.Quotient) (h a b))
    (g.prod fun (a : ι) (b : β) ↦ (c.mk' : (a : M) → c.Quotient) (h' a b))
⊢ Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) (f.prod h) : c.Quotient)
    ((c.mk' : (a : M) → c.Quotient) (g.prod h') : c.Quotient)

Tactic:
rw [map_finsuppProd, map_finsuppProd]

Premises used: map_finsuppProd
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
inst_1 : Zero β
c : Con M
h h' : ι → β → M
f g : ι →₀ β
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β) i)) (h' i ((g : (a : ι) → β) i))
⊢ Eq.{u_3 + 1} (α := c.Quotient) (f.prod fun (a : ι) (b : β) ↦ (c.mk' : (a : M) → c.Quotient) (h a b))
    (g.prod fun (a : ι) (b : β) ↦ (c.mk' : (a : M) → c.Quotient) (h' a b))

Tactic:
Finsupp.prod_congr_of_eq_on_union
    (fun _ _ => Quotient.sound <| H _)
    (fun _ _ => Quotient.sound <| hf _) (fun _ _ => Quotient.sound <| hf' _)

Premises used: Quotient.sound, Finsupp.prod_congr_of_eq_on_union
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
inst_1 : Zero β
c : Con M
h h' : ι → β → M
f g : ι →₀ β
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β) i)) (h' i ((g : (a : ι) → β) i))
⊢ Eq.{u_3 + 1} (α := c.Quotient) (f.prod fun (a : ι) (b : β) ↦ (c.mk' : (a : M) → c.Quotient) (h a b))
    (g.prod fun (a : ι) (b : β) ↦ (c.mk' : (a : M) → c.Quotient) (h' a b))

Tactic:
exact Finsupp.prod_congr_of_eq_on_union
    (fun _ _ => Quotient.sound <| H _)
    (fun _ _ => Quotient.sound <| hf _) (fun _ _ => Quotient.sound <| hf' _)
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
inst_1 : Zero β
c : Con M
h h' : ι → β → M
f g : ι →₀ β
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β) i)) (h' i ((g : (a : ι) → β) i))
⊢ Eq.{u_3 + 1} (α := c.Quotient) (f.prod fun (a : ι) (b : β) ↦ (c.mk' : (a : M) → c.Quotient) (h a b))
    (g.prod fun (a : ι) (b : β) ↦ (c.mk' : (a : M) → c.Quotient) (h' a b))

Tactic:
classical
  exact Finsupp.prod_congr_of_eq_on_union
    (fun _ _ => Quotient.sound <| H _)
    (fun _ _ => Quotient.sound <| hf _) (fun _ _ => Quotient.sound <| hf' _)
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : CommMonoid M
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)
c : Con M
h h' : (i : ι) → β i → M
f g : Π₀ (i : ι), β i
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β a) i)) (h' i ((g : (a : ι) → β a) i))
⊢ (c : (a : M) → M → Prop) (f.prod (β := β) h) (g.prod (β := β) h')

Tactic:
Quotient.exact (show c.mk' _ = c.mk' _ from ?_)

Premises used: Quotient.exact
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : CommMonoid M
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)
c : Con M
h h' : (i : ι) → β i → M
f g : Π₀ (i : ι), β i
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β a) i)) (h' i ((g : (a : ι) → β a) i))
refine :
  Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) (f.prod (β := β) h) : c.Quotient)
    ((c.mk' : (a : M) → c.Quotient) (g.prod (β := β) h') : c.Quotient)
⊢ (c : (a : M) → M → Prop) (f.prod (β := β) h) (g.prod (β := β) h')

Tactic:
refine Quotient.exact (show c.mk' _ = c.mk' _ from ?_)

Premises used: Quotient.exact
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : CommMonoid M
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)
c : Con M
h h' : (i : ι) → β i → M
f g : Π₀ (i : ι), β i
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β a) i)) (h' i ((g : (a : ι) → β a) i))
rw :
  Eq.{u_3 + 1} (α := c.Quotient) (f.prod (β := β) fun (a : ι) (b : β a) ↦ (c.mk' : (a : M) → c.Quotient) (h a b))
    (g.prod (β := β) fun (a : ι) (b : β a) ↦ (c.mk' : (a : M) → c.Quotient) (h' a b))
⊢ Eq (α := c.Quotient) ((c.mk' : (a : M) → c.Quotient) (f.prod (β := β) h) : c.Quotient)
    ((c.mk' : (a : M) → c.Quotient) (g.prod (β := β) h') : c.Quotient)

Tactic:
rw [map_dfinsuppProd, map_dfinsuppProd]

Premises used: map_dfinsuppProd
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : CommMonoid M
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)
c : Con M
h h' : (i : ι) → β i → M
f g : Π₀ (i : ι), β i
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β a) i)) (h' i ((g : (a : ι) → β a) i))
⊢ Eq.{u_3 + 1} (α := c.Quotient) (f.prod (β := β) fun (a : ι) (b : β a) ↦ (c.mk' : (a : M) → c.Quotient) (h a b))
    (g.prod (β := β) fun (a : ι) (b : β a) ↦ (c.mk' : (a : M) → c.Quotient) (h' a b))

Tactic:
DFinsupp.prod_congr_of_eq_on_union
    (fun _ _ => Quotient.sound <| H _)
    (fun _ _ => Quotient.sound <| hf _) (fun _ _ => Quotient.sound <| hf' _)

Premises used: DFinsupp.prod_congr_of_eq_on_union, Quotient.sound
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : CommMonoid M
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)
c : Con M
h h' : (i : ι) → β i → M
f g : Π₀ (i : ι), β i
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β a) i)) (h' i ((g : (a : ι) → β a) i))
⊢ Eq.{u_3 + 1} (α := c.Quotient) (f.prod (β := β) fun (a : ι) (b : β a) ↦ (c.mk' : (a : M) → c.Quotient) (h a b))
    (g.prod (β := β) fun (a : ι) (b : β a) ↦ (c.mk' : (a : M) → c.Quotient) (h' a b))

Tactic:
exact DFinsupp.prod_congr_of_eq_on_union
    (fun _ _ => Quotient.sound <| H _)
    (fun _ _ => Quotient.sound <| hf _) (fun _ _ => Quotient.sound <| hf' _)
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : CommMonoid M
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)
c : Con M
h h' : (i : ι) → β i → M
f g : Π₀ (i : ι), β i
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β a) i)) (h' i ((g : (a : ι) → β a) i))
⊢ Eq.{u_3 + 1} (α := c.Quotient) (f.prod (β := β) fun (a : ι) (b : β a) ↦ (c.mk' : (a : M) → c.Quotient) (h a b))
    (g.prod (β := β) fun (a : ι) (b : β a) ↦ (c.mk' : (a : M) → c.Quotient) (h' a b))

Tactic:
classical
  exact DFinsupp.prod_congr_of_eq_on_union
    (fun _ _ => Quotient.sound <| H _)
    (fun _ _ => Quotient.sound <| hf _) (fun _ _ => Quotient.sound <| hf' _)
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h h' : (i : ι) → AddMonoidHom.{u_2, u_3} (β i) M
f g : Π₀ (i : ι), β i
H :
  ∀ (i : ι),
    (c : (a : M) → M → Prop) ((h i : (a : β i) → M) ((f : (a : ι) → β a) i) : M)
      ((h' i : (a : β i) → M) ((g : (a : ι) → β a) i))
simp_rw :
  (c : (a : M) → M → Prop) (f.sum (β := β) fun (x : ι) ↦ (⇑(h x) : (a : β x) → M))
    (g.sum (β := β) fun (x : ι) ↦ (⇑(h' x) : (a : β x) → M))
⊢ (c : (a : M) → M → Prop) ((DFinsupp.sumAddHom (β := β) h : (a : Π₀ (i : ι), β i) → M) f : M)
    ((DFinsupp.sumAddHom (β := β) h' : (a : Π₀ (i : ι), β i) → M) g)

Tactic:
simp_rw [DFinsupp.sumAddHom_apply]

Premises used: DFinsupp.sumAddHom_apply
-- Module: Mathlib.GroupTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid M
inst_2 : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h h' : (i : ι) → AddMonoidHom.{u_2, u_3} (β i) M
f g : Π₀ (i : ι), β i
H :
  ∀ (i : ι),
    (c : (a : M) → M → Prop) ((h i : (a : β i) → M) ((f : (a : ι) → β a) i) : M)
      ((h' i : (a : β i) → M) ((g : (a : ι) → β a) i))
⊢ (c : (a : M) → M → Prop) (f.sum (β := β) fun (x : ι) ↦ (⇑(h x) : (a : β x) → M))
    (g.sum (β := β) fun (x : ι) ↦ (⇑(h' x) : (a : β x) → M))

Tactic:
c.dfinsuppSum _ _
    (bot_le (a := c) <| map_zero <| h ·) (bot_le (a := c) <| map_zero <| h' ·) H

Premises used: map_zero, AddCon.dfinsuppSum, bot_le