mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
e : α ↪ α
⊢ e.equivOfFiniteSelfEmbedding.toEmbedding = e

Tactic:
ext
  rfl

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
γ : Fin (m + n) → Sort u_3
P : ((i : Fin (m + n)) → γ i) → Prop
h : ∀ (vₘ : (i : Fin m) → γ (castAdd n i)) (vₙ : (j : Fin n) → γ (natAdd m j)), P fun i ↦ addCases vₘ vₙ i
v : (i : Fin (m + n)) → γ i
⊢ P v

Tactic:
convert h (fun i => v (castAdd n i)) (fun j => v (natAdd m j))
    exact (addCases_castAdd_natAdd v _).symm

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
β : Sort u_2
x : β
p : Fin n → β
⊢ (last n).insertNth x p = snoc p x

Tactic:
simp [insertNth_last]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_3
i : Fin (n + 1)
x : α
p : Fin n → α
⊢ i.insertNth x p ∘ rev = i.rev.insertNth x (p ∘ rev)

Tactic:
funext x

Goal state after:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x✝ : α
p : Fin n → α
x : Fin (n + 1)
⊢ (i.insertNth x✝ p ∘ rev) x = i.rev.insertNth x✝ (p ∘ rev) x
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ snoc f a i.rev = cons a (f ∘ rev) i

Tactic:
by
  simpa using insertNth_rev (last n) a f i

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
this : ¬↑k < ↑j
⊢ j.contractNth op g k = op (g k.castSucc) (g k.succ)

Tactic:
contractNth,

Goal state after:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
this : ¬↑k < ↑j
⊢ (if ↑k < ↑j then g k.castSucc else if ↑k = ↑j then op (g k.castSucc) (g k.succ) else g k.succ) =
    op (g k.castSucc) (g k.succ)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑j < ↑k
⊢ j.contractNth op g k = g k.succ

Tactic:
contractNth,

Goal state after:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑j < ↑k
⊢ (if ↑k < ↑j then g k.castSucc else if ↑k = ↑j then op (g k.castSucc) (g k.succ) else g k.succ) = g k.succ
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s : List ℕ
⊢ s ∈ map (map fun x ↦ a + x) l.ranges → (range a).Disjoint s

Tactic:
hs

Goal state after:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s : List ℕ
hs : s ∈ map (map fun x ↦ a + x) l.ranges
⊢ (range a).Disjoint s
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate' (l.length * (n + 1)) = (l.rotate' (l.length * n)).rotate' (l.rotate' (l.length * n)).length

Tactic:
by
        simp [-rotate'_length, Nat.mul_succ, rotate'_rotate']

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

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : p a = true
⊢ (count a (filter p (a :: as).dedup) • if a = a then 1 else 0) = if p a = true then 1 else 0

Tactic:
simp [hp, count_dedup]

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

Goal state before:
pp: α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ l = l'

Tactic:
rw [← take_append_drop _ l, ht, hd, take_append_drop]

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

Goal state before:
pp: M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
a : M
inst✝ : DecidableEq M
h : a ∈ s
⊢ a * (s.erase a).prod = s.prod

Tactic:
rw [← s.coe_toList, coe_erase, prod_coe, prod_coe, List.prod_erase (mem_toList.2 h)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g
a : ↥s
x✝¹ : a ∈ ↑s.attach
b : ↥s
x✝ : b ∈ ↑s.attach
hab : a ≠ b
x : γ
hxa : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) a
hxb : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) b
xa : β
hfa : xa ∈ f ↑a
hga : x ∈ g xa
xb : β
hfb : xb ∈ f ↑b
hgb : x ∈ g xb
⊢ False

Tactic:
refine disjoint_left.mp
            (h2 (mem_disjiUnion.mpr ⟨_, a.prop, hfa⟩) (mem_disjiUnion.mpr ⟨_, b.prop, hfb⟩) ?_) hga
            hgb

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : (↑s).PairwiseDisjoint f
h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g
a : ↥s
x✝¹ : a ∈ ↑s.attach
b : ↥s
x✝ : b ∈ ↑s.attach
hab : a ≠ b
x : γ
hxa : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) a
hxb : x ∈ (fun a ↦ (f ↑a).disjiUnion g ⋯) b
xa : β
hfa : xa ∈ f ↑a
hga : x ∈ g xa
xb : β
hfb : xb ∈ f ↑b
hgb : x ∈ g xb
⊢ xa ≠ xb
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
h : (a :: l).cyclicPermutations = []
⊢ False

Tactic:
by simpa using congr_arg length h

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l.cyclicPermutations ~r l'.cyclicPermutations ↔ l ~r l'

Tactic:
simp only [IsRotated, ← cyclicPermutations_rotate, cyclicPermutations_inj]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).Nontrivial ↔ s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial)

Tactic:
← card_pos,

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).Nontrivial ↔ 0 < #s ∧ 0 < #t ∧ (s.Nontrivial ∨ t.Nontrivial)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.offDiag = ∅

Tactic:
by simp [← Finset.card_eq_zero]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p + 1)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!

Tactic:
rw [factorial_succ]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1))

Tactic:
rw [factorial_succ]

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
⊢ (a ::ₘ s).Nodup → (∀ (a_2 : α), a_2 ∈ a ::ₘ s → (t a_2).Nodup) → ((a ::ₘ s).pi t).Nodup

Tactic:
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
hs : (a ::ₘ s).Nodup
⊢ (∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup) → ((a ::ₘ s).pi t).Nodup
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
⊢ Finite (α ↪ β)

Tactic:
by
  rcases isEmpty_or_nonempty (α ↪ β) with _ | h
  · infer_instance
  · refine h.elim fun f => ?_
    have : Finite α := Finite.of_injective _ f.injective
    exact Finite.of_injective _ DFunLike.coe_injective

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set α
⊢ f '' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f '' s i j

Tactic:
simp_rw [image_iUnion]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ r, ⋂ (_ : ∃ x ∈ S, (x, t) = r), r.1 ×ˢ r.2 = ⋂ s ∈ S, s ×ˢ t

Tactic:
iInter_exists,

Goal state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ r, ⋂ i, ⋂ (_ : i ∈ S ∧ (i, t) = r), r.1 ×ˢ r.2 = ⋂ s ∈ S, s ×ˢ t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ r, ⋂ (_ : ∃ x ∈ T, (s, x) = r), r.1 ×ˢ r.2 = ⋂ t ∈ T, s ×ˢ t

Tactic:
iInter_exists,

Goal state after:
α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ r, ⋂ i, ⋂ (_ : i ∈ T ∧ (s, i) = r), r.1 ×ˢ r.2 = ⋂ t ∈ T, s ×ˢ t
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: N : Type u_5
inst✝ : Group N
K : Subgroup N
⊢ comap (MonoidHom.id N) K = K

Tactic:
ext
  rfl

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
f : G →* N
⊢ (f.domRestrict K).range = map f K

Tactic:
simp_rw [SetLike.ext_iff, mem_range, mem_map, domRestrict_apply, SetLike.exists,
    exists_prop, forall_const]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
e : G ≃* G'
⊢ H.equivMapOfInjective ↑e ⋯ = e.subgroupMap H

