mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : M
y : ↥S
⊢ mk x y * (monoidOf S).toMonoidHom ↑y = (monoidOf S) x

Tactic:
by
      dsimp
      rw [← mk_one_eq_monoidOf_mk, ← mk_one_eq_monoidOf_mk, mk_mul x y y 1, mul_comm y 1]
      conv => rhs; rw [← mul_one 1]; rw [← mul_one x]
      exact mk_eq_mk_iff.2 (Con.symm _ <| (Localization.r S).mul (Con.refl _ (x, 1)) <| one_rel _)

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

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
y : OreLocalization S R
r₁ : R
s₁ : ↥S
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁ * y) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ y

Tactic:
cases y with | _ r₂ s₂
     =>  _ 

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₂ /ₒ s₂)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
x : OreLocalization S X
⊢ (r • 1) • x = r • x

Tactic:
smul_one_smul

Goal state after:
R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
x : OreLocalization S X
⊢ r • x = r • x
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
⊢ m • (r • 1) • x = m • r • x

Tactic:
smul_one_smul

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
⊢ m • r • x = m • r • x
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
y : OreLocalization S X
r₁ : M
s₁ : ↥S
⊢ r • (r₁ /ₒ s₁) • y = (r₁ /ₒ s₁) • r • y

Tactic:
cases y with | _ r₂ s₂
     =>  _ 

Goal state after:
case c.c
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ r • (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = (r₁ /ₒ s₁) • r • (r₂ /ₒ s₂)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
y : OreLocalization S R
r₁ : R
s₁ : ↥S
⊢ r₁ /ₒ s₁ * y = y * (r₁ /ₒ s₁)

Tactic:
cases y with | _ r₂ s₂
     =>  _ 

Goal state after:
case c.c
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₂ /ₒ s₂ * (r₁ /ₒ s₁)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
hb : ↑b₁ < b₂
ha₂ : a₂ ≠ ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * b₂

Tactic:
obtain rfl | hb₂ := eq_or_ne b₂ ⊤

Goal state after:
case inr.inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : ↑b₁ < ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * ⊤

case inr.inr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
hb : ↑b₁ < b₂
ha₂ : a₂ ≠ ⊤
hb₂ : b₂ ≠ ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * b₂
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case succ
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ^[n + 1] b)
hb : b ≤ succ^[n + 1] b
⊢ succ^[n + 1] b ≤ b

Tactic:
rw [iterate_succ_apply'] at h
    exact (not_isSuccPrelimit_succ _ h).elim

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

Goal state before:
pp: case mpr
α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit a
H : ∀ c < a, c ≤ b
ha : b < a
⊢ False

Tactic:
exact h b ⟨ha, fun c hb hc ↦ (H c hc).not_gt hb⟩

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
ha : a ∉ s
⊢ ¬IsMin a

Tactic:
obtain ⟨b, hb⟩ := hs'

Goal state after:
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ∈ s
⊢ ¬IsMin a
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsSuccLimit b
⊢ (isSuccPrelimitRecOn b succ fun a ha ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯) = isSuccLimit b hb

Tactic:
isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit,

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

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsMin b
⊢ (isSuccPrelimitRecOn b succ fun a ha ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯) = isMin b hb

Tactic:
isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit,

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : IsMin b
⊢ (if h : IsMin b then isMin b h else isSuccLimit b ⋯) = isMin b hb
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
i : α
hi : i ≠ ⊥
⊢ P i

Tactic:
obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i)

Goal state after:
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ P (Order.succ^[j] ⊥)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : b ≤ succ a
x : α
⊢ a < x → b ≤ x

Tactic:
exact fun hx ↦ le_of_lt_succ <| lt_of_le_of_lt h <| succ_strictMono hx

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

Goal state before:
pp: case coe
α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
a : α
h : a + 1 = 0
⊢ False

Tactic:
simpa [h] using max_of_succ_le (a := a)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f (a + 1) ≤ f a) → AntitoneOn f s

Tactic:
simpa [Order.succ_eq_add_one] using antitoneOn_of_succ_le hs (f := f)

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

Goal state before:
pp: case succ.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
⊢ f (pred (pred^[n + 1] b)) < f b

Tactic:
have : pred^[n + 1] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩

Goal state after:
case succ.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
⊢ f (pred (pred^[n + 1] b)) < f b
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
⊢ update (s.piecewise f g) i v = s.piecewise (update f i v) g

Tactic:
update_piecewise

Goal state after:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
⊢ s.piecewise (update f i v) (update g i v) = s.piecewise (update f i v) g
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
⊢ update (s.piecewise f g) i v = s.piecewise f (update g i v)

Tactic:
update_piecewise

Goal state after:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
⊢ s.piecewise (update f i v) (update g i v) = s.piecewise f (update g i v)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ((if ¬a = a then count a ↑m else 0) + if a = a then count a ↑m else 0) = count a ↑m

Tactic:
rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]

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

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ decode (encode s) = s

Tactic:
· simp only [decode, h, not_false_iff, encode_of_none_notMem, Embedding.some_apply, map_map,
      comp_apply, Option.some_get]
    convert! s.attach_map_coe

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

Goal state before:
pp: case mk.mk
α : Type u_1
n : ℕ
a : α
val✝¹ : List α
property✝ : val✝¹.length = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ (set ⟨val✝¹, property✝⟩ ⟨val✝, isLt✝⟩ a).get ⟨val✝, isLt✝⟩ = a

Tactic:
simp [Vector.set, get_eq_get_toList]

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
⊢ ⨆ a, ↑a = x

Tactic:
← sSup_eq_iSup',

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
⊢ sSup (Iio x) = x
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
⊢ ⨆ a, ↑a = x ↔ IsSuccPrelimit x

Tactic:
← sSup_eq_iSup',

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
⊢ sSup (Iio x) = x ↔ IsSuccPrelimit x
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ (lift.{u, v} #α ^ sum fun i ↦ #(f i)) = prod fun i ↦ #α ^ (fun i ↦ #(f i)) i

Tactic:
| _ f =>

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a : α
b : β
h : s b (f a)
⊢ ∃ a', f a' = b ∧ r a' a

Tactic:
rcases f.mem_range_of_rel h with ⟨a', rfl⟩
    exact ⟨a', rfl, f.map_rel_iff.1 h⟩

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α × β
ha : IsLUB (Prod.fst '' d) a.1 ∧ IsLUB (Prod.snd '' d) a.2
⊢ IsLUB (Prod.fst '' d) a.1

Tactic:
exact ha.1

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsLeast (bot x f) x

Tactic:
constructor
    · exact fun _ h ↦ h.base_isLeast.1
    · intro y hy
      exact hy (Ici x) (ici_isAdmissible le_map)

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
x : Part α
⊢ x.bind some = x

Tactic:
bind_some_eq_map

Goal state after:
α : Type u_1
x : Part α
⊢ map (fun y ↦ y) x = x
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
H : ∃ m, c ⊆ m ∧ Maximal (fun x ↦ x ∈ {s | c ⊆ s ∧ IsChain r s}) m
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M

pp: case refine_1
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∀ c_1 ⊆ {s | c ⊆ s ∧ IsChain r s},
    IsChain (fun x1 x2 ↦ x1 ⊆ x2) c_1 → c_1.Nonempty → ∃ ub ∈ {s | c ⊆ s ∧ IsChain r s}, ∀ s ∈ c_1, s ⊆ ub

Tactic:
· obtain ⟨M, hcM, hM⟩ := H
    exact ⟨M, ⟨hM.prop.2, fun d hd hMd ↦ hM.eq_of_subset ⟨hcM.trans hMd, hd⟩ hMd⟩, hcM⟩

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∀ c_1 ⊆ {s | c ⊆ s ∧ IsChain r s},
    IsChain (fun x1 x2 ↦ x1 ⊆ x2) c_1 → c_1.Nonempty → ∃ ub ∈ {s | c ⊆ s ∧ IsChain r s}, ∀ s ∈ c_1, s ⊆ ub
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case pos
c : Cardinal.{u}
h : c = 0
⊢ 0 ^ c ≤ 1

pp: case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ^ c ≤ 1

Tactic:
· rw [h, power_zero]

Goal state after:
case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ^ c ≤ 1
Module: Mathlib.SetTheory.Cardinal.Order

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

pp: case neg
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1

Tactic:
· simp [ha, zero_power_le]

Goal state after:
case neg
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
⊢ toNat c = 0 ↔ c = 0 ∨ ℵ₀ ≤ c

Tactic:
← toNat_toENat,

Goal state after:
c : Cardinal.{u}
⊢ (toENat c).toNat = 0 ↔ c = 0 ∨ ℵ₀ ≤ c
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u_1}
h : ↑(toNat c) = c
⊢ c < ℵ₀

Tactic:
by rw [← h]; simp

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
hn : n ≠ 0
⊢ toNat c = n ↔ c = ↑n

Tactic:
← toNat_toENat,

Goal state after:
c : Cardinal.{u}
n : ℕ
hn : n ≠ 0
⊢ (toENat c).toNat = n ↔ c = ↑n
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x y : Cardinal.{u}
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
wlog hle : x ≤ y; · rw [mul_comm, this y x (le_of_not_ge hle), mul_comm]
    cases lt_or_ge y ℵ₀ with
    | inl hy =>
      lift x to ℕ using hle.trans_lt hy; lift y to ℕ using hy
      simp only [← Nat.cast_mul, toENatAux_nat]
    | inr hy =>
      rcases eq_or_ne x 0 with rfl | hx
      · simp
      · simp only [toENatAux_eq_top hy]
        rw [toENatAux_eq_top, ENat.mul_top]
        · rwa [Ne, toENatAux_eq_zero]
        · exact le_mul_of_one_le_of_le (Cardinal.one_le_iff_ne_zero.2 hx) hy

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
r s : R✝
x✝ : M✝
R : Type u_5
S : Type u_6
M : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : SMul S M
f : R →+* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
x : M
⊢ 0 • x = 0

Tactic:
← f.map_zero,

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
r s : R✝
x✝ : M✝
R : Type u_5
S : Type u_6
M : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : SMul S M
f : R →+* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
x : M
⊢ f 0 • x = 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b c : Cardinal.{u}
⊢ ⨆ c, a ^ ↑c ≤ c ↔ ∀ x < b, a ^ x ≤ c

Tactic:
ciSup_le_iff'

Goal state after:
a b c : Cardinal.{u}
⊢ (∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ x < b, a ^ x ≤ c

case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c ↦ a ^ ↑c)
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝¹⁴ : Monoid M
N : Type u_2
inst✝¹³ : Monoid N
P : Type u_3
inst✝¹² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝¹¹ : Monoid A
inst✝¹⁰ : MulDistribMulAction M A
B : Type u_5
inst✝⁹ : Monoid B
inst✝⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝⁷ : Monoid B₁
inst✝⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝⁵ : Monoid C
inst✝⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝³ : Group A'
inst✝² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹ : Group B'
inst✝ : MulDistribMulAction N B'
g : A →ₑ*[φ] B
tF : A →ₑ[⇑φ] B
map_one'✝ : tF.toFun 1 = 1
map_mul'✝ : ∀ (x y : A), tF.toFun (x * y) = tF.toFun x * tF.toFun y
h : (fun m ↦ m.toFun) { toMulActionHom := tF, map_one' := map_one'✝, map_mul' := map_mul'✝ } = (fun m ↦ m.toFun) g
⊢ { toMulActionHom := tF, map_one' := map_one'✝, map_mul' := map_mul'✝ } = g

Tactic:
rcases g with ⟨tG, _, _⟩

Goal state after:
M : Type u_1
inst✝¹⁴ : Monoid M
N : Type u_2
inst✝¹³ : Monoid N
P : Type u_3
inst✝¹² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝¹¹ : Monoid A
inst✝¹⁰ : MulDistribMulAction M A
B : Type u_5
inst✝⁹ : Monoid B
inst✝⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝⁷ : Monoid B₁
inst✝⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝⁵ : Monoid C
inst✝⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝³ : Group A'
inst✝² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹ : Group B'
inst✝ : MulDistribMulAction N B'
tF : A →ₑ[⇑φ] B
map_one'✝¹ : tF.toFun 1 = 1
map_mul'✝¹ : ∀ (x y : A), tF.toFun (x * y) = tF.toFun x * tF.toFun y
tG : A →ₑ[⇑φ] B
map_one'✝ : tG.toFun 1 = 1
map_mul'✝ : ∀ (x y : A), tG.toFun (x * y) = tG.toFun x * tG.toFun y
h :
  (fun m ↦ m.toFun) { toMulActionHom := tF, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun m ↦ m.toFun) { toMulActionHom := tG, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toMulActionHom := tF, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toMulActionHom := tG, map_one' := map_one'✝, map_mul' := map_mul'✝ }
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
⊢ ↑(sInf (Set.range fun i ↦ p i)) = ⋂ i, ↑(p i)

Tactic:
coe_sInf

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
⊢ ⋂ p_1 ∈ Set.range fun i ↦ p i, ↑p_1 = ⋂ i, ↑(p i)
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 α β
e : α ≃ β
s : Set α
⊢ (fun s ↦ ⇑e.symm '' s) ((fun s ↦ ⇑e '' s) s) = s

Tactic:
by simp only [← image_comp, Equiv.symm_comp_self, id, image_id']

Goal state after:
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : m → M
i : m
⊢ (funLeft R M ⇑e ∘ₗ funLeft R M ⇑e.symm) x i = LinearMap.id x i

Tactic:
rw [id_apply, ← funLeft_comp, Equiv.symm_comp_self, LinearMap.funLeft_id]

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

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
⊢ ∀ (x : ι), b ∈ S x → a * b = b * a

Tactic:
j

Goal state after:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
j : ι
⊢ b ∈ S j → a * b = b * a
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : R
i : ι
ha : a ∈ S i
b : R
⊢ ∀ (x : ι), b ∈ S x → a * b = b * a

Tactic:
j

Goal state after:
R : Type u
inst✝¹ : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : R
i : ι
ha : a ∈ S i
b : R
j : ι
⊢ b ∈ S j → a * b = b * a
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 : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ (hd.prod = L.prod ∨ hd.prod = -L.prod)

Tactic:
induction hd with
  | nil => exact ⟨[], List.forall_mem_nil _, Or.inl rfl⟩
  | cons hd tl ih => ?_

Goal state after:
case cons
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 : ∀ y ∈ hd :: tl, y ∈ s ∨ y = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mpr.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
h : x ~ᵤ y
⊢ y ∣ x

Tactic:
· exact h.symm.dvd

Goal state after: