mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
s : Finset ι
hi : i ∉ s
⊢ (∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
    ∀ (f : ℕ → (i : ι) → α i),
      ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i s hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)

Tactic:
ih

Goal state after:
case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ ∀ (f : ℕ → (i : ι) → α i),
    ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i s hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ ∀ (f : ℕ → (i : ι) → α i),
    ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i s hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)

Tactic:
f

Goal state after:
case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
f : ℕ → (i : ι) → α i
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i s hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
h : WellQuasiOrdered r
f : r →r s
hf : Function.Surjective ⇑f
seq : ℕ → β
w✝¹ w✝ : ℕ
hle : w✝¹ < w✝
hr : r ((Function.surjInv hf ∘ seq) w✝¹) ((Function.surjInv hf ∘ seq) w✝)
⊢ s (seq w✝¹) (seq w✝)

Tactic:
simpa [Function.surjInv_eq] using f.map_rel hr

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
hg' : ∀ (n : ℕ), g' n ∈ f '' s
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)

Tactic:
choose g hgs heq using hg'

Goal state after:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
⊢ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
f

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
⊢ (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case h
M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x y : N
hx✝¹ : x ∈ closure s
hy✝¹ : y ∈ closure s
hx✝ : ∃ n, r ^ n • x ∈ closure (r • s)
hy✝ : ∃ n, r ^ n • y ∈ closure (r • s)
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ r ^ ny • r ^ nx • (x * y) ∈ closure (r • s)

Tactic:
← smul_mul_assoc,

Goal state after:
case h
M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x y : N
hx✝¹ : x ∈ closure s
hy✝¹ : y ∈ closure s
hx✝ : ∃ n, r ^ n • x ∈ closure (r • s)
hy✝ : ∃ n, r ^ n • y ∈ closure (r • s)
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ r ^ ny • (r ^ nx • x * y) ∈ closure (r • s)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝ : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r (f (g₁ m)).1 (f (g₁ n)).1
m n : ℕ
hlt : m < n
hle : r' (f (?m.51 m)).2 (f (?m.51 n)).2
⊢ ∃ m n, m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2

Tactic:
exact ⟨g₁ m, g₁ n, g₁.strictMono hlt, h₁ _ _ hlt.le, hle⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
t : Finset ι
hi : i ∉ t
⊢ (∀ (f : ℕ → (i : ι) → α i),
      (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
    ∀ (f : ℕ → (i : ι) → α i),
      (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
        ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)

Tactic:
ih

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
t : Finset ι
hi : i ∉ t
ih :
  ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
      ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
t : Finset ι
hi : i ∉ t
ih :
  ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
      ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)

Tactic:
f

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
t : Finset ι
hi : i ∉ t
ih :
  ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
f : ℕ → (i : ι) → α i
⊢ (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
    ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ (Ioi a).disjUnion (Iio a) ⋯ = {a}ᶜ

Tactic:
ext
  simp [eq_comm]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
h : (fun b ↦ [[b, a]]) b = (fun b ↦ [[b, a]]) c
⊢ b = c

Tactic:
rw [Finset.ext_iff] at h
  exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun n ↦ ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n ↦ ↑(fs n) n) n)
⊢ ¬IsBadSeq r s g

Tactic:
refine (fs n).2.2 g (fun m mn => ?_) hg2
    rw [← h m n mn.le, ← hg1 m mn]

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

Goal state before:
pp: α : Type u_1
s : Setoid α
⊢ Subsingleton (Quotient s) ↔ s = ⊤

Tactic:
by
  simp only [_root_.subsingleton_iff, eq_top_iff, Setoid.le_def, Setoid.top_def, Pi.top_apply]
  refine Quotient.mk'_surjective.forall.trans (forall_congr' fun a => ?_)
  refine Quotient.mk'_surjective.forall.trans (forall_congr' fun b => ?_)
  simp_rw [Prop.top_eq_true, true_implies, Quotient.eq']

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
x : α
b : Bool
⊢ Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)

Tactic:
by
  cases b <;> exact Step.not

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

Goal state before:
pp: α : Type u
x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅

Tactic:
injections

Goal state after:
α : Type u
x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x✝³ = x✝¹
snd_eq✝¹ : x✝² = x✝
tail_eq✝ : x✝⁵ = x✝⁴
fst_eq✝ : x✝³ = x✝¹
snd_eq✝ : (!x✝²) = !x✝
⊢ [] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [(x3, b3)] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [] ++ x✝⁵ = [(x3, b3)] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([(x3, b3)] ++ x✝⁴) L₅

Tactic:
injections

Goal state after:
α : Type u
x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x✝³ = x3
snd_eq✝¹ : x✝² = b3
tail_eq✝ : x✝⁵ = (x✝¹, !x✝) :: x✝⁴
fst_eq✝ : x✝³ = x✝¹
snd_eq✝ : (!x✝²) = x✝
⊢ [] ++ x✝⁵ = [(x3, b3)] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([(x3, b3)] ++ x✝⁴) L₅
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [(x3, b3)] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [(x3, b3)] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([(x3, b3)] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅

Tactic:
injections

Goal state after:
α : Type u
x3 : α
b3 : Bool
x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x3 = x✝¹
snd_eq✝¹ : b3 = x✝
tail_eq✝ : (x✝³, !x✝²) :: x✝⁵ = x✝⁴
fst_eq✝ : x✝³ = x✝¹
snd_eq✝ : x✝² = !x✝
⊢ [(x3, b3)] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([(x3, b3)] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = (x3, b3) :: (x4, b4) :: tl ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [] ++ x✝⁵ = (x3, b3) :: (x4, b4) :: tl ++ x✝⁴ ∨
    ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁴) L₅

Tactic:
injections

Goal state after:
α : Type u
x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x✝³ = x3
snd_eq✝¹ : x✝² = b3
tail_eq✝ : x✝⁵ = tl.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)
fst_eq✝ : x✝³ = x4
snd_eq✝ : (!x✝²) = b4
⊢ [] ++ x✝⁵ = (x3, b3) :: (x4, b4) :: tl ++ x✝⁴ ∨
    ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁴) L₅
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : (x3, b3) :: (x4, b4) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ (x3, b3) :: (x4, b4) :: tl ++ x✝⁵ = [] ++ x✝⁴ ∨
    ∃ L₅, Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅

Tactic:
injections

Goal state after:
α : Type u
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
fst_eq✝¹ : x3 = x✝¹
snd_eq✝¹ : b3 = x✝
tail_eq✝ : tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵) = x✝⁴
fst_eq✝ : x4 = x✝¹
snd_eq✝ : b4 = !x✝
⊢ (x3, b3) :: (x4, b4) :: tl ++ x✝⁵ = [] ++ x✝⁴ ∨
    ∃ L₅, Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case tail.inl
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

Tactic:
have : L₁ ++ (s' ++ (a, b) :: (a, not b) :: e) =
            L₁ ++ s' ++ (a, b) :: (a, not b) :: e := by simp

Goal state after:
case tail.inl
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
⊢ (↑t).PairwiseDisjoint fun j ↦ {i ∈ s | g i = j}

Tactic:
intro x' hx y' hy hne

Goal state after:
case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
⊢ (↑t).PairwiseDisjoint fun j ↦ {i ∈ s | g i = j}

Tactic:
intro x' hx y' hy hne

Goal state after:
case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u_1
⊢ Subgroup.closure (Set.range of) = ⊤

Tactic:
by
  rw [← range_lift_eq_closure, lift_of_eq_id]
  exact MonoidHom.range_eq_top.2 Function.surjective_id

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ : Type u
x✝ : FreeGroup α✝
x : α✝
ih : id <$> of x = of x
⊢ (id <$> of x)⁻¹ = (of x)⁻¹

Tactic:
ih

Goal state after:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ : Type u
x✝ : FreeGroup α✝
x : α✝
ih : id <$> of x = of x
⊢ (of x)⁻¹ = (of x)⁻¹
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

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

Tactic:
by
  rw [range_add_one, prod_insert notMem_range_self]

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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
⊢ (List.map f (a :: s)).prod = ∏ m ∈ (a :: s).toFinset, f m ^ count m (a :: s)

Tactic:
| cons a s IH =>

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ : Type u
x✝ : FreeAbelianGroup α✝
x : α✝
ih : id <$> pure x = pure x
⊢ -id <$> pure x = -pure x

Tactic:
ih

Goal state after:
α : Type u
G : Type u_1
β α✝ : Type u
x✝ : FreeAbelianGroup α✝
x : α✝
ih : id <$> pure x = pure x
⊢ -pure x = -pure x
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x ↦ f x >>= g

Tactic:
ih

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f >>= g) = -pure x >>= fun x ↦ f x >>= g

Tactic:
ih

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= fun x ↦ f x >>= g) = -pure x >>= fun x ↦ f x >>= g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
s : Finset ι
m : ℕ
f : ι → ℕ
h₁ : ∀ x ∈ s, f x = m
⊢ ∑ x ∈ s, f x = #s * m

Tactic:
← Nat.nsmul_eq_mul,

Goal state after:
ι : Type u_1
s : Finset ι
m : ℕ
f : ι → ℕ
h₁ : ∀ x ∈ s, f x = m
⊢ ∑ x ∈ s, f x = #s • m
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
ih : Prod.mk p <$> pure q = (fun b a ↦ (a, b)) <$> pure q <*> pure p
⊢ -Prod.mk p <$> pure q = -((fun b a ↦ (a, b)) <$> pure q <*> pure p)

Tactic:
ih

Goal state after:
case pure.neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
ih : Prod.mk p <$> pure q = (fun b a ↦ (a, b)) <$> pure q <*> pure p
⊢ -((fun b a ↦ (a, b)) <$> pure q <*> pure p) = -((fun b a ↦ (a, b)) <$> pure q <*> pure p)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
p : α✝
ih : Prod.mk <$> pure p <*> y = (fun b a ↦ (a, b)) <$> y <*> pure p
⊢ -(Prod.mk <$> pure p <*> y) = -((fun b a ↦ (a, b)) <$> y <*> pure p)

Tactic:
ih

Goal state after:
case neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
p : α✝
ih : Prod.mk <$> pure p <*> y = (fun b a ↦ (a, b)) <$> y <*> pure p
⊢ -((fun b a ↦ (a, b)) <$> y <*> pure p) = -((fun b a ↦ (a, b)) <$> y <*> pure p)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x✝ : α
⊢ ((map g).comp (map f)) (of x✝) = (map (g ∘ f)) (of x✝)

Tactic:
by simp [map]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
ih : of L1 * of L2 * of L3 = of L1 * (of L2 * of L3)
⊢ -(of L1 * of L2 * of L3) = -(of L1 * (of L2 * of L3))

Tactic:
ih

Goal state after:
case of.of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
ih : of L1 * of L2 * of L3 = of L1 * (of L2 * of L3)
⊢ -(of L1 * (of L2 * of L3)) = -(of L1 * (of L2 * of L3))
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
ih : x * of L2 * of L3 = x * (of L2 * of L3)
⊢ -(x * of L2 * of L3) = -(x * (of L2 * of L3))

Tactic:
ih

Goal state after:
case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
ih : x * of L2 * of L3 = x * (of L2 * of L3)
⊢ -(x * (of L2 * of L3)) = -(x * (of L2 * of L3))
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
⊢ -(x * y * of L3) = -(x * (y * of L3))

Tactic:
ih

Goal state after:
case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
⊢ -(x * (y * of L3)) = -(x * (y * of L3))
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
L : α
ih : (lift fun x₂ ↦ of (1 * x₂)) (of L) = of L
⊢ -(lift fun x₂ ↦ of (1 * x₂)) (of L) = -of L

Tactic:
ih

Goal state after:
case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
L : α
ih : (lift fun x₂ ↦ of (1 * x₂)) (of L) = of L
⊢ -of L = -of L
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
L : α
ih : (lift fun x₁ ↦ of (x₁ * 1)) (of L) = of L
⊢ -(lift fun x₁ ↦ of (x₁ * 1)) (of L) = -of L

Tactic:
ih

Goal state after:
case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
L : α
ih : (lift fun x₁ ↦ of (x₁ * 1)) (of L) = of L
⊢ -of L = -of L
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
ih : (lift ⇑f) (x * of L2) = (lift ⇑f) x * (lift ⇑f) (of L2)
⊢ -(lift ⇑f) (x * of L2) = -((lift ⇑f) x * (lift ⇑f) (of L2))

Tactic:
ih

Goal state after:
case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
ih : (lift ⇑f) (x * of L2) = (lift ⇑f) x * (lift ⇑f) (of L2)
⊢ -((lift ⇑f) x * (lift ⇑f) (of L2)) = -((lift ⇑f) x * (lift ⇑f) (of L2))
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : S.IsLocalizationMap ⇑f
⊢ f ↑1 * f 1 = f ↑1

Tactic:
exact (map_mul ..).symm.trans congr(f $(mul_one _))

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mp.mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : Injective ⇑(f.lift hg)
x y : M
h : (f.lift hg) (f x) = (f.lift hg) (f y)
⊢ f x = f y

Tactic:
exact H h

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
p r : R
s : ↥S
⊢ p /ₒ s * (r /ₒ 1) = p * r /ₒ s

Tactic:
by
  --TODO use coercion r ↦ r /ₒ 1
  simp [oreDiv_mul_char p r s 1 p 1 (by simp)]

Goal state after: