mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
⊢ a ∈ f ⁻¹' f '' U ↔ a ∈ ⋃ g, (fun x ↦ g • x) '' U

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := ⋯
f : α → Quotient (orbitRel G α) := ⋯
a : α
⊢ a ∈ f ⁻¹' f '' U → a ∈ ⋃ g, (fun x ↦ g • x) '' U

case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := ⋯
f : α → Quotient (orbitRel G α) := ⋯
a : α
⊢ a ∈ ⋃ g, (fun x ↦ g • x) '' U → a ∈ f ⁻¹' f '' U
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
⊢ Quotient.mk' ⁻¹' Quotient.mk' '' U = ⋃ g, (fun x ↦ g • x) '' U

Tactic:
by
  let := orbitRel G α
  set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'
  ext a
  constructor
  · rintro ⟨b, hb, hab⟩
    obtain ⟨g, rfl⟩ := Quotient.exact hab
    rw [Set.mem_iUnion]
    exact ⟨g⁻¹, g • a, hb, inv_smul_smul g a⟩
  · intro hx
    rw [Set.mem_iUnion] at hx
    obtain ⟨g, u, hu₁, hu₂⟩ := hx
    rw [Set.mem_preimage, Set.mem_image]
    refine ⟨g⁻¹ • a, ?_, by simp +instances [f, orbitRel, Quotient.eq']⟩
    rw [← hu₂]
    convert! hu₁
    simp only [inv_smul_smul]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ (Ioi a).disjUnion (Iio a) ⋯ = {a}ᶜ

Tactic:
ext

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
a a✝ : α
⊢ a✝ ∈ (Ioi a).disjUnion (Iio a) ⋯ ↔ a✝ ∈ {a}ᶜ
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
a b : α
h : ⟦a⟧ = ⟦b⟧
⊢ ⟦a⟧ = ⟦b⟧

Tactic:
rw [@Quotient.eq] at h ⊢

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
a b : α
h : (orbitRel (↥H) α) a b
⊢ (orbitRel G α) a b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ BddAbove (f ⁻¹' s)

Tactic:
contrapose! hf
  rw [not_bddAbove_iff] at hf
  obtain ⟨φ, hφm, hφs⟩ := Nat.exists_strictMono_subsequence
    fun n ↦ (hf n).casesOn fun m h ↦ h.casesOn fun hs hmn ↦ Exists.intro m ⟨hmn, hs⟩
  rw [partiallyWellOrderedOn_iff_exists_lt] at hs
  obtain ⟨m, n, hmn, hr⟩ := hs (fun n ↦ f (φ n)) hφs
  use (φ m), (φ n)
  exact ⟨hφm hmn, hr⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) ↔ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) → ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

case mpr
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f) → ∃ x, IsBadSeq r s x
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑r * ↑↑u = ↑↑u * ↑r

Tactic:
u.1.prop.comm r

Goal state after:
M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑r * ↑↑u = ↑r * ↑↑u
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
⊢ e x ∈ Set.center N

Tactic:
constructor

Goal state after:
case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (a : N), Commute (e x) a

case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (b c : N), e x * (b * c) = e x * b * c

case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (a b : N), a * b * e x = a * (b * e x)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
⊢ ∃ m n, m < n ∧ f m ≤ f n

Tactic:
by_cases! hc : ∃ n, (ofLex f (g 0)).1 < (ofLex f (g n)).1

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∃ n, (ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ ∃ m n, m < n ∧ f m ≤ f n

case neg
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ ∃ m n, m < n ∧ f m ≤ f n
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case h
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
n : ℕ
hn : (ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ g 0 < g n ∧ f (g 0) ≤ f (g n)

Tactic:
constructor

Goal state after:
case h.left
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
n : ℕ
hn : (ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ g 0 < g n

case h.right
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
n : ℕ
hn : (ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ f (g 0) ≤ f (g n)
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_2
inst✝ : Mul N
S : Set M
T : Set N
hS : S.Nonempty
hT : T.Nonempty
⊢ (S ×ˢ T).centralizer = S.centralizer ×ˢ T.centralizer

Tactic:
ext

Goal state after:
M : Type u_1
inst✝¹ : Mul M
N : Type u_2
inst✝ : Mul N
S : Set M
T : Set N
hS : S.Nonempty
hT : T.Nonempty
x✝ : M × N
⊢ x✝ ∈ (S ×ˢ T).centralizer ↔ x✝ ∈ S.centralizer ×ˢ T.centralizer
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : ((fun c ↦ ⟨f c, g (f c) c⟩) c).fst = ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ ((PSigma.Lex (Subrel rι fun x ↦ x ∈ range f) fun a ↦ Subrel (rπ ↑a on g ↑a) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'

Tactic:
dsimp only [InvImage, (· on ·)] at h' ⊢
    convert! PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1; swap
    · exact ⟨c, h'⟩
    · exact PSigma.subtype_ext (Subtype.ext h') rfl
    · dsimp only [Subtype.coe_mk, Subrel, Order.Preimage] at *
      grind

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

Goal state before:
pp: G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
⊢ a • ↑s = ↑s

Tactic:
ext

Goal state after:
G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
x✝ : G
⊢ x✝ ∈ a • ↑s ↔ x✝ ∈ ↑s
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
⊢ MulOpposite.op a • ↑s = ↑s

Tactic:
ext

Goal state after:
G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
x✝ : G
⊢ x✝ ∈ MulOpposite.op a • ↑s ↔ x✝ ∈ ↑s
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ ↑(normalizer ↑N)
⊢ S * ↑N = ↑N * S

Tactic:
by
  rw [← iUnion_mul_left_image, ← iUnion_mul_right_image]
  simp only [image_mul_left, image_mul_right, Set.preimage]
  congr! 5 with s hs x
  exact (mem_normalizer_iff'.mp (inv_mem (hLE hs)) x).symm

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
⊢ ↑A * ↑(B ⊓ C) = ↑A * ↑B ∩ ↑C

Tactic:
ext

Goal state after:
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ x✝ ∈ ↑A * ↑(B ⊓ C) ↔ x✝ ∈ ↑A * ↑B ∩ ↑C
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) ↔ (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C

Tactic:
constructor

Goal state after:
case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) → (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C

case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C → ∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
⊢ ↑(A ⊓ B) * ↑C = ↑A ∩ (↑B * ↑C)

Tactic:
ext

Goal state after:
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ x✝ ∈ ↑(A ⊓ B) * ↑C ↔ x✝ ∈ ↑A ∩ (↑B * ↑C)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y ∈ ↑C, x * y = x✝) ↔ x✝ ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y ∈ ↑C, x * y = x✝

Tactic:
constructor

Goal state after:
case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y ∈ ↑C, x * y = x✝) → x✝ ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y ∈ ↑C, x * y = x✝

case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (x✝ ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y ∈ ↑C, x * y = x✝) → ∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y ∈ ↑C, x * y = x✝
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.inr
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
hx : x ∈ l
y : α
hy : y ∈ l
hxy : x ≠ y
⊢ x * y = y * x

Tactic:
exact comm hx hy hxy

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
⊢ H.Normal

Tactic:
constructor

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
⊢ ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
⊢ (s.erase a).noncommProd comm' * a = s.noncommProd comm

Tactic:
by
  suffices ∀ b ∈ erase s a, Commute a b by
    rw [← (noncommProd_commute (s.erase a) comm' a this).eq, mul_noncommProd_erase s h comm comm']
  intro b hb
  rcases eq_or_ne a b with rfl | hab
  · rfl
  exact comm h (mem_of_mem_erase hb) hab

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case hac.hab
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (f y)

Tactic:
exact comm_ff.of_refl hx hy

Goal state after:
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
s : Set (Setoid α)
⊢ ⇑(sInf s) = sInf (@r α '' s)

Tactic:
ext

Goal state after:
α : Type u_1
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ (sInf s) x✝¹ x✝ ↔ sInf (@r α '' s) x✝¹ x✝
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
S : Set (Setoid α)
⊢ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, a x_1 y → x x_1 y} = {s | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, x_1 x y → s x y}

Tactic:
ext

Goal state after:
α : Type u_1
S : Set (Setoid α)
x✝ : Setoid α
⊢ x✝ ∈ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, a x_1 y → x x_1 y} ↔
    x✝ ∈ {s | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, x_1 x y → s x y}
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
S : Set (Setoid α)
x✝ : Setoid α
⊢ x✝ ∈ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, a x_1 y → x x_1 y} ↔
    x✝ ∈ {s | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, x_1 x y → s x y}

Tactic:
exact ⟨fun H x y r hr => H hr, fun H r hr x y => H r hr⟩

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c d : Con M
H : ∀ (x y : M), c x y ↔ d x y
⊢ ⇑c = ⇑d

Tactic:
ext

Goal state after:
M : Type u_1
inst✝ : Mul M
c d : Con M
H : ∀ (x y : M), c x y ↔ d x y
x✝¹ x✝ : M
⊢ c x✝¹ x✝ ↔ d x✝¹ x✝
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ ⇑(sInf S) = sInf (DFunLike.coe '' S)

Tactic:
ext

Goal state after:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x✝¹ x✝ : M
⊢ (sInf S) x✝¹ x✝ ↔ sInf (DFunLike.coe '' S) x✝¹ x✝
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ sSup S = conGen fun x y ↦ ∃ c ∈ S, c x y

Tactic:
rw [sSup_def]
  congr! with x y
  simp

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

Goal state before:
pp: α : Type u
x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝) (x✝¹ ++ L₁✝ ++ L₂✝)

Tactic:
constructor

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: L₁) L₂ ↔ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

Tactic:
constructor

Goal state after:
case mp
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: L₁) L₂ → (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂

case mpr
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂ → Step ((a, b) :: L₁) L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refl.refl
α : Type u
p : α × Bool
LL₁ L₁ : List (α × Bool)
⊢ Red L₁ L₁

Tactic:
constructor

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι ⊕ κ → M
⊢ ∏ x ∈ s.disjSum t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)

Tactic:
by
  rw [← map_inl_disjUnion_map_inr, prod_disjUnion, prod_map, prod_map]
  rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'

Tactic:
disjoint_left,

Goal state after:
case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : ι⦄, a ∈ {i ∈ s | g i = x'} → a ∉ {i ∈ s | g i = y'}
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
s t : { d // c ≤ d }
⊢ { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        s ≤
      { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        t ↔
    s ≤ t

Tactic:
constructor

Goal state after:
case mp
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
s t : { d // c ≤ d }
⊢ { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        s ≤
      { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        t →
    s ≤ t

case mpr
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
s t : { d // c ≤ d }
⊢ s ≤ t →
    { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        s ≤
      { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        t
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'

Tactic:
disjoint_left,

Goal state after:
case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : ι⦄, a ∈ {i ∈ s | g i = x'} → a ∉ {i ∈ s | g i = y'}
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
⊢ (c.lift f H).comp c.mk' = f

Tactic:
ext

Goal state after:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x✝ : M
⊢ ((c.lift f H).comp c.mk') x✝ = f x✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f g : ι → M
⊢ ∏ x ∈ s, f x * g x = fold (fun x1 x2 ↦ x1 * x2) (1 * 1) (fun x ↦ f x * g x) s

Tactic:
by rw [one_mul]; rfl

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
⊢ (fun g ↦ ⇑g ∘ of) ((fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) f) = f

Tactic:
ext

Goal state after:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
x✝ : α
⊢ (fun g ↦ ⇑g ∘ of) ((fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) f) x✝ = f x✝
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
g : FreeGroup α →* β
⊢ (fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) ((fun g ↦ ⇑g ∘ of) g) = g

Tactic:
ext

Goal state after:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
g : FreeGroup α →* β
a✝ : α
⊢ ((fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) ((fun g ↦ ⇑g ∘ of) g)) (of a✝) = g (of a✝)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ map f = lift (of ∘ f)

Tactic:
ext

Goal state after:
α : Type u
β : Type v
f : α → β
a✝ : α
⊢ (map f) (of a✝) = (lift (of ∘ f)) (of a✝)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α✝ : Type u
L L₁ L₂ L₃ L₄ : List (α✝ × Bool)
β✝ : Type v
f : α✝ → β✝
x✝ y : FreeGroup α✝
α : Type ?u.38
β : Type ?u.39
e : α ≃ β
x : FreeGroup α
⊢ (map ⇑e.symm) ((map ⇑e) x) = x

Tactic:
by simp [map.comp]

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

Goal state before:
pp: α✝ : Type u
L L₁ L₂ L₃ L₄ : List (α✝ × Bool)
β✝ : Type v
f : α✝ → β✝
x✝ y : FreeGroup α✝
α : Type ?u.38
β : Type ?u.39
e : α ≃ β
x : FreeGroup β
⊢ (map ⇑e) ((map ⇑e.symm) x) = x

Tactic:
by simp [map.comp]

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

Goal state before:
pp: case C1
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
⊢ (fun x ↦ of default ^ x) ((fun x ↦ ((map 1) x).sum) 1) = 1

Tactic:
| C1 =>

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

Goal state before:
pp: case C1
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
⊢ (fun x ↦ x • FreeAddGroup.of default) ((fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) 0) = 0

Tactic:
| C1 =>

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x_1⁻¹ * x ∈ N
⊢ N = ⊤

Tactic:
ext

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x_1⁻¹ * x ∈ N
x✝ : G
⊢ x✝ ∈ N ↔ x✝ ∈ ⊤
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x * x_1⁻¹ ∈ N
⊢ N = ⊤

Tactic:
ext

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x * x_1⁻¹ ∈ N
x✝ : G
⊢ x✝ ∈ N ↔ x✝ ∈ ⊤
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
⊢ QuotientGroup.con f.ker = Con.ker f

Tactic:
ext

Goal state after:
G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
x✝ y✝ : G
⊢ (QuotientGroup.con f.ker) x✝ y✝ ↔ (Con.ker f) x✝ y✝
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
⊢ (mk' N).comp N.subtype = 1

Tactic:
ext

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x✝ : ↥N
⊢ ((mk' N).comp N.subtype) x✝ = 1 x✝
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
⊢ (QuotientGroup.con H).subgroup = H

Tactic:
ext

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
x✝ : G
⊢ x✝ ∈ (QuotientGroup.con H).subgroup ↔ x✝ ∈ H