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

Goal state before:
pp: case pos
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m < g 0 + n'
hn : ¬g 0 + n' < g 0
hm : m < g 0
hmn : List.SublistForall₂ r (f m) (f (g n')).tail
⊢ False

pp: case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m < g 0 + n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ False

Tactic:
· apply hf1.2 m (g n') (lt_of_lt_of_le hm (g.monotone n'.zero_le))
      exact _root_.trans hmn (List.tail_sublistForall₂_self _)

Goal state after:
case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m < g 0 + n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ False
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
⊢ ∅.centralizer = ⊤

Tactic:
simp [centralizer]

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

Goal state before:
pp: case mul
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 ↦ x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 ↦ x1 * x2) x y * (fun x1 x2 ↦ x1 * x2) x' y' ∈ ↑H * ↑N

Tactic:
refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩

Goal state after:
case mul.refine_1
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 ↦ x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ x'⁻¹ * y * x' ∈ N

case mul.refine_2
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 ↦ x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 ↦ x1 * x2) (x * x') (x'⁻¹ * y * x' * y') = (fun x1 x2 ↦ x1 * x2) x y * (fun x1 x2 ↦ x1 * x2) x' y'
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).sum % n = (∑ i ∈ s, f i % n) % n

Tactic:
rw [Finset.sum, Multiset.map_map]

Goal state after:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).sum % n = (Multiset.map (fun i ↦ f i % n) s.val).sum % n
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map (fun x ↦ x % n) (Multiset.map (fun i ↦ f i) s.val)).sum % n = (∑ i ∈ s, f i % n) % n

Tactic:
rw [Finset.sum, Multiset.map_map]

Goal state after:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).sum % n = (Multiset.map (fun i ↦ f i % n) s.val).sum % n
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case cons
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)

Tactic:
dsimp
      exact Nat.add_lt_add_left ih _

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
a : α × Bool
⊢ invRev (a :: L) = invRev L ++ invRev [a]

Tactic:
by
  simp [invRev]

Goal state after:
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)
⊢ f = g

Tactic:
ext x
  have this (x) : f (of x)⁻¹ = g (of x)⁻¹ := by
    trans f (of x)⁻¹ * f (of x) * g (of x)⁻¹
    · simp_rw [mul_assoc, h, ← _root_.map_mul, mul_inv_cancel, _root_.map_one, mul_one]
    · simp_rw [← _root_.map_mul, inv_mul_cancel, _root_.map_one, one_mul]
  induction x <;> simp [*]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ (map f).range = Subgroup.closure (of '' Set.range f)

Tactic:
by
  rw [map_eq_lift, range_lift_eq_closure, Set.range_comp]

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

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
x✝ y✝ : G
⊢ (QuotientGroup.con f.ker) x✝ y✝ ↔ (Con.ker f) x✝ y✝

Tactic:
rw [QuotientGroup.con, Con.rel_mk, Setoid.comm', leftRel_apply, Con.ker_rel, MonoidHom.eq_iff]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h₃ : ∀ (a : ι) (ha : a ∈ s \ {x, g x hx}), g a ⋯ ∈ s \ {x, g x hx}
⊢ ∀ (a : ι) (ha : a ∈ s \ {x, g x hx}), f a * f (g a ⋯) = 1

Tactic:
simp [hg₁]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : DecidableEq ι
inst✝¹ : PartialOrder ι
inst✝ : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I).PairwiseDisjoint f
i j : κ
hdisj : _root_.Disjoint (f i) (f j)
hfij : f i = f j
⊢ g (f i) = 1

Tactic:
← hfij,

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : DecidableEq ι
inst✝¹ : PartialOrder ι
inst✝ : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I).PairwiseDisjoint f
i j : κ
hdisj : _root_.Disjoint (f i) (f i)
hfij : f i = f j
⊢ g (f i) = 1
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
a : G
h : a ∈ Group.conjugatesOfSet base
⊢ a ∈ base

Tactic:
simp_rw [Group.mem_conjugatesOfSet_iff, isConj_iff] at h

Goal state after:
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
a : G
h : ∃ a_1 ∈ base, ∃ c, c * a_1 * c⁻¹ = a
⊢ a ∈ base
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ a ≤ b ↔ f.symm a ≤ f.symm b

Tactic:
rw [← map_le_map_iff f]

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ a ≤ b ↔ f (f.symm a) ≤ f (f.symm b)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ z * (f ↑a.2 * f ↑b.2) = f a.1 * f ↑b.2

Tactic:
← ha

Goal state after:
case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ z * (f ↑a.2 * f ↑b.2) = z * f ↑a.2 * f ↑b.2
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f).symm (f.mk' x y) = mk x y

Tactic:
rw [mk_eq_monoidOf_mk'_apply]; exact mulEquivOfQuotient_symm_mk' _ _

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
inst✝ : IsCancelMul M
⊢ ∀ (r : N), IsLeftRegular r

Tactic:
← Commute.isRightRegular_iff (Commute.all _)

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
inst✝ : IsCancelMul M
⊢ ∀ (r : N), IsRightRegular r
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : WithBot α
h : a ≠ 0
⊢ a * ⊥ = ⊥

Tactic:
mul_bot',

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : WithBot α
h : a ≠ 0
⊢ (if a = 0 then 0 else ⊥) = ⊥
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hy : ¬IsMax y
⊢ x + 1 ≤ y ↔ x < y

Tactic:
rw [← succ_eq_add_one, succ_le_iff_of_not_isMax' hy]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ ∏ j ∈ s, f j = ∏ j ∈ s, g j ↔ f i = g i

Tactic:
by
  classical
  rw [prod_eq_mul_prod_sdiff_singleton_of_mem hi, prod_eq_mul_prod_sdiff_singleton_of_mem hi,
    prod_congr rfl (by simpa), mul_left_inj]

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

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : i = j
⊢ (v.set i a).get j = a

Tactic:
try simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ (v.set i a).get j = v.get j

Tactic:
try simp [*]

Goal state after:
case neg
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ (v.set i a).get j = v.get j
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_1.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b : α
a : β
hab : inr a < inl b
⊢ False

Tactic:
exact not_inr_lt_inl hab

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ (f.transPrincipal g).toRelEmbedding a = g.toRelEmbedding (f a)

Tactic:
by
  rw [InitialSeg.transPrincipal]
  obtain f' | f' := f.principalSumRelIso
  · rw [PrincipalSeg.trans_apply, f.eq_principalSeg]
  · rw [PrincipalSeg.relIsoTrans_apply, f.eq_relIso]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
x : β
⊢ ScottContinuousOn D (Function.const α x)

Tactic:
rintro s _ ⟨a⟩ _ _ _

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
x : β
s : Set α
a✝³ : s ∈ D
a : α
h✝ : a ∈ s
a✝² : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a✝¹ : α
a✝ : IsLUB s a✝¹
⊢ IsLUB (Function.const α x '' s) (Function.const α x a✝¹)
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : CompleteLattice β
x✝ : Set (α →o β)
⊢ IsGLB (DFunLike.coe '' x✝) ⇑(sInf x✝)

Tactic:
by simp [isGLB_pi, Set.image_image, isGLB_biInf]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
⊢ ωScottContinuous f ↔ ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })

Tactic:
refine ⟨fun hf ↦ ⟨hf.monotone, hf.map_ωSup⟩, ?_⟩
  intro hf _ ⟨c, hc⟩ _ _ _ hda
  convert! isLUB_range_ωSup (c.map { toFun := f, monotone' := hf.1 })
  · simp [← hc, ← (Set.range_comp f ⇑c)]
  · rw [← hc] at hda
    rw [← hf.2 c, ωSup_eq_of_isLUB hda]

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
c : Chain (Part α)
i : ℕ
x : α
hx : c i = some x
⊢ Part.ωSup c = some x

Tactic:
rw [ωSup_eq_some]

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : c i = some x
⊢ some x ∈ c
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), c i ≤ x
a : α
i : ℕ
ha : some a = c i
⊢ a ∈ c i

Tactic:
← ha

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), c i ≤ x
a : α
i : ℕ
ha : some a = c i
⊢ a ∈ some a
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
x y : Cardinal.{u}
hle : x ≤ y
hy : y < ℵ₀
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
| inl hy =>

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

Goal state before:
pp: case inl
x y : Cardinal.{u}
hle : x ≤ y
hy : y < ℵ₀
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux

Tactic:
| inl hy =>

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

Goal state before:
pp: ⊢ StrictMonoOn (⇑toENat) (Iic ℵ₀)

Tactic:
by
  simp only [← range_ofENat, StrictMonoOn, forall_mem_range, toENat_ofENat, ofENat_lt_ofENat]
  exact fun _ _ ↦ id

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
x✝ : MulAction (M × N) α
instM : MulAction M α := compHom α (MonoidHom.inl M N)
instN : MulAction N α := compHom α (MonoidHom.inr M N)
m : M
n : N
a : α
⊢ (m, 1) • (1, n) • a = (1, n) • (m, 1) • a

Tactic:
simp_rw [smul_smul, Prod.mk_mul_mk, mul_one, one_mul]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
n : N
a : α
⊢ SMul.smul n a = SMul.smul n a

Tactic:
(conv_rhs => rw [← hM.one_smul (SMul.smul n a)])

Goal state after:
case e_4.e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
n : N
a : α
⊢ SMul.smul n a = 1 • SMul.smul n a
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ Function.RightInverse
    (fun _insts ↦
      have this := ⋯;
      prodOfSMulCommClass M N α)
    fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩

Tactic:
by
    rintro ⟨hM, hN, -⟩
    dsimp only; congr 1
    · ext m a; (conv_rhs => rw [← hN.one_smul a]); rfl
    congr 1
    · funext; congr; ext m a; (conv_rhs => rw [← hN.one_smul a]); rfl
    · ext n a; (conv_rhs => rw [← hM.one_smul (SMul.smul n a)]); rfl
    · exact proof_irrel_heq ..

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
S : Type u_5
M₃ : Type u_11
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M₃
inst✝ : Module S M₃
σ : R →+* S
f g : R →ₛₗ[σ] M₃
h : f 1 = g 1
x : R
⊢ σ x • f 1 = g (x • 1)

Tactic:
g.map_smulₛₗ,

Goal state after:
R : Type u_1
S : Type u_5
M₃ : Type u_11
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M₃
inst✝ : Module S M₃
σ : R →+* S
f g : R →ₛₗ[σ] M₃
h : f 1 = g 1
x : R
⊢ σ x • f 1 = σ x • g 1
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: case add
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, ↑i
hy✝ : y✝ ∈ ⨆ i, ↑i
⊢ t • x✝ ∈ ⨆ a, ↑a → t • y✝ ∈ ⨆ a, ↑a → t • (x✝ + y✝) ∈ ⨆ a, ↑a

Tactic:
simp_rw [smul_add]

Goal state after:
case add
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, ↑i
hy✝ : y✝ ∈ ⨆ i, ↑i
⊢ t • x✝ ∈ ⨆ a, ↑a → t • y✝ ∈ ⨆ a, ↑a → t • x✝ + t • y✝ ∈ ⨆ a, ↑a
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ f.ker ≤ (f ∘ₗ g).ker

Tactic:
rw [← Module.End.mul_eq_comp, h.eq, Module.End.mul_eq_comp]

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ f.ker ≤ (g ∘ₗ f).ker
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₗ[R] M
n m : ℕ
w : n ≤ m
x : M
h : x ∈ (fun n ↦ (f ^ n).ker) n
⊢ x ∈ (fun n ↦ (f ^ n).ker) m

Tactic:
by
    obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le w
    rw [LinearMap.mem_ker] at h
    rw [LinearMap.mem_ker, add_comm, pow_add, Module.End.mul_apply, h, map_zero]

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

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ closure (⋃ i, ↑(S i)) → ∃ i, x ∈ S i

Tactic:
refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ hx

Goal state after:
case refine_1
M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
x✝ : M
⊢ x✝ ∈ ⋃ i, ↑(S i) → ∃ i, x✝ ∈ S i

case refine_2
M : Type u_2
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
⊢ ∀ (x y : M),
    x ∈ closure (⋃ i, ↑(S i)) → y ∈ closure (⋃ i, ↑(S i)) → (∃ i, x ∈ S i) → (∃ i, y ∈ S i) → ∃ i, x * y ∈ S i
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ M.nonUnitalSubsemiringClosure
H1 : NonUnitalSubsemiring R
⊢ x✝ ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1

Tactic:
rintro - ⟨H2, rfl⟩

Goal state after:
case refine_1
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ M.nonUnitalSubsemiringClosure
H1 : NonUnitalSubsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h ↦ ↑H1) H2
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
⊢ s ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1

Tactic:
rintro - ⟨H2, rfl⟩

Goal state after:
case refine_2
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h ↦ ↑H1) H2
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
H1 : Subsemiring R
⊢ x✝ ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1

Tactic:
rintro - ⟨H2, rfl⟩

Goal state after:
case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
H1 : Subsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h ↦ ↑H1) H2
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
⊢ s ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1

Tactic:
rintro - ⟨H2, rfl⟩

Goal state after:
case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h ↦ ↑H1) H2
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : G
⊢ (algebraMap R A) (x✝ • 1) = (algebraMap R A) 1

Tactic:
rw [algebraMap.smul', map_one, smul_one]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ ↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
coe_range,

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ Set.range ⇑f = ↑⊤ ↔ Set.range ⇑f = Set.univ
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
hx : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
induction hx using AddSubmonoid.closure_induction with

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = -x✝

Tactic:
obtain ⟨L, hL⟩ := hL
    exact ⟨L.map (List.cons (-1)),
      List.forall_mem_map.2 fun j hj => List.forall_mem_cons.2 ⟨Or.inr rfl, hL.1 j hj⟩,
      hL.2 ▸
        List.recOn L (by simp)
          (by simp +contextual [List.map_cons, add_comm])⟩

Goal state after: