mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u_1
γ : Type u_2
α : Type u_3
inst✝² : SMul γ α
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : α
m m' : M
ha : m • a = a
hb : m' • a = a
⊢ (m * m') • a = a

Tactic:
← smul_smul,

Goal state after:
M : Type u_1
γ : Type u_2
α : Type u_3
inst✝² : SMul γ α
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : α
m m' : M
ha : m • a = a
hb : m' • a = a
⊢ m • m' • a = a
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
hs : s.IsPWO
ha : a ∈ s
⊢ ∃ b ≤ a, Minimal (fun x ↦ x ∈ s) b

Tactic:
let t : Set s := {x | x ≤ a}
  let h : t.Nonempty := ⟨⟨a, ha⟩, le_rfl⟩
  refine ⟨hs.wellFounded.min t h, hs.wellFounded.min_mem t h,
    (hs.wellFounded.min t h).2, fun y hy hle => ?_⟩
  by_contra hnle
  exact hs.wellFounded.not_lt_min t (x := ⟨y, hy⟩) (hle.trans (hs.wellFounded.min_mem t h))
    ⟨hle, hnle⟩

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ↑[[a, c]] ⊆ ↑([[a, b]] ∪ [[b, c]])

Tactic:
by
    push_cast
    exact Set.uIcc_subset_uIcc_union_uIcc

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

Goal state before:
pp: M : Type u_1
inst✝ : Group M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ Int.ofNat n) (x ^ Int.ofNat n)

Tactic:
simpa only [zpow_natCast, Int.ofNat_eq_natCast] using c.pow n h

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₁₂ : List (α × Bool)
eq : L₁ ++ L₂ = L₁₂
h : Red L L₁₂
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
induction h generalizing L₁ L₂ with
      | refl => exact ⟨_, _, eq.symm, by rfl, by rfl⟩
      | tail hLL' h ih =>
        obtain @⟨s, e, a, b⟩ := h
        rcases List.append_eq_append_iff.1 eq with (⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩)
        · have : L₁ ++ (s' ++ (a, b) :: (a, not b) :: e) =
            L₁ ++ s' ++ (a, b) :: (a, not b) :: e := by simp
          rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
          exact ⟨w₁, w₂, rfl, h₁, h₂.tail Step.not⟩
        · have : s ++ (a, b) :: (a, not b) :: e' ++ L₂ =
            s ++ (a, b) :: (a, not b) :: (e' ++ L₂) := by simp
          rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩
          exact ⟨w₁, w₂, rfl, h₁.tail Step.not, h₂⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : α
⊢ Decidable ((leftRel s) x y)

Tactic:
leftRel_eq

Goal state after:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : α
⊢ Decidable ((fun x y ↦ x⁻¹ * y ∈ s) x y)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ = f (of x)⁻¹ * f (of x) * g (of x)⁻¹

pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ * f (of x) * g (of x)⁻¹ = g (of x)⁻¹

Tactic:
· simp_rw [mul_assoc, h, ← _root_.map_mul, mul_inv_cancel, _root_.map_one, mul_one]

Goal state after:
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ * f (of x) * g (of x)⁻¹ = g (of x)⁻¹
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case neg
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
⊢ Function.Injective ⇑(map f)

Tactic:
Function.injective_iff_hasLeftInverse

Goal state after:
case neg
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
⊢ Function.HasLeftInverse ⇑(map f)
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 c d : G
hab : (leftRel N) a b
hcd : (leftRel N) c d
⊢ (leftRel N) (a * c) (b * d)

Tactic:
leftRel_eq

Goal state after:
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 c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ (fun x y ↦ x⁻¹ * y ∈ N) (a * c) (b * d)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
P : Submonoid M
h : (toAddSubmonoid P).FG
T : Set (Additive M)
hT : AddSubmonoid.closure T = toAddSubmonoid P
hf : T.Finite
⊢ closure (⇑Additive.ofMul ⁻¹' T) = P

Tactic:
by simp [← AddSubmonoid.toSubmonoid'_closure, hT]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
⊢ Subgroup.map (mk' N) N = ⊥

Tactic:
by aesop

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutatorSet G ⊆ ↑f.ker

Tactic:
rintro x ⟨p, q, rfl⟩

Goal state after:
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
p q : G
⊢ ⁅p, q⁆ ∈ ↑f.ker
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_5
inst✝³ : DecidableEq ι
inst✝² : CommMonoid κ
inst✝¹ : LT κ
inst✝ : MulLeftStrictMono κ
s : Finset ι
d : ι
hd : d ∈ s
f : ι → κ
hdf : 1 < f d
| ∏ m ∈ s, f m

Tactic:
rw [← Finset.insert_erase hd]

Goal state after:
ι : Type u_1
κ : Type u_5
inst✝³ : DecidableEq ι
inst✝² : CommMonoid κ
inst✝¹ : LT κ
inst✝ : MulLeftStrictMono κ
s : Finset ι
d : ι
hd : d ∈ s
f : ι → κ
hdf : 1 < f d
| ∏ m ∈ insert d (s.erase d), f m
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
⊢ 0 >>= f >>= g = 0 >>= fun x ↦ f x >>= g

Tactic:
rw [zero_bind]

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
⊢ 0 >>= g = 0 >>= 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 γ✝
⊢ 0 >>= g = 0 >>= fun x ↦ f x >>= g

Tactic:
rw [zero_bind]

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
⊢ 0 = 0 >>= 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 γ✝
⊢ 0 = 0 >>= fun x ↦ f x >>= g

Tactic:
rw [zero_bind]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁

Tactic:
rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x✝ : α
h : (lift (g ∘ f)) (of x✝) = (lift g) ((map f) (of x✝))
⊢ (lift (g ∘ f)) (-of x✝) = (lift g) ((map f) (-of x✝))

Tactic:
| neg _ h =>

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
⊢ commutatorSet G ⊆ ↑N

Tactic:
rintro x ⟨p, q, rfl⟩

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ⁅p, q⁆ ∈ ↑N
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ P (u • r₂) ⟨v * ↑s₁, s₁vS⟩ = P (↑u • r₂) ⟨↑u * ↑s₂, ⋯⟩

Tactic:
simp only [← hs₂]

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ P (u • r₂) (u * s₂) = P (↑u • r₂) ⟨↑u * ↑s₂, ⋯⟩
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case 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 : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
w✝¹ : M × ↥S
h✝¹ : z * f ↑w✝¹.2 = f w✝¹.1
w✝ : M × ↥S
h✝ : w * f ↑w✝.2 = f w✝.1
⊢ f.mk' (f.sec z).1 (f.sec z).2 = w

Tactic:
← f.mk'_sec w

Goal state after:
case 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 : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
w✝¹ : M × ↥S
h✝¹ : z * f ↑w✝¹.2 = f w✝¹.1
w✝ : M × ↥S
h✝ : w * f ↑w✝.2 = f w✝.1
⊢ f.mk' (f.sec z).1 (f.sec z).2 = f.mk' (f.sec w).1 (f.sec w).2
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
h : Commute r ↑s
n : ℕ
ih : (r /ₒ s) ^ n = r ^ n /ₒ s ^ n
⊢ r /ₒ s * (r ^ n /ₒ s ^ n) = r * r ^ n /ₒ (s ^ n * s)

Tactic:
oreDiv_mul_char (r' := r) (s' := s ^ n)

Goal state after:
case succ
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
h : Commute r ↑s
n : ℕ
ih : (r /ₒ s) ^ n = r ^ n /ₒ s ^ n
⊢ r * r ^ n /ₒ (s ^ n * s) = r * r ^ n /ₒ (s ^ n * s)

case succ.huv
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
h : Commute r ↑s
n : ℕ
ih : (r /ₒ s) ^ n = r ^ n /ₒ s ^ n
⊢ ↑(s ^ n) * r = r * ↑(s ^ n)
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - ↑n
⊢ pred (x - ↑n) = x - (↑n + ↑1)

Tactic:
pred_eq_sub_one,

Goal state after:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - ↑n
⊢ x - ↑n - 1 = x - (↑n + ↑1)
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hx : ¬IsMin x
⊢ pred x < y ↔ x ≤ y

Tactic:
pred_lt_iff_of_not_isMin hx

Goal state after:
α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hx : ¬IsMin x
⊢ x ≤ y ↔ x ≤ y
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg.inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∉ s
h✝¹ : ⟨x, hx⟩ ≤ ⟨x, hx⟩
y : α
hy : y ∈ s
h✝ : ⟨y, hy⟩ ≤ ⟨x, hx⟩
h : ⟨y, hy⟩ < ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩

Tactic:
simp only [Subtype.mk_lt_mk] at h

Goal state after:
case neg.inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∉ s
h✝¹ : ⟨x, hx⟩ ≤ ⟨x, hx⟩
y : α
hy : y ∈ s
h✝ : ⟨y, hy⟩ ≤ ⟨x, hx⟩
h : y < x
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f g : (i : ι) → π i
⊢ (univ.erase i).piecewise f g = update f i (g i)

Tactic:
← compl_singleton,

Goal state after:
ι : Type u_1
π : ι → Sort u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f g : (i : ι) → π i
⊢ {i}ᶜ.piecewise f g = update f i (g i)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∏ p ∈ r, f p = ∏ x ∈ s.sigma t, f (x.fst, x.snd)

Tactic:
apply prod_equiv (Equiv.sigmaEquivProd _ _).symm <;> simp [h]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : Sigma κ → Set α
⊢ ⋃ ij ∈ s.sigma fun x ↦ Finset.univ, f ij = ⋃ i ∈ s, ⋃ j, f ⟨i, j⟩

Tactic:
by aesop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : (i : ι) → κ i → Set α
⊢ ⋃ i ∈ s, ⋃ j, f i j = ⋃ ij ∈ s.sigma fun x ↦ Finset.univ, f ij.fst ij.snd

Tactic:
by aesop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : Sigma κ → Set α
⊢ ⋂ ij ∈ s.sigma fun x ↦ Finset.univ, f ij = ⋂ i ∈ s, ⋂ j, f ⟨i, j⟩

Tactic:
by aesop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : (i : ι) → κ i → Set α
⊢ ⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun x ↦ Finset.univ, f ij.fst ij.snd

Tactic:
by aesop

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
⊢ { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 } =
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }

Tactic:
obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2

Goal state after:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
⊢ { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 } =
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ (ofFn f).toList = List.ofFn f

Tactic:
rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁸ : LE α
inst✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a : α
b : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
⊢ ∀ {a b : α₁ ⊕ β₁}, ((↑ea).sumCongr ↑eb) a ≤ ((↑ea).sumCongr ↑eb) b ↔ a ≤ b

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s t : Set α
hs : IsUpperSet s
⊢ IsLowerSet (Subtype.val ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s t : Set α
hs : IsUpperSet s
ht : IsLowerSet t
⊢ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : IsUpperSet (range ⇑e)
a : α
⊢ ⇑e '' Ici a = Ici (e a)

Tactic:
by
  rw [← e.preimage_Ici, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ici_subset (mem_range_self _)]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g : β →o γ
a b : α
hab : a ≤ b
x✝² x✝¹ : ℕ
x✝ : x✝² ≤ x✝¹
⊢ (fun x ↦
        match x with
        | 0 => a
        | x => b)
      x✝² ≤
    (fun x ↦
        match x with
        | 0 => a
        | x => b)
      x✝¹

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
x✝ : α
⊢ ((pair a b hab) 0 = x✝ ∨ ∃ n, (pair a b hab) (n + 1) = x✝) ↔ x✝ ∈ {a, b}

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ChainClosure r ∅

Tactic:
have : ChainClosure r (⋃₀ ∅) := ChainClosure.union fun a h => (notMem_empty _ h).elim
  simpa using this

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
z : α
hz : z ∈ c
hzy : ¬f z ≤ y
⊢ y ≤ z

Tactic:
← bot_eq_of_le_or_map_le le_map (hc hz)

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy' : y < cSup c
z : α
hy : y ∈ {z_1 | z_1 ∈ bot x f ∧ (z_1 ≤ z ∨ f z ≤ z_1)}
hz : z ∈ c
hzy : ¬f z ≤ y
⊢ y ≤ z
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
hc' : cSup c ∈ bot x f
⊢ f y ≤ cSup c

Tactic:
← bot_eq_of_le_or_map_le le_map (hc hz)

Goal state after:
case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
hc' : cSup c ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ f y ≤ cSup c
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ (ωSup (c.map { toFun := f, monotone' := ⋯ })) (g (ωSup c)) =
    ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })

Tactic:
hg.map_ωSup

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ (ωSup (c.map { toFun := f, monotone' := ⋯ })) (ωSup (c.map { toFun := g, monotone' := ⋯ })) =
    ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝¹ : Surjective h
this✝ : Injective h
a : α
h✝ : a ∉ s
this : a ∈ g '' (f '' s)ᶜ
x : β
left✝ : x ∈ (f '' s)ᶜ
hx : g x = a
⊢ g (invFun g a) = a

Tactic:
exact Function.invFun_eq ⟨x, hx⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
n : ℕ∞
x : Cardinal.{u_1}
hx : x < ℵ₀
⊢ ↑n ≤ x ↔ n ≤ x.toENatAux

Tactic:
lift x to ℕ using hx

Goal state after:
case inl
n : ℕ∞
x : ℕ
⊢ ↑n ≤ ↑x ↔ n ≤ (↑x).toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
x : Cardinal.{u_1}
n : ℕ
hx : x < ℵ₀
⊢ x.toENatAux ≤ ↑n ↔ x ≤ ↑n

Tactic:
lift x to ℕ using hx

Goal state after:
case inl
n x : ℕ
⊢ (↑x).toENatAux ≤ ↑n ↔ ↑x ≤ ↑n
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
⊢ toENat #α = toENat #β

Tactic:
rw [← toENat_lift, lift_mk_eq.{_, _, v}.mpr ⟨e⟩, toENat_lift]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ ¬IsSMulRegular M 0 ↔ Nontrivial M

Tactic:
rw [nontrivial_iff, not_iff_comm, zero_iff_subsingleton, subsingleton_iff]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : M), x = y
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ lift.{u, w} (iSup f) ≤ t

Tactic:
lift_iSup hf

Goal state after:
ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ ⨆ i, lift.{u, w} (f i) ≤ t
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ lift.{u, w} (iSup f) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t

Tactic:
lift_iSup hf

Goal state after:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ ⨆ i, lift.{u, w} (f i) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.Countable ∧ Infinite ↑s ↔ Countable ↑s ∧ Infinite ↑s

Tactic:
countable_coe_iff

Goal state after:
α : Type u_1
s : Set α
⊢ s.Countable ∧ Infinite ↑s ↔ s.Countable ∧ Infinite ↑s