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

Goal state before:
pp: case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ ↑s₄' * ↑s₃' * ↑s₁' * ↑s = ↑s₄' * r₃' * ↑s₂' * ↑s

Tactic:
mul_assoc (s₄' : R),

Goal state after:
case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ ↑s₄' * (↑s₃' * ↑s₁') * ↑s = ↑s₄' * r₃' * ↑s₂' * ↑s
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 : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹
⊢ f ↑y = f ↑z

Tactic:
rw [← mul_one (f y), eq_comm, ← mul_inv_left hf y (f z) 1, h]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹
⊢ f ↑z * ↑((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹ = 1
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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : z * f ↑x.2 = f x.1
v : P
hv : k v = x.1
w : P
hw : k w = ↑x.2
⊢ z * f.toMonoidHom (↑k w) = f.toMonoidHom (↑k v)

Tactic:
MonoidHom.coe_coe,

Goal state after:
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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : z * f ↑x.2 = f x.1
v : P
hv : k v = x.1
w : P
hw : k w = ↑x.2
⊢ z * f.toMonoidHom (k w) = f.toMonoidHom (k v)
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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
⊢ f.toMonoidHom (↑k x) = f.toMonoidHom (↑k y) → ∃ c, ↑c * x = ↑c * y

Tactic:
MonoidHom.coe_coe,

Goal state after:
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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
⊢ f.toMonoidHom (k x) = f.toMonoidHom (k y) → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ (rc * rb) • r₃ /ₒ (sc * (sa * s₁)) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))

Tactic:
rw [← mul_assoc, mul_smul]

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ rc • rb • r₃ /ₒ (sc * sa * s₁) = (r₁ /ₒ s₁) • (rb • r₃ /ₒ (sb * s₂))
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : b ≠ 0
⊢ ⊤ * b = ⊤

Tactic:
top_mul',

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : b ≠ 0
⊢ (if b = 0 then 0 else ⊤) = ⊤
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr.coe.top
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
x : R
hx : ↑x ≠ 0
hy : ⊤ ≠ 0
⊢ map (⇑f) (↑x * ⊤) = map ⇑f ↑x * map ⇑f ⊤

Tactic:
have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx

Goal state after:
case inr.inr.coe.top
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
this✝ : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
x : R
hx : ↑x ≠ 0
hy : ⊤ ≠ 0
this : ↑(f x) ≠ 0
⊢ map (⇑f) (↑x * ⊤) = map ⇑f ↑x * map ⇑f ⊤
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝⁷ : DecidableEq α
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : OrderBot α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : PosMulStrictMono α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
x✝ : n + 2 ≠ 0
x y : WithTop α
h : x < y
⊢ (fun a ↦ a ^ (n + 2)) x < (fun a ↦ a ^ (n + 2)) y

Tactic:
by
    simp_rw [pow_succ _ (n + 1)]
    exact WithTop.mul_lt_mul (WithTop.pow_right_strictMono n.succ_ne_zero h) h

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, succ^[n] a = b) ↔ a ≤ b

Tactic:
refine ⟨?_, exists_succ_iterate_of_le⟩

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, succ^[n] a = b) → a ≤ b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Tactic:
rw [Or.comm]

Goal state after:
case inr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[m] r ≤ succ^[n] r ∨ succ^[n] r ≤ succ^[m] r
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccLimit a
b : ↑s
hb : b < a
⊢ ∃ b, b < ↑a

Tactic:
exact ⟨b, hb⟩

Goal state after:
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
⊢ Ioo a b = ∅

Tactic:
ext x
    suffices a < x → b ≤ x by simpa
    exact fun hx ↦ le_of_lt_succ <| lt_of_le_of_lt h <| succ_strictMono hx

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

Goal state before:
pp: n : ℕ∞
hn : n ≠ ⊤
m : ℕ∞
⊢ (m - n).toNat = m.toNat - n.toNat

Tactic:
by
  lift n to ℕ using hn
  induction m
  · rw [top_sub_natCast, toNat_top, zero_tsub]
  · rw [← natCast_sub, toNat_natCast, toNat_natCast, toNat_natCast]

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

Goal state before:
pp: case neg
α✝ : 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⟩
⊢ IsMin ⟨x, hx⟩

Tactic:
rintro ⟨y, hy⟩ h

Goal state after:
case neg
α✝ : 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⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inr.inr.coe.top
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
x : ℕ
hx : ↑x ≠ 0
hy : ⊤ ≠ 0
⊢ map (⇑f) (↑x * ⊤) = map ⇑f ↑x * map ⇑f ⊤

Tactic:
have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx

Goal state after:
case inr.inr.coe.top
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
this✝ : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
x : ℕ
hx : ↑x ≠ 0
hy : ⊤ ≠ 0
this : ↑(f x) ≠ 0
⊢ map (⇑f) (↑x * ⊤) = map ⇑f ↑x * map ⇑f ⊤
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ (∏ i, if p i then a else 1) = if ∃ i, p i then a else 1

Tactic:
simp [prod_ite_one univ p (by simpa using h)]

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

Goal state before:
pp: case succ.succ.refine_2
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ ∀ (i : Fin (n + 1)),
    (scanl f (f b v.head) v.tail).get i.succ =
      f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.succ.castSucc) ((v.head ::ᵥ v.tail).get i.succ)

Tactic:
· intro i'
      simp only [hn, Fin.castSucc_succ, get_cons_succ]

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

Goal state before:
pp: m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (mOfFn fun i ↦ pure (f i)) = pure (ofFn f)

Tactic:
mOfFn,

Goal state after:
m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (do
      let a ← pure (f 0)
      let v ← mOfFn fun i ↦ pure (f i.succ)
      pure (a ::ᵥ v)) =
    pure (ofFn f)
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
⊢ (⋃ i, t i).Countable

Tactic:
have := fun i ↦ (ht i).to_subtype

Goal state after:
α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
this : ∀ (i : ι), Countable ↑(t i)
⊢ (⋃ i, t i).Countable
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
inst✝ : Countable α
⊢ {s | s.Finite}.Countable

Tactic:
simpa using countable_ofPred_finite_subset countable_univ

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y < x
⊢ y = (sumLexIioIci x) (toLex (Sum.inl ⟨y, h⟩))

Tactic:
sumLexIioIci_apply_inl

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y < x
⊢ y = ↑⟨y, h⟩
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ ↑a✝

Tactic:
simp only [elim_inr, elim_inl, Lex.sep, bot_le]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
⊢ ∃ γ t, IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)

Tactic:
obtain f | f := f.principalSumRelIso

Goal state after:
case inl
α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst✝ : IsWellOrder β s
f✝ : r ≼i s
f : r ≺i s
⊢ ∃ γ t, IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)

case inr
α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst✝ : IsWellOrder β s
f✝ : r ≼i s
f : r ≃r s
⊢ ∃ γ t, IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)
Module: Mathlib.Order.FixedPoints

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

Tactic:
refine (lfp_le _ ?_).antisymm (lfp_le _ (Eq.le ?_))

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

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.Zorn

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
ih : ∀ c ⊆ Ici a, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub
x : α
hax : a ≤ x
⊢ ∃ m, x ≤ m ∧ IsMax m

Tactic:
by
  let ⟨m, hxm, ham, hm⟩ := zorn_le_nonempty₀ (Ici a) (fun c hca hc y hy ↦ ?_) x hax
  · exact ⟨m, hxm, fun z hmz => hm (ham.trans hmz) hmz⟩
  · have ⟨ub, hub⟩ := ih c hca hc y hy
    exact ⟨ub, (hca hy).trans (hub y hy), hub⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
c : Chain (Part α)
a b : α
ha : some a ∈ c
hb : some b ∈ c
⊢ a = b

Tactic:
by
  obtain ⟨i, ha⟩ := ha; replace ha := ha.symm
  obtain ⟨j, hb⟩ := hb; replace hb := hb.symm
  rw [eq_some_iff] at ha hb
  rcases le_total i j with hij | hji
  · have := c.monotone hij _ ha; apply mem_unique this hb
  · have := c.monotone hji _ hb; apply Eq.symm; apply mem_unique this ha

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ ωSup (c.map (f.partBind g)) ≤ x ↔ ωSup (c.map f) >>= ωSup (c.map g) ≤ x

Tactic:
simp only [ωSup_le_iff, Part.bind_le]

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ (∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x) ↔ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
h : ¬Acc (fun x1 x2 ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x1 x2 ↦ x1 < x2) c
h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun x1 x2 ↦ x1 < x2) j
⊢ c ≤ j

Tactic:
have : #_ ≤ #_ := ⟨h_1 ⟨j, hj⟩⟩

Goal state after:
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x1 x2 ↦ x1 < x2) c
h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun x1 x2 ↦ x1 < x2) j
this : #(Quotient.out (f ⟨c, hc⟩)) ≤ #(Quotient.out (f ⟨j, hj⟩))
⊢ c ≤ j
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{max u v, v} (f i) ≤ ⨆ i, lift.{u, v} (f i)

Tactic:
lift_umax.{v, u}

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} (f i) ≤ ⨆ i, lift.{u, v} (f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
⊢ 1 ≤ c ↔ 0 < c

Tactic:
rw [← succ_zero, succ_le_iff]

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ 1 ≤ c ↔ c ≠ 0

Tactic:
by
  rw [Cardinal.one_le_iff_pos, pos_iff_ne_zero]

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

Goal state before:
pp: α : Type u
β : Type v
⊢ lift.{max u v, v} #β = lift.{u, v} #β

Tactic:
lift_umax.{v, u}

Goal state after:
α : Type u
β : Type v
⊢ lift.{u, v} #β = lift.{u, v} #β
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✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a : M
x : α × β
inst✝¹ : SMulCommClass M N α
inst✝ : SMulCommClass M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ x✝² • x✝¹ • x✝ = x✝¹ • x✝² • x✝

Tactic:
ext <;> exact smul_comm ..

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

Goal state before:
pp: M : Type u_1
β : Type u_4
inst✝³ : SMul M β
α : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction M α
a : M
c : β
⊢ a • (0, c) = (0, a • c)

Tactic:
rw [Prod.smul_mk, smul_zero]

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

Goal state before:
pp: M : Type u_1
α : Type u_3
inst✝³ : SMul M α
β : Type u_5
inst✝² : Monoid M
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction M β
a : M
b : α
⊢ a • (b, 0) = (a • b, 0)

Tactic:
rw [Prod.smul_mk, smul_zero]

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R'
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁵ : Monoid S'
inst✝⁴ : DistribMulAction S' M
inst✝³ : SMulCommClass R S' M
inst✝² : Monoid T'
inst✝¹ : DistribMulAction T' M
inst✝ : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
x y : M
⊢ (a • ⇑f) (x + y) = (a • ⇑f) x + (a • ⇑f) y

Tactic:
simp only [DomMulAct.smul_apply, f.map_add, smul_add]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
b : R
y : M₁
⊢ f (b • y) • x = (RingHom.id R) b • f y • x

Tactic:
RingHom.id_apply,

Goal state after:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
b : R
y : M₁
⊢ f (b • y) • x = b • f y • x
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝ : SMul R M
ι : Sort u_1
p : ι → SubMulAction R M
x : M
⊢ x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i

Tactic:
change x ∈ ⋂ s ∈ Set.range p, s ↔ _
  simp

Goal state after:
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
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
by
  have := le_sSup hs
  rw [LE.le] at this
  exact this

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_2
N : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
x y : M
ha : x ~ᵤ y
⊢ f x ~ᵤ f y

Tactic:
obtain ⟨u, ha⟩ := ha

Goal state after:
M : Type u_2
N : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
x y : M
u : Mˣ
ha : x * ↑u = y
⊢ f x ~ᵤ f y
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ y ∣ x ↔ IsUnit y ∨ x ~ᵤ y

Tactic:
constructor
  · rintro ⟨z, hz⟩
    obtain (h | h) := hx.isUnit_or_isUnit hz
    · exact Or.inl h
    · rw [hz]
      exact Or.inr (associated_mul_unit_left _ _ h)
  · rintro (hy | h)
    · exact hy.dvd
    · exact h.symm.dvd

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
⊢ ∀ {a : Associates M}, a ≠ 0 → IsLeftRegular a

Tactic:
rintro ⟨a⟩ ha ⟨b⟩ ⟨c⟩ h

Goal state after:
case mk.mk.mk
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
a✝ : Associates M
a : M
ha : Quot.mk (⇑(Associated.setoid M)) a ≠ 0
a₁✝ : Associates M
b : M
a₂✝ : Associates M
c : M
h :
  (fun x ↦ Quot.mk (⇑(Associated.setoid M)) a * x) (Quot.mk (⇑(Associated.setoid M)) b) =
    (fun x ↦ Quot.mk (⇑(Associated.setoid M)) a * x) (Quot.mk (⇑(Associated.setoid M)) c)
⊢ Quot.mk (⇑(Associated.setoid M)) b = Quot.mk (⇑(Associated.setoid M)) c
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
⊢ p ⊔ p' = ⊤ ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v

Tactic:
rw [eq_top_iff']

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
⊢ (∀ (x : M), x ∈ p ⊔ p') ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : CompleteLattice α
⊢ (∀ (b : α), ∃ s, IsLUB s b ∧ ∀ a ∈ s, IsAtom a) ↔ ∀ (b : α), ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
isLUB_iff_sSup_eq,

Goal state after:
α : Type u_4
inst✝ : CompleteLattice α
⊢ (∀ (b : α), ∃ s, sSup s = b ∧ ∀ a ∈ s, IsAtom a) ↔ ∀ (b : α), ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : CompleteLattice α
⊢ IsCoatomistic α ↔ ∀ (b : α), ∃ s, b = sInf s ∧ ∀ a ∈ s, IsCoatom a

Tactic:
isCoatomistic_iff,

Goal state after:
α : Type u_4
inst✝ : CompleteLattice α
⊢ (∀ (b : α), ∃ s, IsGLB s b ∧ ∀ a ∈ s, IsCoatom a) ↔ ∀ (b : α), ∃ s, b = sInf s ∧ ∀ a ∈ s, IsCoatom a
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Type u_4
π : ι → Type u
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ IsAtom f ↔ ∃ i a, IsAtom a ∧ f = Function.update ⊥ i a

Tactic:
by
  simp [← bot_covBy_iff, covBy_iff_exists_right_eq]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ s i ∈ lowerBounds (upperBounds (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s}))

Tactic:
· refine fun j hj ↦ (isLUB_atoms_le (s i)).2 fun x ⟨hx₁, hx₂⟩ ↦ ?_
      exact hj ⟨Function.update ⊥ i x, ⟨⟨_, x, hx₁, rfl⟩, by simp [update_le_iff, hx₂]⟩, by simp⟩

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ t.sup id
t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y
x : α
hxs : x ∈ s
hsupx : t.sup id ≤ x
⊢ ∃ x ∈ s, k ≤ x

Tactic:
exact ⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩

Goal state after: