mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
⊢ ∃ a, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ (Set.mem_univ _), ?_⟩

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
⊢ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
⊢ s.Finite

Tactic:
by_contra! hi

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
hi : s.Infinite
⊢ False
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b c : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidablePred fun x ↦ x < c
hcb : c ≤ b
⊢ {x ∈ Ico a b | x < c} = Ico a c

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hac : a ≤ c
⊢ {x ∈ Ico a b | c ≤ x} = Ico c b

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Ioc a b) = Ioc ↑a ↑b

Tactic:
subtype_Ioc_eq

Goal state after:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioc ↑a ↑b)) = Ioc ↑a ↑b
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_2.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
hf : f (g m) = f (g n)
h : m < n
⊢ m = n

Tactic:
rfl

Goal state after:
case inr.refine_2.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
hf : f (g m) = f (g n)
h : m < n
⊢ m = n
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLE α
inst✝ : LocallyFiniteOrder α
a : { x // x ≤ y }
⊢ y ≤ y

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_2.inr.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m : ℕ
hf : f (g m) = f (g m)
⊢ m = m

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
⊢ s.Finite

Tactic:
by_contra! hi

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
hi : s.Infinite
⊢ False
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_2.inr.inr
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
hf : f (g m) = f (g n)
h : n < m
⊢ m = n

Tactic:
rfl

Goal state after:
case inr.refine_2.inr.inr
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
hf : f (g m) = f (g n)
h : n < m
⊢ m = n
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ x ≤ a
hab : a < b
⊢ {x ∈ Ico a b | x ≤ a} = {a}

Tactic:
grind

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ ∃ n, r ^ n • x ∈ closure (r • s)

Tactic:
induction hx using closure_induction with
  | mem x hx => exact ⟨1, subset_closure ⟨_, hx, by rw [pow_one]⟩⟩
  | one => exact ⟨0, by simp⟩
  | mul x y _ _ hx hy =>
    obtain ⟨⟨nx, hx⟩, ⟨ny, hy⟩⟩ := And.intro hx hy
    use ny + nx
    rw [pow_add, mul_smul, ← smul_mul_assoc, mul_comm, ← smul_mul_assoc]
    exact mul_mem hy hx

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ closure s⁻¹ ↔ x⁻¹ ∈ closure s

Tactic:
by
  rw [closure_inv, mem_inv]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Icc a b) - 1 - 1 = #(Icc a b) - 2

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Ioc a b ∩ Ioc c d = Ioc (max a c) (min b d)

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ {x ∈ Ico a b | x < c} = Ico a (min b c)

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ {x ∈ Ico a b | c ≤ x} = Ico (max a c) b

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ {x ∈ Ioo a b | x < c} = Ioo a (min b c)

Tactic:
grind

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

Goal state before:
pp: α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrderBot α
a b : α
⊢ {x ∈ Iio a | x < b} = Iio (min a b)

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b \ Ico a c = Ico (max a c) b

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b \ Ico c b = Ico a (min b c)

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iic b \ Ioc a b = Iic (min a b)

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
h : a ≤ b
⊢ Iic a ∪ Ioc a b = Iic b

Tactic:
grind

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

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a a✝ : α
⊢ a ∈ orbit (Quotient.mk'' a✝) ↔ (orbitRel G α) a a✝

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
⊢ orbit (Quotient.mk' (φ x)) = MulAction.orbit G (φ x)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.WellFoundedSet

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

Tactic:
let fs : ∀ n : ℕ, { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } := by
    refine Nat.rec ?_ fun n fn => ?_
    · exact ⟨(minBadSeqOfBadSeq r rk s 0 f0 hf0).1, (minBadSeqOfBadSeq r rk s 0 f0 hf0).2.2⟩
    · exact ⟨(minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).1,
        (minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).2.2⟩

Goal state after:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
⊢ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case zero
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m : ℕ
⊢ ↑(fs m) m = ↑(fs (m + 0)) m

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case succ
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m k : ℕ
ih : ↑(fs m) m = ↑(fs (m + k)) m
⊢ ↑(minBadSeqOfBadSeq r rk s (m + k + 1) ↑(fs (m + k)) ⋯) m = ↑(fs (m + (k + 1))) m

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ center.commMonoid.toMonoid = (center M).toMonoid

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: 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

Tactic:
obtain ⟨n, hn⟩ := hc

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
n : ℕ
hn : (ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ ∃ m n, m < n ∧ f m ≤ f n
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : (∀ (a : M), z₁ * a = a * z₁) ∧ (∀ (b c : M), z₁ * (b * c) = z₁ * b * c) ∧ ∀ (a b : M), a * b * z₁ = a * (b * z₁)
hz₂ : (∀ (a : M), z₂ * a = a * z₂) ∧ (∀ (b c : M), z₂ * (b * c) = z₂ * b * c) ∧ ∀ (a b : M), a * b * z₂ = a * (b * z₂)
⊢ (∀ (a : M), z₁ * z₂ * a = a * (z₁ * z₂)) ∧
    (∀ (b c : M), z₁ * z₂ * (b * c) = z₁ * z₂ * b * c) ∧ ∀ (a b : M), a * b * (z₁ * z₂) = a * (b * (z₁ * z₂))

Tactic:
grind

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

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
⊢ (∀ (i : ι),
      (∀ (a : A i), x i * a = a * x i) ∧
        (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)) →
    (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
      (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
        ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_4
inst✝ : Group G
H : Subgroup G
g h : ↥H
⊢ ↑(toConjAct g • h) = toConjAct ↑g • ↑h

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g h : G
⊢ (∃ x, x • h = g) ↔ ∃ c, c * h * c⁻¹ = g

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ofConjAct (toConjAct.toMonoidHom g)⁻¹ * ↑h * g = g⁻¹ * ↑h * g

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
s : Set G
⊢ g ∈ centralizer s ↔ ∀ h ∈ s, ⁅g, h⁆ = 1

Tactic:
by
  refine forall₂_congr fun _ _ ↦ ?_
  rw [commutatorElement_def, mul_inv_eq_iff_eq_mul, mul_inv_eq_iff_eq_mul, one_mul, eq_comm]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.convert_6
ι : 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' : f c = f c'
h'' : rπ (f c') (h' ▸ g (f c) c) (g (f c') c')
⊢ (rπ (f c') on g (f c')) c c'

Tactic:
grind

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Subgroup G
⊢ ↑s = ↑⊥ ↔ ↑s = 1

Tactic:
rfl

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
⊢ {x | ∃ a ∈ s, f a = x}.Pairwise Commute

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ _

Goal state after:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
x : α
hx : x ∈ s
y : α
hy : y ∈ s
a✝ : f x ≠ f y
⊢ Commute (f x) (f y)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
G : Type u_7
inst✝¹ : FunLike G M N
inst✝ : MonoidHomClass G M N
g : G
f : ι → M
s : Finset ι
⊢ (Multiset.map (⇑g ∘ f) s.val).prod = (Multiset.map (fun x ↦ g (f x)) s.val).prod

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
e : ι ↪ κ
f : κ → M
⊢ (Multiset.map ((fun x ↦ f x) ∘ ⇑e) s.val).prod = ∏ x ∈ s, f (e x)

Tactic:
rfl

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

Goal state before:
pp: case h.inl
α : 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 hy : x ∈ l
⊢ x * x = x * x

Tactic:
rfl

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f g : ι → M
h : p
⊢ ∏ x ∈ s, f x = ∏ x ∈ s, f x

Tactic:
rfl

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f g : ι → M
h : ¬p
⊢ ∏ x ∈ s, g x = ∏ x ∈ s, g x

Tactic:
rfl

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
h : p
⊢ ∏ x ∈ s, f h x = ∏ x ∈ s, f h x

Tactic:
rfl

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

Goal state before:
pp: case inl
α : 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
hb : a ∈ s.erase a
⊢ Commute a a

Tactic:
rfl

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
h : ¬p
⊢ ∏ x ∈ s, g h x = ∏ x ∈ s, g h x

Tactic:
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).sum % n = (Multiset.map (fun i ↦ f i % n) s.val).sum % n

Tactic:
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:
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).sum % n = (Multiset.map (fun i ↦ f i % n) s.val).sum % n

Tactic:
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:
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)
⊢ (f a ::ₘ Multiset.map f s.val).noncommProd ⋯ = (Multiset.map f s.val).noncommProd ⋯ * f a

Tactic:
Multiset.noncommProd_cons'

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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : List M
⊢ s.prod = s.sum

Tactic:
rfl

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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : List (Additive M)
⊢ s.sum = s.prod

Tactic:
rfl

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

Goal state before:
pp: M : Type u_3
inst✝ : AddMonoid M
s : List M
⊢ s.sum = s.prod

Tactic:
rfl

Goal state after:
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
⊢ (List.map Subtype.val l).prod ∈ S

Tactic:
← coe_list_prod

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.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : AddMonoid M
s : List (Multiplicative M)
⊢ s.prod = s.sum

Tactic:
rfl

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ s.prod = s.sum

Tactic:
rfl

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset (Additive M)
⊢ s.sum = s.prod

Tactic:
rfl

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

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
s : Multiset M
⊢ s.sum = s.prod

Tactic:
rfl

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

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
s : Multiset (Multiplicative M)
⊢ s.prod = s.sum

Tactic:
rfl

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
a₁✝ : α
a₂✝ : β
⊢ (fun q ↦ q.liftOn' (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯)
      ((fun x ↦
          match x with
          | (x, y) => Quotient.map₂ Prod.mk ⋯ x y)
        (Quotient.mk'' a₁✝, Quotient.mk'' a₂✝)) =
    (Quotient.mk'' a₁✝, Quotient.mk'' a₂✝)

Tactic:
rfl

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
a✝ : α × β
⊢ (fun x ↦
        match x with
        | (x, y) => Quotient.map₂ Prod.mk ⋯ x y)
      ((fun q ↦ q.liftOn' (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯) (Quotient.mk'' a✝)) =
    Quotient.mk'' a✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ (sInf s) x✝¹ x✝ ↔ ∀ i ∈ s, i x✝¹ x✝

Tactic:
rfl

Goal state after:
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:
rfl

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:
rfl

Goal state after:
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:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient (ker (Quot.mapRight h))
y : Quot ⇑r
w : α
⊢ ⟦Quotient.mk'' w⟧ = Quotient.mk'' (Quotient.mk'' w)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient s
y : α
⊢ ⟦y⟧ = Quotient.mk'' y

Tactic:
rfl

Goal state after:
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
y : M → M → Prop
iseqv✝¹ : Equivalence y
mul'✝¹ :
  ∀ {w x y_1 z : M},
    { r := y, iseqv := iseqv✝¹ } w x →
      { r := y, iseqv := iseqv✝¹ } y_1 z → { r := y, iseqv := iseqv✝¹ } (w * y_1) (x * z)
iseqv✝ : Equivalence y
mul'✝ :
  ∀ {w x y_1 z : M},
    { r := y, iseqv := iseqv✝ } w x → { r := y, iseqv := iseqv✝ } y_1 z → { r := y, iseqv := iseqv✝ } (w * y_1) (x * z)
h :
  (fun c ↦ ⇑c.toSetoid) { r := y, iseqv := iseqv✝, mul' := mul'✝ } =
    (fun c ↦ ⇑c.toSetoid) { r := y, iseqv := iseqv✝¹, mul' := mul'✝¹ }
⊢ { r := y, iseqv := iseqv✝, mul' := mul'✝ } = { r := y, iseqv := iseqv✝¹, mul' := mul'✝¹ }

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x✝¹ x✝ : M
⊢ (sInf S) x✝¹ x✝ ↔ ∀ i ∈ S, i x✝¹ x✝

Tactic:
rfl

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

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

Tactic:
Function.comp_def

Goal state after:
M : Type u_1
inst✝ : Mul M
ι : Sort u_4
f : ι → Con M
⊢ ⨅ x, ⇑(f x) = ⨅ i, ⇑(f i)
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refl
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ (x : M), s x x

Tactic:
exact s.refl'

Goal state after:
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 c : Con M
x✝ y✝ : M
⊢ id (x✝ * y✝) = id x✝ * id y✝

Tactic:
rfl

Goal state after: