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

Goal state before:
pp: case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f a = f a ⊓ f b

Tactic:
inf_eq_left.2 (OrderHomClass.mono f h : f a ≤ f b)

Goal state after:
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f a = f a
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case cons
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
a✝¹ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
hfg : f a✝¹ b✝ = g a✝¹ b✝
a✝ : Forall₂ (fun a b ↦ f a b = g a b) l₁✝ l₂✝
ih : zipWith f l₁✝ l₂✝ = zipWith g l₁✝ l₂✝
⊢ zipWith f (a✝¹ :: l₁✝) (b✝ :: l₂✝) = zipWith g (a✝¹ :: l₁✝) (b✝ :: l₂✝)

Tactic:
exact congr_arg₂ _ hfg ih

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
y : α
⊢ y ∈ s → x < y → ∃ z ∈ t, x < z ∧ z < y

Tactic:
hy

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ x < y → ∃ z ∈ t, x < z ∧ z < y
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
⊢ y ∈ ↑s → x < y → f x < f y

Tactic:
hy

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
⊢ x < y → f x < f y
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ (s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t

Tactic:
constructor <;> intro h

Goal state after:
case cons.mp
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
⊢ s <+ a :: t

case cons.mpr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case inr
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen n l
⊢ (a :: l').length = n + 1

Tactic:
· exact congr_arg (· + 1) (length_of_sublistsLen h)

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
t : Finset γ
f : β → γ → α
a : α
⊢ (s.sup fun b ↦ t.sup (f b)) ≤ a ↔ (t.sup fun c ↦ s.sup fun b ↦ f b c) ≤ a

Tactic:
simpa using forall₂_comm

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
hx : x ∈ S
y : α
T : Set α
hT : T ∈ s
⊢ y ∈ T → x ≠ y → r x y

Tactic:
hy

Goal state after:
α : Type u_1
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
r : α → α → Prop
h : ∀ a ∈ s, a.Pairwise r
x : α
S : Set α
hS : S ∈ s
hx : x ∈ S
y : α
T : Set α
hT : T ∈ s
hy : y ∈ T
⊢ x ≠ y → r x y
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset β
t : Finset γ
hs : s.Nonempty
ht : t.Nonempty
f : β → γ → α
a : α
⊢ (s.sup' hs fun b ↦ t.sup' ht (f b)) ≤ a ↔ (t.sup' ht fun c ↦ s.sup' hs fun b ↦ f b c) ≤ a

Tactic:
simpa using forall₂_comm

Goal state after:
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f

Tactic:
by
  simp only [hp, ciSup_unique]
  simp only [iSup]
  congr
  apply Subset.antisymm
  · rintro - ⟨i, rfl⟩
    simp
  · rintro - ⟨i, rfl⟩
    simp

Goal state after:
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Preorder β
f : β → α
a✝ : β
hf : Monotone f
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ f ↑x
H : BddAbove (range fun x ↦ f ↑x)
a : β
h : a ∈ Iic a✝
⊢ f ↑⟨a, h⟩ ≤ f ↑⟨a✝, ⋯⟩

Tactic:
exact hf h

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

Goal state before:
pp: α : Type u
ι✝ : Sort v
κ : ι✝ → Sort w
inst✝¹ : Order.Frame α
inst✝ : Finite ι✝
f : (a : ι✝) → κ a → α
ι : Type v
⊢ ∀ {κ : ι → Type w} [Finite ι] (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
κ

Goal state after:
α : Type u
ι✝ : Sort v
κ✝ : ι✝ → Sort w
inst✝¹ : Order.Frame α
inst✝ : Finite ι✝
f : (a : ι✝) → κ✝ a → α
ι : Type v
κ : ι → Type w
⊢ ∀ [Finite ι] (f : (a : ι) → κ a → α), ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Finset α
hs : s.Nonempty
⊢ s.sup' hs id = sSup ↑s

Tactic:
sup'_eq_csSup_image s hs,

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Finset α
hs : s.Nonempty
⊢ sSup (id '' ↑s) = sSup ↑s
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
β : ι → Type u_6
f : (i : ι) → α i → β i
⊢ ∀ (x : (i : ι) × β i), (x ∈ univ.sigma fun i ↦ range (f i)) ↔ x ∈ range fun x ↦ ⟨x.fst, f x.fst x.snd⟩

Tactic:
simp [range, Sigma.forall]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
β : (i : ι) → α i → Type u_7
s : Set ι
t : (i : ι) → Set (α i)
u : (p : (i : ι) × α i) → Set (β p.fst p.snd)
⊢ Sigma.uncurry ⁻¹' (s.sigma t).pi u = s.pi fun i ↦ (t i).pi fun j ↦ u ⟨i, j⟩

Tactic:
by
  ext x
  simp only [mem_preimage, mem_pi, mem_sigma_iff, and_imp]
  exact ⟨fun h i hi j hj ↦ h ⟨i, j⟩ hi hj, fun h p hp1 hp2 ↦ h p.1 hp1 p.2 hp2⟩

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

Goal state before:
pp: case inl.mpr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ (∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨i, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨i, b⟩.snd)) →
    x ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩

Tactic:
· rintro ⟨⟨⟩, ⟨⟩, hx⟩
      rw [sigmaLift, dif_pos rfl, mem_map]
      exact ⟨_, hx, by simp⟩

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
Q : ι → Prop
f : ι → α
g : α → β
i : ι
hg : StrictMonoOn g (f '' ofPred Q)
h : MinimalFor Q (g ∘ f) i
j : ι
hj : Q j
hle : f j ≤ f i
this : ¬f i ≤ f j
⊢ False

Tactic:
exact h.not_lt hj <| hg ⟨j, hj, rfl⟩ ⟨i, h.prop, rfl⟩ <| lt_of_le_not_ge hle this

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : ¬Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
· rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad
      obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → n ∉ bad := by
        by_cases he : hbad.toFinset.Nonempty
        · refine
            ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
        · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
      have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) := by
        intro n
        have h := hm _ (Nat.le_add_left m n)
        simp only [bad, exists_prop, not_not, Set.mem_ofPred_eq, not_forall] at h
        obtain ⟨n', hn1, hn2⟩ := h
        refine ⟨n + n' - n - m, by lia, ?_⟩
        convert! hn2
        lia
      let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
      exact
        ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
              Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
          Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_2
α : 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
⊢ (Set.range (f ∘ ⇑g)).Infinite

Tactic:
refine Set.infinite_range_of_injective fun m n (hf : f (g m) = f (g n)) ↦ ?_

Goal state after:
case inr.refine_2
α : 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)
⊢ 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 b : { x // x ≤ y }
⊢ b ∈ Ioc a ⟨y, ⋯⟩ ↔ a < b

Tactic:
simp only [Finset.mem_Ioc, and_iff_left_iff_imp]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLE α
inst✝ : LocallyFiniteOrder α
a b : { x // x ≤ y }
⊢ a < b → b ≤ ⟨y, ⋯⟩
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
f : ι → α
s : Finset ι
i : α
hi : i ∈ image f s
⊢ i ≤ s.sup f

Tactic:
obtain ⟨j, hj, rfl⟩ := mem_image.1 hi

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
f : ι → α
s : Finset ι
j : ι
hj : j ∈ s
hi : f j ∈ image f s
⊢ f j ≤ s.sup f
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : 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 : ℕ
mn : m ≤ m + k
⊢ ↑(fs m) m = ↑(fs (m + k)) m

Tactic:
clear mn

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
m k : ℕ
⊢ ↑(fs m) m = ↑(fs (m + k)) m
Module: Mathlib.GroupTheory.Subsemigroup.Center

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
z : M
⊢ z ∈ center M ↔ z ∈ Set.center M

Tactic:
exact Iff.rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
z : G
⊢ z ∈ center G ↔ z ∈ Set.center G

Tactic:
exact Iff.rfl

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

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x : G
hx : x ∈ (ConjClasses.mk g).carrier
y : G
⊢ y ∈ (ConjClasses.mk g).carrier → x = y

Tactic:
hy

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x : G
hx : x ∈ (ConjClasses.mk g).carrier
y : G
hy : y ∈ (ConjClasses.mk g).carrier
⊢ x = y
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
z : M
⊢ z ∈ center M ↔ z ∈ Set.center M

Tactic:
exact Iff.rfl

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := ⋯
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a})
⊢ MonotoneOn f (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a})

Tactic:
rintro b ⟨-, hb⟩ c ⟨-, hc⟩ hbc

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x ↦ (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a})
b : Lex (α × β)
hb : b ∈ (fun x ↦ (ofLex x).1) ⁻¹' {a}
c : Lex (α × β)
hc : c ∈ (fun x ↦ (ofLex x).1) ⁻¹' {a}
hbc : b ≤ c
⊢ f b ≤ f c
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
x : α
hx : x ∈ {x | x ∈ ↑tl}
y : α
⊢ y ∈ {x | x ∈ ↑tl} → x ≠ y → Commute x y

Tactic:
hy

Goal state after:
case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
x : α
hx : x ∈ {x | x ∈ ↑tl}
y : α
hy : y ∈ {x | x ∈ ↑tl}
⊢ x ≠ y → Commute x y
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x : α
hx : x ∈ {x | x ∈ a ::ₘ ⟦tl⟧}
y : α
⊢ y ∈ {x | x ∈ a ::ₘ ⟦tl⟧} → x ≠ y → Commute x y

Tactic:
hy

Goal state after:
case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x : α
hx : x ∈ {x | x ∈ a ::ₘ ⟦tl⟧}
y : α
hy : y ∈ {x | x ∈ a ::ₘ ⟦tl⟧}
⊢ x ≠ y → Commute x y
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:
by
  ext
  simp only [coe_inf, Set.mem_mul, Set.mem_inter_iff]
  constructor
  · rintro ⟨y, ⟨hyA, hyB⟩, z, hz, rfl⟩
    refine ⟨A.mul_mem hyA (h hz), ?_⟩
    exact ⟨y, hyB, z, hz, rfl⟩
  rintro ⟨hyz, y, hy, z, hz, rfl⟩
  refine ⟨y, ⟨?_, hy⟩, z, hz, rfl⟩
  suffices y * z * z⁻¹ ∈ A by simpa
  exact mul_mem hyz (inv_mem (h hz))

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

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

Tactic:
hy

Goal state after:
case h
α : 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
⊢ x * y = y * x
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : 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 : α
⊢ y ∈ ↑s → x ≠ y → (fun x y ↦ Commute ((f * g) x) ((f * g) y)) x y

Tactic:
hy

Goal state after:
α : 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
⊢ x ≠ y → (fun x y ↦ Commute ((f * g) x) ((f * g) y)) x y
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
x y : α
h : f x = f y
⊢ r x y

Tactic:
exact hf h

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' : κ
⊢ y' ∈ ↑t → x' ≠ y' → (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'

Tactic:
hy

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
⊢ x' ≠ y' → (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'
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' : κ
⊢ y' ∈ ↑t → x' ≠ y' → (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'

Tactic:
hy

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
⊢ x' ≠ y' → (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ ∏ a ∈ s₁, f a = ∏ a ∈ s₂, g a

Tactic:
classical
  conv_lhs => rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]
  conv_rhs => rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]
  exact prod_congr rfl (by simpa)

Goal state after:
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
x✝ y✝ : G
⊢ y✝⁻¹ * x✝ ∈ f.ker ↔ (Con.ker f) x✝ y✝

Tactic:
Con.ker_rel,

Goal state after:
G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
x✝ y✝ : G
⊢ y✝⁻¹ * x✝ ∈ f.ker ↔ f x✝ = f y✝
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
P : Submonoid M
h : P.FG
S : Set M
hS : closure S = P
hf : S.Finite
⊢ AddSubmonoid.closure (⇑Additive.toMul ⁻¹' S) = toAddSubmonoid P

Tactic:
simp [← Submonoid.toAddSubmonoid_closure, hS]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s t : Finset M
⊢ (closure ↑s ⊔ closure ↑t).FG

Tactic:
exact ⟨s ∪ t, by simp [closure_union]⟩

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

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ (lift N φ HN).ker = ⊥ ↔ N = φ.ker

Tactic:
QuotientGroup.ker_lift,

Goal state after:
G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ Subgroup.map (mk' N) φ.ker = ⊥ ↔ N = φ.ker
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
s t : Finset G
⊢ (closure ↑s ⊔ closure ↑t).FG

Tactic:
exact ⟨s ∪ t, by simp [closure_union]⟩

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : Monoid M
G✝ : Type u_3
H : Type u_4
inst✝⁴ : Group G✝
inst✝³ : AddGroup H
ι : Type u_5
inst✝² : Finite ι
G : ι → Type u_6
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), Group.FG (G i)
⊢ (Subgroup.pi Set.univ fun i ↦ ⊤).FG

Tactic:
exact .pi fun i => Group.FG.out

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ : Type u
x✝ : FreeAbelianGroup α✝
x : α✝
ih : id <$> pure x = pure x
⊢ id <$> (-pure x) = -pure x

Tactic:
FreeAbelianGroup.map_neg,

Goal state after:
α : Type u
G : Type u_1
β α✝ : Type u
x✝ : FreeAbelianGroup α✝
x : α✝
ih : id <$> pure x = pure x
⊢ -id <$> pure x = -pure x
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
ih : Prod.mk p <$> pure q = (fun b a ↦ (a, b)) <$> pure q <*> pure p
⊢ Prod.mk p <$> (-pure q) = (fun b a ↦ (a, b)) <$> (-pure q) <*> pure p

Tactic:
FreeAbelianGroup.map_neg,

Goal state after:
case pure.neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
ih : Prod.mk p <$> pure q = (fun b a ↦ (a, b)) <$> pure q <*> pure p
⊢ -Prod.mk p <$> pure q = (fun b a ↦ (a, b)) <$> (-pure q) <*> pure p
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
ih : Prod.mk p <$> pure q = (fun b a ↦ (a, b)) <$> pure q <*> pure p
⊢ -Prod.mk p <$> pure q = (fun b a ↦ (a, b)) <$> (-pure q) <*> pure p

Tactic:
FreeAbelianGroup.map_neg,

Goal state after:
case pure.neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
ih : Prod.mk p <$> pure q = (fun b a ↦ (a, b)) <$> pure q <*> pure p
⊢ -Prod.mk p <$> pure q = -(fun b a ↦ (a, b)) <$> pure q <*> pure p
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
p : α✝
ih : Prod.mk <$> pure p <*> y = (fun b a ↦ (a, b)) <$> y <*> pure p
⊢ Prod.mk <$> (-pure p) <*> y = (fun b a ↦ (a, b)) <$> y <*> -pure p

Tactic:
FreeAbelianGroup.map_neg,

Goal state after:
case neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
p : α✝
ih : Prod.mk <$> pure p <*> y = (fun b a ↦ (a, b)) <$> y <*> pure p
⊢ -Prod.mk <$> pure p <*> y = (fun b a ↦ (a, b)) <$> y <*> -pure p
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
⊢ y ∈ H₂ → ∀ h ∈ ↑H₃, ⁅h, ⁅x, y⁆⁆ = 1

Tactic:
hy

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
⊢ ∀ h ∈ ↑H₃, ⁅h, ⁅x, y⁆⁆ = 1
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
z x y : FreeAbelianGroup T
hx : (lift fun x ↦ 1) x • of default = x
hy : (lift fun x ↦ 1) y • of default = y
⊢ x + (lift fun x ↦ 1) y • of default = x + y

Tactic:
hy

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
z x y : FreeAbelianGroup T
hx : (lift fun x ↦ 1) x • of default = x
hy : (lift fun x ↦ 1) y • of default = y
⊢ x + y = x + y
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}
x✝² x✝¹ : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
x✝ : (r' S) (p, q) (x, y)
t : ↥S
ht : ↑t * (↑(x, y).2 * (p, q).1) = ↑t * (↑(p, q).2 * (x, y).1)
⊢ b (p, q) (x, y)

Tactic:
← one_mul (p, q),

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}
x✝² x✝¹ : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
x✝ : (r' S) (p, q) (x, y)
t : ↥S
ht : ↑t * (↑(x, y).2 * (p, q).1) = ↑t * (↑(p, q).2 * (x, y).1)
⊢ b (1 * (p, q)) (x, y)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
y : OreLocalization S R
z : OreLocalization S X
r₁ : R
s₁ : ↥S
⊢ (r₁ /ₒ s₁ * y) • z = (r₁ /ₒ s₁) • y • z

Tactic:
cases y with | _ r₂ s₂
   =>  _ 

Goal state after:
case c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
z : OreLocalization S X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) • z = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • z