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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Surjective f ↔ ∀ (i : ι), Surjective ((U i).restrictPreimage f)

Tactic:
refine ⟨fun H i => (U i).restrictPreimage_surjective H, fun H x => ?_⟩
  obtain ⟨i, hi⟩ :=
    Set.mem_iUnion.mp
      (show x ∈ Set.iUnion U by rw [hU]; trivial)
  exact ⟨_, congr_arg Subtype.val (H i ⟨x, hi⟩).choose_spec⟩

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update g i x = g / mulSingle i (g i) * mulSingle i x

Tactic:
ext j
  rcases eq_or_ne i j with (rfl | h)
  · simp
  · simp [h, eqComm]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
a b : G
h : a * b ∈ H
⊢ b * a ∈ H

Tactic:
have : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H := nH.conj_mem (a * b) h a⁻¹

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
a b : G
h : a * b ∈ H
this : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H
⊢ b * a ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
⊢ H = ⊥

Tactic:
rw [Subgroup.eq_bot_iff_forall]

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
⊢ ∀ x ∈ H, x = 1
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑(e.symm.trans e)) H = H

Tactic:
MulEquiv.symm_trans_self,

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑(MulEquiv.refl N)) H = H
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
K L : Subgroup N
hf : Surjective ⇑f
⊢ comap f K ≤ comap f L ∧ ¬comap f L ≤ comap f K ↔ K ≤ L ∧ ¬L ≤ K

Tactic:
comap_le_comap_of_surjective hf

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

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
⊢ x ∈ s ⊔ t → ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
intro hx

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ s ⊔ t
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set M
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
simp_rw [closure, op_sInf, Set.preimage_ofPred_eq, Subsemigroup.coe_unop]
  congr with a
  exact MulOpposite.unop_surjective.forall

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
x✝ : (fun x ↦ x ∈ Set.range encode) x
n : α
hn : encode n = x
⊢ (decode₂ α (encode n)).isSome = true

Tactic:
encodek₂

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
x✝ : (fun x ↦ x ∈ Set.range encode) x
n : α
hn : encode n = x
⊢ (some n).isSome = true
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
x : α
hx : encode x = ↑n
⊢ (decode₂ α (encode x)).isSome = true

Tactic:
encodek₂

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
x : α
hx : encode x = ↑n
⊢ (some x).isSome = true
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : α
⊢ decode₂ α (encode x✝) = some x✝

Tactic:
encodek₂

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : α
⊢ some x✝ = some x✝
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : α → Type u_3
inst✝¹ : Encodable α
inst✝ : (a : α) → Encodable (γ a)
x✝ : Sigma γ
a : α
b : γ a
⊢ decodeSigma (encodeSigma ⟨a, b⟩) = some ⟨a, b⟩

Tactic:
simp [encodeSigma, decodeSigma, unpair_pair, encodek]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g h : G
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x * g⁻¹ = h) ↔ h ∈ s)

