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

Goal state before:
pp: α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst✝ : DecidableEq α
⊢ s.pi t = ∅ ↔ ∃ a ∈ s, t a = ∅

Tactic:
contrapose!

Goal state after:
α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst✝ : DecidableEq α
⊢ (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
⊢ ¬a ∈ s

Tactic:
simp only [nodup_cons] at hs

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
hs : ¬a ∈ s ∧ s.Nodup
⊢ ¬a ∈ s
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
⊢ s.Nodup

Tactic:
simp only [nodup_cons] at hs

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : ¬a ∈ s ∧ s.Nodup
⊢ s.Nodup
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: r n : ℕ
h : r < n / 2
⊢ r < n - r

Tactic:
Nat.lt_sub_iff_add_lt,

Goal state after:
r n : ℕ
h : r < n / 2
⊢ r + r < n
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : DecidableEq (ι → α)
s : Finset α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ s.piDiag ι ⊆ Fintype.piFinset fun x ↦ s

Tactic:
simp [← piFinset_filter_const]

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
⊢ Pairwise (Disjoint on fun b ↦ Multiset.map (Pi.cons s a b) (s.pi t)) (t a)

Tactic:
refine (ht a <| mem_cons_self _ _).pairwise ?_

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
⊢ ∀ (a_1 : β a),
    a_1 ∈ t a → ∀ (b : β a), b ∈ t a → a_1 ≠ b → (Disjoint on fun b ↦ Multiset.map (Pi.cons s a b) (s.pi t)) a_1 b
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (image2 f s t).Infinite
⊢ (s ×ˢ t).Infinite

Tactic:
rw [← image_uncurry_prod] at h

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (uncurry f '' s ×ˢ t).Infinite
⊢ (s ×ˢ t).Infinite
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ SemiconjBy (↑((Units.map f) c)) (f a) (f b)

Tactic:
Units.coe_map,

Goal state after:
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ SemiconjBy (f ↑c) (f a) (f b)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
⊢ InjOn f (⋃ i, s i)

Tactic:
intro x hx y hy hxy
  rcases mem_iUnion.1 hx with ⟨i, hx⟩
  rcases mem_iUnion.1 hy with ⟨j, hy⟩
  rcases hs i j with ⟨k, hi, hj⟩
  exact hf k (hi hx) (hj hy) hxy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
⊢ s ×ˢ ⋂ i, t i = ⋂ i, s ×ˢ t i

Tactic:
ext x
  simp only [mem_prod, mem_iInter]
  exact ⟨fun h i => ⟨h.1, h.2 i⟩, fun h => ⟨(h hι.some).1, fun i => (h i).2⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = (Prod.mk '' s).seq t

Tactic:
rw [seq_eq_image2, image2_image_left, image2_mk_eq_prod]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

Tactic:
contrapose! +distrib
    rintro (hs | rfl)
    · exact hs.zpow
    · simp

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

Goal state before:
pp: case mp
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x⁻¹) → ∃ x, x ∈ H ∧ P x

Tactic:
· rintro ⟨x, x_in, hx⟩
      exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x) → ∃ x, x ∈ H ∧ P x⁻¹

Tactic:
· rintro ⟨x, x_in, hx⟩
      exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ¬∀ x ∈ H, x = 1

Tactic:
simp only [ne_eq, not_forall, exists_prop]

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∃ n, x ^ n = 1

Tactic:
exact ⟨0, zpow_zero x⟩

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

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

Tactic:
constructor <;> rintro rfl

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 (↑e) (map (↑e.symm) H) = H

case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑e.symm) (map (↑e) K) = K
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
I : Set ι
x : (i : ι) → M i
⊢ (x ∈ pi I fun i ↦ ⊤) ↔ x ∈ ⊤

Tactic:
by simp [mem_pi]

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

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
H : (i : ι) → Submonoid (M i)
x : (i : ι) → M i
⊢ x ∈ pi ∅ H ↔ x ∈ ⊤

Tactic:
by simp [mem_pi]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
⊢ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (Additive.ofMul x))

Tactic:
by
  ext
  exact Set.mem_image_iff_of_inverse (congrFun rfl) (congrFun rfl)

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

Goal state before:
pp: η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
x : (i : η) → f i
⊢ (x ∈ pi I fun i ↦ ⊤) ↔ x ∈ ⊤

Tactic:
by simp [mem_pi]

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

Goal state before:
pp: η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
x : (i : η) → f i
⊢ x ∈ pi ∅ H ↔ x ∈ ⊤

Tactic:
by simp [mem_pi]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s t : Set α
⊢ image2 (fun x1 x2 ↦ x1 • x2) (op '' s) t = t * s

Tactic:
← image2_mul,

Goal state after:
α : Type u_2
inst✝ : Mul α
s t : Set α
⊢ image2 (fun x1 x2 ↦ x1 • x2) (op '' s) t = image2 (fun x1 x2 ↦ x1 * x2) t s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * (b * a * b⁻¹) * c⁻¹ ∈ H

Tactic:
rw [mul_assoc, mul_assoc, ← mul_inv_rev, ← mul_assoc, ← mul_assoc]; exact h (c * b)

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x ∈ y :: ys
⊢ x ≤ (y :: ys).prod

Tactic:
| cons y ys ih =>

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

Goal state before:
pp: M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
H : Subgroup G
⊢ Subgroup.map H.subtype ((I.inertia G).subgroupOf H) = I.inertia G ⊓ H

Tactic:
Subgroup.subgroupOf_map_subtype

Goal state after:
M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
H : Subgroup G
⊢ I.inertia G ⊓ H = I.inertia G ⊓ H
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (x ^ (m.succ % n)) ^ k = x ^ (k * (↑(m % n)).toNat) * x ^ k

Tactic:
← pow_eq_pow_mod _ hx

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (x ^ m.succ) ^ k = x ^ (k * (↑(m % n)).toNat) * x ^ k
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (x ^ m.succ) ^ k = (x ^ (m % n)) ^ k * x ^ k

Tactic:
← pow_eq_pow_mod _ hx

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (x ^ m.succ) ^ k = (x ^ m) ^ k * x ^ k
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
⊢ ⇑Additive.ofMul '' ↑(Submonoid.powers x) = ↑(AddSubmonoid.multiples (Additive.ofMul x))

Tactic:
by
  ext
  exact Set.mem_image_iff_of_inverse (congrFun rfl) (congrFun rfl)

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
this : ∀ a ∈ s, a < ↑x + 1
⊢ ∀ a ∈ Multiset.filter (fun x ↦ x ∈ s) (Multiset.range (↑x).succ), a ∈ s

Tactic:
simp [-Multiset.range_succ]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
h : f x ≤ f y
⊢ x ≤ y

Tactic:
← inf_eq_left,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
h : f x ≤ f y
⊢ x ⊓ y = x
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s t : Multiset α
le : s ≤ t
l₁✝ l₂✝ : List α
hsub : l₁✝ <+ l₂✝
⊢ l₁✝.sublists' <+ l₂✝.sublists'

Tactic:
exact Sublist.sublists' hsub

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ ∀ (x : List α), x ∈ l.sublists' → ∀ (y : List α), y ∈ l.sublists' → ↑x = ↑y → x = y

Tactic:
exact fun x sx y sy e =>
        (h.perm_iff_eq_of_sublist (mem_sublists'.1 sx) (mem_sublists'.1 sy)).1 (Quotient.exact e)

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
⊢ (∅.sup fun x ↦ ⊥) = ⊥

Tactic:
exact sup_empty

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

Goal state before:
pp: α : Type u_1
s t : Finset α
a : α
ht : t ∈ s.powerset
h : a ∉ s
⊢ a ∈ t → a ∈ s

Tactic:
apply mem_powerset.1 ht

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = ∅ → #s < n

Tactic:
contrapose!

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
⊢ n ≤ #s → (powersetCard n s).Nonempty
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Finset α)
s : Finset α
⊢ s.powerset = (range (#s + 1)).biUnion fun i ↦ powersetCard i s

Tactic:
simpa only [disjiUnion_eq_biUnion] using powerset_card_disjiUnion s

Goal state after:
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:
rw [OrderIso.symm_apply_eq]
  rfl

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: ι : Type u_5
s : Set ι
x : ι
⊢ (∃ i, ∃ (x_1 : x ∈ s), ⟨x, ⋯⟩ ∈ i) ↔ x ∈ s

Tactic:
exact ⟨fun ⟨_, hx, _⟩ ↦ hx, fun hx ↦ ⟨{⟨x, hx⟩}, hx, by simp⟩⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ ¬a ⋖ b ↔ ∃ c, a < c ∧ c < b

Tactic:
CovBy,

Goal state after:
α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ ¬(a < b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ c, a < c ∧ c < b
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅

Tactic:
contrapose!

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ (x : α), P (insert x s) → x ∈ s

Tactic:
exact ⟨fun h ↦ ⟨h.1, fun x ↦ h.mem_of_prop_insert⟩,
    fun h ↦ ⟨h.1, fun t ht hst x hxt ↦ h.2 x (hP ht <| insert_subset hxt hst)⟩⟩

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

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℕ
⊢ iInf f = 0

Tactic:
rw [iInf_of_isEmpty, sInf_empty]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k ≤ n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k ≤ n), u (k + 1)

Tactic:
simp_rw [← Nat.lt_succ_iff, iSup_lt_succ']

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

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ (Ioi a).Nonempty ↔ ¬IsMax a

Tactic:
contrapose!

Goal state after:
α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioi a = ∅ ↔ IsMax a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ (Iio a).Nonempty ↔ ¬IsMin a

Tactic:
contrapose!

Goal state after:
α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iio a = ∅ ↔ IsMin a
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : Set M
m n : ℕ
hmn : m ∣ n
⊢ closure (s ^ n) ≤ closure (s ^ m)

Tactic:
obtain ⟨k, rfl⟩ := hmn
  simp [pow_mul]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
h : m < n
⊢ rᶜ (f m) (f n)

pp: case refine_2.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
h : n < m
⊢ rᶜ (f m) (f n)

Tactic:
· exact H _ _ h

Goal state after:
case refine_2.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
h : n < m
⊢ rᶜ (f m) (f n)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a : α
⊢ insert a (Ioi a) = Ici a

Tactic:
ext
  simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = cons a (Ioi a) ⋯

Tactic:
by
  classical rw [cons_eq_insert, Ioi_insert]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Icc x z) < #(Icc x y)
h₁ : TransGen (fun x1 x2 ↦ x1 ⩿ x2) x z
h₂ : z ⩿ y
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
exact .tail h₁ h₂

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

Goal state before:
pp: M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑r * ↑((Units.map (Submonoid.center M).subtype) u) = ↑((Units.map (Submonoid.center M).subtype) u * r)

Tactic:
Units.coe_map,

Goal state after:
M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑r * (Submonoid.center M).subtype ↑u = ↑((Units.map (Submonoid.center M).subtype) u * r)
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑r * ↑↑u = ↑((Units.map (Submonoid.center M).subtype) u) * ↑r

Tactic:
Units.coe_map,

Goal state after:
M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑r * ↑↑u = (Submonoid.center M).subtype ↑u * ↑r
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
    use (g 0), (g n)
    constructor
    · by_contra hx
      simp_all
    · exact Prod.Lex.toLex_le_toLex.mpr <| .inl hn

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
m n : ℕ
hmn : m ∣ n
⊢ closure (s ^ n) ≤ closure (s ^ m)

Tactic:
obtain ⟨k, rfl⟩ := hmn
  simp [pow_mul]

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

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

Tactic:
dsimp only [Function.onFun]
        rw [← h₂ _ hx, ← h₂ _ hy]
        subst h₁
        exact comm hx hy h

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x✝ y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x✝ = ↑y
x : M
⊢ ↑(f (f x)) * ↑(f x) * (↑x * ↑(f x)) = ↑(f (f x)) * (↑(f x) * ↑x) * ↑(f x)

Tactic:
simp_rw [mul_assoc]

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

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

Tactic:
by
  rw [← prod_union_inter, disjoint_iff_inter_eq_empty.mp h]; exact (mul_one _).symm

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ ⋃ x, ⋃ (hx : x ∈ N), (fun x_1 ↦ x_1 * ↑⟨x, hx⟩) '' s = s * ↑N

Tactic:
← image2_mul,

Goal state after:
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ ⋃ x, ⋃ (hx : x ∈ N), (fun x_1 ↦ x_1 * ↑⟨x, hx⟩) '' s = image2 (fun x1 x2 ↦ x1 * x2) s ↑N
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : FreeGroup α
⊢ (fun x ↦ of default ^ x) ((fun x ↦ ((map 1) x).sum) x) = x

Tactic:
induction x with
    | C1 => simp
    | of x => simp [Unique.default_eq x]
    | inv_of x hx => simp [Unique.default_eq x]
    | mul x y hx hy => simp [zpow_add, hx, hy]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∏ x ∈ s, f x = ∏ x ∈ s with f x ≠ 1, f x

Tactic:
by rw [prod_filter_ne_one]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case h
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.closure ↑(Finset.image (⇑f) s) = ⊤

Tactic:
rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
      MonoidHom.mrange_eq_top]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
⊢ ∀ {a b : { N // N.Normal }},
    { toFun := fun N ↦ QuotientGroup.con ↑N, invFun := fun c ↦ ⟨c.subgroup, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun N ↦ QuotientGroup.con ↑N, invFun := fun c ↦ ⟨c.subgroup, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
simp only [QuotientGroup.con, Equiv.coe_fn_mk, Con.le_def, Con.rel_mk, leftRel_apply]
    refine ⟨fun h x _ ↦ ?_, fun hle _ _ h ↦ hle h⟩
    specialize @h 1 x
    simp_all

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ (lift (⇑g ∘ f)) a = g ((lift f) a)

Tactic:
rw [← AddMonoidHom.comp_apply g (lift f)]

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ (lift (⇑g ∘ f)) a = (g.comp (lift f)) a
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
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1

Tactic:
· rw [h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx), h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy]
    simp [mul_assoc]

Goal state after: