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

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ ⋯.fix
      (fun a IH ↦
        if h : IsSuccPrelimit a then isSuccPrelimit a h IH
        else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
      (Order.succ b) =
    succ b hb (prelimitRecOn b succ isSuccPrelimit)

Tactic:
WellFounded.fix_eq,

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
⊢ (if h : IsSuccPrelimit (Order.succ b) then
      isSuccPrelimit (Order.succ b) h fun y x ↦
        ⋯.fix
          (fun a IH ↦
            if h : IsSuccPrelimit a then isSuccPrelimit a h IH
            else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
          y
    else
      cast ⋯
        (succ (Classical.choose ⋯) ⋯
          ((fun y x ↦
              ⋯.fix
                (fun a IH ↦
                  if h : IsSuccPrelimit a then isSuccPrelimit a h IH
                  else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
                y)
            (Classical.choose ⋯) ⋯))) =
    succ b hb (prelimitRecOn b succ isSuccPrelimit)
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
⊢ (if h : IsMin b then isMin b h
    else
      isSuccLimit b ⋯ fun x x_1 ↦
        prelimitRecOn x 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

Tactic:
dif_neg hb.not_isMin

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
⊢ (isSuccLimit b ⋯ fun x x_1 ↦
      prelimitRecOn x 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.Data.ENat.Basic

Goal state before:
pp: case coe
n a✝ : ℕ
⊢ a✝ - n = a✝ - (↑n).toNat

Tactic:
toNat_natCast

Goal state after:
case coe
n a✝ : ℕ
⊢ a✝ - n = a✝ - n
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑(a✝¹ * a✝)).toNat = a✝¹ * a✝

Tactic:
toNat_natCast

Goal state after:
case coe.coe
a✝¹ a✝ : ℕ
⊢ a✝¹ * a✝ = a✝¹ * a✝
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inr.inr.coe
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
y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hy : y ≠ 0
x : ℕ
hx : ↑x ≠ 0
⊢ map (⇑f) (↑x * y) = map ⇑f ↑x * map (⇑f) y

Tactic:
| coe x =>

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

Goal state before:
pp: case coe
m : ℕ
n : ℕ∞
⊢ n + 1 ≤ ↑m ↔ n < ↑m

Tactic:
simp [add_one_le_iff']

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:
rw [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn]

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 ← pure (ofFn fun i ↦ f i.succ)
      pure (a ::ᵥ v)) =
    pure (f 0 ::ᵥ ofFn fun i ↦ f i.succ)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a b : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
⊢ a ∈ s ∨ a ∈ replicate (↑i) b ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s

Tactic:
or_comm,

Goal state after:
α : Type u_1
n : ℕ
a b : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
⊢ a ∈ replicate (↑i) b ∨ a ∈ s ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ (↑m).card < n + 1

Tactic:
m.2,

Goal state after:
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ n < n + 1
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ n - (↑m₂.snd).card = ↑m₂.fst

Tactic:
m₂.2.2,

Goal state after:
α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ n - (n - ↑m₂.fst) = ↑m₂.fst
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ #(ULift α) ^ #((i : ι) × Quotient.out #(f i)) = #((i : ι) → Quotient.out (#α ^ #(f i)))

Tactic:
power_def

Goal state after:
case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ #((i : ι) × Quotient.out #(f i) → ULift α) = #((i : ι) → Quotient.out #(f i → α))
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝² : Std.Trichotomous s
inst✝¹ : Std.Irrefl s
inst✝ : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → f y = g y
x : β
⊢ s x (f b) ↔ s x (g b)

Tactic:
f.exists_eq_iff_rel,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝² : Std.Trichotomous s
inst✝¹ : Std.Irrefl s
inst✝ : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → f y = g y
x : β
⊢ (∃ a', f a' = x ∧ r a' b) ↔ s x (g b)
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
⊢ ∃ a, f a = b

Tactic:
apply IsWellFounded.induction s b

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
⊢ ∀ (x : β), (∀ (y : β), s y x → ∃ a, f a = y) → ∃ a, f a = x
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
⊢ Surjective ⇑f ∨ ∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b

Tactic:
apply or_iff_not_imp_right.2
  intro h b
  push Not at h
  apply IsWellFounded.induction s b
  intro x IH
  obtain ⟨y, ⟨hy, hs⟩ | ⟨hy, hs⟩⟩ := h x
  · obtain (rfl | h) := (trichotomous y x).resolve_left hs
    · exact hy
    · obtain ⟨z, rfl⟩ := hy
      exact f.mem_range_of_rel h
  · obtain ⟨z, rfl⟩ := IH y hs
    cases hy (Set.mem_range_self z)

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : IsLUB d (p₁, p₂)
⊢ IsLUB ((fun b ↦ b.1 ⊔ b.2) '' d) ((fun b ↦ b.1 ⊔ b.2) (p₁, p₂))

Tactic:
simp only [IsLUB, IsLeast, upperBounds, Prod.forall, mem_ofPred_eq, Prod.mk_le_mk] at hdp

Goal state after:
β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
⊢ IsLUB ((fun b ↦ b.1 ⊔ b.2) '' d) ((fun b ↦ b.1 ⊔ b.2) (p₁, p₂))
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ f (⨆ n, (⇑f)^[n] ⊥) = ⨆ n, (⇑f)^[n] ⊥

Tactic:
exact Function.mem_fixedPoints.mp (ωSup_iterate_mem_fixedPoint
      ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le)

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ lfp f ≤ ⨆ n, (⇑f)^[n] ⊥

pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ lfp f

Tactic:
· apply lfp_le_fixed
    exact Function.mem_fixedPoints.mp (ωSup_iterate_mem_fixedPoint
      ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le)

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ lfp f
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ (a ∩ b).get hab = a.get ⋯ ∩ b.get ⋯

Tactic:
by
  simp [inter_def]; aesop

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
left✝ : z ∈ bot x f
hz' : z ≤ y
⊢ f z ≤ f y

pp: case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
left✝ : z ∈ bot x f
hz' : f y ≤ z
⊢ f z ≤ f y

Tactic:
· rcases le_iff_lt_or_eq.1 hz' with (hz' | rfl)
      · exact le_trans (hy.map_le_of_mem_of_lt hz hz') (le_map y)
      · exact le_refl (f z)

Goal state after:
case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
left✝ : z ∈ bot x f
hz' : f y ≤ z
⊢ f z ≤ f y
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:
obtain ⟨i, ha⟩ := ha

Goal state after:
α : Type u_2
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : some a = c i
⊢ a = b
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1.inr.inl
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : sy ⊆ sz
⊢ r y z ∨ r z y

pp: case refine_1.inr.inr
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : sz ⊆ sy
⊢ r y z ∨ r z y

Tactic:
· exact (hcs₀ hsz).right (h hysy) hzsz hyz

Goal state after:
case refine_1.inr.inr
α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
cs : Set (Set α)
hcs₀ : cs ⊆ {s | c ⊆ s ∧ IsChain r s}
hcs₁ : IsChain (fun x1 x2 ↦ x1 ⊆ x2) cs
s : Set α
hs : s ∈ cs
y : α
sy : Set α
hsy : sy ∈ cs
hysy : y ∈ sy
z : α
sz : Set α
hsz : sz ∈ cs
hzsz : z ∈ sz
hyz : y ≠ z
hsseq : sy ≠ sz
h : sz ⊆ sy
⊢ r y z ∨ r z y
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 : α
ha : some a ∈ c
⊢ a ∈ x

Tactic:
obtain ⟨i, ha⟩ := 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 ∈ x
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (bot x f)

Tactic:
intro y hy z hz _

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
z : α
hz : z ∈ bot x f
a✝ : y ≠ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case refine_2
α β : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
⊢ b < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding a →
    b ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding

Tactic:
refine inductionOn₂ a b fun α β h ↦ ?_
    obtain ⟨e⟩ := h.le
    replace e := e.congr (Equiv.refl β) Equiv.ulift
    refine ⟨#(range e), mk_congr (Equiv.ulift.trans <| Equiv.symm ?_)⟩
    apply (e.codRestrict _ mem_range_self).equivOfSurjective
    rintro ⟨a, ⟨b, rfl⟩⟩
    exact ⟨b, rfl⟩

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

Goal state before:
pp: α β : Type u
⊢ Cardinal.{u} ≤i Cardinal.{max u v}

Tactic:
refine ⟨(OrderEmbedding.ofMapLEIff lift ?_).ltEmbedding, ?_⟩ <;> intro a b
  · refine inductionOn₂ a b fun _ _ ↦ ?_
    rw [← lift_umax, lift_mk_le.{v, u, u}, le_def]
  · refine inductionOn₂ a b fun α β h ↦ ?_
    obtain ⟨e⟩ := h.le
    replace e := e.congr (Equiv.refl β) Equiv.ulift
    refine ⟨#(range e), mk_congr (Equiv.ulift.trans <| Equiv.symm ?_)⟩
    apply (e.codRestrict _ mem_range_self).equivOfSurjective
    rintro ⟨a, ⟨b, rfl⟩⟩
    exact ⟨b, rfl⟩

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

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))

Tactic:
have := H i

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))

Tactic:
have := H i

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : ℕ
⊢ ↑(toNat ↑c) = ↑c

Tactic:
toNat_natCast

Goal state after:
c : ℕ
⊢ ↑c = ↑c
Module: Mathlib.SetTheory.Cardinal.ToNat

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

Tactic:
rw [← h]; simp

Goal state after:
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
P : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : Monoid N✝
inst✝³ : Monoid P
M : Type u_4
N : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid N
φ : M →* N
ψ : N →* N
inst✝ : IsId ψ
⊢ ψ.comp φ = φ

Tactic:
simp only [IsId.eq_id, MonoidHom.id_comp]

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

Goal state before:
pp: f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : BddAbove s
⊢ BddAbove (f '' s)

Tactic:
by
  rw [bddAbove_iff_small] at hs ⊢
  exact small_lift _

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

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a + b ↔ ℵ₀ ≤ a ∨ ℵ₀ ≤ b

Tactic:
simp only [← not_lt, add_lt_aleph0_iff, not_and_or]

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

Goal state before:
pp: α β : Type u
f : α ↪ β
s : Set α
⊢ #↑(⇑f '' s) = #↑s

Tactic:
simpa using mk_image_embedding_lift f s

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

Goal state before:
pp: α : Type u
ι : Type v
A : ι → Set α
s : Set ι
⊢ lift.{v, u} #↑(⋃ x, A ↑x) ≤ lift.{u, v} #↑s * ⨆ x, lift.{v, u} #↑(A ↑x)

Tactic:
apply mk_iUnion_le_lift

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

Goal state before:
pp: α : Type u
x : α
⊢ 2 ≤ #α ↔ ∃ y, y ≠ x

Tactic:
two_le_iff,

Goal state after:
α : Type u
x : α
⊢ (∃ x y, x ≠ y) ↔ ∃ y, y ≠ x
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ x * ((algebraMap R A) r * y) = (algebraMap R A) r * (x * y)

Tactic:
rw [← mul_assoc, ← commutes, mul_assoc]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S✝ : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_14
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
c : ℤ
x : M
⊢ fₗ (c • x) = c • fₗ x

Tactic:
by
    induction c with
    | zero => simp
    | succ n ih => simp [add_smul]
    | pred n ih => simp [sub_smul]

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

Goal state before:
pp: R : Type u_10
inst✝³ : Semiring R
S : Type u_11
inst✝² : Semiring S
N' : Type u_13
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
⊢ f = g

Tactic:
by
  ext x
  rw [← mul_one x, ← smul_eq_mul, f.map_smulₑ, g.map_smulₑ, h]

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)
t : R
m : M
h : m ∈ (sSup (toAddSubmonoid '' s)).carrier
⊢ t • m ∈ (sSup (toAddSubmonoid '' s)).carrier

Tactic:
simp_rw [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, sSup_eq_iSup'] at h ⊢
        induction h using AddSubmonoid.iSup_induction' with
        | mem p x hx =>
          obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p
          suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
            exact this (smul_mem p t hx)
          apply le_sSup
          rw [Subtype.range_coe_subtype]
          exact ⟨p, hp, rfl⟩
        | zero => simpa only [smul_zero] using zero_mem _
        | add _ _ _ _ mx my => revert mx my; simp_rw [smul_add]; exact add_mem

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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R M
x✝ : M₂
⊢ x✝ ∈ map (↑e) K ↔ x✝ ∈ comap (↑e.symm) K

Tactic:
mem_map_equiv,

Goal state after:
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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R M
x✝ : M₂
⊢ e.symm x✝ ∈ K ↔ x✝ ∈ comap (↑e.symm) K
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Semiring R
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module S N
inst✝ : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
c : S
fₗ : N →ₗ[S] N₂
h : pₗ ≤ comap fₗ qₗ
⊢ c • fₗ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}

Tactic:
exact le_trans h (comap_le_comap_smul qₗ fₗ c)

Goal state after:
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:
simp only [eq_top_iff, le_prod_iff, ← srange_eq_map, srange_fst, srange_snd]

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

Goal state before:
pp: case mp
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ Submonoid.map f (algebraMapSubmonoid A M) → x ∈ algebraMapSubmonoid B M

pp: case mpr
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ algebraMapSubmonoid B M → x ∈ Submonoid.map f (algebraMapSubmonoid A M)

Tactic:
· rintro ⟨a, ⟨r, hr, rfl⟩, rfl⟩
    simp only [AlgHom.commutes]
    use r

Goal state after:
case mpr
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ algebraMapSubmonoid B M → x ∈ Submonoid.map f (algebraMapSubmonoid A M)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
u : Mˣ
⊢ x * (↑u * ↑u⁻¹) = x

Tactic:
Units.mul_inv,

Goal state after:
M : Type u_1
inst✝ : Monoid M
x : M
u : Mˣ
⊢ x * 1 = x
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x ∈ ↑(nonZeroDivisorsLeft M₀) ↔ x ∈ {x | x ≠ 0}

Tactic:
simp only [SetLike.mem_coe, mem_nonZeroDivisorsLeft_iff, mul_eq_zero, Set.mem_ofPred_eq]

Goal state after:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ (∀ (y : M₀), x = 0 ∨ y = 0 → y = 0) ↔ x ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: N : Type u_2
inst✝ : CommMonoid N
u a b : N
hu : IsUnit u
⊢ u * a ~ᵤ b ↔ a ~ᵤ b

Tactic:
rw [mul_comm]
  exact associated_mul_isUnit_left_iff hu

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

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₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Bijective ⇑f
x : M₂
⊢ f ((ofBijective f h).symm x) = x

Tactic:
rw [← ofBijective_apply f (hf := h) ((ofBijective f h).symm x), apply_symm_apply]

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

Goal state before:
pp: case inr
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
s t : Set S
r✝ : S
n✝ : M
hr : r✝ ∈ t
hn : n✝ ∈ N
⊢ r✝ • n✝ ∈ s • N ⊔ t • N

Tactic:
· exact Submodule.mem_sup_right (mem_set_smul_of_mem_mem hr hn)

Goal state after:
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 : Submodule R M
s : Set M
⊢ p ⊔ span R s = span R (↑p ∪ s)

Tactic:
by rw [Submodule.span_union, p.span_eq]

Goal state after:
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 : Submodule R M
s : Set M
⊢ span R s ⊔ p = span R (s ∪ ↑p)

Tactic:
by rw [Submodule.span_union, p.span_eq]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
h : WellFounded fun x1 x2 ↦ x1 < x2
a b : α
hab : a < b
hmem : h.min (Set.Ioc a b) ⋯ ∈ Set.Ioc a b
⊢ a ⋖ h.min (Set.Ioc a b) ⋯ ∧ h.min (Set.Ioc a b) ⋯ ≤ b

Tactic:
exact ⟨⟨hmem.1,fun c hac hlt ↦ WellFounded.not_lt_min h
      (Set.Ioc a b) ⟨hac, hlt.le.trans hmem.2⟩ hlt⟩, hmem.2⟩

Goal state after: