awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
N : Type u_4
inst : CommMonoid N
s t : Submonoid N
rw : s ⊔ t = map (s.subtype.coprod t.subtype) ⊤
rw₁ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t) ⊔ mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₂ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₃ :
  s ⊔ t =
    mrange ((s.subtype.coprod t.subtype).comp (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₄ : s ⊔ t = mrange s.subtype ⊔ map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₅ : s ⊔ t = mrange s.subtype ⊔ mrange ((s.subtype.coprod t.subtype).comp (inr ↥s ↥t))
rw₆ : s ⊔ t = mrange s.subtype ⊔ mrange t.subtype
rw₇ : s ⊔ t = s ⊔ mrange t.subtype
rw₈ rw₉ : s ⊔ t = s ⊔ t
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)

Tactic:
rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
    coprod_comp_inr, mrange_subtype, mrange_subtype]

Premises used: MonoidHom.coprod_comp_inr, Submonoid.mrange_inl_sup_mrange_inr, MonoidHom.mrange_eq_map, Submonoid.mrange_subtype, Submonoid.map_sup, MonoidHom.map_mrange, MonoidHom.coprod_comp_inl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
N : Type u_4
inst : CommMonoid N
s t : Submonoid N
x : N
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
simp only [sup_eq_range, mem_mrange, coprod_apply, coe_subtype, Prod.exists,
    Subtype.exists, exists_prop]

Premises used: MonoidHom.coprod_apply, Subtype.exists, Submonoid.coe_subtype, exists_prop, Prod.exists, Submonoid.sup_eq_range, MonoidHom.mem_mrange
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
N : Type u_4
inst : CommMonoid N
P : N → Prop
s t : Submonoid N
simp : (∀ (x x_1 : N), x_1 ∈ s → ∀ x_2 ∈ t, x_1 * x_2 = x → P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)
⊢ (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)

Tactic:
simp [mem_sup]

Premises used: Submonoid.mem_sup
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
N : Type u_4
inst : CommMonoid N
P : N → Prop
s t : Submonoid N
⊢ (∀ (x x_1 : N), x_1 ∈ s → ∀ x_2 ∈ t, x_1 * x_2 = x → P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
N : Type u_4
inst : CommMonoid N
P : N → Prop
s t : Submonoid N
⊢ (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ * x₂)

Tactic:
simp [mem_sup]

Premises used: Submonoid.mem_sup
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
A : Type u_2
inst : AddMonoid A
x : A
⊢ Eq (α := AddSubmonoid A) (closure {x})
    (AddMonoidHom.mrange (F := ℕ →+ A) ((multiplesHom A : (a : A) → ℕ →+ A) x : ℕ →+ A))

Tactic:
closure_eq_of_le (Set.singleton_subset_iff.2 ⟨1, one_nsmul x⟩) fun _ ⟨_n, hn⟩ =>
    hn ▸ nsmul_mem (subset_closure <| Set.mem_singleton _) _

Premises used: Iff.mpr, Set.mem_singleton, Set.singleton_subset_iff, _private.0.AddSubmonoid.closure_singleton_eq.match_1, AddSubmonoid.subset_closure, Membership.mem, Eq.rec, nsmul_mem, AddSubmonoid.closure, Exists.intro, AddSubmonoid.closure_eq_of_le, Singleton.singleton, OfNat.ofNat, one_nsmul
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
A : Type u_2
inst : AddMonoid A
x y : A
rw : (∃ (x_1 : ℕ), (((multiplesHom A : (a : A) → ℕ →+ A) x : ℕ →+ A) : (a : ℕ) → A) x_1 = y) ↔ ∃ (n : ℕ), n • x = y
⊢ Membership.mem (γ := AddSubmonoid A) (closure {x}) y ↔ ∃ (n : ℕ), n • x = y

Tactic:
rw [closure_singleton_eq, AddMonoidHom.mem_mrange]

Premises used: AddSubmonoid.closure_singleton_eq, AddMonoidHom.mem_mrange
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
A : Type u_2
inst : AddMonoid A
x y : A
⊢ (∃ (x_1 : ℕ), (((multiplesHom A : (a : A) → ℕ →+ A) x : ℕ →+ A) : (a : ℕ) → A) x_1 = y) ↔ ∃ (n : ℕ), n • x = y

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
A : Type u_2
inst : AddMonoid A
⊢ Eq (α := AddSubmonoid A) (closure {0}) ⊥

Tactic:
simp [eq_bot_iff_forall, mem_closure_singleton, nsmul_zero]

Premises used: nsmul_zero, AddSubmonoid.mem_closure_singleton, AddSubmonoid.eq_bot_iff_forall
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
A : Type u_2
B : Type u_3
inst : AddMonoid A
x n : A
i : ℕ
⊢ (fun (i : ℕ) ↦ i • x) i = n ↔ (((multiplesHom A : (a : A) → ℕ →+ A) x : ℕ →+ A) : (a : ℕ) → A) i = n

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
A : Type u_4
inst : CommMonoid A
a b c : A
rw :
  (∃ (y : A),
      Membership.mem (γ := Submonoid A) (closure {a}) y ∧
        ∃ (z : A), Membership.mem (γ := Submonoid A) (closure {b}) z ∧ y * z = c) ↔
    ∃ (m : ℕ) (n : ℕ), a ^ m * b ^ n = c
⊢ Membership.mem (γ := Submonoid A) (closure {a, b}) c ↔ ∃ (m : ℕ) (n : ℕ), a ^ m * b ^ n = c

Tactic:
rw [← Set.singleton_union, Submonoid.closure_union, mem_sup]

Premises used: Submonoid.mem_sup, Set.singleton_union, Submonoid.closure_union
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
A : Type u_4
inst : CommMonoid A
a b c : A
simp_rw :
  (∃ (y : A), (∃ (n : ℕ), a ^ n = y) ∧ ∃ (z : A), (∃ (n : ℕ), b ^ n = z) ∧ y * z = c) ↔
    ∃ (m : ℕ) (n : ℕ), a ^ m * b ^ n = c
⊢ (∃ (y : A),
      Membership.mem (γ := Submonoid A) (closure {a}) y ∧
        ∃ (z : A), Membership.mem (γ := Submonoid A) (closure {b}) z ∧ y * z = c) ↔
    ∃ (m : ℕ) (n : ℕ), a ^ m * b ^ n = c

Tactic:
simp_rw [mem_closure_singleton, exists_exists_eq_and]

Premises used: Submonoid.mem_closure_singleton, exists_exists_eq_and
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
x : M
h :
  ∀ (x_1 : Additive M),
    Membership.mem (γ := Set (Additive M)) ((⇑Additive.ofMul : (a : M) → Additive M) '' (↑(Submonoid.powers x) : Set M))
        x_1 ↔
      x_1 ∈
        (↑(AddSubmonoid.multiples ((Additive.ofMul : (a : M) → Additive M) x) : AddSubmonoid (Additive M)) :
          Set (Additive M))
⊢ (⇑Additive.ofMul : (a : M) → Additive M) '' (↑(Submonoid.powers x) : Set M) =
    (↑(AddSubmonoid.multiples ((Additive.ofMul : (a : M) → Additive M) x) : AddSubmonoid (Additive M)) :
      Set (Additive M))

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
x : M
x_1 : Additive M
⊢ Membership.mem (γ := Set (Additive M)) ((⇑Additive.ofMul : (a : M) → Additive M) '' (↑(Submonoid.powers x) : Set M))
      x_1 ↔
    x_1 ∈
      (↑(AddSubmonoid.multiples ((Additive.ofMul : (a : M) → Additive M) x) : AddSubmonoid (Additive M)) :
        Set (Additive M))

Tactic:
Set.mem_image_iff_of_inverse (congrFun rfl) (congrFun rfl)

Premises used: Set.Mem, Additive, congrFun, Set.mem_image_iff_of_inverse, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
M : Type u_1
inst : Monoid M
x : M
x_1 : Additive M
⊢ Membership.mem (γ := Set (Additive M)) ((⇑Additive.ofMul : (a : M) → Additive M) '' (↑(Submonoid.powers x) : Set M))
      x_1 ↔
    x_1 ∈
      (↑(AddSubmonoid.multiples ((Additive.ofMul : (a : M) → Additive M) x) : AddSubmonoid (Additive M)) :
        Set (Additive M))

Tactic:
exact Set.mem_image_iff_of_inverse (congrFun rfl) (congrFun rfl)

Premises used: congrFun, Set.mem_image_iff_of_inverse, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
A : Type u_2
inst : AddMonoid A
x : A
symm :
  (↑(Submonoid.powers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Submonoid (Multiplicative A)) :
      Set (Multiplicative A)) =
    (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) '' (↑(AddSubmonoid.multiples x) : Set A)
⊢ (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) '' (↑(AddSubmonoid.multiples x) : Set A) =
    (↑(Submonoid.powers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Submonoid (Multiplicative A)) :
      Set (Multiplicative A))

Tactic:
symm
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
A : Type u_2
inst : AddMonoid A
x : A
rw :
  (⇑(Equiv.symm Multiplicative.ofAdd) : (a : Multiplicative A) → A) ''
      (↑(Submonoid.powers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Submonoid (Multiplicative A)) :
        Set (Multiplicative A)) =
    (↑(AddSubmonoid.multiples x) : Set A)
⊢ (↑(Submonoid.powers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Submonoid (Multiplicative A)) :
      Set (Multiplicative A)) =
    (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) '' (↑(AddSubmonoid.multiples x) : Set A)

Tactic:
rw [Equiv.eq_image_iff_symm_image_eq]

Premises used: Equiv.eq_image_iff_symm_image_eq
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
A : Type u_2
inst : AddMonoid A
x : A
⊢ (⇑(Equiv.symm Multiplicative.ofAdd) : (a : Multiplicative A) → A) ''
      (↑(Submonoid.powers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Submonoid (Multiplicative A)) :
        Set (Multiplicative A)) =
    (↑(AddSubmonoid.multiples x) : Set A)

Tactic:
ofMul_image_powers_eq_multiples_ofMul

Premises used: Additive, ofMul_image_powers_eq_multiples_ofMul, Multiplicative
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
A : Type u_2
inst : AddMonoid A
x : A
⊢ (⇑(Equiv.symm Multiplicative.ofAdd) : (a : Multiplicative A) → A) ''
      (↑(Submonoid.powers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Submonoid (Multiplicative A)) :
        Set (Multiplicative A)) =
    (↑(AddSubmonoid.multiples x) : Set A)

Tactic:
exact ofMul_image_powers_eq_multiples_ofMul

Premises used: ofMul_image_powers_eq_multiples_ofMul
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
h :
  ∀ (x : ℕ),
    Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure {1}) x ↔ Membership.mem (γ := AddSubmonoid ℕ) ⊤ x
⊢ Eq (α := AddSubmonoid ℕ) (AddSubmonoid.closure {1}) ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Submonoid.Membership
Goal:
x : ℕ
⊢ Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure {1}) x ↔ Membership.mem (γ := AddSubmonoid ℕ) ⊤ x

Tactic:
simp [AddSubmonoid.mem_closure_singleton]

Premises used: AddSubmonoid.mem_closure_singleton
-- Module: Mathlib.Algebra.Group.Submonoid.MulAction
Goal:
M' : Type u_1
α : Type u_2
β : Type u_3
S' : Type u_4
inst : SetLike S' M'
s : S'
inst_1 : MulOneClass M'
inst_2 : SMul M' β
inst_3 : SMul α β
inst_4 : SMulCommClass M' α β
⊢ SMulCommClass.{u_1, u_2, u_3} (↥s) α β

Tactic:
⟨fun a _ _ => smul_comm (a : M') _ _⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val
-- Module: Mathlib.Algebra.Group.Submonoid.MulAction
Goal:
M' : Type u_1
α : Type u_2
β : Type u_3
S' : Type u_4
inst : SetLike S' M'
s : S'
inst_1 : MulOneClass M'
inst_2 : SMul α β
inst_3 : SMul M' β
inst_4 : SMulCommClass α M' β
⊢ SMulCommClass.{u_2, u_1, u_3} α (↥s) β

Tactic:
⟨fun a s => smul_comm a (s : M')⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, Subtype.val
-- Module: Mathlib.Algebra.Group.Submonoid.MulAction
Goal:
M' : Type u_1
α : Type u_2
β : Type u_3
S' : Type u_4
inst : SetLike S' M'
s : S'
inst_1 : MulOneClass M'
inst_2 : SMul α β
inst_3 : SMul M' α
inst_4 : SMul M' β
inst_5 : IsScalarTower M' α β
⊢ IsScalarTower.{u_1, u_2, u_3} (↥s) α β

Tactic:
⟨fun a => smul_assoc (a : M')⟩

Premises used: smul_assoc, IsScalarTower.mk, Subtype.val
-- Module: Mathlib.Algebra.Group.Submonoid.MulAction
Goal:
M' : Type u_1
α : Type u_2
β : Type u_3
inst : MulOneClass M'
inst_1 : SMul M' β
inst_2 : SMul α β
inst_3 : SMulCommClass M' α β
S : Submonoid M'
⊢ SMulCommClass.{u_1, u_2, u_3} (↥S) α β

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Group.Submonoid.MulAction
Goal:
M' : Type u_1
α : Type u_2
β : Type u_3
inst : MulOneClass M'
inst_1 : SMul α β
inst_2 : SMul M' β
inst_3 : SMulCommClass α M' β
S : Submonoid M'
⊢ SMulCommClass.{u_2, u_1, u_3} α (↥S) β

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Group.Submonoid.MulAction
Goal:
M' : Type u_1
α : Type u_2
β : Type u_3
inst : MulOneClass M'
inst_1 : SMul α β
inst_2 : SMul M' α
inst_3 : SMul M' β
inst_4 : IsScalarTower M' α β
S : Submonoid M'
⊢ IsScalarTower.{u_1, u_2, u_3} (↥S) α β

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Group.Submonoid.MulAction
Goal:
M' : Type u_1
α : Type u_2
inst : MulOneClass M'
inst_1 : SMul M' α
S : Submonoid M'
g : ↥S
a : α
⊢ g • a = (↑g : M') • a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.MulAction
Goal:
M' : Type u_1
α : Type u_2
inst : MulOneClass M'
inst_1 : SMul M' α
S : Submonoid M'
g : M'
hg : g ∈ S
a : α
⊢ Subtype.mk (p := fun (x : M') ↦ x ∈ S) g hg • a = g • a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Submonoid.MulAction
Goal:
M' : Type u_1
α : Type u_2
β_1 : Type u_3
inst : Monoid M'
β : Type u_4
S : Type u_5
inst_1 : SMul M' α
inst_2 : SMul M' β
inst_3 : SMul α β
inst_4 : SetLike S M'
h : SMulDistribClass M' α β
N' : S
⊢ SMulDistribClass.{u_1, u_2, u_4} (↥N') α β

Tactic:
⟨fun g _ _ ↦ h.smul_distrib_smul g _ _⟩

Premises used: SMulDistribClass.smul_distrib_smul, SMulDistribClass.mk, Subtype.val
-- Module: Mathlib.Algebra.Group.Submonoid.MulAction
Goal:
M' : Type u_1
α : Type u_2
β : Type u_3
inst : Monoid M'
S : Submonoid M'
⊢ IsScalarTower (↥S) M' M'

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
x : Mᵐᵒᵖ
S : Submonoid M
⊢ x ∈ S.op ↔ MulOpposite.unop x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
H : Submonoid M
⊢ H.op.toSubsemigroup = H.op

Tactic:
rfl

Premises used: Subsemigroup.op, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
x : M
S : Submonoid Mᵐᵒᵖ
⊢ x ∈ S.unop ↔ MulOpposite.op x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Group.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
H : Submonoid Mᵐᵒᵖ
⊢ H.unop.toSubsemigroup = H.unop

Tactic:
rfl

Premises used: Subsemigroup.unop, rfl
-- Module: Mathlib.Algebra.Group.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
S : Submonoid M
⊢ S.op.unop = S

Tactic:
rfl

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

Tactic:
rfl

Premises used: Set.Mem, Submonoid.op, MulOpposite, setOf, Set.preimage, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
S₁ : Submonoid M
S₂ : Submonoid 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.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
S₁ : Submonoid Mᵐᵒᵖ
S₂ : Submonoid 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.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
S₁ S₂ : Submonoid 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.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
S₁ S₂ : Submonoid 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.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := Submonoid M) Submonoid.op

Tactic:
opEquiv.injective

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

Tactic:
opEquiv.symm.injective

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

Tactic:
opEquiv.eq_iff_eq

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

Tactic:
opEquiv.symm.eq_iff_eq

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

Tactic:
opEquiv.map_bot

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

Tactic:
op_injective.eq_iff' op_bot

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

Tactic:
opEquiv.symm.map_bot

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

Tactic:
unop_injective.eq_iff' unop_bot

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

Tactic:
rfl

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

Tactic:
op_injective.eq_iff' op_top

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

Tactic:
rfl

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

Tactic:
unop_injective.eq_iff' unop_top

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

Tactic:
opEquiv.map_sup _ _

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

Tactic:
opEquiv.symm.map_sup _ _

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
opEquiv.map_sSup_eq_sSup_symm_preimage _

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

Tactic:
opEquiv.symm.map_sSup_eq_sSup_symm_preimage _

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

Tactic:
opEquiv.map_sInf_eq_sInf_symm_preimage _

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

Tactic:
opEquiv.symm.map_sInf_eq_sInf_symm_preimage _

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

Tactic:
opEquiv.map_iSup _

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

Tactic:
opEquiv.symm.map_iSup _

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

Tactic:
opEquiv.map_iInf _

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

Tactic:
opEquiv.symm.map_iInf _

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

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

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

Tactic:
congr with a
-- Module: Mathlib.Algebra.Group.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
s : Set M
a : Submonoid 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.Submonoid.MulOpposite
Goal:
M : Type u_2
inst : MulOneClass M
s : Set M
a : Submonoid 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