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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n ↪ α
⊢ map f univ = { val := ↑(List.ofFn ⇑f), nodup := ⋯ }

Tactic:
simp [Finset.map]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
y : Fin (n + 1)
hi : y.castSucc ≠ last (n + 1)
⊢ (last n).predAbove y.castSucc = y.castSucc.castPred hi

Tactic:
exact predAbove_last_castSucc

Goal state after:
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #s + #sᶜ = Fintype.card α

Tactic:
rw [Finset.card_compl, ← Nat.add_sub_assoc (card_le_univ s), Nat.add_sub_cancel_left]

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

Goal state before:
pp: case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : ¬j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j

Tactic:
simp [init, h, castSucc_inj]

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : card α ≤ 1
⊢ False

Tactic:
by rw [← ha] at h; cases h with | step h => cases h;

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : ¬p x
⊢ op (g x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))

Tactic:
have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : a = b
⊢ R a b

Tactic:
cases heq; apply refl

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

Goal state before:
pp: case refine_1
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b ∨ a = b ∧ Lex r l₁ l₂
⊢ Lex r (a :: l₁) (b :: l₂)

pp: case refine_2
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r (a :: l₁) (b :: l₂)
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂

Tactic:
· rcases h with (h | ⟨rfl, h⟩)
      · exact Lex.rel h
      · exact Lex.cons h

Goal state after:
case refine_2
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r (a :: l₁) (b :: l₂)
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • s) = n • filter p s

Tactic:
refine s.induction_on ?_ ?_
  · simp only [filter_zero, nsmul_zero]
  · intro a ha ih
    rw [nsmul_cons, filter_add, ih, filter_cons, nsmul_add]
    congr
    split_ifs with hp <;>
      · simp only [filter_eq_self, nsmul_zero, filter_eq_nil]
        intro b hb
        rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ (l.alternatingProd ^ (-1) ^ l.length)⁻¹ * a ^ (-1) ^ l.length = ((a / l.alternatingProd) ^ (-1) ^ l.length)⁻¹⁻¹

Tactic:
inv_inv

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ (l.alternatingProd ^ (-1) ^ l.length)⁻¹ * a ^ (-1) ^ l.length = (a / l.alternatingProd) ^ (-1) ^ l.length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = (l.length + k) % l.length

pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ n % l.length ≤ l.length

Tactic:
add_mod_left,

Goal state after:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = k % l.length

α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ n % l.length ≤ l.length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
x : α
⊢ l ~r [x] ↔ [x] = l

Tactic:
isRotated_singleton_iff,

Goal state after:
α : Type u
l : List α
x : α
⊢ l = [x] ↔ [x] = l
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
⊢ n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !

Tactic:
rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]

Goal state after:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
⊢ n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * (n.choose k.succ * k.succ ! * (n - k.succ)!)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)

Tactic:
exact Nat.dvd_mul_left _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ Nodup (Quotient.map List.offDiag ⋯ s.val)

Tactic:
rcases s with ⟨⟨s⟩, hs⟩
    exact hs.offDiag

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ ↑(s ∪ t).offDiag = ↑(s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s)

Tactic:
push_cast
    exact Set.offDiag_union (disjoint_coe.2 h)

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:
by 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:
by rw [factorial_succ]

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

Goal state before:
pp: case refine_2
α : 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
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (image2 f s t).Infinite

Tactic:
· rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
    · exact hs.image2_left hb (hfs _ hb)
    · exact ht.image2_right ha (hft _ ha)

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s t : Set α
⊢ s⁻¹⁻¹ ⊆ t⁻¹ ↔ s ⊆ t⁻¹

Tactic:
inv_inv

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
s t : Set α
⊢ s ⊆ t⁻¹ ↔ s ⊆ t⁻¹
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
⊢ ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i

Tactic:
x'

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
x' : α
⊢ w ∈ t x' → ∃ i, z ∈ s i ∧ w ∈ t i
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun a_1 ↦ a_1⁻¹ * a⁻¹⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty ↔
    ((fun x ↦ x⁻¹ * a) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty

Tactic:
inv_inv

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

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

Tactic:
by
  simp_rw [image2_iUnion_right]

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun a_1 ↦ a⁻¹⁻¹ * a_1⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty ↔
    ((fun x ↦ a * x⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty

Tactic:
inv_inv

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ∀ (f : F) (s : Set α), ⇑f '' s ^ (n + 2) = (⇑f '' s) ^ (n + 2)

Tactic:
simp [image_mul, pow_succ _ n.succ, image_pow_of_ne_zero]

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
n : G
hn : n ∈ H
g : G
⊢ g = g⁻¹⁻¹

Tactic:
inv_inv

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
n : G
hn : n ∈ H
g : G
⊢ g = g
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
⊢ (∀ (h : G), h ∈ S ↔ g⁻¹ * h * g⁻¹⁻¹ ∈ S) ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S

Tactic:
inv_inv

Goal state after:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
⊢ (∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S) ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → f a = 1 → a = 1
x : G
hx : x ∈ ↑s
y : G
hy : y ∈ ↑s
hxy : f x = f y
⊢ x = y

Tactic:
refine mul_inv_eq_one.1 <| h _ (mul_mem ?_ (inv_mem ?_)) ?_

Goal state after:
case refine_1
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → f a = 1 → a = 1
x : G
hx : x ∈ ↑s
y : G
hy : y ∈ ↑s
hxy : f x = f y
⊢ x ∈ s

case refine_2
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → f a = 1 → a = 1
x : G
hx : x ∈ ↑s
y : G
hy : y ∈ ↑s
hxy : f x = f y
⊢ y ∈ s

case refine_3
F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → f a = 1 → a = 1
x : G
hx : x ∈ ↑s
y : G
hy : y ∈ ↑s
hxy : f x = f y
⊢ f (x * y⁻¹) = 1
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
⊢ map 1 K ≤ ⊥

Tactic:
by
    rintro x ⟨y, _, rfl⟩
    simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
h : Disjoint H K
⊢ Disjoint (map f H) (map f K)

Tactic:
disjoint_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
h : Disjoint H K
⊢ map f H ⊓ map f K = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊥ ↔ Disjoint H K

Tactic:
disjoint_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊥ ↔ H ⊓ K = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊥ ↔ Disjoint H K

Tactic:
rw [disjoint_iff, ← bot_subgroupOf, subgroupOf_inj, bot_inf_eq]

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
f : G →* N
H : Subgroup N
⊢ f.range ⊓ H = ⊥ ↔ Disjoint H f.range

Tactic:
disjoint_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ f.range ⊓ H = ⊥ ↔ H ⊓ f.range = ⊥
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective ⇑f
H K : Submonoid M
h : Disjoint H K
⊢ Disjoint (map f H) (map f K)

Tactic:
disjoint_iff,

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective ⇑f
H K : Submonoid M
h : Disjoint H K
⊢ map f H ⊓ map f K = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ normalClosure ↑⊥ = ⊥

Tactic:
normalClosure_eq_self

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ⊥ = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G ≃* N
⊢ map f.toMonoidHom (normalizer ↑H) = normalizer ↑(map f.toMonoidHom H)

Tactic:
ext x
  simp only [mem_normalizer_iff, mem_map_equiv]
  rw [f.toEquiv.forall_congr]
  intro
  simp

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

Goal state before:
pp: case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ ∀ (i : α), i ∈ l → f i ≤ max (f i) (g i)

Tactic:
intros

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ f i✝ ≤ max (f i✝) (g i✝)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ ∀ (i : α), i ∈ l → g i ≤ max (f i) (g i)

Tactic:
intros

Goal state after:
case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ g i✝ ≤ max (f i✝) (g i✝)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ ∀ (i : α), i ∈ l → min (f i) (g i) ≤ f i

Tactic:
intros

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ min (f i✝) (g i✝) ≤ f i✝
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ ∀ (i : α), i ∈ l → min (f i) (g i) ≤ g i

Tactic:
intros

Goal state after:
case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ min (f i✝) (g i✝) ≤ g i✝
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h✝ : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
h : c⁻¹ * x * c⁻¹⁻¹ ∈ N
⊢ c⁻¹ * x * c ∈ N

Tactic:
inv_inv

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h✝ : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
h : c⁻¹ * x * c ∈ N
⊢ c⁻¹ * x * c ∈ N
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
N : Type u_5
inst✝³ : Group N
M : Type u_6
inst✝² : AddGroup M
I : AddSubgroup M
G : Type u_7
inst✝¹ : Group G
inst✝ : MulAction G M
⊢ 1 ∈ {σ | ∀ (x : M), σ • x - x ∈ I}

Tactic:
by simp [zero_mem]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
a b : Lex (α × β)
this : DecidableLT (Lex (α × β))
⊢ ∀ {a b : Lex (α × β)}, compare a b = Ordering.eq ↔ (a == b) = true

Tactic:
by
      simp [compare_def, compareLex, compareOn, Ordering.then_eq_eq]

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

Goal state before:
pp: case refine_2
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
x : M
hx : x ∈ s
⊢ ∀ (y : M),
    (∀ (y_1 : N) (z : α), (y • y_1) • z = y • y_1 • z) → ∀ (y_1 : N) (z : α), ((x * y) • y_1) • z = (x * y) • y_1 • z

Tactic:
x'

Goal state after:
case refine_2
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
x : M
hx : x ∈ s
x' : M
⊢ (∀ (y : N) (z : α), (x' • y) • z = x' • y • z) → ∀ (y : N) (z : α), ((x * x') • y) • z = (x * x') • y • z
Module: Mathlib.Algebra.Group.Submonoid.Membership

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

Tactic:
x'

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝² : Monoid M
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), x • y • z = y • x • z
x : M
hx : x ∈ s
x' : M
⊢ (∀ (n : N) (a : α), x' • n • a = n • x' • a) → ∀ (n : N) (a : α), (x * x') • n • a = n • (x * x') • a
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = max (↑a) tl.maximum
⊢ (a :: (tl ++ [hd])).maximum = max (↑a) (tl ++ [hd]).maximum

Tactic:
rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Lattice α
inst✝⁵ : Lattice β
inst✝⁴ : FunLike F α β
inst✝³ : OrderBot α
inst✝² : OrderBot β
inst✝¹ : BotHomClass F α β
inst✝ : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
⊢ Disjoint (f a) (f b)

Tactic:
disjoint_iff,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Lattice α
inst✝⁵ : Lattice β
inst✝⁴ : FunLike F α β
inst✝³ : OrderBot α
inst✝² : OrderBot β
inst✝¹ : BotHomClass F α β
inst✝ : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
⊢ f a ⊓ f b = ⊥
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    (Array.foldl (fun r l ↦ r.push (x :: l)) y.toList.toArray y.toList.toArray).toList =
      (Array.foldl (fun r l ↦ r.push (x :: l)) y y).toList

Tactic:
intros

Goal state after:
α : Type u
l : List α
x✝ : α
y✝ : Array (List α)
⊢ (Array.foldl (fun r l ↦ r.push (x✝ :: l)) y✝.toList.toArray y✝.toList.toArray).toList =
    (Array.foldl (fun r l ↦ r.push (x✝ :: l)) y✝ y✝).toList
Module: Mathlib.Data.Finset.Lattice.Fold

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

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

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

case inr
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
hs : s.Nonempty
⊢ (s.sup fun x ↦ ⊥) = ⊥
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case g_sup
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ∀ (x y : { x // P x }), ↑(x ⊔ y) = ↑x ⊔ ↑y

Tactic:
intros

Goal state after:
case g_sup
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
x✝ y✝ : { x // P x }
⊢ ↑(x✝ ⊔ y✝) = ↑x✝ ⊔ ↑y✝
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case bot
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ↑⊥ = ⊥

Tactic:
intros

Goal state after:
case bot
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ↑⊥ = ⊥
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ ∀ (a : β), g ({a}.sup' ⋯ f) = {a}.sup' ⋯ (g ∘ f)

Tactic:
intros

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
a✝ : β
⊢ g ({a✝}.sup' ⋯ f) = {a✝}.sup' ⋯ (g ∘ f)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ ∀ (a : β) (s : Finset β) (h : a ∉ s) (hs : s.Nonempty),
    g (s.sup' hs f) = s.sup' hs (g ∘ f) → g ((cons a s h).sup' ⋯ f) = (cons a s h).sup' ⋯ (g ∘ f)

Tactic:
intros

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
a✝¹ : β
s✝ : Finset β
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : g (s✝.sup' hs✝ f) = s✝.sup' hs✝ (g ∘ f)
⊢ g ((cons a✝¹ s✝ h✝).sup' ⋯ f) = (cons a✝¹ s✝ h✝).sup' ⋯ (g ∘ f)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
⊢ ∀ (a : ι), f ({a}.sup' ⋯ g) = {a}.sup' ⋯ (⇑f ∘ g)

Tactic:
intros

Goal state after:
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
a✝ : ι
⊢ f ({a✝}.sup' ⋯ g) = {a✝}.sup' ⋯ (⇑f ∘ g)