mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : ℕ
fn : { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f }

Tactic:
exact ⟨(minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).1,
        (minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).2.2⟩

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g * a⁻¹ = a⁻¹ * g

Tactic:
rw [mul_inv_eq_iff_eq_mul, mul_assoc, eq_inv_mul_iff_mul_eq, ha g hg]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
hHnK : normalizer ↑H ≤ normalizer ↑K
⊢ normalizer ↑H ≤ normalizer ↑(K ⊔ H)

Tactic:
rw [sup_comm]

Goal state after:
G : Type u_2
inst✝ : Group G
H K : Subgroup G
hHnK : normalizer ↑H ≤ normalizer ↑K
⊢ normalizer ↑H ≤ normalizer ↑(H ⊔ K)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
h : Gᵐᵒᵖ
s : Set G
⊢ (fun y ↦ h • y) '' (fun x ↦ g * x) ⁻¹' s = (fun x ↦ g * x) ⁻¹' (fun y ↦ h • y) '' s

Tactic:
simp [preimage_preimage, mul_assoc]

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

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
s : Multiset M
⊢ ofAdd s.sum = (Multiset.map (⇑ofAdd) s).prod

Tactic:
by
  simp [ofAdd]; rfl

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

Goal state before:
pp: α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ (L1 ++ L2).length + 2 = (L1 ++ (x, b) :: (x, !b) :: L2).length

Tactic:
List.length_append,

Goal state after:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ L1.length + L2.length + 2 = (L1 ++ (x, b) :: (x, !b) :: L2).length
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a b c : FreeGroup α), a * b * c = a * (b * c)

Tactic:
rintro ⟨L₁⟩ ⟨L₂⟩ ⟨L₃⟩

Goal state after:
case mk.mk.mk
α : Type u
L L₁✝ L₂✝ L₃✝ L₄ : List (α × Bool)
a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
c✝ : FreeGroup α
L₃ : List (α × Bool)
⊢ Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂ * Quot.mk Red.Step L₃ =
    Quot.mk Red.Step L₁ * (Quot.mk Red.Step L₂ * Quot.mk Red.Step L₃)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ ∏ a ∈ s₁, f a = ∏ a ∈ s₂, g a

Tactic:
conv_lhs => rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]

Goal state after:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ ∏ a ∈ s₁ ∩ s₂, f a = ∏ a ∈ s₂, g a
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
a : α
⊢ (lift f) (of a) = f a

Tactic:
by simp only [lift_apply_of]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∏ i, f i = ∏ i, g i

Tactic:
rw [← prod_subset s.toFinset.subset_univ (by simpa), prod_subtype (p := (· ∈ s)) _ (by simp)]
  congr! with ⟨x, h⟩
  exact w x h

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG ↔ (toAddSubgroup P).FG

Tactic:
Subgroup.fg_iff_submonoid_fg,

Goal state after:
G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG ↔ (toAddSubgroup P).FG
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 : f i = ⊥
hfij : f i = f j
⊢ g (f i) = 1

Tactic:
hdisj,

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 : f i = ⊥
hfij : f i = f j
⊢ g ⊥ = 1
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer ↑H₂

Tactic:
rw [eq_bot_iff, commutator_le]

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ ⊥) ↔ H₁ ≤ centralizer ↑H₂
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z : FreeAbelianGroup α
⊢ x * y * z = x * (y * z)

Tactic:
by
    induction z using FreeAbelianGroup.induction_on with
    | zero => simp only [mul_zero]
    | of L3 =>
      induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, zero_mul]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]
      | neg L2 ih => rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
      | add y₁ y₂ ih₁ ih₂ => rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
    | neg L3 ih => rw [mul_neg, mul_neg, mul_neg, ih]
    | add z₁ z₂ ih₁ ih₂ => rw [mul_add, mul_add, mul_add, ih₁, ih₂]

Goal state after:
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
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
w v : P
⊢ (f.lift hg) z * w = v ↔ g (f.sec z).1 * w = g ↑(f.sec z).2 * v

Tactic:
rw [mul_comm, lift_apply, ← mul_assoc, mul_inv_left hg, mul_comm]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ u * ↑y.2 * x.1 = u * (↑x.2 * y.1)

Tactic:
e₂,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ v * ↑x.2 * x.1 = u * (↑x.2 * y.1)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ u * (↑y.2 * x.1) = u * (↑x.2 * y.1)

Tactic:
by rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]

Goal state after:
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 : S.LocalizationMap N
x y : M
c : ↥S
h : f ↑c * f x = f ↑c * f y
u : Nˣ
hu : ↑u = f ↑c
⊢ f x = f y

Tactic:
rw [← hu] at h

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
u : Nˣ
h : ↑u * f x = ↑u * f y
hu : ↑u = f ↑c
⊢ f x = f y
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsMin b
⊢ limitRecOn b isMin succ isSuccLimit = isMin b hb

Tactic:
limitRecOn,

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsMin b
⊢ (prelimitRecOn b succ fun a ha IH ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) = isMin b hb
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccLimit b
⊢ limitRecOn b isMin succ isSuccLimit = isSuccLimit b hb fun x x_1 ↦ limitRecOn x isMin succ isSuccLimit

Tactic:
limitRecOn,

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccLimit b
⊢ (prelimitRecOn b succ fun a ha IH ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    isSuccLimit b hb fun x x_1 ↦ limitRecOn x isMin succ isSuccLimit
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
⊢ limitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb (limitRecOn b isMin succ isSuccLimit)

Tactic:
limitRecOn,

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
⊢ (prelimitRecOn (Order.succ b) succ fun a ha IH ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    succ b hb (limitRecOn b isMin succ isSuccLimit)
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - ↑(n + 1)

Tactic:
rw [Nat.cast_add_one, ← sub_sub]

Goal state after:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - ↑n - 1
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
x✝ : ℕ
⊢ ↑(↑x✝).toNat = ↑x✝ ↔ ↑x✝ ≠ ⊤

Tactic:
by simp [toNat_natCast]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, ¬p x
⊢ (∏ x ∈ s, if p x then k (f x) else k (g x)) = ∏ x ∈ s, k (g x)

Tactic:
exact prod_ite_of_false h _ _

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

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable (Sigma π)

Tactic:
rcases exists_injective_nat α with ⟨f, hf⟩
  choose g hg using fun a => exists_injective_nat (π a)
  exact ((Equiv.sigmaEquivProd ℕ ℕ).injective.comp <| hf.sigma_map hg).countable

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

Goal state before:
pp: α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable ((a : α) → π a)

Tactic:
have (n : ℕ) : Countable (Fin n → ℕ) := by
    induction n with
    | zero => infer_instance
    | succ n ihn => exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Fin.consEquiv fun _ ↦ ℕ)
  rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
  have f := fun a => (nonempty_embedding_nat (π a)).some
  exact ((Embedding.piCongrRight f).trans (Equiv.piCongrLeft' _ e).toEmbedding).countable

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

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v).eraseIdx ↑⟨i, ⋯⟩).insertIdx j a =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j.succ, hj⟩.pred ⋯)) a

Tactic:
simp; rfl

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).toList.prod = (take (↑i) v).toList.prod * a * (drop (↑i + 1) v).toList.prod

Tactic:
refine (List.prod_set v.toList i a).trans ?_
  simp_all

Goal state after:
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
y : α
hy : y < x
⊢ y < ⨆ a, succ ↑a

Tactic:
lt_ciSup_iff' H

Goal state after:
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
H : BddAbove (range fun a ↦ succ ↑a)
y : α
hy : y < x
⊢ ∃ i, y < succ ↑i
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f✝ : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f✝.top = g.top
f : (Subrel (Sum.Lex r s) fun x ↦ Sum.Lex r s x g.top) ≃r r
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
exact ⟨Sum.inl <| (f.symm.trans g.subrelIso).toInitialSeg⟩

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

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ (⇑f)^[n₁] ((⇑f)^[n₂] (a₁ ⊔ a₂)) = (⇑f)^[n₁] ((⇑f)^[n₂] (a₂ ⊔ a₁))

Tactic:
rw [sup_comm]

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

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ (⇑f)^[n₁] ((⇑f)^[n₂] a₂ ⊔ a₁) = (⇑f)^[n₁] (a₁ ⊔ (⇑f)^[n₂] a₂)

Tactic:
rw [sup_comm]

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: case refine_1
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
⊢ (lfp.comp h) (lfp h.onDiag) ≤ lfp h.onDiag

pp: case refine_2
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
⊢ h.onDiag (lfp (lfp.comp h)) = lfp (lfp.comp h)

Tactic:
· exact lfp_le _ h.onDiag.map_lfp.le

Goal state after:
case refine_2
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
⊢ h.onDiag (lfp (lfp.comp h)) = lfp (lfp.comp h)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ωSup c ≤ a

Tactic:
ωSup_le_iff

Goal state after:
case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ∀ (i : ℕ), c i ≤ a
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union.inr.inl
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : c₁ ⊆ c₃
h' : c₃ = c₁
⊢ False

Tactic:
exact h₁ h'.subset

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

Goal state before:
pp: a b c : Cardinal.{u_1}
h : b ≤ c
⊢ a ^ b ≤ max (a ^ c) 1

Tactic:
by
  by_cases ha : a = 0
  · simp [ha, zero_power_le]
  · exact (power_le_power_left ha h).trans (le_max_left _ _)

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

Goal state before:
pp: S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
⊢ ∃ n, lift.{u_1, 0} #↑S = ↑n

Tactic:
suffices S.Finite by
      lift S to Finset ℕ using this
      simp

Goal state after:
S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
⊢ S.Finite
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg.right
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 * b < ℵ₀

Tactic:
exact (mul_le_mul' ha le_rfl).trans_lt h

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : Module S R
inst✝³ : IsTorsionFree S R
inst✝² : IsScalarTower S R R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R M
s : S
hs : IsRegular s
x y : M
hxy : (fun x ↦ s • x) x = (fun x ↦ s • x) y
⊢ (fun x ↦ (s • 1) • x) x = (fun x ↦ (s • 1) • x) y

Tactic:
simpa using hxy

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : Module S R
inst✝³ : IsTorsionFree S R
inst✝² : IsScalarTower S R R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R M
s : S
hs : IsRegular s
x✝ y✝ : M
hxy✝ : (fun x ↦ s • x) x✝ = (fun x ↦ s • x) y✝
x y : R
hxy : (fun x ↦ s • 1 * x) x = (fun x ↦ s • 1 * x) y
⊢ (fun x ↦ s • x) x = (fun x ↦ s • x) y

Tactic:
simpa using hxy

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsTorsionFree R M
inst✝⁴ : Module S R
inst✝³ : IsTorsionFree S R
inst✝² : IsScalarTower S R R
inst✝¹ : SMulCommClass S R R
inst✝ : IsScalarTower S R M
s : S
hs : IsRegular s
x✝ y✝ : M
hxy✝ : (fun x ↦ s • x) x✝ = (fun x ↦ s • x) y✝
x y : R
hxy : (fun x ↦ x * s • 1) x = (fun x ↦ x * s • 1) y
⊢ (fun x ↦ s • x) x = (fun x ↦ s • x) y

Tactic:
simpa using hxy

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

Goal state before:
pp: case fst
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝² x✝¹ : R
x✝ : M × N
⊢ ((x✝² + x✝¹) • x✝).1 = (x✝² • x✝ + x✝¹ • x✝).1

Tactic:
exact add_smul ..

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

Goal state before:
pp: case snd
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝² x✝¹ : R
x✝ : M × N
⊢ ((x✝² + x✝¹) • x✝).2 = (x✝² • x✝ + x✝¹ • x✝).2

Tactic:
exact add_smul ..

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : SetLike S M
inst✝² : Monoid R
inst✝¹ : MulAction R M
inst✝ : SMulMemClass S R M
s : S
r : Rˣ
x : M
hx : x ∈ ↑s
⊢ x ∈ ↑r • ↑s

Tactic:
exact ⟨r⁻¹ • x, SMulMemClass.smul_mem (↑r⁻¹ : R) hx, by simp [← Units.smul_def]⟩

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
f : F
a b : α
⊢ f (a ⊔ b) = f a ⊔ f b

Tactic:
rw [← sSup_pair, map_sSup]
      simp only [Set.image_pair, sSup_insert, sSup_singleton]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
⊢ map f p < map f q ↔ p < q

Tactic:
by
  rw [lt_iff_le_and_ne, lt_iff_le_and_ne, map_le_map_iff_of_injective hf,
    (map_injective_of_injective hf).ne_iff]

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

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ i, p i ∧ x ∈ S i

Tactic:
iSup_subtype',

Goal state after:
M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ x ∈ ⨆ x, S ↑x ↔ ∃ i, p i ∧ x ∈ S i
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : Nonempty M
inst✝ : Nonempty N
s : Subsemigroup M
t : Subsemigroup N
⊢ s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

Tactic:
by
  simp only [eq_top_iff, le_prod_iff, ← srange_eq_map, srange_fst, srange_snd]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
a : R
⊢ a ∈ Set.center R ↔
    AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧
      AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧
        AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)

Tactic:
rw [Set.mem_center_iff, isMulCentral_iff]
  simp [DFunLike.ext_iff, commute_iff_eq]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
⊢ ↑(closure s) = ↑(AddSubmonoid.closure ↑(Subsemigroup.closure s))

Tactic:
simp [← Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid,
    Subsemigroup.nonUnitalSubsemiringClosure_eq_closure]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd = -1
⊢ -1 * tl.prod = -L.prod

Tactic:
neg_one_mul,

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd = -1
⊢ -tl.prod = -L.prod
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd = -1
⊢ -1 * -L.prod = L.prod

Tactic:
neg_one_mul,

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd = -1
⊢ - -L.prod = L.prod