mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (f x) (f y)

Tactic:
]

Goal state after:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (f x) (f y)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).sum % n = (Multiset.map (fun i ↦ f i % n) s.val).sum % n

Tactic:
]

Goal state after:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).sum % n = (Multiset.map (fun i ↦ f i % n) s.val).sum % n
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
n : G
hn : n ∈ H
g : G
⊢ n ∈ H

Tactic:
]

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ n ∈ H
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).sum % n = (∑ i ∈ s, f i % n) % n

Tactic:
rw [Finset.sum, Multiset.map_map]; rfl

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).prod % n = (Multiset.map (fun i ↦ f i % n) s.val).prod % n

Tactic:
]

Goal state after:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).prod % n = (Multiset.map (fun i ↦ f i % n) s.val).prod % n
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
l : List α
f : α → β
comm : (↑l.toFinset).Pairwise (Commute on f)
hl : l.dedup = l
⊢ l.toFinset.noncommProd f comm = (List.map f l).prod

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
l : List α
f : α → β
comm : (↑l.toFinset).Pairwise (Commute on f)
hl : l.dedup = l
⊢ l.toFinset.noncommProd f comm = (List.map f l).prod
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).sum % n = (Multiset.map (fun i ↦ f i % n) s.val).sum % n

Tactic:
]

Goal state after:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).sum % n = (Multiset.map (fun i ↦ f i % n) s.val).sum % n
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).sum % n = (∑ i ∈ s, f i % n) % n

Tactic:
rw [Finset.sum, Multiset.map_map]; rfl

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha)).Pairwise (Commute on f)
⊢ (cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯

Tactic:
by
  simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons]

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).prod % n = (Multiset.map (fun i ↦ f i % n) s.val).prod % n

Tactic:
]

Goal state after:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).prod % n = (Multiset.map (fun i ↦ f i % n) s.val).prod % n
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
i : ↥s
⊢ ∏ x ∈ map (Embedding.subtype fun x ↦ x ∈ s) (s.attach.erase i), f x =
    ∏ j ∈ s.erase ((Embedding.subtype fun x ↦ x ∈ s) i), f j

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
i : ↥s
⊢ ∏ x ∈ map (Embedding.subtype fun x ↦ x ∈ s) (s.attach.erase i), f x =
    ∏ j ∈ s.erase ((Embedding.subtype fun x ↦ x ∈ s) i), f j
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ ConjAct.toConjAct g • H = H ↔ g⁻¹ ∈ normalizer ↑H

Tactic:
]

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ ConjAct.toConjAct g • H = H ↔ g⁻¹ ∈ normalizer ↑H
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ m ^ (Multiset.map f s.val).card = m ^ #s

pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ ∀ x ∈ Multiset.map f s.val, x = m

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ m ^ (Multiset.map f s.val).card = m ^ #s

α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ ∀ x ∈ Multiset.map f s.val, x = m
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ ↑l, Disjoint b a

Tactic:
]

Goal state after:
α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ ↑l, Disjoint b a
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y✝ : β
h : ∀ x ∈ s, Commute y✝ (f x)
y : β
⊢ (∃ a ∈ s.val, f a = y) → Commute y✝ y

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y✝ : β
h : ∀ x ∈ s, Commute y✝ (f x)
y : β
⊢ (∃ a ∈ s.val, f a = y) → Commute y✝ y
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_6
inst✝ : DecidableEq α
s : Finset ι
a : α
f : ι → Multiset α
⊢ (map (fun b ↦ count a (f b)) s.val).sum = (map (fun x ↦ count a (f x)) s.val).sum

Tactic:
]

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

Goal state before:
pp: M : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
S : Multiset M
⊢ (map id S.toFinset.val).prod ∣ S.prod

Tactic:
]

Goal state after:
M : Type u_3
inst✝¹ : DecidableEq M
inst✝ : CommMonoid M
S : Multiset M
⊢ (map id S.toFinset.val).prod ∣ S.prod
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List ↥S
⊢ ↑l.prod ∈ S

Tactic:
]

Goal state after:
M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List ↥S
⊢ ↑l.prod ∈ S
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: B : Type u_3
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset ↥S
⊢ ↑m.prod ∈ S

Tactic:
]

Goal state after:
B : Type u_3
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset ↥S
⊢ ↑m.prod ∈ S
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
y : M
⊢ (∃ a ∈ t.val, f a = y) → y ∈ S

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
y : M
⊢ (∃ a ∈ t.val, f a = y) → y ∈ S
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case cons
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (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)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem)).Pairwise fun x y ↦ Commute (g x) (f y)
⊢ f x * s.noncommProd f ⋯ * (g x * s.noncommProd g ⋯) = f x * s.noncommProd f ⋯ * (g x * s.noncommProd g ⋯)

pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (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)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem)).Pairwise fun x y ↦ Commute (g x) (f y)
y : α
hy : y ∈ s
⊢ Commute (g x) (f y)

Tactic:
]

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (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)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem)).Pairwise fun x y ↦ Commute (g x) (f y)
y : α
hy : y ∈ s
⊢ Commute (g x) (f y)
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Pi.mulSingle i (x i) i = x i

pp: case convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ univ.erase i, Pi.mulSingle x_1 (x x_1) i = 1

Tactic:
]

Goal state after:
case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Pi.mulSingle i (x i) i = x i

case convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ univ.erase i, Pi.mulSingle x_1 (x x_1) i = 1
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case intro
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ univ.noncommProd (fun i ↦ f (Pi.mulSingle i (x i))) ⋯ = univ.noncommProd (fun i ↦ g (Pi.mulSingle i (x i))) ⋯

Tactic:
]

Goal state after:
case intro
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ univ.noncommProd (fun i ↦ f (Pi.mulSingle i (x i))) ⋯ = univ.noncommProd (fun i ↦ g (Pi.mulSingle i (x i))) ⋯
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Finset M
⊢ (∃ f t, ↑t ⊆ ↑s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x) →
    ∃ f, Function.support f ⊆ ↑s ∧ ∏ a ∈ s, a ^ f a = x

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Finset M
⊢ (∃ f t, ↑t ⊆ ↑s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x) →
    ∃ f, Function.support f ⊆ ↑s ∧ ∏ a ∈ s, a ^ f a = x
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
a✝ : (i : ι) → α i
i : ι
⊢ Quotient.mk'' ((fun i ↦ (Quotient.mk'' (a✝ i)).out) i) = Quotient.mk'' (a✝ i)

Tactic:
]

Goal state after:
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
a✝ : (i : ι) → α i
i : ι
⊢ Quotient.mk'' ((fun i ↦ (Quotient.mk'' (a✝ i)).out) i) = Quotient.mk'' (a✝ i)
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
s : Setoid α
⊢ (∀ {x y : α}, ⊤ x y → s x y) ↔ ∀ (x y : α), s x y

Tactic:
]

Goal state after:
α : Type u_1
s : Setoid α
⊢ (∀ {x y : α}, ⊤ x y → s x y) ↔ ∀ (x y : α), s x y
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
r s : Setoid α
⊢ r ⊔ s = sInf {s_1 | ∀ ⦃x y : α⦄, r x y ∨ s x y → s_1 x y}

Tactic:
]

Goal state after:
α : Type u_1
r s : Setoid α
⊢ r ⊔ s = sInf {s_1 | ∀ ⦃x y : α⦄, r x y ∨ s x y → s_1 x y}
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
r s : Setoid α
⊢ (EqvGen.setoid fun x y ↦ r x y ∨ s x y) = EqvGen.setoid (⇑r ⊔ ⇑s)

Tactic:
]

Goal state after:
α : Type u_1
r s : Setoid α
⊢ (EqvGen.setoid fun x y ↦ r x y ∨ s x y) = EqvGen.setoid (⇑r ⊔ ⇑s)
Module: Mathlib.Data.Setoid.Basic

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

Tactic:
]

Goal state after:
α : Type u_1
S : Set (Setoid α)
⊢ sSup S = sInf {s | ∀ ⦃x y : α⦄, (∃ r ∈ S, r x y) → s x y}
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
s : Set (Setoid α)
⊢ (EqvGen.setoid fun x y ↦ ∃ r ∈ s, r x y) = EqvGen.setoid (⨆ a ∈ s, ⇑a)

Tactic:
]

Goal state after:
α : Type u_1
s : Set (Setoid α)
⊢ (EqvGen.setoid fun x y ↦ ∃ r ∈ s, r x y) = EqvGen.setoid (⨆ a ∈ s, ⇑a)
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
r : Setoid α
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → s x y} ≤ r

Tactic:
]

Goal state after:
α : Type u_1
r : Setoid α
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → s x y} ≤ r
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → s x y
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → s x y} ≤ s

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → s x y
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → s x y} ≤ s
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x✝ : Quotient r
x : α
⊢ g ⟦x⟧ = g ⟦x⟧

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ r.map f = Relation.EqvGen.setoid ⇑(r.mapOfSurjective f h hf)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ r.map f = Relation.EqvGen.setoid ⇑(r.mapOfSurjective f h hf)
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
r : Setoid β
x y : α
⊢ (comap f r) x y ↔ r (f x) (f y)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
r : Setoid β
x y : α
⊢ (comap f r) x y ↔ r (f x) (f y)
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
⊢ ((Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) on f) ≤ ⇑r

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
⊢ ((Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) on f) ≤ ⇑r
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
⊢ comap f (r.map f) = r

Tactic:
by
  apply le_antisymm _ le_comap_map
  rw [le_iff_rel_le, comap_rel_eq, coe_map_of_ker_le _ _ hf]
  rintro x y (⟨a, b, h, ha, hb⟩ | h)
  · replace ha := hf ha
    replace hb := hf hb
    exact trans (symm ha) (trans h hb)
  · exact hf h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : Setoid α
f : α → β
r : Setoid α
s : Setoid (Quotient r)
x y : α
h : r x y
⊢ s (Quotient.mk' y) (Quotient.mk' y)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ Relation.EqvGen r a b ↔ ⊤ ≤ Relation.EqvGen r a b

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
a b : α
⊢ Relation.EqvGen r a b ↔ ⊤ ≤ Relation.EqvGen r a b
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x y : M
h : (sInf S).toSetoid x y
r : Setoid M
x✝ : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ c.toSetoid x y

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x y : M
h : (sInf S).toSetoid x y
r : Setoid M
x✝ : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ c.toSetoid x y
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_4
f : ι → Con M
⊢ ⨅ x, ⇑(f x) = ⨅ i, ⇑(f i)

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c : Con M
⊢ c = ⊤ ↔ c = ⊤

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c : Con M
⊢ c = ⊥ ↔ c = ⊥

Tactic:
]

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

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

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ conGen (sSup (DFunLike.coe '' S)) = conGen fun x y ↦ ∃ c ∈ S, c x y
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ d : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
c : Con N
w x y z : M
h1 : (Setoid.comap f c.toSetoid) w x
h2 : (Setoid.comap f c.toSetoid) y z
⊢ c (f w * f y) (f x * f z)

Tactic:
]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ d : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
c : Con N
w x y z : M
h1 : (Setoid.comap f c.toSetoid) w x
h2 : (Setoid.comap f c.toSetoid) y z
⊢ c (f w * f y) (f x * f z)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ L1.length + L2.length + 2 = L1.length + ((x, b) :: (x, !b) :: L2).length

Tactic:
]

Goal state after:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ L1.length + L2.length + 2 = L1.length + ((x, b) :: (x, !b) :: L2).length
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:
]

Goal state after:
α : Type u
x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝) (x✝¹ ++ L₁✝ ++ L₂✝)
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
⊢ (↑x' * ↑y' = 1) = (↑x' * ↑y' = 1)

Tactic:
]

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

Goal state before:
pp: case refine_2.refine_1
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ (↑y' * ↑x' = 1) = (↑y' * ↑x' = 1)

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝ : CommMonoid M
h : a ∉ s
f : ι → M
⊢ f a * ∏ x ∈ s, f x = f a * ∏ x ∈ s, f x

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
h : a ∉ s
f : ι → M
⊢ f a * ∏ x ∈ s, f x = f a * ∏ x ∈ s, f x

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
a b : ι
h : a ≠ b
⊢ f a * f b = f a * f b

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
⊢ ∏ x ∈ s, f x = ∏ x ∈ s, f x

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝ : CommMonoid M
f g : ι → M
h : s₁ = s₂
⊢ (∀ x ∈ s₂, f x = g x) → s₂.prod f = s₂.prod g

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝ : CommMonoid M
f g : ι → M
h : s₁ = s₂
⊢ (∀ x ∈ s₂, f x = g x) → s₂.prod f = s₂.prod g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

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

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝ : CommMonoid M
f : ι → M
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x = fold (fun x1 x2 ↦ x1 * x2) 1 (fun x ↦ f x) (s₁.disjUnion s₂ h)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ ∅, f x

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ ∅, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : ι) → Decidable ¬p x
f : ι → M
this : DecidableEq ι
⊢ ∏ x ∈ s, f x = ∏ x ∈ s, f x

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : ι) → Decidable ¬p x
f : ι → M
⊢ ∏ x ∈ s, f x = ∏ x ∈ s, f x

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝² : CommMonoid M
f : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∏ x ∈ s with Xor (p x) (q x), f x = ∏ x ∈ s with p x ∧ ¬q x ∨ q x ∧ ¬p x, f x

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝² : CommMonoid M
f : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∏ x ∈ s with Xor (p x) (q x), f x = ∏ x ∈ s with p x ∧ ¬q x ∨ q x ∧ ¬p x, f x