Tactic:
ext
  rfl

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ (∃ y_1, (∃ n, x ^ n = y_1) ∧ ∃ z_1, (∃ n, y ^ n = z_1) ∧ y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z

Tactic:
exists_exists_eq_and

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

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

Tactic:
Set.preimage_preimage,

Goal state after:
M : Type u_2
inst✝ : Mul M
s : Set Mᵐᵒᵖ
⊢ closure s = closure ((fun x ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s)
Module: Mathlib.Algebra.Group.Submonoid.MulOpposite

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

Tactic:
Set.preimage_preimage,

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ closure s = closure ((fun x ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s)
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
e : M ≃* N
⊢ S.equivMapOfInjective ↑e ⋯ = e.submonoidMap S

Tactic:
ext
  rfl

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)

Tactic:
Set.preimage_preimage,

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ closure s = closure ((fun x ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s)
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

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

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

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

Goal state before:
pp: case refine_3
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
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * x * g⁻¹ * (g * y * g⁻¹) ∈ normalClosure s

Tactic:
exact mul_mem ihx ihy

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

Goal state before:
pp: case refine_3
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
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * (x * y) * g⁻¹ ∈ normalClosure s

Tactic:
rw [← conj_mul]
      exact mul_mem ihx ihy

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

Goal state before:
pp: case refine_3
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N

Tactic:
exact mul_mem ihx ihy

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : CommGroup β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
x : α × β
s : Set α
f : F
⊢ x • graphOn (⇑f) s = graphOn (fun a ↦ x.2 / f x.1 * f a) (x.1 • s)

Tactic:
by
  ext ⟨a, b⟩
  simp [mem_smul_set_iff_inv_smul_mem, inv_mul_eq_iff_eq_mul, mul_left_comm _ _⁻¹,
    eq_inv_mul_iff_mul_eq, ← mul_div_right_comm, div_eq_iff_eq_mul, mul_comm b]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ H ⊔ N ≤ normalizer ↑N

Tactic:
exact sup_le hLE le_normalizer

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mp.right
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
hab : s i✝ a b
⊢ r ⟨i✝, a⟩.fst ⟨i✝, b⟩.fst ∨ ∃ h, s ⟨i✝, b⟩.fst (h ▸ ⟨i✝, a⟩.snd) ⟨i✝, b⟩.snd

Tactic:
exact Or.inr ⟨rfl, hab⟩

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

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
a b : M
l : List M
hl₁ : ∀ (x : M), x ∈ a :: b :: l → 1 < x
x✝ : a :: b :: l ≠ []
⊢ 1 < (a :: b :: l).prod

Tactic:
simp only [forall_eq_or_imp, List.mem_cons] at hl₁

Goal state after:
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < (a :: b :: l).prod
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mp.right
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
b₁✝ b₂✝ : α i
hab : s i b₁✝ b₂✝
⊢ r ⟨i, b₁✝⟩.fst ⟨i, b₂✝⟩.fst ∨ ∃ h, s ⟨i, b₂✝⟩.fst (h ▸ ⟨i, b₁✝⟩.snd) ⟨i, b₂✝⟩.snd

Tactic:
exact Or.inr ⟨rfl, hab⟩

Goal state after:
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
⊢ ∀ (a : α) (b : β), ∃ b_1, toLex (a, b) < b_1

Tactic:
intro a b

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
a : α
b : β
⊢ ∃ b_1, toLex (a, b) < b_1
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
⊢ ∀ (a : α) (b : β), ∃ b_1, toLex (a, b) < b_1

Tactic:
intro a b

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
a : α
b : β
⊢ ∃ b_1, toLex (a, b) < b_1
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 ^ (k * (↑(m.succ % n)).toNat) = x ^ (k * (↑(m % n)).toNat) * x ^ k

Tactic:
Int.toNat_natCast,

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 ^ (k * (m.succ % n)) = 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 ^ (k * (↑(m % n)).toNat) * x ^ k

Tactic:
Int.toNat_natCast,

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)) * x ^ k
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ (∃ y, (∃ n, a ^ n = y) ∧ ∃ z, (∃ n, b ^ n = z) ∧ y * z = c) ↔ ∃ m n, a ^ m * b ^ n = c

Tactic:
exists_exists_eq_and

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

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

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

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: ⊢ ofNat (ℕ × ℕ) = unpair

Tactic:
by funext; simp

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

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ powersetAux' (a :: l) = powersetAux' l ++ List.map (cons a) (powersetAux' l)

Tactic:
simp [powersetAux']

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

Goal state before:
pp: α : Type u_1
a₁ a₂ : Multiset α
a : a₁.powerset = a₂.powerset
⊢ a₁ = a₂

Tactic:
exact le_antisymm
    (powerset_le_powerset_iff_le.mp (le_of_eq a))
    (powerset_le_powerset_iff_le.mp (le_of_eq a.symm))

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ ∃ a ∈ powersetCard n.succ u, x ∈ a

Tactic:
refine ⟨insert x t, ?_, mem_insert_self _ _⟩

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ u
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
⊢ P α

Tactic:
obtain ⟨p⟩ :=
    let f_empty := fun i => by convert! h_empty
    let h_option : ∀ {α : Type u} [Fintype α] [DecidableEq α],
          (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α) := by
      rintro α hα - Pα hα'
      convert! h_option α (Pα _)
    @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
      f_empty h_option α _ (Classical.decEq α)

Goal state after:
case mk
P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
x✝ : Trunc (∀ (h : Fintype α), P α)
p : ∀ (h : Fintype α), P α
⊢ P α
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
⊢ ∀ y ∈ f '' ↑s, ∃ x ∈ Set.range fun i ↦ ⨆ (_ : i ∈ s), f i, y ≤ x

Tactic:
simp only [Set.mem_image, mem_coe, ciSup_eq_ite, dite_eq_ite, Set.mem_range,
      exists_exists_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    intro i hi
    refine ⟨i, ?_⟩
    simp [hi]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
c : α
H : ∀ (x : ι), f x ≤ c
⊢ ∀ b ∈ range f, b ≤ c

Tactic:
rwa [forall_mem_range]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
l : List ι
f : ι → α
h : l ≠ []
⊢ ∃ x ∈ l, sSup ∅ ≤ f x

Tactic:
by simpa using exists_mem_of_ne_nil _ h

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
x : α
s : Set α
inst✝ : Preorder α
h : s.Subsingleton
⊢ Minimal (fun x ↦ x ∈ s) x ↔ x ∈ s

Tactic:
by
  obtain (rfl | ⟨x, rfl⟩) := h.eq_empty_or_singleton <;> simp

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

Goal state before:
pp: s : Set ℕ
⊢ ¬BddAbove s → sSup s = sSup ∅

Tactic:
hs

Goal state after:
s : Set ℕ
hs : ¬BddAbove s
⊢ sSup s = sSup ∅
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:
by
  rw [← sup_iSup_nat_succ]
  simp

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ image (fun j ↦ n✝ + 1 - 1 - j) (Ico 0 (n✝ + 1)) = Ico 0 (n✝ + 1)

Tactic:
Nat.Ico_image_const_sub_eq_Ico (Nat.zero_le _)

Goal state after:
case succ
n✝ : ℕ
⊢ Ico (n✝ + 1 - 1 + 1 - (n✝ + 1)) (n✝ + 1 - 1 + 1 - 0) = Ico 0 (n✝ + 1)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : Finite α
inst✝ : Std.Refl r
f : ℕ → α
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
obtain ⟨m, n, h, hf⟩ := Set.finite_univ.exists_lt_map_eq_of_forall_mem (f := f)
    fun _ ↦ Set.mem_univ _

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝¹ : Finite α
inst✝ : Std.Refl r
f : ℕ → α
m n : ℕ
h : m < n
hf : f m = f n
⊢ ∃ m n, m < n ∧ r (f m) (f n)
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : Set M
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ closure s ≤ closure (s ^ n)

Tactic:
← subset_pow hs hn

Goal state after:
M : Type u_3
inst✝ : Monoid M
s : Set M
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ closure s ≤ closure s
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ #(Iio a) = #(Iic a) - 1

Tactic:
by
  rw [Iic_eq_cons_Iio, card_cons, Nat.add_sub_cancel_right]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
g h : M
Hg : g ∈ Set.center M
u : Mˣ
hu : SemiconjBy (↑u) g h
⊢ g = h

Tactic:
← u.mul_left_inj,

Goal state after:
M : Type u_2
inst✝ : Monoid M
g h : M
Hg : g ∈ Set.center M
u : Mˣ
hu : SemiconjBy (↑u) g h
⊢ g * ↑u = h * ↑u
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ closure s ≤ closure (s ^ n)

Tactic:
← subset_pow hs hn

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ closure s ≤ closure s
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
N H : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ ↑(H ⊔ N) = ↑H * ↑N

Tactic:
coe_mul_of_left_le_normalizer_right _ _ hLE

Goal state after:
G : Type u_2
inst✝ : Group G
N H : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ ↑H * ↑N = ↑H * ↑N
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
a : α
comm : {x | x ∈ a ::ₘ s}.Pairwise Commute
⊢ (a ::ₘ s).noncommProd comm = s.noncommProd ⋯ * a

Tactic:
induction s using Quotient.inductionOn with | _ s
  simp only [quot_mk_to_coe, cons_coe, noncommProd_coe, List.prod_cons]
  induction s with
  | nil => simp
  | cons hd tl IH =>
    rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]
    · congr 1
      apply comm.of_refl <;> simp
    · intro x hx y hy
      simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy
      apply comm
      · cases hx <;> simp [*]
      · cases hy <;> simp [*]

Goal state after: