mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b ∨ Lex r s b a

Tactic:
rintro ⟨i, a⟩ ⟨j, b⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a : α i
j : ι
b : α j
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
⊢ ∀ {a b : (i : ι) × α i}, Lex r s a b ∨ a = b ∨ Lex r s b a

Tactic:
rintro ⟨i, a⟩ ⟨j, b⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
j : ι
b : α j
⊢ Lex r s ⟨i, a⟩ ⟨j, b⟩ ∨ ⟨i, a⟩ = ⟨j, b⟩ ∨ Lex r s ⟨j, b⟩ ⟨i, a⟩
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case left
ι : Sort u_1
α : ι → Sort u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ ⟨a₁✝, a⟩ ⟨a₂✝, b⟩

Tactic:
exact Lex.left _ _ (hr _ _ hij)

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
s✝ t r : Set α
s : ι → Set α
h : Pairwise (Disjoint on s)
⊢ Injective fun x ↦ ↑x.snd

Tactic:
rintro ⟨i, x, hx⟩ ⟨j, -, hx'⟩ rfl
    obtain rfl : i = j := h.eq (not_disjoint_iff.2 ⟨_, hx, hx'⟩)
    rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_right : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ s), motive x hx → motive (x * y) ⋯
x : M
h : x ∈ closure s
⊢ { unop' := x } ∈ closure (MulOpposite.unop ⁻¹' s)

Tactic:
by rwa [← op_closure]

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

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

Tactic:
simp [@forall_comm _ β]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
f : β → α
inst✝ : DecidableEq β
s : Finset γ
Hs : s.Nonempty
t : γ → Finset β
Ht : ∀ (b : γ), (t b).Nonempty
c : α
⊢ (s.biUnion t).sup' ⋯ f ≤ c ↔ (s.sup' Hs fun b ↦ (t b).sup' ⋯ f) ≤ c

Tactic:
simp [@forall_comm _ β]

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Bot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
P : β → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
this✝ : OrderBot { x // P x } := Subtype.orderBot Pbot
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ (SupHom.subtypeVal Psup).toFun ⊥ = ⊥

Tactic:
simp [Subtype.coe_bot Pbot]

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
P : β → Prop
Pbot : P ⊥
Ptop : P ⊤
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
this✝ : Lattice { x // P x } := Subtype.lattice Psup Pinf
this : BoundedOrder (Subtype P) := Subtype.boundedOrder Pbot Ptop
⊢ (LatticeHom.subtypeVal Psup Pinf).toFun ⊥ = ⊥

Tactic:
simp [Subtype.coe_bot Pbot]

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ l.reverse.Nodup ↔ l.Nodup

Tactic:
nodup_reverse

Goal state after:
α : Type u
l : List α
⊢ l.Nodup ↔ l.Nodup
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.inf fun b ↦ a \ f b) = a \ s.sup f

Tactic:
induction hs using Finset.Nonempty.cons_induction with
  | singleton => rw [sup_singleton, inf_singleton]
  | cons _ _ _ _ ih => rw [sup_cons, inf_cons, ih, sdiff_sup]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ∈ powersetCard n (map f s) ↔ t ∈ map (mapEmbedding f).toEmbedding (powersetCard n s)

Tactic:
simp only [mem_powersetCard, mem_map]
    constructor
    · classical
      intro h
      have : map f (filter (fun x => (f x ∈ t)) s) = t := by grind
      refine ⟨_, ?_, this⟩
      rw [← card_map f, this, h.2]; simp
    · rintro ⟨a, ⟨has, rfl⟩, rfl⟩
      simp [has]

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

Goal state before:
pp: case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ (∃ b ∈ s, a ≤ f b) → a ≤ s.sup f

Tactic:
· exact fun ⟨b, hb, hle⟩ => le_trans hle (le_sup hb)

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

Goal state before:
pp: ι : Type u_5
α : Type u_7
inst✝² : LinearOrder α
inst✝¹ : BoundedOrder α
inst✝ : Nontrivial α
s : Finset ι
f : ι → α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
simp only [← top_le_iff]

Goal state after:
ι : Type u_5
α : Type u_7
inst✝² : LinearOrder α
inst✝¹ : BoundedOrder α
inst✝ : Nontrivial α
s : Finset ι
f : ι → α
⊢ ⊤ ≤ s.sup f ↔ ∃ b ∈ s, ⊤ ≤ f b
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ a < s.sup' H f ↔ ∃ b ∈ s, a < f b

Tactic:
← WithBot.coe_lt_coe,

Goal state after:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ ↑a < ↑(s.sup' H f) ↔ ∃ b ∈ s, a < f b
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ s.sup' H f < a ↔ ∀ i ∈ s, f i < a

Tactic:
← WithBot.coe_lt_coe,

Goal state after:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ ↑(s.sup' H f) < ↑a ↔ ∀ i ∈ s, f i < a
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Finite ι
f : ι → Set α
inst✝ : ∀ (i : ι), Finite ↑(f i)
this : Fintype (PLift ι)
⊢ Finite ↑(⋃ i, f i)

Tactic:
have : ∀ i, Fintype (f i) := fun i => Fintype.ofFinite _

Goal state after:
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : Finite ι
f : ι → Set α
inst✝ : ∀ (i : ι), Finite ↑(f i)
this✝ : Fintype (PLift ι)
this : (i : ι) → Fintype ↑(f i)
⊢ Finite ↑(⋃ i, f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
h : s.Nonempty
hs : s.Finite
⊢ sSup s ∈ s

Tactic:
by
  lift s to Finset α using hs
  exact Finset.Nonempty.csSup_mem h

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

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
hs : Pairwise fun i j ↦ Disjoint (s i) (s j)
h : (⋃ i, s i).Finite
u : ↑{i | (s i).Nonempty} → ↑(⋃ i, s i) := fun i ↦ ⟨Exists.choose ⋯, ⋯⟩
i : ι
hi : i ∈ {i | (s i).Nonempty}
j : ι
hj : j ∈ {i | (s i).Nonempty}
hij : u ⟨i, hi⟩ = u ⟨j, hj⟩
⊢ ↑(u ⟨j, hj⟩) ∈ s ↑⟨j, hj⟩

Tactic:
exact hj.choose_spec

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 → α
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
suffices ∀ {ι : Type v} {κ : ι → Type w} [Finite ι] (f : Π a, κ a → α),
      ⨅ a, ⨆ b, f a b = ⨆ g : (Π a, κ a), ⨅ a, f a (g a) by
    simpa [← Equiv.plift.symm.iInf_comp, ← Equiv.plift.symm.iSup_comp,
        ← (Equiv.plift.piCongr fun a => @Equiv.plift (κ a.down)).symm.iSup_comp] using!
      this (κ := fun a => PLift (κ a.down)) fun (a : PLift ι) b => f a.down b.down

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.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ ⨅ i ∈ s, i = sInf s

Tactic:
rw [← csInf_image (Subtype.range_coe ▸ hs), Set.image_id']

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ ⨅ i, ↑i ≤ sInf ∅
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)

Tactic:
simp only [Maximal, and_congr_right_iff]
  exact fun _ ↦ ⟨fun h x hxs hx ↦ hxs <| h hx (subset_insert _ _) (mem_insert_self x s),
    fun h t ht hst x hxt ↦ by_contra fun hxs ↦ h x hxs (hP ht (insert_subset hxt hst))⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Iio b = Iic a

Tactic:
← Iic_union_Ioo_eq_Iio h.lt,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Iic a ∪ Ioo a b = Iic a
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : WithTop α
⊢ ¬a ⋖ ⊤

Tactic:
by
  simp [covBy_top_iff]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ↑a ⋖ ⊤ ↔ IsMax a

Tactic:
simp [covBy_iff_Ioo_eq, ← image_coe_Ioi]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s
hs : P s
h : ¬Minimal P s
⊢ ∃ x, x ∈ s ∧ P (s \ {x})

Tactic:
by
  simpa [Set.minimal_iff_forall_sdiff_singleton hP, hs] using h

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case mpr
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ k + 1 ∈ s ∧ k ∉ s → sInf s = k + 1

Tactic:
· rintro ⟨H, H'⟩
    rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]
    exact ⟨H, fun n hnk hns ↦ H' <| hs n k (Nat.lt_succ_iff.mp hnk) hns⟩

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ Nat.find ⋯ + n = sInf {m | p m}

Tactic:
Nat.sInf_def hp

Goal state after:
case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ Nat.find ⋯ + n = Nat.find hp
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
⊢ Nat.find ⋯ + n = Nat.find hp

Tactic:
Nat.sInf_def hp

Goal state after:
case inr
n : ℕ
p : ℕ → Prop
m : ℕ
hm : m ∈ {m | p (m + n)}
hp : ∃ n, n ∈ {m | p m}
hn : n ≤ Nat.find hp
⊢ Nat.find ⋯ + n = Nat.find hp
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t

Tactic:
have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
      simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
        Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
    cases this
    exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
      ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]

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

Goal state before:
pp: n a : ℕ
⊢ Multiset.map (fun x ↦ x % a) (Multiset.Ico n (n + a)) = Multiset.range a

Tactic:
convert! congr_arg Finset.val (image_Ico_mod n a)
  refine ((nodup_map_iff_inj_on (Finset.Ico _ _).nodup).2 <| ?_).dedup.symm
  exact mod_injOn_Ico _ _

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
tfae_2_to_3 : {b | ReflTransGen r b a}.WellFoundedOn r → {b | TransGen r b a}.WellFoundedOn r
⊢ {b | TransGen r b a}.WellFoundedOn r → Acc r a

Tactic:
refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)

Goal state after:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
tfae_2_to_3 : {b | ReflTransGen r b a}.WellFoundedOn r → {b | TransGen r b a}.WellFoundedOn r
h : {b | TransGen r b a}.WellFoundedOn r
b : α
hb : r b a
⊢ Fibration (Subrel r fun x ↦ x ∈ {b | TransGen r b a}) r Subtype.val
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ici a ⊂ Ici b ↔ b < a

Tactic:
simp [← coe_ssubset]

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iic a ⊂ Iic b ↔ a < b

Tactic:
simp [← coe_ssubset]

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

Goal state after:
ι : Type u_1
α : Type u_2
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : OrderBot α
⊢ Unique ↥{⊥}
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Preorder α
p : α → Prop
inst✝⁵ : DecidablePred p
y : α
F : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : Preorder M
inst✝³ : Preorder N
inst✝² : EquivLike F M N
inst✝¹ : OrderIsoClass F M N
f : F
inst✝ : LocallyFiniteOrder N
⊢ ∀ (a b x : M), x ∈ map { toFun := EquivLike.inv f, inj' := ⋯ } (finsetIoo (f a) (f b)) ↔ a < x ∧ x < b

Tactic:
by
    simp [finset_mem_Ioo, EquivLike.inv_apply_eq, map_lt_map_iff]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
⊢ (insert a s).IsWF ↔ s.IsWF

Tactic:
simp only [← singleton_union, isWF_union, isWF_singleton, true_and]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
⊢ (insert a s).IsWF ↔ s.IsWF

Tactic:
by
  simp only [← singleton_union, isWF_union, isWF_singleton, true_and]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Preorder α
f : ι → α
s : Set ι
h✝ : (f '' s).IsPWO
hs : s.Nonempty
a : ι
ha : a ∈ s
h : Minimal (fun x ↦ x ∈ f '' s) (f a)
⊢ ∃ i, MinimalFor (fun x ↦ x ∈ s) f i

Tactic:
exact ⟨a, ha, fun b hb => h.2 (mem_image_of_mem _ hb)⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc (b ⊓ a) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)

Tactic:
sup_comm

Goal state after:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc (b ⊓ a) (b ⊔ a) = Icc (b ⊓ a) (b ⊔ a)
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
⊢ ⟦a⟧ = ⟦b⟧ ↔ ⟦↑a⟧ = ⟦↑b⟧

Tactic:
← @Quotient.mk''_eq_mk,

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
⊢ Quotient.mk'' a = Quotient.mk'' b ↔ Quotient.mk'' ↑a = Quotient.mk'' ↑b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case pos
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
    (if n < g 0 then f n else (f (g (n - g 0))).tail)
hn : n < g 0
⊢ List.SublistForall₂ r (f m) (f n)

Tactic:
rwa [if_pos hn, if_pos (mn.trans hn)] at hmn

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g k : G
⊢ k ∈ centralizer {g} ↔ k * g = g * k

Tactic:
by
  simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq]
  exact eq_comm

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalizerMonoidHom.ker = (centralizer ↑H).subgroupOf (normalizer ↑H)

Tactic:
simp [Subgroup.ext_iff, DFunLike.ext_iff, Subtype.ext_iff,
    mem_subgroupOf, mem_centralizer_iff, eq_mul_inv_iff_mul_eq, eq_comm]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
mul_right : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯
mul_inv_cancel : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯
x : G
h : x ∈ closure s
⊢ { unop' := x } ∈ closure (MulOpposite.unop ⁻¹' s)

Tactic:
by rwa [← op_closure]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
g : G
hg : g ∈ normalizer ↑H ⊓ normalizer ↑K
⊢ g ∈ normalizer ↑(H ⊔ K)

Tactic:
simp_rw [mem_inf, mem_normalizer_iff_map_conj_eq, map_sup, hg.1, hg.2] at hg ⊢

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
hHnK : normalizer ↑H ≤ normalizer ↑K
⊢ normalizer ↑H ≤ normalizer ↑(K ⊔ H)

Tactic:
sup_comm

Goal state after:
G : Type u_2
inst✝ : Group G
H K : Subgroup G
hHnK : normalizer ↑H ≤ normalizer ↑K
⊢ normalizer ↑H ≤ normalizer ↑(H ⊔ K)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ MulAut.conj h • H = H

Tactic:
by
  refine le_antisymm ?_ ?_
  · exact (conj_smul_le_of_le (le_refl H) ⟨h, hh⟩)
  · rw [subset_pointwise_smul_iff, ← map_inv]
    exact conj_smul_le_of_le (le_refl H) ⟨h⁻¹, H.inv_mem hh⟩

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

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
S : Set (Setoid α)
⊢ sSup S = EqvGen.setoid fun x y ↦ ∃ r ∈ S, r x y

Tactic:
eqvGen_eq

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
r : Setoid α
⊢ EqvGen.setoid ⇑r ≤ r

Tactic:
eqvGen_eq

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
⊢ EqvGen.setoid r ≤ s

Tactic:
eqvGen_eq

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
hu : s' ⊆ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
have hf : ∀ c ∈ s, c ∉ s' → f c = 1 := by grind

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
hu : s' ⊆ s
hf : ∀ c ∈ s, c ∉ s' → f c = 1
⊢ ∏ x ∈ s, f x = f a * f b
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝ : FreeGroup Unit
L : List (Unit × Bool)
⊢ (fun x ↦ of () ^ x) ((fun x ↦ ((map fun x ↦ 1) x).sum) (Quot.mk Red.Step L)) = Quot.mk Red.Step L

Tactic:
simp only [quot_mk_eq_mk, map.mk, sum_mk, List.map_map]

Goal state after:
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝ : FreeGroup Unit
L : List (Unit × Bool)
⊢ of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) L).sum = mk L
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ x ∈ insert n (range n), f x = f n * ∏ x ∈ range n, f x

Tactic:
prod_insert notMem_range_self

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ f n * ∏ x ∈ range n, f x = f n * ∏ x ∈ range n, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case zero
M : Type u_4
inst✝ : CommMonoid M
f s : ℕ → M
base : s 0 = 1
step : ∀ k < 0, s (k + 1) = s k * f k
⊢ 1 = s 0

Tactic:
base

Goal state after:
case zero
M : Type u_4
inst✝ : CommMonoid M
f s : ℕ → M
base : s 0 = 1
step : ∀ k < 0, s (k + 1) = s k * f k
⊢ 1 = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f s : ℕ → M
base : s 0 = 1
n : ℕ
step : ∀ k < n, s (k + 1) = s k * f k
⊢ ∏ k ∈ range n, f k = s n

Tactic:
induction n with
  | zero => rw [Finset.prod_range_zero, base]
  | succ k hk =>
    rw [Finset.prod_range_succ, step _ (Nat.lt_succ_self _), hk]
    exact fun _ hl ↦ step _ (Nat.lt_succ_of_lt hl)

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type u
f : FreeAbelianGroup (α → β)
x y : FreeAbelianGroup α
⊢ (lift fun x_1 ↦ x_1 <$> (x + y)) f = (lift fun x_1 ↦ x_1 <$> x) f + (lift fun x ↦ x <$> y) f

Tactic:
simp [← Pi.add_def]

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ (QuotientGroup.mk' N) ⁅x, y⁆ = 1

Tactic:
QuotientGroup.mk'_apply,

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ↑⁅x, y⁆ = 1
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x' y' : G ⧸ N
⊢ x' * y' = y' * x'

Tactic:
obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective N x'
    obtain ⟨y, rfl⟩ := QuotientGroup.mk'_surjective N y'
    rw [← commutatorElement_eq_one_iff_mul_comm, ← map_commutatorElement, QuotientGroup.mk'_apply,
      QuotientGroup.eq_one_iff]
    apply hGN
    rw [commutator_eq_closure]
    exact Subgroup.subset_closure (commutator_mem_commutatorSet x y)

Goal state after: