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

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
r' : Finset α
hnr' : n < r'.card
hr' : r' ⊆ ⋯.toFinset ∨ r' ⊆ ⋯.toFinset
⊢ n < (↑r').ncard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
r' : Finset α
hnr' : n < r'.card
hr' : r' ⊆ ⋯.toFinset ∨ r' ⊆ ⋯.toFinset
⊢ ↑r' ⊆ s ∨ ↑r' ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Finset α
hs : ↑s.card < ENat.card α
⊢ ∃ a, a ∉ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.ncard = 1

Tactic:
rw [ncard_singleton]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (∃ a, s = {a}) → s.ncard = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 1 ↔ ∃ a, s = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
ncard_le_one hs

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
hs : ∅.Finite
⊢ ∅.ncard ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Nonempty α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∃ x, s ⊆ {x}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
⊢ ∀ (a : ↥(H ⊔ N)), ∃ a_1, φ a_1 = Quotient.mk'' a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
s : Set α
⊢ s.ncard ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Finite ↑s
⊢ 1 < s.ncard ↔ s.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ 1 < s.ncard ↔ s.Nontrivial ∧ s.Finite

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ✝ : G →* H✝
H N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
φ_surjective : Surjective ⇑φ
⊢ N.subgroupOf H = φ.ker

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 1 < s.ncard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hn : 0 < s.ncard
he : Even s.ncard
h : s.ncard = 1
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hn : s.Nonempty
he : Even s.ncard
⊢ 1 < s.ncard

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M✝ : Type x
inst✝ : Monoid M✝
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
⊢ Subgroup.map (mk' N) M ≤ (map N M (MonoidHom.id G) h).ker

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 2 < s.ncard ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 2 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M✝ : Type x
inst✝ : Monoid M✝
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
⊢ (map M (Subgroup.map (mk' N) M) (mk' N) ⋯).comp (quotientQuotientEquivQuotientAux N M h) =
    MonoidHom.id ((G ⧸ N) ⧸ Subgroup.map (mk' N) M)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 3 < s.ncard ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M✝ : Type x
inst✝ : Monoid M✝
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
⊢ (quotientQuotientEquivQuotientAux N M h).comp (map M (Subgroup.map (mk' N) M) (mk' N) ⋯) = MonoidHom.id (G ⧸ M)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 3 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup (G ⧸ N)
⊢ N ≤ Subgroup.comap (mk' N) H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
N H : Subgroup G
inst✝ : N.Normal
⊢ Subgroup.comap (mk' N) (Subgroup.map (mk' N) H) = N ⊔ H

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : 1 < s.ncard
a : α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
φ : G →* H
N : Subgroup G
hn : N.Normal
H' : Subgroup (G ⧸ N)
⊢ H' ≤ (mk' N).range

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N✝ : Subgroup G
nN : N✝.Normal
H✝ : Type v
inst✝¹ : Group H✝
M : Type x
inst✝ : Monoid M
φ : G →* H✝
N : Subgroup G
hn : N.Normal
x✝ : { H // N ≤ H }
H : Subgroup G
hH : N ≤ H
⊢ ↑((fun H' ↦ ⟨Subgroup.comap (mk' N) H', ⋯⟩) ((fun H ↦ Subgroup.map (mk' N) ↑H) ⟨H, hH⟩)) = ↑⟨H, hH⟩

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝ : Group G
⊢ Subsingleton (G ⧸ ⊤)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝ : Group G
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
⊢ x ∈ H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
H₁ : Subgroup G
inst✝¹ : H₁.Normal
H₂ : Subgroup (G ⧸ H₁)
inst✝ : H₂.Normal
⊢ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) =
    Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H✝ : Type v
inst✝³ : Group H✝
M : Type x
inst✝² : Monoid M
φ : G →* H✝
A : Type u_1
inst✝¹ : CommGroup A
H : Subgroup G
inst✝ : H.Normal
x✝ : ↥(domRestrictHom H A).ker
f : G →* A
hf : f ∈ (domRestrictHom H A).ker
⊢ H ≤ f.ker

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H✝ : Type v
inst✝³ : Group H✝
M : Type x
inst✝² : Monoid M
φ : G →* H✝
A : Type u_1
inst✝¹ : CommGroup A
H : Subgroup G
inst✝ : H.Normal
x✝ : ↥(domRestrictHom H A).ker
⊢ (fun f ↦ ⟨f.comp (mk' H), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨f, hf⟩ => lift H f ⋯)
        x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
hs : s.Finite
⊢ s.ncard = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H
x y : G × H
⊢ x ∈ {x | f x.1 = x.2} → y ∈ {x | f x.1 = x.2} → x * y ∈ {x | f x.1 = x.2}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
⊢ f.mgraph = mrange ((id G).prod f)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H✝ : Type v
inst✝³ : Group H✝
M : Type x
inst✝² : Monoid M
φ : G →* H✝
A : Type u_1
inst✝¹ : CommGroup A
H : Subgroup G
inst✝ : H.Normal
x✝ : G ⧸ H →* A
⊢ (fun x ↦
        match x with
        | ⟨f, hf⟩ => lift H f ⋯)
      ((fun f ↦ ⟨f.comp (mk' H), ⋯⟩) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁴ : Group G
N : Subgroup G
nN : N.Normal
H✝ : Type v
inst✝³ : Group H✝
M : Type x
inst✝² : Monoid M
φ : G →* H✝
A : Type u_1
inst✝¹ : CommGroup A
H : Subgroup G
inst✝ : H.Normal
x✝¹ x✝ : ↥(domRestrictHom H A).ker
⊢ (match x✝¹ * x✝ with
    | ⟨f, hf⟩ => lift H f ⋯) =
    (match x✝¹ with
      | ⟨f, hf⟩ => lift H f ⋯) *
      match x✝ with
      | ⟨f, hf⟩ => lift H f ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℕ
a : R
⊢ ↑(↑n * a) = n • ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ y, f y = (a, b)) ↔ f' a = b
g₁ g₂ : G
⊢ f (g₁ * g₂) = ((Prod.fst ∘ ⇑f) g₁ * (Prod.fst ∘ ⇑f) g₂, f' ((Prod.fst ∘ ⇑f) g₁) * f' ((Prod.fst ∘ ⇑f) g₂))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℤ
a : R
⊢ ↑(↑n * a) = n • ↑a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝ : (i : ι) → CommGroup (A i)
n : ℕ
⊢ (fun x ↦ ↑(1 x)) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ y, f y = (a, b)) ↔ f' a = b
⊢ ∀ (x y : H), f' (x * y) = f' x * f' y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_3
s : Set α
⊢ (sumEquiv.symm (s, s)).ncard = s.ncard + s.ncard

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝ : (i : ι) → CommGroup (A i)
n : ℕ
x y : (i : ι) → A i
⊢ (fun x_1 ↦ ↑((x * y) x_1)) = (fun x_1 ↦ ↑(x x_1)) * fun x ↦ ↑(y x)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝ : (i : ι) → CommGroup (A i)
n : ℕ
φ : ((i : ι) → A i) →* (i : ι) → A i ⧸ (powMonoidHom n).range :=
  { toFun := fun x x_1 ↦ ↑(x x_1), map_one' := ⋯, map_mul' := ⋯ }
y : (i : ι) → A i ⧸ (powMonoidHom n).range
⊢ (φ fun i ↦ Quotient.out (y i)) = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ f', mrange f = f'.mgraph

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝ : (i : ι) → CommGroup (A i)
n : ℕ
φ : ((i : ι) → A i) →* (i : ι) → A i ⧸ (powMonoidHom n).range :=
  { toFun := fun x x_1 ↦ ↑(x x_1), map_one' := ⋯, map_mul' := ⋯ }
⊢ (powMonoidHom n).range = φ.ker

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
⊢ Surjective (Prod.fst ∘ ⇑(MulEquiv.prodComm.toMonoidHom.comp f))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
⊢ ∀ (g₁ g₂ : G),
    ((MulEquiv.prodComm.toMonoidHom.comp f) g₁).1 = ((MulEquiv.prodComm.toMonoidHom.comp f) g₂).1 →
      ((MulEquiv.prodComm.toMonoidHom.comp f) g₁).2 = ((MulEquiv.prodComm.toMonoidHom.comp f) g₂).2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
h : H
i : I
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
h : H
⊢ e₂ (e₁ h) = h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
i : I
⊢ e₁ (e₂ i) = i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
⊢ ∃ e, mrange f = e.toMonoidHom.mgraph

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: H : Type u_2
I : Type u_3
inst✝¹ : Monoid H
inst✝ : Monoid I
G : Submonoid (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
⊢ ∃ f, G = f.mgraph

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
this : ∀ (a b : α), f a = f b → a ≠ b → a = x ∨ a = g (f x)
⊢ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: H : Type u_2
I : Type u_3
inst✝¹ : Monoid H
inst✝ : Monoid I
G : Submonoid (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
hG₂ : Bijective (Prod.snd ∘ ⇑G.subtype)
⊢ ∃ e, G = e.toMonoidHom.mgraph

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : G →* H
x : G × H
⊢ x ∈ f.mgraph.carrier → x⁻¹ ∈ f.mgraph.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ f.graph = ((id G).prod f).range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ f', f.range = f'.graph

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
⊢ ∃ e, f.range = e.toMonoidHom.graph

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: H : Type u_2
I : Type u_3
inst✝¹ : Group H
inst✝ : Group I
G : Subgroup (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
⊢ ∃ f, G = f.graph

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: H : Type u_2
I : Type u_3
inst✝¹ : Group H
inst✝ : Group I
G : Subgroup (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
hG₂ : Bijective (Prod.snd ∘ ⇑G.subtype)
⊢ ∃ e, G = e.toMonoidHom.graph

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Surjective f
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
rcases isEmpty_or_nonempty α
  · simp
  -- pick an inverse `g` to `f`
  let g := Function.surjInv hf
  -- the "decreases cardinality by at most one condition" becomes "`g` misses at most one element"
  rw [← Set.ncard_range_of_injective (Function.injective_surjInv hf),
    ← Set.ncard_add_ncard_compl (Set.range g), add_le_add_iff_left]
  replace hf : ∀ b, f (g b) = b := Function.surjInv_eq hf
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [Set.ncard_le_one_iff_subset_singleton] at h
    -- if `g` misses at most one element, let `x` be this element
    obtain ⟨x, hx⟩ := h
    simp only [Set.subset_def, Set.mem_compl_iff] at hx
    -- we show that the only possible collision is between `x` and `g (f x)`
    suffices ∀ a b : α, f a = f b → a ≠ b → a = x ∨ a = g (f x) by grind
    intro a b
    by_cases ha : a ∈ Set.range g <;> by_cases hb : b ∈ Set.range g <;> grind
  · -- we must show that any two elements `a` and `b` missed by `g` are equal
    rw [Set.ncard_le_one]
    simp only [Set.mem_compl_iff, Set.mem_range, not_exists, ← ne_eq]
    intro a ha b hb
    -- there is a collision between `a` and `g (f a)`, and between `b` and `g (f b)`
    simpa [(ha (f b)).symm] using congrArg (a ∈ ·) (h a (g (f a)) b (g (f b))
      (hf (f a)).symm (hf (f b)).symm (ha (f a)).symm (hb (f b)).symm)

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Surjective f
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : Finite ↑s
f : α → β
⊢ s.ncard ≤ (f '' s).ncard + 1 ↔
    ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, ∀ d ∈ s, f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x y : M
⊢ p.quotientRel x y ↔ -(x - y) ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
x : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ mk x = 0 ↔ x ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x✝ y✝ : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
S : Type u_3
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
P : Submodule R M
a : S
x y : M
h : P.quotientRel x y
⊢ -(a • x) + a • y ∈ P.toAddSubgroup

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
S : Type u_3
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
P : Submodule R M
⊢ mk 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p p' : Submodule R M
S : Type u_3
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
P : Submodule R M
x✝¹ x✝ : M
⊢ mk (x✝¹ + x✝) = mk x✝¹ + mk x✝

Tactic:
by

Goal state after: