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

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -pure x >>= f >>= g = -pure x >>= fun x ↦ f x >>= g

Tactic:
by iterate 3 rw [neg_bind] <;> try rw [ih]

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

Goal state before:
pp: case right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆

Tactic:
· rintro _ ⟨p, hp, rfl⟩ _ ⟨q, hq, rfl⟩
    rw [← map_commutatorElement]
    exact mem_map_of_mem _ (commutator_mem_commutator hp hq)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
⊢ _root_.commutator G ≤ N

Tactic:
by
  -- It is enough to prove that Q = G ⧸ N is commutative
  apply quotient_commutative_iff_commutator_le.mp
  -- Q is a quotient of H
  let φ : H →ₙ* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
  -- It is enough to prove that φ is surjective
  apply Function.Surjective.mul_comm (f := φ) _ hH
  -- We have to prove that `MonoidHom.range φ = ⊤`
  have : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤ := by
    rw [← MonoidHom.range_eq_map, MonoidHom.range_eq_top]
    exact QuotientGroup.mk'_surjective N
  rw [MulHom.coe_coe, ← MonoidHom.range_eq_top, MonoidHom.range_eq_map, ← Subgroup.map_map, ← this,
    Subgroup.map_eq_map_iff, QuotientGroup.ker_mk', sup_comm, ← hHN, ← MonoidHom.range_eq_map]
  simp

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)
x y : N
⊢ f ↑(f.sec (x * y)).2 * (x * y) * f ↑(f.sec y).2 * f ↑(f.sec x).2 =
    f ↑(f.sec y).2 * y * f ↑(f.sec (x * y)).2 * (f ↑(f.sec x).2 * x)

Tactic:
← toMonoidHom_apply

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)
x y : N
⊢ f.toMonoidHom ↑(f.sec (x * y)).2 * (x * y) * f.toMonoidHom ↑(f.sec y).2 * f.toMonoidHom ↑(f.sec x).2 =
    f.toMonoidHom ↑(f.sec y).2 * y * f.toMonoidHom ↑(f.sec (x * y)).2 * (f.toMonoidHom ↑(f.sec x).2 * x)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
g : S.LocalizationMap N
toMulHom✝ : M →ₙ* N
isLocalizationMap✝ : S.IsLocalizationMap toMulHom✝.toFun
⊢ { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ }.toMonoidHom = g.toMonoidHom →
    { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ } = g

Tactic:
congr! with eq

Goal state after:
case mk.e'_6
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
g : S.LocalizationMap N
toMulHom✝ : M →ₙ* N
isLocalizationMap✝ : S.IsLocalizationMap toMulHom✝.toFun
eq : { toMulHom := toMulHom✝, isLocalizationMap := isLocalizationMap✝ }.toMonoidHom = g.toMonoidHom
⊢ toMulHom✝ = g.toMulHom
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
⊢ Bijective ⇑f

Tactic:
refine ⟨fun g g' eq ↦ ?_, fun m ↦ ?_⟩
    · have ⟨c, eq⟩ := h.exists_of_eq eq
      exact mul_left_cancel eq
    · have ⟨x, eq⟩ := h.surj m
      use x.1 / x.2
      rw [div_eq_mul_inv, map_mul, ← eq, mul_assoc, ← map_mul, mul_inv_cancel, h.map_one, mul_one]

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
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ φ (r /ₒ s) = ↑(fS s)⁻¹ * φ (r /ₒ 1)

Tactic:
← one_mul (φ (r /ₒ s)),

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ 1 * φ (r /ₒ s) = ↑(fS s)⁻¹ * φ (r /ₒ 1)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ ↑(fS s)⁻¹ * (φ (numeratorHom ↑s) * φ (r /ₒ s)) = ↑(fS s)⁻¹ * φ (r /ₒ 1)

Tactic:
← φ.map_mul,

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ ↑(fS s)⁻¹ * φ (numeratorHom ↑s * (r /ₒ s)) = ↑(fS s)⁻¹ * φ (r /ₒ 1)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : MonoidWithZero α
inst✝² : NoZeroDivisors α
inst✝¹ : Nontrivial α
x : WithTop α
n : ℕ
inst✝ : Preorder α
⊢ x ^ n ≠ ⊤ ↔ x ≠ ⊤ ∨ n = 0

Tactic:
pow_ne_top_iff

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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ v₁ < v₂ ∨ v₂ ≤ v₁

Tactic:
rw [Classical.or_iff_not_imp_right]

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ ¬v₂ ≤ v₁ → v₁ < v₂
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case neg
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
⊢ a < b ∧ succ a ≠ b

Tactic:
refine ⟨ha, fun hab => ?_⟩

Goal state after:
case neg
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
hab : succ a = b
⊢ False
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
⊢ prelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb (prelimitRecOn b succ isSuccPrelimit)

Tactic:
by
  have h := mt IsSuccPrelimit.isMax hb
  have H := Classical.choose_spec (not_isSuccPrelimit_iff_succ_eq.1 h)
  rw [prelimitRecOn, WellFounded.fix_eq, dif_neg h]
  have {a c : α} {ha hc} {x : ∀ a, motive a} (h : a = c) :
    cast (congr_arg (motive ∘ Order.succ) h) (succ a ha (x a)) = succ c hc (x c) := by subst h; rfl
  exact this <| (succ_eq_succ_iff_of_not_isMax H.1 hb).1 H.2

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ f (succ^[n] (EquivLike.inv f a)) = f (EquivLike.inv f b) → succ^[n] a = b

Tactic:
EquivLike.apply_inv_apply

Goal state after:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ f (succ^[n] (EquivLike.inv f a)) = b → succ^[n] a = b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ f (pred^[n] (EquivLike.inv f b)) = f (EquivLike.inv f a) → pred^[n] b = a

Tactic:
EquivLike.apply_inv_apply

Goal state after:
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
a b : Y
h : a ≤ b
n : ℕ
⊢ f (pred^[n] (EquivLike.inv f b)) = a → pred^[n] b = a
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ
⊢ ↑n < ↑n + 1

Tactic:
by
  rw [← Nat.cast_one, ← Nat.cast_add, natCast_lt_natCast]
  exact lt_add_one n

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

Goal state before:
pp: α✝ : 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 : ⟨x, hx⟩ ≤ if h : pred ↑⟨x, hx⟩ ∈ s then ⟨pred ↑⟨x, hx⟩, h⟩ else ⟨x, hx⟩
⊢ IsMin ⟨x, hx⟩

Tactic:
by
    dsimp at h
    split_ifs at h with h'
    · simp only [Subtype.mk_le_mk, Order.le_pred_iff_isMin] at h
      rintro ⟨y, _⟩ hy
      simp [h hy]
    · rintro ⟨y, hy⟩ h
      rcases h.lt_or_eq with h | h
      · simp only [Subtype.mk_lt_mk] at h
        have := h.le_pred
        absurd h'
        apply out' hy hx
        simp [this, Order.pred_le]
      · simp [h]

Goal state after:
Module: Mathlib.Data.Finset.Piecewise

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

Tactic:
by
  ext i
  by_cases h : i ∈ s <;> simp [h]

Goal state after:
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
⊢ Nonempty (α ≃ ↥t)

Tactic:
rwa [← Fintype.card_eq, Fintype.card_coe]

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:
by
  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.Sym.Basic

Goal state before:
pp: α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map id s) = ↑s

Tactic:
simp only [map, id_eq, Multiset.map_id', ← val_eq_coe]

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
⊢ decodeList 0 = some []

Tactic:
rw [decodeList]

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
⊢ ∃ a ∈ decodeList 0, encodeList a = 0

Tactic:
rw [decodeList]

Goal state after:
α : Type u_1
inst✝ : Denumerable α
⊢ ∃ a ∈ some [], encodeList a = 0
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → ↑s
hf : Surjective f
⊢ ∃ f, s = range f

Tactic:
refine ⟨(↑) ∘ f, ?_⟩

Goal state after:
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → ↑s
hf : Surjective f
⊢ s = range (Subtype.val ∘ f)
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
⊢ ∃ f, s = range f

Tactic:
by
  rcases hc.exists_surjective hs with ⟨f, hf⟩
  refine ⟨(↑) ∘ f, ?_⟩
  rw [hf.range_comp, Subtype.range_coe]

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

Goal state before:
pp: n : ℕ
F : Type u → Type u
inst✝ : Applicative F
α β : Type u
f : α → F β
x : α
⊢ ∀ (xs : Vector α n), Vector.traverse f (x ::ᵥ xs) = cons <$> f x <*> Vector.traverse f xs

Tactic:
by
  rintro ⟨xs, rfl⟩; rfl

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≺i s
⊢ (match Sum.inl f' with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)

Tactic:
rw [PrincipalSeg.trans_apply, f.eq_principalSeg]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
⊢ a.toOption.elim b f = if h : a.Dom then f (a.get h) else b

Tactic:
split_ifs with h
  · rw [h.toOption]
    rfl
  · rw [Part.toOption_eq_none_iff.2 h]
    rfl

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_4
o : Option α
h₁ : (↑o).Dom
h₂ : { Dom := o.isSome = true, get := o.get }.Dom
⊢ (↑o).get h₁ = { Dom := o.isSome = true, get := o.get }.get h₂

Tactic:
by
    cases o
    · simp at h₂
    · rfl

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
x : β
hx : ∀ (i : ℕ), c i ≤ x
⊢ ωSup (c.map f) ≤ f x

Tactic:
apply ωSup_le

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), f x ≤ f y → x ≤ y
h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f)
c : Chain β
x : β
hx : ∀ (i : ℕ), c i ≤ x
⊢ ∀ (i : ℕ), (c.map f) i ≤ f x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ ωSup
      (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ })))) ≤
    ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })

Tactic:
apply ωSup_le

Goal state after:
case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ ∀ (i : ℕ),
    (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
          (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ }))))
        i ≤
      ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ ωSup ((c.map { toFun := g, monotone' := ⋯ }).map ↑(f (c i))) ≤
    ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })

Tactic:
apply ωSup_le

Goal state after:
case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ ∀ (i_1 : ℕ),
    ((c.map { toFun := g, monotone' := ⋯ }).map ↑(f (c i))) i_1 ≤
      ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })
Module: Mathlib.SetTheory.Cardinal.Order

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

Tactic:
refine ⟨#(range e), mk_congr (Equiv.ulift.trans <| Equiv.symm ?_)⟩

Goal state after:
case refine_2
α✝ β✝ : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h : #β < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding #α
e : β ↪ α
⊢ β ≃ ↑(Set.range ⇑e)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup ((iterateChain (↑f) x h).map ↑f) ≤ ωSup (iterateChain (↑f) x h)

Tactic:
apply ωSup_le

Goal state after:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ∀ (i : ℕ), ((iterateChain (↑f) x h).map ↑f) i ≤ ωSup (iterateChain (↑f) x h)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup (iterateChain (↑f) x h) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
apply ωSup_le

Goal state after:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ∀ (i : ℕ), (iterateChain (↑f) x h) i ≤ ωSup ((iterateChain (↑f) x h).map ↑f)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a

Tactic:
apply ωSup_le

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
⊢ ∀ (i : ℕ), (iterateChain (↑f) x h) i ≤ a
Module: Mathlib.SetTheory.Cardinal.ENat

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

Tactic:
simp only [toENatAux_eq_top hy, add_top]

Goal state after:
case inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
⊢ (x + y).toENatAux = ⊤
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case e'_3
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ (range fun i ↦ lift.{u, v} (f i)) = lift.{u, v} '' range f

Tactic:
← comp_apply (f := lift),

Goal state after:
case e'_3
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ (range fun i ↦ (lift.{u, v} ∘ f) i) = lift.{u, v} '' range f
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ False

Tactic:
have := small_lift.{_, v} Cardinal.{max u v}

Goal state after:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : Small.{max u v, max (u + 1) (v + 1)} Cardinal.{max u v}
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m ^ n < ℵ₀

Tactic:
← Nat.cast_pow

Goal state after:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m ^ n) < ℵ₀
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
⊢ g ∘ₛₗ ↑e₁₂.symm = f ↔ g = f ∘ₛₗ ↑e₁₂

Tactic:
by
  constructor <;> intro H <;> ext
  · simp [← H]
  · simp [H]

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
⊢ ↑e₁₂.symm ∘ₛₗ g = f ↔ g = ↑e₁₂ ∘ₛₗ f

Tactic:
by
  constructor <;> intro H <;> ext
  · simp [← H]
  · simp [H]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Surjective ⇑f'
n : ℕ
⊢ Surjective ⇑(f' ^ (n + 1))

Tactic:
rw [iterate_succ]
    exact (iterate_surjective h n).comp h

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : SubMulAction R M
x : M
hx : x ∈ p
⊢ -x ∈ p

Tactic:
rw [← neg_one_smul R]

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : SubMulAction R M
x : M
hx : x ∈ p
⊢ -1 • x ∈ p
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
⊢ Subsingleton (Submodule R M) ↔ Subsingleton (AddSubmonoid M)

Tactic:
← subsingleton_iff_bot_eq_top,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊥ = ⊤ ↔ Subsingleton (AddSubmonoid M)
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
⊢ ⊥ = ⊤ ↔ Subsingleton (AddSubmonoid M)

Tactic:
← subsingleton_iff_bot_eq_top,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊥ = ⊤ ↔ ⊥ = ⊤
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
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₂
f : M →ₛₗ[τ₁₂] M₂
s : Set (Submodule R M)
hs : sSup s = ⊤
h : ∀ m ∈ s, f ∘ₛₗ m.subtype = 0
⊢ sSup s ≤ f.ker

Tactic:
sSup_le_iff,

Goal state after:
R : Type u_1
R₂ : Type u_2
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₂
f : M →ₛₗ[τ₁₂] M₂
s : Set (Submodule R M)
hs : sSup s = ⊤
h : ∀ m ∈ s, f ∘ₛₗ m.subtype = 0
⊢ ∀ b ∈ s, b ≤ f.ker
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
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
p' : Submodule R ↥p
x : M₂
⊢ x ∈ comap f (map p.subtype p') → x ∈ comap (codRestrict p f hf) p'

Tactic:
rintro ⟨⟨_, _⟩, h, ⟨⟩⟩; exact h

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
⊢ f.rangeS = ⊤ ↔ Function.Surjective ⇑f

Tactic:
by
  simp [← Set.range_eq_univ, SetLike.ext'_iff]

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

Goal state before:
pp: case mul.mem
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx : x✝ ∈ ↑(Subsemigroup.closure s)
hy : y✝ ∈ ↑(Subsemigroup.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
exact AddSubgroup.subset_closure (mul_mem hx hy)

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

Goal state before:
pp: case mem.mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ Subsemigroup.closure s
hy✝ : y✝ ∈ Subsemigroup.closure s
h₁ : x✝ ∈ closure s
h₂ : y✝ ∈ closure s
⊢ x✝ * y✝ ∈ closure s

Tactic:
exact mul_mem h₁ h₂

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

Goal state before:
pp: case mul.mem
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx : x✝ ∈ ↑(Submonoid.closure s)
hy : y✝ ∈ ↑(Submonoid.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
exact AddSubgroup.subset_closure (mul_mem hx hy)

Goal state after: