awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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
-- 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:
classical
  simp_rw [DFinsupp.sumAddHom_apply]
  exact c.dfinsuppSum _ _
    (bot_le (a := c) <| map_zero <| h ·) (bot_le (a := c) <| map_zero <| h' ·) H

Premises used: DFinsupp.sumAddHom_apply
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
mk :
  ∀ (toSetoid : Setoid M)
    (mul' :
      ∀ {w x y z : M},
        (toSetoid : M → M → Prop) w x → (toSetoid : M → M → Prop) y z → (toSetoid : M → M → Prop) (w * y) (x * z)),
    { toSetoid := toSetoid, mul' := @mul' : Con M }.toSetoid = d.toSetoid →
      { toSetoid := toSetoid, mul' := @mul' : Con M } = d
⊢ c.toSetoid = d.toSetoid → c = d

Tactic:
cases c
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
d : Con M
toSetoid : Setoid M
mul' :
  ∀ {w x y z : M},
    (toSetoid : M → M → Prop) w x → (toSetoid : M → M → Prop) y z → (toSetoid : M → M → Prop) (w * y) (x * z)
⊢ { toSetoid := toSetoid, mul' := @mul' : Con M }.toSetoid = d.toSetoid →
    { toSetoid := toSetoid, mul' := @mul' : Con M } = d

Tactic:
congr!
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
⊢ c.toSetoid = d.toSetoid ↔ c = d

Tactic:
toSetoid_injective.eq_iff

Premises used: Function.Injective.eq_iff, Con.toSetoid_injective
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c d x y : Con M
h :
  Eq.{u_1 + 1} (α := (a : M) → M → Prop) ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) x)
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) y)
rcases :
  ∀ (x : M → M → Prop) (iseqv : Equivalence x)
    (mul' :
      ∀ {w x_1 y z : M},
        ({ r := x, iseqv := iseqv } : M → M → Prop) w x_1 →
          ({ r := x, iseqv := iseqv } : M → M → Prop) y z →
            ({ r := x, iseqv := iseqv } : M → M → Prop) (w * y) (x_1 * z))
    (h :
      Eq.{u_1 + 1} (α := (a : M) → M → Prop)
        ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := x, iseqv := iseqv, mul' := @mul' })
        ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) y)),
    { r := x, iseqv := iseqv, mul' := @mul' : Con M } = y
⊢ x = y

Tactic:
rcases x with ⟨⟨x, _⟩, _⟩
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c d y : Con M
x : M → M → Prop
iseqv : Equivalence x
mul' :
  ∀ {w x_1 y z : M},
    ({ r := x, iseqv := iseqv } : M → M → Prop) w x_1 →
      ({ r := x, iseqv := iseqv } : M → M → Prop) y z → ({ r := x, iseqv := iseqv } : M → M → Prop) (w * y) (x_1 * z)
h :
  Eq.{u_1 + 1} (α := (a : M) → M → Prop)
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := x, iseqv := iseqv, mul' := @mul' })
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) y)
rcases :
  ∀ (y : M → M → Prop) (iseqv_1 : Equivalence y)
    (mul'_1 :
      ∀ {w x y_1 z : M},
        ({ r := y, iseqv := iseqv_1 } : M → M → Prop) w x →
          ({ r := y, iseqv := iseqv_1 } : M → M → Prop) y_1 z →
            ({ r := y, iseqv := iseqv_1 } : M → M → Prop) (w * y_1) (x * z))
    (h :
      Eq.{u_1 + 1} (α := (a : M) → M → Prop)
        ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := x, iseqv := iseqv, mul' := @mul' })
        ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop))
          { r := y, iseqv := iseqv_1, mul' := @mul'_1 })),
    { r := x, iseqv := iseqv, mul' := @mul' : Con M } = { r := y, iseqv := iseqv_1, mul' := @mul'_1 }
⊢ { r := x, iseqv := iseqv, mul' := @mul' : Con M } = y

Tactic:
rcases y with ⟨⟨y, _⟩, _⟩
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c d : Con M
x : M → M → Prop
iseqv : Equivalence x
mul' :
  ∀ {w x_1 y z : M},
    ({ r := x, iseqv := iseqv } : M → M → Prop) w x_1 →
      ({ r := x, iseqv := iseqv } : M → M → Prop) y z → ({ r := x, iseqv := iseqv } : M → M → Prop) (w * y) (x_1 * z)
y : M → M → Prop
iseqv_1 : Equivalence y
mul'_1 :
  ∀ {w x y_1 z : M},
    ({ r := y, iseqv := iseqv_1 } : M → M → Prop) w x →
      ({ r := y, iseqv := iseqv_1 } : M → M → Prop) y_1 z →
        ({ r := y, iseqv := iseqv_1 } : M → M → Prop) (w * y_1) (x * z)
h :
  Eq.{u_1 + 1} (α := (a : M) → M → Prop)
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := x, iseqv := iseqv, mul' := @mul' })
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := y, iseqv := iseqv_1, mul' := @mul'_1 })
⊢ x = y

Tactic:
have : x = y := h
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c d : Con M
x : M → M → Prop
iseqv : Equivalence x
mul' :
  ∀ {w x_1 y z : M},
    ({ r := x, iseqv := iseqv } : M → M → Prop) w x_1 →
      ({ r := x, iseqv := iseqv } : M → M → Prop) y z → ({ r := x, iseqv := iseqv } : M → M → Prop) (w * y) (x_1 * z)
y : M → M → Prop
iseqv_1 : Equivalence y
mul'_1 :
  ∀ {w x y_1 z : M},
    ({ r := y, iseqv := iseqv_1 } : M → M → Prop) w x →
      ({ r := y, iseqv := iseqv_1 } : M → M → Prop) y_1 z →
        ({ r := y, iseqv := iseqv_1 } : M → M → Prop) (w * y_1) (x * z)
h :
  Eq.{u_1 + 1} (α := (a : M) → M → Prop)
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := x, iseqv := iseqv, mul' := @mul' })
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := y, iseqv := iseqv_1, mul' := @mul'_1 })
this : x = y
subst :
  ∀ (iseqv : Equivalence y)
    (mul' :
      ∀ {w x y_1 z : M},
        ({ r := y, iseqv := iseqv } : M → M → Prop) w x →
          ({ r := y, iseqv := iseqv } : M → M → Prop) y_1 z →
            ({ r := y, iseqv := iseqv } : M → M → Prop) (w * y_1) (x * z))
    (h :
      Eq.{u_1 + 1} (α := (a : M) → M → Prop)
        ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := y, iseqv := iseqv, mul' := @mul' })
        ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop))
          { r := y, iseqv := iseqv_1, mul' := @mul'_1 })),
    { r := y, iseqv := iseqv, mul' := @mul' : Con M } = { r := y, iseqv := iseqv_1, mul' := @mul'_1 }
⊢ { r := x, iseqv := iseqv, mul' := @mul' : Con M } = { r := y, iseqv := iseqv_1, mul' := @mul'_1 }

Tactic:
subst x
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c d : Con M
y : M → M → Prop
iseqv : Equivalence y
mul' :
  ∀ {w x y_1 z : M},
    ({ r := y, iseqv := iseqv } : M → M → Prop) w x →
      ({ r := y, iseqv := iseqv } : M → M → Prop) y_1 z → ({ r := y, iseqv := iseqv } : M → M → Prop) (w * y_1) (x * z)
iseqv_1 : Equivalence y
mul'_1 :
  ∀ {w x y_1 z : M},
    ({ r := y, iseqv := iseqv_1 } : M → M → Prop) w x →
      ({ r := y, iseqv := iseqv_1 } : M → M → Prop) y_1 z →
        ({ r := y, iseqv := iseqv_1 } : M → M → Prop) (w * y_1) (x * z)
h :
  Eq.{u_1 + 1} (α := (a : M) → M → Prop)
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := y, iseqv := iseqv_1, mul' := @mul'_1 })
    ((fun (c : Con M) ↦ ((⇑c.toSetoid : M → M → Prop) : M → M → Prop)) { r := y, iseqv := iseqv, mul' := @mul' })
⊢ { r := y, iseqv := iseqv_1, mul' := @mul'_1 : Con M } = { r := y, iseqv := iseqv, mul' := @mul' }

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
⊢ Eq (α := M → M → Prop) (⇑c.toSetoid : M → M → Prop) (⇑c : (a : M) → M → Prop)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
x : M
⊢ (c : (a : M) → M → Prop) x x

Tactic:
c.toSetoid.refl' x

Premises used: Setoid.refl', Con.toSetoid
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
x y : M
⊢ (c : (a : M) → M → Prop) x y → (c : (a : M) → M → Prop) y x

Tactic:
c.toSetoid.symm'

Premises used: Setoid.symm', Con.toSetoid
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
x y z : M
⊢ (c : (a : M) → M → Prop) x y → (c : (a : M) → M → Prop) y z → (c : (a : M) → M → Prop) x z

Tactic:
c.toSetoid.trans'

Premises used: Setoid.trans', Con.toSetoid
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
w x y z : M
⊢ (c : (a : M) → M → Prop) w x → (c : (a : M) → M → Prop) y z → (c : (a : M) → M → Prop) (w * y) (x * z)

Tactic:
c.mul'

Premises used: Con.mul'
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
s : Setoid M
h : ∀ {w x y z : M}, (s : M → M → Prop) w x → (s : M → M → Prop) y z → (s : M → M → Prop) (w * y) (x * z)
a b : M
⊢ ({ toSetoid := s, mul' := @h : Con M } : (a : M) → M → Prop) a b ↔ (s : M → M → Prop) a b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
H : Eq (α := (a : M) → M → Prop) (⇑c : (a : M) → M → Prop) (⇑d : (a : M) → M → Prop)
⊢ c = d

Tactic:
DFunLike.coe_injective H

Premises used: DFunLike.coe_injective
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
H h : ∀ (x x_1 : M), (c : (a : M) → M → Prop) x x_1 ↔ (d : (a : M) → M → Prop) x x_1
⊢ Eq (α := (a : M) → M → Prop) (⇑c : (a : M) → M → Prop) (⇑d : (a : M) → M → Prop)

Tactic:
ext
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
H : ∀ (x y : M), (c : (a : M) → M → Prop) x y ↔ (d : (a : M) → M → Prop) x y
x x_1 : M
⊢ (c : (a : M) → M → Prop) x x_1 ↔ (d : (a : M) → M → Prop) x x_1

Tactic:
apply H
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
⊢ Eq (α := (a : M) → M → Prop) (⇑c : (a : M) → M → Prop) (⇑d : (a : M) → M → Prop) ↔ c = d

Tactic:
DFunLike.coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, DFunLike.coe_injective
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_4
inst : Mul M
c : Con M
x : M
⊢ Eq (α := Quot (α := M) (⇑c : (a : M) → M → Prop)) (Quot.mk (⇑c : (a : M) → M → Prop) x) (↑x : c.Quotient)

Tactic:
rfl

Premises used: Con.toQuotient, rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
cM : Con M
cN : Con N
φ : cM.Quotient → cN.Quotient → Sort u_4
a : M
b : N
f : (x : M) → (y : N) → φ (↑x : cM.Quotient) (↑y : cN.Quotient)
h :
  ∀ (x : M) (y : N) (x' : M) (y' : N), (cM : (a : M) → M → Prop) x x' → (cN : (a : N) → N → Prop) y y' → f x y ≍ f x' y'
⊢ Con.hrecOn₂ (φ := φ) (↑a : cM.Quotient) (↑b : cN.Quotient) f h = f a b

Tactic:
rfl

Premises used: Con.hrecOn₂, Quotient.hrecOn₂', Quotient.hrecOn₂, Quot.hrecOn₂, Con.toQuotient, rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
C : c.Quotient → Prop
q : c.Quotient
H : ∀ (x : M), C (↑x : c.Quotient)
⊢ C q

Tactic:
Quotient.inductionOn' q H

Premises used: Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
c : Con M
d : Con N
C : c.Quotient → d.Quotient → Prop
p : c.Quotient
q : d.Quotient
H : ∀ (x : M) (y : N), C (↑x : c.Quotient) (↑y : d.Quotient)
⊢ C p q

Tactic:
Quotient.inductionOn₂' p q H

Premises used: Quotient.inductionOn₂'
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
a b : M
⊢ Eq (α := c.Quotient) (↑a : c.Quotient) (↑b : c.Quotient) ↔ (c : (a : M) → M → Prop) a b

Tactic:
Quotient.eq''

Premises used: Quotient.eq'', Con.Quotient, Con.toQuotient
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
x y : M
⊢ (↑(x * y) : c.Quotient) = HMul.hMul (α := c.Quotient) (↑x : c.Quotient) (↑y : c.Quotient)

Tactic:
rfl

Premises used: Quotient.map₂, Con.toQuotient, rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
β : Sort u_4
c : Con M
f : M → β
h : ∀ (a b : M), (c : (a : M) → M → Prop) a b → f a = f b
x : M
⊢ Con.liftOn (↑x : c.Quotient) f h = f x

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
⊢ c ≤ d ↔ ∀ {x y : M}, (c : (a : M) → M → Prop) x y → (d : (a : M) → M → Prop) x y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
x y : M
h : ((sInf S).toSetoid : M → M → Prop) x y
r : Setoid M
h_1 : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
rw : (c.toSetoid : M → M → Prop) x y
⊢ (r : M → M → Prop) x y

Tactic:
rw [← hr]
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
x y : M
h : ((sInf S).toSetoid : M → M → Prop) x y
r : Setoid M
h_1 : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ (c.toSetoid : M → M → Prop) x y

Tactic:
h c hS
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
x y : M
h : ((sInf S).toSetoid : M → M → Prop) x y
r : Setoid M
h_1 : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ (c.toSetoid : M → M → Prop) x y

Tactic:
exact h c hS
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
h : ∀ (x x_1 : M), (sInf S : (a : M) → M → Prop) x x_1 ↔ sInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' S) x x_1
⊢ Eq (α := (a : M) → M → Prop) (⇑(sInf S) : (a : M) → M → Prop) (sInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' S))

Tactic:
ext
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
x x_1 : M
h : (sInf S : (a : M) → M → Prop) x x_1 ↔ ∀ (i : Con M) (i_1 : i ∈ S), (i : (a : M) → M → Prop) x x_1
⊢ (sInf S : (a : M) → M → Prop) x x_1 ↔ sInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' S) x x_1

Tactic:
simp only [sInf_image, iInf_apply, iInf_Prop_eq]

Premises used: iInf_apply, sInf_image, iInf_Prop_eq
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
S : Set (Con M)
x x_1 : M
⊢ (sInf S : (a : M) → M → Prop) x x_1 ↔ ∀ (i : Con M) (i_1 : i ∈ S), (i : (a : M) → M → Prop) x x_1

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
ι : Sort u_4
f : ι → Con M
rw :
  Eq (α := (a : M) → M → Prop) (⇑(sInf (Set.range f)) : (a : M) → M → Prop) (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
rw₁ :
  Eq (α := (a : M) → M → Prop) (sInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) '' Set.range f))
    (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
rw₂ :
  Eq (α := (a : M) → M → Prop) (sInf (Set.range (DFunLike.coe (β := fun (x : M) ↦ M → Prop) ∘ f)))
    (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
rw₃ :
  Eq (α := (a : M) → M → Prop) (iInf (DFunLike.coe (β := fun (x : M) ↦ M → Prop) ∘ f))
    (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
rw₄ rw₅ :
  Eq.{u_1 + 1} (α := (a : M) → M → Prop) (⨅ (x : ι), (⇑(f x) : (a : M) → M → Prop))
    (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))
⊢ Eq (α := (a : M) → M → Prop) (⇑(iInf f) : (a : M) → M → Prop) (⨅ (i : ι), (⇑(f i) : (a : M) → M → Prop))

Tactic:
rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]

Premises used: Set.range_comp, iInf, Function.comp_def, Con.coe_sInf, sInf_range
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
c d : Con M
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ :
  ∀ {w x y z : M}, (⊤ : M → M → Prop) w x → (⊤ : M → M → Prop) y z → (⊤ : M → M → Prop) (w * y) (x * z)
⊢ ∀ {w x y z : M}, (⊤ : M → M → Prop) w x → (⊤ : M → M → Prop) y z → (⊤ : M → M → Prop) (w * y) (x * z)

Tactic:
tauto
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
⊢ Eq (α := (a : M) → M → Prop) (⇑(c ⊓ d) : (a : M) → M → Prop) ((⇑c : (a : M) → M → Prop) ⊓ (⇑d : (a : M) → M → Prop))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
⊢ Eq.{u_1 + 1} (α := Setoid M) (toSetoid ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
⊢ Eq.{u_1 + 1} (α := Setoid M) (toSetoid ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
rw : c.toSetoid = toSetoid ⊤ ↔ c = ⊤
rw₁ rw₂ : c = ⊤ ↔ c = ⊤
⊢ c.toSetoid = ⊤ ↔ c = ⊤

Tactic:
rw [← toSetoid_top, toSetoid_inj]

Premises used: Con.toSetoid_inj, Con.toSetoid_top
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c : Con M
rw : c.toSetoid = toSetoid ⊥ ↔ c = ⊥
rw₁ rw₂ : c = ⊥ ↔ c = ⊥
⊢ c.toSetoid = ⊥ ↔ c = ⊥

Tactic:
rw [← toSetoid_bot, toSetoid_inj]

Premises used: Con.toSetoid_inj, Con.toSetoid_bot
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
c d : Con M
x y : M
⊢ (c ⊓ d : (a : M) → M → Prop) x y ↔ (c : (a : M) → M → Prop) x y ∧ (d : (a : M) → M → Prop) x y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
of : ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y
refl : ∀ (x : M), (s : (a : M) → M → Prop) x x
symm : ∀ {x y : M}, ConGen.Rel r x y → (s : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) y x
trans :
  ∀ {x y z : M},
    ConGen.Rel r x y →
      ConGen.Rel r y z → (s : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) y z → (s : (a : M) → M → Prop) x z
mul :
  ∀ {w x y z : M},
    ConGen.Rel r w x →
      ConGen.Rel r y z →
        (s : (a : M) → M → Prop) w x → (s : (a : M) → M → Prop) y z → (s : (a : M) → M → Prop) (w * y) (x * z)
⊢ (s : (a : M) → M → Prop) x y

Tactic:
apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy

Premises used: ConGen.Rel.recOn
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
⊢ ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y

Tactic:
fun x y h => hs x y h
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
⊢ ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y

Tactic:
exact fun x y h => hs x y h
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
⊢ ∀ (x : M), (s : (a : M) → M → Prop) x x

Tactic:
s.refl'

Premises used: Setoid.refl', Con.toSetoid
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
⊢ ∀ (x : M), (s : (a : M) → M → Prop) x x

Tactic:
exact s.refl'

Premises used: Setoid.refl', Con.toSetoid
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
x_1 y_1 : M
⊢ ConGen.Rel r x_1 y_1 → (s : (a : M) → M → Prop) x_1 y_1 → (s : (a : M) → M → Prop) y_1 x_1

Tactic:
fun _ => s.symm'

Premises used: Setoid.symm', Con.toSetoid
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → (s : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) y x

Tactic:
exact fun _ => s.symm'

Premises used: Setoid.symm', Con.toSetoid
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
x_1 y_1 z : M
⊢ ConGen.Rel r x_1 y_1 →
    ConGen.Rel r y_1 z →
      (s : (a : M) → M → Prop) x_1 y_1 → (s : (a : M) → M → Prop) y_1 z → (s : (a : M) → M → Prop) x_1 z

Tactic:
fun _ _ => s.trans'

Premises used: Setoid.trans', Con.toSetoid
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
⊢ ∀ {x y z : M},
    ConGen.Rel r x y →
      ConGen.Rel r y z → (s : (a : M) → M → Prop) x y → (s : (a : M) → M → Prop) y z → (s : (a : M) → M → Prop) x z

Tactic:
exact fun _ _ => s.trans'

Premises used: Setoid.trans', Con.toSetoid
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
w x_1 y_1 z : M
⊢ ConGen.Rel r w x_1 →
    ConGen.Rel r y_1 z →
      (s : (a : M) → M → Prop) w x_1 → (s : (a : M) → M → Prop) y_1 z → (s : (a : M) → M → Prop) (w * y_1) (x_1 * z)

Tactic:
fun _ _ => s.mul

Premises used: Con.mul
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
s : Con M
hs : Membership.mem (γ := Set (Con M)) {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} s
x y : M
hxy : (conGen r : (a : M) → M → Prop) x y
⊢ ∀ {w x y z : M},
    ConGen.Rel r w x →
      ConGen.Rel r y z →
        (s : (a : M) → M → Prop) w x → (s : (a : M) → M → Prop) y z → (s : (a : M) → M → Prop) (w * y) (x * z)

Tactic:
exact fun _ _ => s.mul

Premises used: Con.mul
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
c : Con M
h : ∀ (x y : M), r x y → (c : (a : M) → M → Prop) x y
rw : sInf {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} ≤ c
⊢ conGen r ≤ c

Tactic:
rw [conGen_eq]

Premises used: Con.conGen_eq
-- Module: Mathlib.GroupTheory.Congruence.Defs
Goal:
M : Type u_1
inst : Mul M
r : M → M → Prop
c : Con M
h : ∀ (x y : M), r x y → (c : (a : M) → M → Prop) x y
⊢ sInf {s : Con M | ∀ (x y : M), r x y → (s : (a : M) → M → Prop) x y} ≤ c

Tactic:
sInf_le h

Premises used: sInf_le