Tactic:
simp_rw [mul_inv_eq_iff_eq_mul, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, exists_eq_right, iff_comm]

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x } ⊕ { x // q x }
⊢ (subtypeOrLeftEmbedding p q)
      (Sum.elim (⇑(Subtype.impEmbedding p (fun x ↦ p x ∨ q x) ⋯)) (⇑(Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯)) x) =
    x

Tactic:
cases x with
    | inl x => grind
    | inr x =>
      simp only [Sum.elim_inr]
      rw [subtypeOrLeftEmbedding_apply_right]
      · grind
      · suffices ¬p x by simpa
        intro hp
        simpa using h.le_bot x ⟨hp, x.prop⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
⊢ IsScalarTower M N α

Tactic:
by
  refine ⟨fun x => Submonoid.induction_of_closure_eq_top_left htop x ?_ ?_⟩
  · intro y z
    rw [one_smul, one_smul]
  · clear x
    intro x hx x' hx' y z
    rw [mul_smul, mul_smul, hs x hx, hx']

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
⊢ toFunAux (ofNat s (n + 1)) = n + 1

Tactic:
have h₂ : {x ∈ range (succ (ofNat s n)) | x ∈ s} =
        insert ↑(ofNat s n) {x ∈ range (ofNat s n) | x ∈ s} := by
      simp only [Finset.ext_iff, mem_insert, mem_range, mem_filter]
      exact fun m =>
        ⟨fun h => by
          simp only [h.2, and_true]
          exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1)),
         fun h =>
          h.elim (fun h => h.symm ▸ ⟨lt_succ_self _, (ofNat s n).prop⟩) fun h =>
            ⟨h.1.trans (lt_succ_self _), h.2⟩⟩

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
h₂ : {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})
⊢ toFunAux (ofNat s (n + 1)) = n + 1
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (↑(insert a s)) (max a (s.max' H))

Tactic:
by
    rw [coe_insert]
    exact (isGreatest_max' _ _).insert _

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

Goal state before:
pp: case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
⊢ motive s

Tactic:
← insert_erase has

Goal state after:
case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
⊢ motive (Insert.insert a (s.erase a))
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : i ∈ lowerBounds ↑s ∧ i ∈ upperBounds (lowerBounds ↑s)
⊢ i = s.min' hs

Tactic:
mem_lowerBounds,

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : (∀ x ∈ ↑s, i ≤ x) ∧ i ∈ upperBounds (lowerBounds ↑s)
⊢ i = s.min' hs
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case succ.cons
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : powersetCardAux (n + 1) l₁✝ ~ powersetCardAux (n + 1) l₂✝
⊢ powersetCardAux (n + 1) (x✝ :: l₁✝) ~ powersetCardAux (n + 1) (x✝ :: l₂✝)

Tactic:
simp only [powersetCardAux_cons]

Goal state after:
case succ.cons
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : powersetCardAux (n + 1) l₁✝ ~ powersetCardAux (n + 1) l₂✝
⊢ powersetCardAux (n + 1) l₁✝ ++ List.map (cons x✝) (powersetCardAux n l₁✝) ~
    powersetCardAux (n + 1) l₂✝ ++ List.map (cons x✝) (powersetCardAux n l₂✝)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.inr
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₂ l₁' : List α
h : (l₁', l₂) ∈ l.sublists'.zip l.sublists'.reverse
⊢ a :: l₁' ++ l₂ ~ a :: l

Tactic:
exact (IH _ _ h).cons _

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : IsEmpty β
f : β → α
S : Finset β
⊢ S.sup f = ⊥

Tactic:
rw [Finset.sup_eq_bot_iff]

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : IsEmpty β
f : β → α
S : Finset β
⊢ ∀ s ∈ S, f s = ⊥
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ image some (eraseNone s) = s.erase none

Tactic:
ext (_ | x)

Goal state after:
case none
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ none ∈ image some (eraseNone s) ↔ none ∈ s.erase none

case some
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ some x ∈ image some (eraseNone s) ↔ some x ∈ s.erase none
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ insertNone (eraseNone s) = insert none s

Tactic:
ext (_ | x)

Goal state after:
case none
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ none ∈ insertNone (eraseNone s) ↔ none ∈ insert none s

case some
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ some x ∈ insertNone (eraseNone s) ↔ some x ∈ insert none s
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h✝ : Nonempty ι
⊢ ⨆ i, ⨆ (h : p i), f i h = sSup ∅

Tactic:
have (i : ι) : IsEmpty (p i) := ⟨hp i⟩

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h✝ : Nonempty ι
this : ∀ (i : ι), IsEmpty (p i)
⊢ ⨆ i, ⨆ (h : p i), f i h = sSup ∅
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (range fun x ↦ f ↑x)
hne : s.Nonempty
this : Nonempty ↑s
⊢ l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)

Tactic:
refine gc.l_ciSup_of_directed ?_ hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (range fun x ↦ f ↑x)
hne : s.Nonempty
this : Nonempty ↑s
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ f ↑i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
⊢ ↑(⨆ i ∈ s, f i) = ⨆ i ∈ s, ↑(f i)

Tactic:
refine le_antisymm ((WithBot.coe_iSup (OrderTop.bddAbove _)).trans_le <|
    iSup_le_iff.mpr fun i ↦ ?_) <| iSup_le_iff.mpr <| fun _ ↦ iSup_le_iff.mpr <|
      fun hi ↦ WithBot.coe_le_coe.mpr (le_biSup _ hi)

Goal state after:
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
⊢ ↑(⨆ (_ : i ∈ s), f i) ≤ ⨆ i ∈ s, ↑(f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Set ι
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i ∈ f '' s

Tactic:
lift s to Finset ι using hs
  simp only [Finset.mem_coe] at h
  simpa using Finset.ciSup_mem_image f h

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

Goal state before:
pp: case mp
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ x ∈ t → ∃ i, x ∈ s ↑i ∩ t

pp: case mpr
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ (∃ i, x ∈ s ↑i ∩ t) → x ∈ t

Tactic:
· intro x_in
      rcases mem_iUnion.mp (hI x_in) with ⟨i, _, ⟨hi, rfl⟩, H⟩
      exact ⟨⟨i, hi⟩, ⟨H, x_in⟩⟩

Goal state after:
case mpr
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ (∃ i, x ∈ s ↑i ∩ t) → x ∈ t
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h : a ≠ ⊤
⊢ subtypeOrderIso.symm a = ↑⟨a, h⟩

Tactic:
OrderIso.symm_apply_eq

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h : a ≠ ⊤
⊢ a = subtypeOrderIso ↑⟨a, h⟩
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hn : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) c
s : Set α
hs : s.Finite
hsc : ↑hs.toFinset ⊆ ⋃ i ∈ c, i
this : ∃ i ∈ c, ↑hs.toFinset ⊆ i
⊢ ∃ t ∈ c, s ⊆ t

Tactic:
exact hs.coe_toFinset ▸ this

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
h : (a₁, b₁) ⋖ (a₂, b₂)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂

Tactic:
obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h.wcovBy
    · exact Or.inr ⟨mk_covBy_mk_iff_right.1 h, rfl⟩
    · exact Or.inl ⟨mk_covBy_mk_iff_left.1 h, rfl⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, (∃ a_1 ∈ t i, ⟨i, a_1⟩ = a) → ¬∃ a_2 ∈ t j, ⟨j, a_2⟩ = a

Tactic:
rintro _ ⟨y, _, rfl⟩ ⟨z, _, hz'⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
y : α i
left✝¹ : y ∈ t i
z : α j
left✝ : z ∈ t j
hz' : ⟨j, z⟩ = ⟨i, y⟩
⊢ False
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' ↑s) ↑s
⊢ (s.preimage f ⋯).sup f = s.sup id

Tactic:
have hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x := hf.invOn_invFunOn.2

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' ↑s) ↑s
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x
⊢ (s.preimage f ⋯).sup f = s.sup id
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
h : Minimal (fun x ↦ P x ∨ Q x) x
⊢ Minimal P x ∨ Minimal Q x

Tactic:
by
  obtain ⟨h | h, hmin⟩ := h
  · exact .inl ⟨h, fun y hy hyx ↦ hmin (Or.inl hy) hyx⟩
  exact .inr ⟨h, fun y hy hyx ↦ hmin (Or.inr hy) hyx⟩

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
⊢ MinimalFor Q f i

Tactic:
refine ⟨h.prop, fun j hj hle ↦ ?_⟩
  by_contra
  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.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ a ::ₘ Ioo a b = Ico a b

Tactic:
classical
    rw [Ioo, ← Finset.insert_val_of_notMem left_notMem_Ioo, Finset.Ioo_insert_left h]
    rfl

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : ℕ →o α
n m : ℕ
h : n ≤ m
⊢ ¬(a n ≤ a m ∧ a n ≠ a m) ↔ a n = a m

Tactic:
simp [a.mono h]

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

Goal state before:
pp: P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : seed.succ ≤ x✝
hP✝ : P x✝
⊢ x✝ < k * x✝

Tactic:
convert! (Nat.mul_lt_mul_right <| seed.succ_pos.trans_le hl).2 hk

Goal state after:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n x✝ : ℕ
hl : seed.succ ≤ x✝
hP✝ : P x✝
⊢ x✝ = 1 * x✝
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : OrderBot α
⊢ Unique ↥(Iic ⊥)

Tactic:
by
  rw [Iic_bot]
  infer_instance

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

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

Tactic:
intro hx

Goal state after:
case mpr
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 : α
hx : a ∈ ⋃ g, (fun x ↦ g • x) '' U
⊢ a ∈ f ⁻¹' f '' U
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ ConjClasses.mk (h * g * h⁻¹) = Quot.mk (⇑(IsConj.setoid G)) g

Tactic:
apply mk_eq_mk_iff_isConj.mpr

Goal state after:
case refine_3.mk
G : Type u_2
inst✝ : Group G
a✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
h : G
⊢ IsConj (h * g * h⁻¹) g
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : c ∈ centralizer s
hn : n ∈ normalizer s
⊢ n * c * n⁻¹ ∈ centralizer s

Tactic:
refine mem_centralizer_iff_commutator_eq_one'.mpr fun g hg ↦ ?_

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : c ∈ centralizer s
hn : n ∈ normalizer s
g : G
hg : g ∈ s
⊢ ⁅n * c * n⁻¹, g⁆ = 1
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : c ∈ centralizer s
hn : n ∈ normalizer s
g : G
hg : g ∈ s
this : n * (c * (n⁻¹ * g * n) * c⁻¹ * n⁻¹ * g⁻¹) = 1
⊢ ⁅n * c * n⁻¹, g⁆ = 1

Tactic:
simpa [commutatorElement_def, mul_assoc]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ normalizer {g} = centralizer {g}

Tactic:
refine ext fun h ↦ ⟨?_, ?_⟩
  · rintro hh g rfl
    exact mul_eq_of_eq_mul_inv (hh g |>.mp rfl).symm
  · refine fun hh g ↦ ⟨?_, ?_⟩ <;> rintro rfl
    · exact (eq_mul_inv_of_mul_eq <| hh g rfl).symm
    · simpa using hh _ rfl

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ s * ↑(closure s) = ↑(closure s)

Tactic:
by
  rw [← smul_eq_mul, ← Set.iUnion_smul_set]
  have h a (ha : a ∈ s) : a • (closure s : Set G) = closure s :=
    smul_coe_set <| subset_closure ha
  simp +contextual [h, hs]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj ↑h • P ≤ H

Tactic:
rintro - ⟨g, hg, rfl⟩

Goal state after:
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
g : G
hg : g ∈ ↑P
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj ↑h)) g ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj h • P.subgroupOf H ≤ (MulAut.conj ↑h • P).subgroupOf H

Tactic:
rintro - ⟨g, hg, rfl⟩

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h g : ↥H
hg : g ∈ ↑(P.subgroupOf H)
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut ↥H) ↥H) (MulAut.conj h)) g ∈ (MulAut.conj ↑h • P).subgroupOf H
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
⊢ ∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j

