mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ ⋃ i ∈ s, ⋃ j ∈ t, {f i j}

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ ⋃ i ∈ s, ⋃ j ∈ t, {f i j}
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun x ↦ a⁻¹ * x) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun x ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun x ↦ a⁻¹ * x) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun x ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun x ↦ x * a⁻¹) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun x ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun x ↦ x * a⁻¹) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun x ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ⋃ a ∈ s, (fun b ↦ (a, b)) '' t

Tactic:
by
  rw [iUnion_image_left, image2_mk_eq_prod]

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ ((fun x ↦ Prod.swap ∘ x) ∘ Prod.mk '' t).seq s = ((fun b a ↦ (a, b)) '' t).seq s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ ((fun x ↦ Prod.swap ∘ x) ∘ Prod.mk '' t).seq s = ((fun b a ↦ (a, b)) '' t).seq s
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s * t⁻¹

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s * t⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
rintro ⟨rfl, hn⟩
    exact empty_zpow hn

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
b : α
⊢ (fun x ↦ x * b) ⁻¹' 1 = {b⁻¹}

Tactic:
by
  rw [← image_mul_right', image_one, one_mul]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ p x

Tactic:
by
  induction x using dense_induction s with
  | closure => exact closure
  | mem x hx => exact mem x hx
  | one => exact one
  | mul _ _ h₁ h₂ => exact mul _ _ h₁ h₂

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' (fun x ↦ x⁻¹) '' s = (fun x ↦ x⁻¹) '' ⇑f '' s

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' (fun x ↦ x⁻¹) '' s = (fun x ↦ x⁻¹) '' ⇑f '' s
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ (s.pi t)⁻¹ ↔ x ∈ s.pi fun i ↦ (t i)⁻¹

Tactic:
;

Goal state after:
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ (s.pi t)⁻¹ ↔ x ∈ s.pi fun i ↦ (t i)⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x * y⁻¹ ∈ H

Tactic:
;

Goal state after:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x * y⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toSubmonoid✝ : Submonoid G
inv_mem'✝ : ∀ {x : G}, x ∈ toSubmonoid✝.carrier → x⁻¹ ∈ toSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }) =
    { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }

Tactic:
;

Goal state after:
case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toSubmonoid✝ : Submonoid G
inv_mem'✝ : ∀ {x : G}, x ∈ toSubmonoid✝.carrier → x⁻¹ ∈ toSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }) =
    { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toAddSubmonoid✝ : AddSubmonoid (Additive G)
neg_mem'✝ : ∀ {x : Additive G}, x ∈ toAddSubmonoid✝.carrier → -x ∈ toAddSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }) =
    { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }

Tactic:
;

Goal state after:
case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toAddSubmonoid✝ : AddSubmonoid (Additive G)
neg_mem'✝ : ∀ {x : Additive G}, x ∈ toAddSubmonoid✝.carrier → -x ∈ toAddSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }) =
    { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toAddSubmonoid✝ : AddSubmonoid A
neg_mem'✝ : ∀ {x : A}, x ∈ toAddSubmonoid✝.carrier → -x ∈ toAddSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }) =
    { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }

Tactic:
;

Goal state after:
case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toAddSubmonoid✝ : AddSubmonoid A
neg_mem'✝ : ∀ {x : A}, x ∈ toAddSubmonoid✝.carrier → -x ∈ toAddSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }) =
    { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toSubmonoid✝ : Submonoid (Multiplicative A)
inv_mem'✝ : ∀ {x : Multiplicative A}, x ∈ toSubmonoid✝.carrier → x⁻¹ ∈ toSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }) =
    { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }

Tactic:
;

Goal state after:
case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toSubmonoid✝ : Submonoid (Multiplicative A)
inv_mem'✝ : ∀ {x : Multiplicative A}, x ∈ toSubmonoid✝.carrier → x⁻¹ ∈ toSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }) =
    { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N✝ : Type u_5
inst✝² : Group N✝
P : Type u_6
inst✝¹ : Group P
N : Type u_7
inst✝ : Group N
f : G →* N
H : Subgroup N
a : G
ha : a ∈ ⇑f ⁻¹' ↑H
⊢ (f a)⁻¹ ∈ H

Tactic:
;

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N✝ : Type u_5
inst✝² : Group N✝
P : Type u_6
inst✝¹ : Group P
N : Type u_7
inst✝ : Group N
f : G →* N
H : Subgroup N
a : G
ha : a ∈ ⇑f ⁻¹' ↑H
⊢ (f a)⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
h : Disjoint H K
⊢ Disjoint (map f H) (map f K)

Tactic:
by
  rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ↑K ∩ H.toSubsemigroup.1 = ↑(H ⊓ K)

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ↑K ∩ H.toSubsemigroup.1 = ↑(H ⊓ K)
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (K ⊓ H).subgroupOf K = H.subgroupOf K

Tactic:
inf_comm,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊓ K).subgroupOf K = H.subgroupOf K
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
x✝ : N
⊢ x✝ ∈ f.range ↔ x✝ ∈ map f ⊤

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
x✝ : N
⊢ x✝ ∈ f.range ↔ x✝ ∈ map f ⊤
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
g : N →* P
f : G →* N
⊢ map g (map f ⊤) = map (g.comp f) ⊤

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : Group G
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
g : N →* P
f : G →* N
⊢ map g (map f ⊤) = map (g.comp f) ⊤
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
s : Set N
x : G
hx : x ∈ ⇑f ⁻¹' s
⊢ f x ∈ closure s

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
s : Set N
x : G
hx : x ∈ ⇑f ⁻¹' s
⊢ f x ∈ closure s
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a

Tactic:
simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
    SetLike.mem_coe, forall_exists_index]

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : G) (x : ι), a ∈ S x → ∀ (b : G) (x : ι), b ∈ S x → a * b = b * a
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
M : Type u_7
inst✝ : MulOneClass M
f : G →* G'
g : G' →* M
h : g.comp f = 1
y : G
⊢ f y ∈ g.ker

Tactic:
;

Goal state after:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
M : Type u_7
inst✝ : MulOneClass M
f : G →* G'
g : G' →* M
h : g.comp f = 1
y : G
⊢ f y ∈ g.ker
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
hx : x ∈ comap f (map f H)
⊢ x ∈ H ⊔ f.ker

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
hx : x ∈ comap f (map f H)
⊢ x ∈ H ⊔ f.ker
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
y : C
hy : y ∈ s
z : C
hz : z ∈ t
⊢ y * z ∈ s ⊔ t

Tactic:
;

Goal state after:
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
y : C
hy : y ∈ s
z : C
hz : z ∈ t
⊢ y * z ∈ s ⊔ t
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ f.range ⊓ H = ⊥ ↔ H ⊓ f.range = ⊥

Tactic:
inf_comm

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ H ⊓ f.range = ⊥ ↔ H ⊓ f.range = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ s ⊔ t
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
;

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ s ⊔ t
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
y : G
hy : y ∈ s
z : G
hz : z ∈ t
⊢ y * z ∈ s ⊔ t

Tactic:
;

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
y : G
hy : y ∈ s
z : G
hz : z ∈ t
⊢ y * z ∈ s ⊔ t
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
x✝ : M
⊢ ((↑e).comp (powMonoidHom n)) x✝ = ((powMonoidHom n).comp ↑e) x✝

Tactic:
;

Goal state after:
M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
x✝ : M
⊢ ((↑e).comp (powMonoidHom n)) x✝ = ((powMonoidHom n).comp ↑e) x✝
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
toSubsemigroup✝ : Subsemigroup M
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
        { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) =
    { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }

Tactic:
;

Goal state after:
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
toSubsemigroup✝ : Subsemigroup M
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
        { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) =
    { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
toAddSubsemigroup✝ : AddSubsemigroup (Additive M)
zero_mem'✝ : 0 ∈ toAddSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
        { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) =
    { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }

Tactic:
;

Goal state after:
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
toAddSubsemigroup✝ : AddSubsemigroup (Additive M)
zero_mem'✝ : 0 ∈ toAddSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
        { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) =
    { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
toAddSubsemigroup✝ : AddSubsemigroup A
zero_mem'✝ : 0 ∈ toAddSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
        { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) =
    { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }

Tactic:
;

Goal state after:
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
toAddSubsemigroup✝ : AddSubsemigroup A
zero_mem'✝ : 0 ∈ toAddSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
        { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) =
    { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
toSubsemigroup✝ : Subsemigroup (Multiplicative A)
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
        { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) =
    { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }

Tactic:
;

Goal state after:
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
toSubsemigroup✝ : Subsemigroup (Multiplicative A)
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
        { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) =
    { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f a✝ * f b✝ ∈ S

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f a✝ * f b✝ ∈ S
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
⊢ 1 ∈ S

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
⊢ 1 ∈ S
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective ⇑f
H K : Submonoid M
h : Disjoint H K
⊢ Disjoint (map f H) (map f K)

Tactic:
by
  rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]

Goal state after:
Module: Mathlib.Data.Countable.Defs

Goal state before:
pp: α : Sort u
inst✝ : Nonempty α
⊢ Uncountable α ↔ ∀ (f : ℕ → α), ¬Surjective f

Tactic:
by
  rw [← not_countable_iff, countable_iff_exists_surjective, not_exists]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
x✝ : ↥M'
⊢ (domRestrict 1 M') x✝ = 1 x✝

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
x✝ : ↥M'
⊢ (domRestrict 1 M') x✝ = 1 x✝
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
x✝² x✝¹ : M →* A
x✝ : ↥M'
⊢ ((x✝² * x✝¹).domRestrict M') x✝ = (x✝².domRestrict M' * x✝¹.domRestrict M') x✝

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
x✝² x✝¹ : M →* A
x✝ : ↥M'
⊢ ((x✝² * x✝¹).domRestrict M') x✝ = (x✝².domRestrict M' * x✝¹.domRestrict M') x✝
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x y : Mˣ
⊢ ⟨↑x * ↑y, ⋯⟩ = ⟨↑x, ⋯⟩ * ⟨↑y, ⋯⟩

Tactic:
;

Goal state after:
M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x y : Mˣ
⊢ ⟨↑x * ↑y, ⋯⟩ = ⟨↑x, ⋯⟩ * ⟨↑y, ⋯⟩