awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subsemigroup.Membership
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
C : (x : M) → Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul :
  ∀ (x y : M) (hx : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₁
x₃ y : M
w : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) x₃
Cx : C x₃ w
w_1 : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) y
Cy : C y w_1
⊢ ∃ (hx'' : Membership.mem (γ := Subsemigroup M) (⨆ (i : ι), S i) (x₃ * y)), C (x₃ * y) hx''

Tactic:
exact ⟨_, mul _ _ _ _ Cx Cy⟩
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
x : Mᵐᵒᵖ
S : Subsemigroup M
⊢ x ∈ S.op ↔ MulOpposite.unop x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
x : M
S : Subsemigroup Mᵐᵒᵖ
⊢ x ∈ S.unop ↔ MulOpposite.op x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S : Subsemigroup M
⊢ S.op.unop = S

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Subsemigroup.unop, MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S : Subsemigroup Mᵐᵒᵖ
⊢ S.unop.op = S

Tactic:
rfl

Premises used: Set.Mem, MulOpposite, setOf, Subsemigroup.op, Set.preimage, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S₁ : Subsemigroup M
S₂ : Subsemigroup Mᵐᵒᵖ
⊢ S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S₁ : Subsemigroup Mᵐᵒᵖ
S₂ : Subsemigroup M
⊢ S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S₁ S₂ : Subsemigroup M
⊢ S₁.op ≤ S₂.op ↔ S₁ ≤ S₂

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S₁ S₂ : Subsemigroup Mᵐᵒᵖ
⊢ S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂

Tactic:
MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, MulOpposite, setOf, Set.preimage, MulOpposite.unop, MulOpposite.unop_surjective, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := Subsemigroup M) Subsemigroup.op

Tactic:
opEquiv.injective

Premises used: Subsemigroup.opEquiv, Subsemigroup.op, OrderIso.injective
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := Subsemigroup Mᵐᵒᵖ) Subsemigroup.unop

Tactic:
opEquiv.symm.injective

Premises used: Subsemigroup.opEquiv, OrderIso.symm, OrderIso.injective, Subsemigroup.unop
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S T : Subsemigroup M
⊢ S.op = T.op ↔ S = T

Tactic:
opEquiv.eq_iff_eq

Premises used: RelIso.eq_iff_eq, Subsemigroup.opEquiv, Subsemigroup.op
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S T : Subsemigroup Mᵐᵒᵖ
⊢ S.unop = T.unop ↔ S = T

Tactic:
opEquiv.symm.eq_iff_eq

Premises used: RelIso.eq_iff_eq, Subsemigroup.opEquiv, OrderIso.symm, Subsemigroup.unop
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
⊢ Eq.{u_2 + 1} (α := Subsemigroup Mᵐᵒᵖ) (Subsemigroup.op ⊥) ⊥

Tactic:
opEquiv.map_bot

Premises used: Subsemigroup.opEquiv, Subsemigroup.op, OrderIso.map_bot
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S : Subsemigroup M
⊢ S.op = ⊥ ↔ S = ⊥

Tactic:
op_injective.eq_iff' op_bot

Premises used: Function.Injective.eq_iff', Subsemigroup.op_bot, Subsemigroup.op_injective
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
⊢ Eq.{u_2 + 1} (α := Subsemigroup M) (Subsemigroup.unop ⊥) ⊥

Tactic:
opEquiv.symm.map_bot

Premises used: Subsemigroup.opEquiv, OrderIso.symm, Subsemigroup.unop, OrderIso.map_bot
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S : Subsemigroup Mᵐᵒᵖ
⊢ S.unop = ⊥ ↔ S = ⊥

Tactic:
unop_injective.eq_iff' unop_bot

Premises used: Function.Injective.eq_iff', Subsemigroup.unop_injective, Subsemigroup.unop_bot
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
⊢ Eq.{u_2 + 1} (α := Subsemigroup Mᵐᵒᵖ) (Subsemigroup.op ⊤) ⊤

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Subsemigroup.op, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S : Subsemigroup M
⊢ S.op = ⊤ ↔ S = ⊤

Tactic:
op_injective.eq_iff' op_top

Premises used: Function.Injective.eq_iff', Subsemigroup.op_injective, Subsemigroup.op_top
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
⊢ Eq.{u_2 + 1} (α := Subsemigroup M) (Subsemigroup.unop ⊤) ⊤

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, Subsemigroup.unop, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S : Subsemigroup Mᵐᵒᵖ
⊢ S.unop = ⊤ ↔ S = ⊤

Tactic:
unop_injective.eq_iff' unop_top

Premises used: Function.Injective.eq_iff', Subsemigroup.unop_injective, Subsemigroup.unop_top
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S₁ S₂ : Subsemigroup M
⊢ (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op

Tactic:
opEquiv.map_sup _ _

Premises used: Set.Mem, setOf, Subsemigroup.opEquiv, Subsemigroup.op, OrderIso.map_sup
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S₁ S₂ : Subsemigroup Mᵐᵒᵖ
⊢ (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop

Tactic:
opEquiv.symm.map_sup _ _

Premises used: Set.Mem, setOf, Subsemigroup.opEquiv, OrderIso.symm, Subsemigroup.unop, OrderIso.map_sup
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S₁ S₂ : Subsemigroup M
⊢ (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Subsemigroup.op, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S₁ S₂ : Subsemigroup Mᵐᵒᵖ
⊢ (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Set.preimage, Subsemigroup.unop, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S : Set (Subsemigroup M)
⊢ (sSup S).op = sSup (Subsemigroup.unop ⁻¹' S)

Tactic:
opEquiv.map_sSup_eq_sSup_symm_preimage _

Premises used: Set.Mem, Subsemigroup.opEquiv, OrderIso.map_sSup_eq_sSup_symm_preimage, Subsemigroup.op, Subsemigroup.unop
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S : Set (Subsemigroup Mᵐᵒᵖ)
⊢ (sSup S).unop = sSup (Subsemigroup.op ⁻¹' S)

Tactic:
opEquiv.symm.map_sSup_eq_sSup_symm_preimage _

Premises used: Set.Mem, Subsemigroup.opEquiv, OrderIso.map_sSup_eq_sSup_symm_preimage, OrderIso.symm, Subsemigroup.op, Subsemigroup.unop
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S : Set (Subsemigroup M)
⊢ (sInf S).op = sInf (Subsemigroup.unop ⁻¹' S)

Tactic:
opEquiv.map_sInf_eq_sInf_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sInf_eq_sInf_symm_preimage, Subsemigroup.opEquiv, Subsemigroup.op, Subsemigroup.unop
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
S : Set (Subsemigroup Mᵐᵒᵖ)
⊢ (sInf S).unop = sInf (Subsemigroup.op ⁻¹' S)

Tactic:
opEquiv.symm.map_sInf_eq_sInf_symm_preimage _

Premises used: Set.Mem, OrderIso.map_sInf_eq_sInf_symm_preimage, Subsemigroup.opEquiv, OrderIso.symm, Subsemigroup.op, Subsemigroup.unop
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
⊢ (iSup S).op = ⨆ (i : ι), (S i).op

Tactic:
opEquiv.map_iSup _

Premises used: OrderIso.map_iSup, Subsemigroup.opEquiv, Subsemigroup.op
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup Mᵐᵒᵖ
⊢ (iSup S).unop = ⨆ (i : ι), (S i).unop

Tactic:
opEquiv.symm.map_iSup _

Premises used: OrderIso.map_iSup, Subsemigroup.opEquiv, OrderIso.symm, Subsemigroup.unop
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup M
⊢ (iInf S).op = ⨅ (i : ι), (S i).op

Tactic:
opEquiv.map_iInf _

Premises used: Subsemigroup.opEquiv, OrderIso.map_iInf, Subsemigroup.op
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
ι : Sort u_1
M : Type u_2
inst : Mul M
S : ι → Subsemigroup Mᵐᵒᵖ
⊢ (iInf S).unop = ⨅ (i : ι), (S i).unop

Tactic:
opEquiv.symm.map_iInf _

Premises used: Subsemigroup.opEquiv, OrderIso.map_iInf, OrderIso.symm, Subsemigroup.unop
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
s : Set M
simp_rw :
  Eq.{u_2 + 1} (α := Subsemigroup Mᵐᵒᵖ) (sInf {a : Subsemigroup Mᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Mᵐᵒᵖ)})
    (sInf {S : Subsemigroup Mᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑S : Set Mᵐᵒᵖ)})
⊢ Eq (α := Subsemigroup Mᵐᵒᵖ) (Subsemigroup.op (closure s)) (closure (MulOpposite.unop ⁻¹' s))

Tactic:
simp_rw [closure, op_sInf, Set.preimage_setOf_eq, Subsemigroup.coe_unop]

Premises used: Subsemigroup.coe_unop, Set.preimage_setOf_eq, Subsemigroup.op_sInf, Subsemigroup.closure
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
s : Set M
e_a : ∀ (a : Subsemigroup Mᵐᵒᵖ), s ⊆ MulOpposite.op ⁻¹' (↑a : Set Mᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Mᵐᵒᵖ)
⊢ Eq.{u_2 + 1} (α := Subsemigroup Mᵐᵒᵖ) (sInf {a : Subsemigroup Mᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Mᵐᵒᵖ)})
    (sInf {S : Subsemigroup Mᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑S : Set Mᵐᵒᵖ)})

Tactic:
congr with a
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
s : Set M
a : Subsemigroup Mᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' (↑a : Set Mᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Mᵐᵒᵖ)

Tactic:
MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, MulOpposite, setOf, Set.Subset, Set.preimage, MulOpposite.unop, MulOpposite.unop_surjective, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
s : Set M
a : Subsemigroup Mᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' (↑a : Set Mᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Mᵐᵒᵖ)

Tactic:
exact MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, MulOpposite.unop_surjective
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
s : Set Mᵐᵒᵖ
rw : Eq (α := Subsemigroup Mᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
⊢ Eq (α := Subsemigroup M) (Subsemigroup.unop (closure s)) (closure (MulOpposite.op ⁻¹' s))

Tactic:
rw [← op_inj, op_unop, op_closure]

Premises used: Subsemigroup.op_closure, Subsemigroup.op_unop, Subsemigroup.op_inj
-- Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Goal:
M : Type u_2
inst : Mul M
s : Set Mᵐᵒᵖ
simp_rw :
  Eq (α := Subsemigroup Mᵐᵒᵖ) (closure s) (closure ((fun (x : Mᵐᵒᵖ) ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s))
simp_rw₁ : Eq (α := Subsemigroup Mᵐᵒᵖ) (closure s) (closure ((fun (x : Mᵐᵒᵖ) ↦ x) ⁻¹' s))
⊢ Eq (α := Subsemigroup Mᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))

Tactic:
simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Premises used: Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id'
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
inst : Mul M
S : Set M
⊢ Eq (α := AddSubsemigroup (Additive M))
    ((toAddSubsemigroup : (a : Subsemigroup M) → AddSubsemigroup (Additive M)) (closure S) :
      AddSubsemigroup (Additive M))
    (AddSubsemigroup.closure ((⇑Additive.toMul : (a : Additive M) → M) ⁻¹' S) : AddSubsemigroup (Additive M))

Tactic:
le_antisymm
    (Subsemigroup.toAddSubsemigroup.le_symm_apply.1 <|
      Subsemigroup.closure_le.2 (AddSubsemigroup.subset_closure (M := Additive M)))
    (AddSubsemigroup.closure_le.2 (Subsemigroup.subset_closure (M := M)))

Premises used: Iff.mpr, AddSubsemigroup.subset_closure, Subsemigroup.closure_le, AddSubsemigroup.closure_le, le_antisymm, Subsemigroup.subset_closure, OrderIso.le_symm_apply, Iff.mp, Subsemigroup.toAddSubsemigroup
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
inst : Mul M
S : Set (Additive M)
⊢ Eq (α := Subsemigroup M)
    ((toSubsemigroup' : (a : AddSubsemigroup (Additive M)) → Subsemigroup M) (closure S) : Subsemigroup M)
    (Subsemigroup.closure ((⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' S) : Subsemigroup M)

Tactic:
le_antisymm
    (AddSubsemigroup.toSubsemigroup'.le_symm_apply.1 <|
      AddSubsemigroup.closure_le.2 (Subsemigroup.subset_closure (M := M)))
    (Subsemigroup.closure_le.2 <| AddSubsemigroup.subset_closure (M := Additive M))

Premises used: Iff.mpr, AddSubsemigroup.subset_closure, Subsemigroup.closure_le, AddSubsemigroup.closure_le, le_antisymm, Subsemigroup.subset_closure, OrderIso.le_symm_apply, Iff.mp, AddSubsemigroup.toSubsemigroup'
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
A : Type u_5
inst : Add A
S : Set A
⊢ Eq (α := Subsemigroup (Multiplicative A))
    ((toSubsemigroup : (a : AddSubsemigroup A) → Subsemigroup (Multiplicative A)) (closure S) :
      Subsemigroup (Multiplicative A))
    (Subsemigroup.closure ((⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' S) :
      Subsemigroup (Multiplicative A))

Tactic:
le_antisymm
    (AddSubsemigroup.toSubsemigroup.to_galoisConnection.l_le <|
      AddSubsemigroup.closure_le.2 <| Subsemigroup.subset_closure (M := Multiplicative A))
    (Subsemigroup.closure_le.2 <| AddSubsemigroup.subset_closure (M := A))

Premises used: Iff.mpr, OrderIso.to_galoisConnection, AddSubsemigroup.subset_closure, GaloisConnection.l_le, Subsemigroup.closure_le, AddSubsemigroup.closure_le, le_antisymm, Subsemigroup.subset_closure, AddSubsemigroup.toSubsemigroup
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
A : Type u_5
inst : Add A
S : Set (Multiplicative A)
⊢ Eq (α := AddSubsemigroup A)
    ((toAddSubsemigroup' : (a : Subsemigroup (Multiplicative A)) → AddSubsemigroup A) (closure S) : AddSubsemigroup A)
    (AddSubsemigroup.closure ((⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' S) : AddSubsemigroup A)

Tactic:
le_antisymm
    (Subsemigroup.toAddSubsemigroup'.to_galoisConnection.l_le <|
      Subsemigroup.closure_le.2 <| AddSubsemigroup.subset_closure (M := A))
    (AddSubsemigroup.closure_le.2 <| Subsemigroup.subset_closure (M := Multiplicative A))

Premises used: Iff.mpr, OrderIso.to_galoisConnection, Subsemigroup.toAddSubsemigroup', AddSubsemigroup.subset_closure, GaloisConnection.l_le, Subsemigroup.closure_le, AddSubsemigroup.closure_le, le_antisymm, Subsemigroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
S_1 : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a b : M
ha : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) a
hb : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) b
rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ∈ S
⊢ Membership.mem (α := N) S ((f : (a : M) → N) (a * b) : N)

Tactic:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
S_1 : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a b : M
ha : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) a
hb : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) b
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ∈ S

Tactic:
mul_mem ha hb

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
S_1 : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a b : M
ha : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) a
hb : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) b
⊢ HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ∈ S

Tactic:
exact mul_mem ha hb

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
S : Subsemigroup N
f : M →ₙ* N
⊢ (↑(comap f S) : Set M) = (⇑f : (a : M) → N) ⁻¹' (↑S : Set N)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
S : Subsemigroup N
f : M →ₙ* N
x : M
⊢ x ∈ comap f S ↔ Membership.mem (α := N) S ((f : (a : M) → N) x : N)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
S : Subsemigroup P
g : N →ₙ* P
f : M →ₙ* N
⊢ comap f (comap g S) = comap (g.comp f) S

Tactic:
rfl

Premises used: Set.Mem, Subsemigroup.comap, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
P : Type u_3
inst : Mul P
S : Subsemigroup P
⊢ ∀ (x : P), x ∈ comap (MulHom.id P) S ↔ x ∈ S

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
S_1 : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ (↑S : Set M)
y : M
hy : y ∈ (↑S : Set M)
rw rw₁ :
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) =
    HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ (f : (a : M) → N) (x * y) = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
S_1 : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ (↑S : Set M)
y : M
hy : y ∈ (↑S : Set M)
⊢ Membership.mem (γ := Set N) ((⇑f : (a : M) → N) '' (↑S : Set M))
    (HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N))

Tactic:
exact ⟨x * y, @mul_mem (Subsemigroup M) M _ _ _ _ _ _ hx hy, by rw [map_mul]⟩
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
S : Subsemigroup M
⊢ (↑(map f S) : Set N) = (⇑f : (a : M) → N) '' (↑S : Set M)

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
S : Subsemigroup M
y : N
⊢ y ∈ map f S ↔ ∃ x ∈ S, (f : (a : M) → N) x = y

Tactic:
mem_image _ _ _

Premises used: Set.Mem, setOf, Set.mem_image, Set.image
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ S
⊢ Membership.mem (α := N) (map f S) ((f : (a : M) → N) x : N)

Tactic:
mem_image_of_mem f hx

Premises used: Set.Mem, setOf, Set.mem_image_of_mem, Set.image, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
S : Subsemigroup M
x : ↥S
⊢ Membership.mem (α := N) (map f S) ((f : (a : M) → N) (↑x : M) : N)

Tactic:
mem_map_of_mem f x.prop

Premises used: Subsemigroup.mem_map_of_mem, Subtype.prop
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : Mul M
inst_1 : Mul N
inst_2 : Mul P
S : Subsemigroup M
g : N →ₙ* P
f : M →ₙ* N
⊢ map g (map f S) = map (g.comp f) S

Tactic:
SetLike.coe_injective <| image_image _ _ _

Premises used: Set.image_image, SetLike.coe_injective
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : Subsemigroup M
x : M
⊢ Membership.mem (α := N) (map f S) ((f : (a : M) → N) x : N) ↔ x ∈ S

Tactic:
hf.mem_set_image

Premises used: Set.Mem, setOf, Set.image, Function.Injective.mem_set_image
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
S : Subsemigroup M
T : Subsemigroup N
⊢ map f S ≤ T ↔ S ≤ comap f T

Tactic:
image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _ _ =>
  map_le_iff_le_comap

Premises used: Subsemigroup.map_le_iff_le_comap, GaloisConnection
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
S : Subsemigroup M
T : Subsemigroup N
f : M →ₙ* N
⊢ S ≤ comap f T → map f S ≤ T

Tactic:
(gc_map_comap f).l_le

Premises used: Subsemigroup.gc_map_comap, GaloisConnection.l_le
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
S : Subsemigroup M
T : Subsemigroup N
f : M →ₙ* N
⊢ map f S ≤ T → S ≤ comap f T

Tactic:
(gc_map_comap f).le_u

Premises used: Subsemigroup.gc_map_comap, GaloisConnection.le_u
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
S : Subsemigroup M
f : M →ₙ* N
⊢ S ≤ comap f (map f S)

Tactic:
(gc_map_comap f).le_u_l _

Premises used: Subsemigroup.gc_map_comap, GaloisConnection.le_u_l
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
S : Subsemigroup N
f : M →ₙ* N
⊢ map f (comap f S) ≤ S

Tactic:
(gc_map_comap f).l_u_le _

Premises used: Subsemigroup.gc_map_comap, GaloisConnection.l_u_le
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
⊢ Monotone (map f)

Tactic:
(gc_map_comap f).monotone_l

Premises used: Subsemigroup.gc_map_comap, GaloisConnection.monotone_l
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : M →ₙ* N
⊢ Monotone (comap f)

Tactic:
(gc_map_comap f).monotone_u

Premises used: GaloisConnection.monotone_u, Subsemigroup.gc_map_comap
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
S : Subsemigroup M
f : M →ₙ* N
⊢ map f (comap f (map f S)) = map f S

Tactic:
(gc_map_comap f).l_u_l_eq_l _

Premises used: GaloisConnection.l_u_l_eq_l, Subsemigroup.gc_map_comap
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
S : Subsemigroup N
f : M →ₙ* N
⊢ comap f (map f (comap f S)) = comap f S

Tactic:
(gc_map_comap f).u_l_u_eq_u _

Premises used: Subsemigroup.gc_map_comap, GaloisConnection.u_l_u_eq_u