Tactic:
rw [← Function.Embedding.coe_subtype, ← prod_map]
  simp [attach_map_val]

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

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

Tactic:
simp [ofAdd]

Goal state after:
M : Type u_3
inst✝ : AddMonoid M
s : List M
⊢ s.sum = s.prod
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

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

Tactic:
simp [ofAdd]

Goal state after:
M : Type u_3
inst✝ : AddCommMonoid M
s : Multiset M
⊢ s.sum = s.prod
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ insert i (univ.erase i),
    (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M x_1) (x x_1)) = Pi.mulSingle x_1 (x x_1) i

Tactic:
intro j _; dsimp

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

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

Tactic:
rw [eqvGen_eq]
  apply congr_arg sInf
  simp only [le_def, or_imp, ← forall_and]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ n.succ) (x ^ n.succ)

Tactic:
simpa [pow_succ] using c.mul (Con.pow c n h) h

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a b c : FreeGroup α), a * b * c = a * (b * c)

Tactic:
by rintro ⟨L₁⟩ ⟨L₂⟩ ⟨L₃⟩; simp

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
H : Step L₁ L₂
⊢ Lift.aux f L₁ = Lift.aux f L₂

Tactic:
by
  obtain @⟨_, _, _, b⟩ := H; cases b <;> simp [Lift.aux, List.prod_append]

Goal state after: