awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
S T : Subsemigroup M
f : M →ₙ* N
⊢ map f (S ⊔ T) = map f S ⊔ map f T

Tactic:
(gc_map_comap f).l_sup

Premises used: Subsemigroup.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
ι : Sort u_5
f : M →ₙ* N
s : ι → Subsemigroup M
⊢ map f (iSup s) = ⨆ (i : ι), map f (s i)

Tactic:
(gc_map_comap f).l_iSup

Premises used: Subsemigroup.gc_map_comap, GaloisConnection.l_iSup
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
S T : Subsemigroup M
f : M →ₙ* N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ map f (S ⊓ T) = map f S ⊓ map f T

Tactic:
SetLike.coe_injective (Set.image_inter hf)

Premises used: Set.image_inter, 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
ι : Sort u_5
inst_2 : Nonempty ι
f : M →ₙ* N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
s : ι → Subsemigroup M
a : (↑(map f (iInf s)) : Set N) = (↑(⨅ (i : ι), map f (s i)) : Set N)
⊢ map f (iInf s) = ⨅ (i : ι), map f (s i)

Tactic:
apply SetLike.coe_injective

Premises used: 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
ι : Sort u_5
inst_2 : Nonempty ι
f : M →ₙ* N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
s : ι → Subsemigroup M
⊢ (↑(map f (iInf s)) : Set N) = (↑(⨅ (i : ι), map f (s i)) : Set N)

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Premises used: Set.InjOn.image_iInter_eq, Set.injOn_of_injective
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
S T : Subsemigroup N
f : M →ₙ* N
⊢ comap f (S ⊓ T) = comap f S ⊓ comap f T

Tactic:
(gc_map_comap f).u_inf

Premises used: Subsemigroup.gc_map_comap, GaloisConnection.u_inf
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
ι : Sort u_5
f : M →ₙ* N
s : ι → Subsemigroup N
⊢ comap f (iInf s) = ⨅ (i : ι), comap f (s i)

Tactic:
(gc_map_comap f).u_iInf

Premises used: Subsemigroup.gc_map_comap, GaloisConnection.u_iInf
-- 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
⊢ map f ⊥ = ⊥

Tactic:
(gc_map_comap f).l_bot

Premises used: Subsemigroup.gc_map_comap, GaloisConnection.l_bot
-- 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
⊢ comap f ⊤ = ⊤

Tactic:
(gc_map_comap f).u_top

Premises used: Subsemigroup.gc_map_comap, GaloisConnection.u_top
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
inst : Mul M
S : Subsemigroup M
⊢ map (MulHom.id M) S = S

Tactic:
ext fun _ => ⟨fun ⟨_, h, rfl⟩ => h, fun h => ⟨_, h, rfl⟩⟩

Premises used: Subsemigroup.ext, Membership.mem, _private.0.Subsemigroup.map_id.match_1, And.intro, Iff.intro, Exists.intro, rfl
-- 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
ι : Type u_5
f : M →ₙ* N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : Subsemigroup M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S

Tactic:
simp [mem_comap, mem_map, hf.eq_iff]

Premises used: Subsemigroup.mem_map, Function.Injective.eq_iff, Subsemigroup.mem_comap
-- 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
⊢ comap f (map f S) = S

Tactic:
(gciMapComap hf).u_l_eq _

Premises used: Subsemigroup.gciMapComap, GaloisCoinsertion.u_l_eq
-- 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)
⊢ Function.Surjective (comap f)

Tactic:
(gciMapComap hf).u_surjective

Premises used: Subsemigroup.gciMapComap, GaloisCoinsertion.u_surjective
-- 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)
⊢ Function.Injective (map f)

Tactic:
(gciMapComap hf).l_injective

Premises used: GaloisCoinsertion.l_injective, Subsemigroup.gciMapComap
-- 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 T : Subsemigroup M
⊢ comap f (map f S ⊓ map f T) = S ⊓ T

Tactic:
(gciMapComap hf).u_inf_l _ _

Premises used: Subsemigroup.gciMapComap, GaloisCoinsertion.u_inf_l
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
ι : Type u_5
f : M →ₙ* N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : ι → Subsemigroup M
⊢ comap f (⨅ (i : ι), map f (S i)) = iInf S

Tactic:
(gciMapComap hf).u_iInf_l _

Premises used: GaloisCoinsertion.u_iInf_l, Subsemigroup.gciMapComap
-- 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 T : Subsemigroup M
⊢ comap f (map f S ⊔ map f T) = S ⊔ T

Tactic:
(gciMapComap hf).u_sup_l _ _

Premises used: Subsemigroup.gciMapComap, GaloisCoinsertion.u_sup_l
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
ι : Type u_5
f : M →ₙ* N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : ι → Subsemigroup M
⊢ comap f (⨆ (i : ι), map f (S i)) = iSup S

Tactic:
(gciMapComap hf).u_iSup_l _

Premises used: Subsemigroup.gciMapComap, GaloisCoinsertion.u_iSup_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
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : Subsemigroup M
⊢ map f S ≤ map f T ↔ S ≤ T

Tactic:
(gciMapComap hf).l_le_l_iff

Premises used: GaloisCoinsertion.l_le_l_iff, Subsemigroup.gciMapComap
-- 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)
⊢ StrictMono (map f)

Tactic:
(gciMapComap hf).strictMono_l

Premises used: Subsemigroup.gciMapComap, GaloisCoinsertion.strictMono_l
-- 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
ι : Type u_5
f : M →ₙ* N
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : Subsemigroup N
x : N
h : x ∈ S
y : M
hy : (f : (a : M) → N) y = x
⊢ y ∈ comap f S ∧ (f : (a : M) → N) y = x

Tactic:
simp [hy, h]
-- 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.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : Subsemigroup N
⊢ map f (comap f S) = S

Tactic:
(giMapComap hf).l_u_eq _

Premises used: Subsemigroup.giMapComap, GaloisInsertion.l_u_eq
-- 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.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Function.Surjective (map f)

Tactic:
(giMapComap hf).l_surjective

Premises used: Subsemigroup.giMapComap, GaloisInsertion.l_surjective
-- 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.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Function.Injective (comap f)

Tactic:
(giMapComap hf).u_injective

Premises used: GaloisInsertion.u_injective, Subsemigroup.giMapComap
-- 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.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : Subsemigroup N
⊢ map f (comap f S ⊓ comap f T) = S ⊓ T

Tactic:
(giMapComap hf).l_inf_u _ _

Premises used: Subsemigroup.giMapComap, GaloisInsertion.l_inf_u
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
ι : Type u_5
f : M →ₙ* N
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : ι → Subsemigroup N
⊢ map f (⨅ (i : ι), comap f (S i)) = iInf S

Tactic:
(giMapComap hf).l_iInf_u _

Premises used: GaloisInsertion.l_iInf_u, Subsemigroup.giMapComap
-- 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.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : Subsemigroup N
⊢ map f (comap f S ⊔ comap f T) = S ⊔ T

Tactic:
(giMapComap hf).l_sup_u _ _

Premises used: GaloisInsertion.l_sup_u, Subsemigroup.giMapComap
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
ι : Type u_5
f : M →ₙ* N
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : ι → Subsemigroup N
⊢ map f (⨆ (i : ι), comap f (S i)) = iSup S

Tactic:
(giMapComap hf).l_iSup_u _

Premises used: Subsemigroup.giMapComap, GaloisInsertion.l_iSup_u
-- 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.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S T : Subsemigroup N
⊢ comap f S ≤ comap f T ↔ S ≤ T

Tactic:
(giMapComap hf).u_le_u_iff

Premises used: Subsemigroup.giMapComap, GaloisInsertion.u_le_u_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
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ StrictMono (comap f)

Tactic:
(giMapComap hf).strictMono_u

Premises used: GaloisInsertion.strictMono_u, Subsemigroup.giMapComap
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
inst : Mul M
⊢ Eq (α := ↥⊤ →ₙ* M) (↑topEquiv : ↥⊤ →ₙ* M) (MulMemClass.subtype ⊤)

Tactic:
rfl

Premises used: MulHomClass.toMulHom, MulMemClass.subtype, 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 M
f : M →ₙ* N
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : ↥S
⊢ Eq.{u_2 + 1} (α := N) ((↑((S.equivMapOfInjective f hf : (a : ↥S) → ↥(map f S)) x) : N) : N)
    ((f : (a : M) → N) (↑x : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
inst : Mul M
s : Set M
⊢ Eq (α := Subsemigroup ↥(closure s))
    (closure (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Subsemigroup M) (closure s) x) ⁻¹' s)) ⊤

Tactic:
eq_top_iff.2 fun x _ ↦ Subtype.recOn x fun _ hx' ↦
    closure_induction (fun _ h ↦ subset_closure h) (fun _ _ _ _ ↦ mul_mem) hx'

Premises used: Iff.mpr, eq_top_iff, Subtype.recOn
-- 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
⊢ (↑(s.prod t) : Set (M × N)) = (↑s : Set M) ×ˢ (↑t : Set N)

Tactic:
rfl

Premises used: setOf, Set.prod, 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 M
t : Subsemigroup N
p : M × N
⊢ p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.prod
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
s₁ s₂ : Subsemigroup M
t₁ t₂ : Subsemigroup N
hs : s₁ ≤ s₂
ht : t₁ ≤ t₂
⊢ s₁.prod t₁ ≤ s₂.prod t₂

Tactic:
Set.prod_mono hs ht

Premises used: Set.Mem, setOf, Set.prod, Set.Subset, Set.prod_mono
-- 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
x : M × N
⊢ Membership.mem (γ := Subsemigroup (M × N)) (s.prod ⊤) x ↔
    Membership.mem (γ := Subsemigroup (M × N)) (comap (MulHom.fst M N) s) x

Tactic:
simp [mem_prod, MulHom.coe_fst]

Premises used: MulHom.coe_fst, Subsemigroup.mem_prod
-- 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
x : M × N
⊢ Membership.mem (γ := Subsemigroup (M × N)) (prod ⊤ s) x ↔
    Membership.mem (γ := Subsemigroup (M × N)) (comap (MulHom.snd M N) s) x

Tactic:
simp [mem_prod, MulHom.coe_snd]

Premises used: MulHom.coe_snd, Subsemigroup.mem_prod
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
⊢ Eq (α := Subsemigroup (M × N)) (prod ⊤ ⊤) ⊤

Tactic:
(top_prod _).trans <| comap_top _

Premises used: Subsemigroup.top_prod, Subsemigroup.comap_top, Eq.trans
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
⊢ (↑(prod ⊥ ⊥) : Set (M × N)) = (↑⊥ : Set (M × N))

Tactic:
simp [coe_prod]

Premises used: Subsemigroup.coe_prod
-- 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
K : Subsemigroup M
x : N
⊢ Membership.mem (γ := Subsemigroup N) (map (↑f : M →ₙ* N) K) x ↔
    Membership.mem (α := M) K ((f.symm : (a : N) → M) x : M)

Tactic:
@Set.mem_image_equiv _ _ (K : Set M) f.toEquiv x

Premises used: Set.Mem, setOf, Set.image, Set.mem_image_equiv
-- 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
K : Subsemigroup M
⊢ Eq (α := Subsemigroup N) (map (↑f : M →ₙ* N) K) (comap (↑f.symm : N →ₙ* M) K)

Tactic:
SetLike.coe_injective (f.toEquiv.image_eq_preimage_symm K)

Premises used: MulEquiv.toEquiv, SetLike.coe_injective, Equiv.image_eq_preimage_symm, SetLike.coe
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
f : N ≃* M
K : Subsemigroup M
⊢ Eq (α := Subsemigroup N) (comap (↑f : N →ₙ* M) K) (map (↑f.symm : M →ₙ* N) K)

Tactic:
(map_equiv_eq_comap_symm f.symm K).symm

Premises used: Subsemigroup.map_equiv_eq_comap_symm, Equiv.symm, Eq.symm, MulEquiv.symm
-- 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
⊢ Eq (α := Subsemigroup N) (map (↑f : M →ₙ* N) ⊤) ⊤

Tactic:
SetLike.coe_injective <| Set.image_univ.trans f.surjective.range_eq

Premises used: Set.image_univ, MulEquiv.surjective, SetLike.coe_injective, Function.Surjective.range_eq, Eq.trans
-- 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
u : Subsemigroup (M × N)
mp : u ≤ s.prod t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
mpr : map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ s.prod t
⊢ u ≤ s.prod t ↔ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
constructor
-- 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
u : Subsemigroup (M × N)
h : u ≤ s.prod t
mp : map (fst M N) u ≤ s
mp₁ : map (snd M N) u ≤ t
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
constructor
-- 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
u : Subsemigroup (M × N)
h : u ≤ s.prod t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ (↑u : Set (M × N))
⊢ Membership.mem (α := M) s ((fst M N : (a : M × N) → M) (y1, y2) : M)

Tactic:
(h hy1).1

Premises used: Set.Mem, And.left
-- 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
u : Subsemigroup (M × N)
h : u ≤ s.prod t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ (↑u : Set (M × N))
⊢ Membership.mem (α := M) s ((fst M N : (a : M × N) → M) (y1, y2) : M)

Tactic:
exact (h hy1).1

Premises used: And.left
-- 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
u : Subsemigroup (M × N)
h : u ≤ s.prod t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ (↑u : Set (M × N))
⊢ Membership.mem (α := N) t ((snd M N : (a : M × N) → N) (y1, y2) : N)

Tactic:
(h hy1).2

Premises used: Set.Mem, And.right
-- 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
u : Subsemigroup (M × N)
h : u ≤ s.prod t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ (↑u : Set (M × N))
⊢ Membership.mem (α := N) t ((snd M N : (a : M × N) → N) (y1, y2) : N)

Tactic:
exact (h hy1).2

Premises used: And.right
-- 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
u : Subsemigroup (M × N)
hH : map (fst M N) u ≤ s
hK : map (snd M N) u ≤ t
x1 : M
x2 : N
h : (x1, x2) ∈ u
⊢ (x1, x2) ∈ s.prod t

Tactic:
⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

Premises used: Set.Mem, setOf, Set.prod, And.intro, Exists.intro, 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 M
t : Subsemigroup N
u : Subsemigroup (M × N)
hH : map (fst M N) u ≤ s
hK : map (snd M N) u ≤ t
x1 : M
x2 : N
h : (x1, x2) ∈ u
⊢ (x1, x2) ∈ s.prod t

Tactic:
exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, 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
⊢ (↑f.srange : Set N) = Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: setOf, Set.range, 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
y : N
⊢ y ∈ f.srange ↔ ∃ (x : M), (f : (a : M) → N) x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- 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 : ∀ (x y : M), f (x * y) = f x * f y
x y : N
hx : x ∈ Set.range f
hy : y ∈ Set.range f
⊢ x * y ∈ Set.range f

Tactic:
(srange ⟨f, hf⟩).mul_mem hx hy

Premises used: Subsemigroup.mul_mem, Set.Mem, setOf, MulHom.mk, MulHom.srange, Set.range
-- 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 : Subsemigroup M
f : M → N
hf : ∀ (x y : M), f (x * y) = f x * f y
a b : N
⊢ a ∈ Set.range f → b ∈ Set.range f → a * b ∈ Set.range f

Tactic:
srange_mk_aux_mul hf

Premises used: _private.0.MulHom.srange_mk_aux_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 : Subsemigroup M
f : M → N
hf : ∀ (x y : M), f (x * y) = f x * f y
⊢ ∀ {a b : N}, a ∈ Set.range f → b ∈ Set.range f → a * b ∈ Set.range f

Tactic:
exact srange_mk_aux_mul hf

Premises used: _private.0.MulHom.srange_mk_aux_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
hf : ∀ (x y : M), f (x * y) = f x * f y
⊢ { toFun := f, map_mul' := hf : M →ₙ* N }.srange = { carrier := Set.range f, mul_mem' := ⋯ }

Tactic:
rfl

Premises used: Subsemigroup.copy, MulHom.srange, 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
⊢ f.srange = map f ⊤

Tactic:
copy_eq _

Premises used: MulHom.srange, Subsemigroup.copy_eq
-- 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
g : N →ₙ* P
f : M →ₙ* N
⊢ map g f.srange = (g.comp f).srange

Tactic:
simpa only [srange_eq_map] using (⊤ : Subsemigroup M).map_map g f

Premises used: Subsemigroup.map_map, MulHom.srange_eq_map, Top.top
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
inst : Mul M
N : Type u_5
inst_1 : Mul N
f : M →ₙ* N
rw :
  Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
    Eq.{u_5 + 1} (α := Set N) (Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
rw₁ rw₂ :
  Eq.{u_5 + 1} (α := Set N) (Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ ↔
    Eq.{u_5 + 1} (α := Set N) (Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
⊢ (↑f.srange : Set N) = (↑⊤ : Set N) ↔
    Eq.{u_5 + 1} (α := Set N) (Set.range.{u_5, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ

Tactic:
rw [coe_srange, coe_top]

Premises used: MulHom.coe_srange, Subsemigroup.coe_top
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
inst : Mul M
N : Type u_5
inst_1 : Mul N
f : M →ₙ* N
hf : Function.Surjective.{u_1 + 1, u_5 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ f.srange = ⊤

Tactic:
srange_eq_top_iff_surjective.2 hf

Premises used: Iff.mpr, MulHom.srange_eq_top_iff_surjective
-- 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 : Set N
⊢ closure ((⇑f : (a : M) → N) ⁻¹' s) ≤ comap f (closure s)

Tactic:
closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

Premises used: Iff.mpr, Subsemigroup.closure_le, Subsemigroup.mem_comap, Subsemigroup.subset_closure, SetLike.mem_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 : Set M
⊢ map f (closure s) = closure ((⇑f : (a : M) → N) '' s)

Tactic:
Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Subsemigroup.gi N).gc (Subsemigroup.gi M).gc
    fun _ ↦ rfl

Premises used: GaloisConnection.l_comm_of_u_comm, Subsemigroup.gc_map_comap, Subsemigroup.gi, Set.image_preimage, rfl, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
σ : Type u_4
inst : Mul M
N : Type u_5
inst_1 : Mul N
inst_2 : SetLike σ M
inst_3 : MulMemClass σ M
f : M →ₙ* N
S : σ
x : ↥S
⊢ Eq.{u_5 + 1} (α := N) ((f.restrict S : (a : ↥S) → N) x : N) ((f : (a : M) → N) (↑x : M) : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
inst : Mul M
N : Type u_5
inst_1 : Mul N
f : M →ₙ* N
x : M
⊢ Eq.{u_5 + 1} (α := N) ((↑((f.srangeRestrict : (a : M) → ↥f.srange) x) : N) : N) ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: 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
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := ↥f.srange) (⇑f.srangeRestrict : (a : M) → ↥f.srange)

Tactic:
fun ⟨_, ⟨x, rfl⟩⟩ => ⟨x, rfl⟩

Premises used: Exists, _private.0.MulHom.srangeRestrict_surjective.match_1, Exists.intro, Eq, DFunLike.coe, Function.Surjective, MulHom.srangeRestrict, rfl
-- Module: Mathlib.Algebra.Group.Subsemigroup.Operations
Goal:
M : Type u_1
N : Type u_2
inst : Mul M
inst_1 : Mul N
M' : Type u_5
N' : Type u_6
inst_2 : Mul M'
inst_3 : Mul N'
f : M →ₙ* N
g : M' →ₙ* N'
S : Subsemigroup N
S' : Subsemigroup N'
⊢ comap (f.prodMap g) (S.prod S') = (comap f S).prod (comap g S')

Tactic:
SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _

Premises used: SetLike.coe_injective, Set.preimage_prod_map_prod, DFunLike.coe