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
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
x y : M
⊢ mk (x * y) 1 = mk (x * y) (1 * 1)

Tactic:
mul_one

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
x y : M
⊢ mk (x * y) 1 = mk (x * y) 1
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case h
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
m : M
x : G × ↥S
eq : m * f ↑x.2 = f x.1
⊢ m * 1 = m

Tactic:
mul_one

Goal state after:
case h
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
m : M
x : G × ↥S
eq : m * f ↑x.2 = f x.1
⊢ m = m
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
a : α
⊢ ↑(a * 1) = ↑a

Tactic:
mul_one

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
a : α
⊢ ↑a = ↑a
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
r✝ : X
s✝ : ↥S
⊢ oreNum r s✝ • r✝ /ₒ oreDenom r s✝ = oreNum (r * 1) s✝ • r✝ /ₒ oreDenom (r * 1) s✝

Tactic:
mul_one

Goal state after:
case c
M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
r✝ : X
s✝ : ↥S
⊢ oreNum r s✝ • r✝ /ₒ oreDenom r s✝ = oreNum r s✝ • r✝ /ₒ oreDenom r s✝
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: 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 • 1 * r₁ /ₒ (s₁ * 1)) • (r₂ /ₒ s₂) = (r₁ * r • 1 /ₒ s₁) • (r₂ /ₒ s₂)

Tactic:
mul_one

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 • 1 * r₁ /ₒ s₁) • (r₂ /ₒ s₂) = (r₁ * r • 1 /ₒ s₁) • (r₂ /ₒ s₂)
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x

Tactic:
apply hf.seq_pos_lt_seq_of_le_of_lt hn

Goal state after:
case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[0] x ≤ g^[0] x

case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)

case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
⊢ False

Tactic:
obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt

Goal state after:
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
c : α
hc : c ∈ s
hbc : b < c
hca : c ≤ a
⊢ False
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ b ≤ succ a ∧ a ≤ b ↔ b = a ∨ b = succ a

Tactic:
rw [and_comm]

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a
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, pred^[n] b = a

Tactic:
by
    refine (exists_pred_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_
    intro n
    rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]
    rintro rfl
    clear h
    induction n generalizing b with
    | zero => simp
    | succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_pred]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n] a ∈ s
⊢ f a ≤ f (succ^[n] a)

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at hb ⊢
    have : succ^[n] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
    by_cases hb' : IsMax (succ^[n] a)
    · rw [succ_eq_iff_isMax.2 hb']
      exact hn this
    · exact (hn this).trans (hf _ hb' this hb)

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

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

Tactic:
natCast_one,

Goal state after:
case coe
m : ℕ
a✝ : ℕ∞
⊢ a✝ < ↑m + 1 ↔ ↑a✝ ≤ ↑m
Module: Mathlib.Data.ENat.Basic

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

Tactic:
natCast_one,

Goal state after:
case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑n + 1 ≤ a✝ ↔ ↑n < ↑a✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ i ∈ s.attach, f i = (∏ x ∈ {x | x ∈ s}.attach, f ⟨↑x, ⋯⟩) * 1

Tactic:
mul_one

Goal state after:
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ i ∈ s.attach, f i = ∏ x ∈ {x | x ∈ s}.attach, f ⟨↑x, ⋯⟩
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ (cons a v).toList = a :: v.toList

Tactic:
by
  cases v; rfl

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
⊢ (List.scanl f b v.toList).length = n + 1

Tactic:
rw [List.length_scanl, toList_length]

Goal state after:
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
⊢ ↑m₁.fst = ↑m₂.fst

Tactic:
by
      rw [← Nat.sub_sub_self (Nat.le_of_lt_succ m₁.1.is_lt), ← m₁.2.2, val_eq_coe, h,
        ← val_eq_coe, m₂.2.2, Nat.sub_sub_self (Nat.le_of_lt_succ m₂.1.is_lt)]

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
b : α
hb : b ∈ filter (fun x ↦ a ≠ x) ↑(replicate (↑m.fst) a)
⊢ False

Tactic:
mem_filter,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
b : α
hb : b ∈ ↑(replicate (↑m.fst) a) ∧ a ≠ b
⊢ False
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ ≤ j

Tactic:
simpa [Nat.lt_succ_iff] using hij

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
inst✝ : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
⊢ Countable α

Tactic:
by
  simp_rw [← Set.countable_univ_iff, ← Set.preimage_univ (f := f), ← Set.iUnion_of_singleton,
    Set.preimage_iUnion, Set.countable_iUnion h]

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
A : Injective F
⊢ Countable ↑{t | (f t).Nonempty}

Tactic:
exact Injective.countable A

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

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

Tactic:
by
  rw [symm_apply_eq, sumLexIioIci_apply_inl]

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Basic

Goal state before:
pp: α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn f (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
by
  simpa only [h.comp_eq] using bijOn_fixedPoints_comp g f

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl.inl
α : 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
y : β
hy : y ∈ Set.range ⇑f
IH : ∀ (y_1 : β), s y_1 y → ∃ a, f a = y_1
hs : ¬s y y
⊢ ∃ a, f a = y

Tactic:
exact hy

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(collapseF f a) ∈ {b | ∀ (a' : α), r a' a → s (↑(collapseF f a')) b}

Tactic:
rw [collapseF, IsWellFounded.fix_eq]

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(have H := ⋯;
      ⟨⋯.min
          {b |
            ∀ (a_1 : α) (h : r a_1 a),
              s
                (↑((fun y x ↦
                      IsWellFounded.fix r
                        (fun a IH ↦
                          have H := ⋯;
                          ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                        y)
                    a_1 h))
                b}
          ⋯,
        ⋯⟩) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(IsWellFounded.fix r
                (fun a IH ↦
                  have H := ⋯;
                  ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩)
                a'))
            b}
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b ↑(collapseF f a)

Tactic:
rw [collapseF, IsWellFounded.fix_eq]

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(have H := ⋯;
        ⟨⋯.min
            {b |
              ∀ (a_1 : α) (h : r a_1 a),
                s
                  (↑((fun y x ↦
                        IsWellFounded.fix r
                          (fun a IH ↦
                            have H := ⋯;
                            ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                          y)
                      a_1 h))
                  b}
            ⋯,
          ⋯⟩)
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b ≤ f a → ∃ c ≤ a, f c = b

pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ (∃ c ≤ a, f c = b) → b ≤ f a

Tactic:
· intro h
    obtain ⟨c, hc⟩ := f.mem_range_of_le h
    refine ⟨c, ?_, hc⟩
    rwa [← hc, f.le_iff_le] at h

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ (∃ c ≤ a, f c = b) → b ≤ f a
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
replace hb := hb.symm

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

Goal state before:
pp: case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : a ∈ some (Classical.choose h_1)
h' : some (Classical.choose h_1) ∈ c
⊢ some a ∈ c

Tactic:
rw [← eq_some_iff] at h

Goal state after:
case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : some (Classical.choose h_1) = some a
h' : some (Classical.choose h_1) ∈ c
⊢ some a ∈ c
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 γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ ((c.map g).map (Pi.evalOrderHom b)) i
j : ℕ
hb : Part.some b = (c.map f) j
⊢ y ∈ x

Tactic:
replace hb := hb.symm

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ ((c.map g).map (Pi.evalOrderHom b)) i
j : ℕ
hb : (c.map f) j = Part.some b
⊢ y ∈ x
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
c : Cardinal.{u}
ha : c ≤ ℵ₀
⊢ toENat (lift.{v, u} c) = toENat c

Tactic:
lift c to ℕ∞ using ha; 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
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₂₃.comp φ₁ = φ₁₂₃
⊢ φ₃.comp φ₁₂ = φ₁₂₃

Tactic:
by simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]

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
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₃.comp φ₁₂ = φ₁₂₃
⊢ φ₂₃.comp φ₁ = φ₁₂₃

Tactic:
by simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]

Goal state after:
Module: Mathlib.Logic.Function.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
φ : M → N
ψ : N → N
inst✝ : IsId ψ
⊢ ψ ∘ φ = φ

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

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case inr.inl
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = 0
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂

pp: case inr.inr
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = -1
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂

Tactic:
· simp [Int.sign_eq_zero_iff_zero.mp h]

Goal state after:
case inr.inr
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = -1
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ prod f = 1

Tactic:
Cardinal.prod,

Goal state after:
case refine_2
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ #((i : PEmpty.{u + 1}) → Quotient.out (f i)) = 1
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i, f i)

Tactic:
Cardinal.prod,

Goal state after:
case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ #((i : Option α) → Quotient.out (f i)) = lift.{u, v} (∏ i, f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
h : Fintype α
f : α → Cardinal.{v}
⊢ prod f = lift.{u, v} (∏ i, f i)

Tactic:
by
  revert f
  refine Fintype.induction_empty_option ?_ ?_ ?_ α (h_fintype := h)
  · intro α β hβ e h f
    let := Fintype.ofEquiv β e.symm
    rw [← e.prod_comp f, ← h]
    exact mk_congr (e.piCongrLeft _).symm
  · intro f
    rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]
  · intro α hα h f
    rw [Cardinal.prod, mk_congr Equiv.piOptionEquivProd, mk_prod, lift_umax.{v, u}, mk_out, ←
        Cardinal.prod, lift_prod, Fintype.prod_option, lift_mul, ← h fun a => f (some a)]
    simp only [lift_id]

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

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

Tactic:
by
  rw [lift_iSup bddAbove_of_small]
  exact ciSup_le' fun i => lift_le_sum f i

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

Goal state before:
pp: α : Type u
β : Type v
⊢ #↑(range Sum.inr) = lift.{u, v} #β

Tactic:
by
  rw [← lift_id'.{v, u} #_, (Equiv.Set.rangeInr α β).lift_cardinal_eq, lift_umax.{v, u}]

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

Goal state before:
pp: b c a : Cardinal.{u}
h : c < b
⊢ a ^ c ≤ a ^< b

Tactic:
by
  refine le_ciSup (f := fun y : Iio b => a ^ (y : Cardinal)) ?_ ⟨c, h⟩
  rw [← image_eq_range]
  exact bddAbove_image.{u, u} _ bddAbove_Iio

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ a ^< 0 = 0

Tactic:
convert! Cardinal.iSup_of_empty _
  exact Subtype.isEmpty_of_false fun x => mem_Iio.not.mpr not_lt_zero

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ r • (x * 1) = r • x

Tactic:
mul_one

Goal state after:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ r • x = r • x
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : algebraMap R A = algebraMap R A
⊢ (fun x1 x2 ↦ x1 • x2) = fun x1 x2 ↦ x1 • x2

Tactic:
funext r a

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : algebraMap R A = algebraMap R A
r : R
a : A
⊢ r • a = r • a
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁶ : CommSemiring R✝
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
inst✝² : Semiring B
inst✝¹ : Algebra R✝ B
R : Type ?u.22
A : Type ?u.24
x✝¹ : CommSemiring R
x✝ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (a : R) (x y : A), a • (x + y) = a • x + a • y

Tactic:
by simp [smul_def', mul_add]

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

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
f g : X →ₑ[φ] Y
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by cases f; cases g; congr

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f : M →ₑ[id] M
m : M
⊢ f (m * 1) = f m

Tactic:
mul_one

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f : M →ₑ[id] M
m : M
⊢ f m = f m
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f * g) 1 = f (g 1 * 1)

Tactic:
mul_one

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f g : M →ₑ[id] M
⊢ (f * g) 1 = f (g 1)
Module: Mathlib.Algebra.Module.Equiv.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M
h : f 1 = g 1
x : R
⊢ f x = g x

Tactic:
by
    rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, g.map_smulₛₗ]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝⁴ : FunLike F α β
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f g : sSupHom α β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by cases f; cases g; congr

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

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * (x✝ * ↑n) + x✝¹ * x✝ = x✝¹ * (x✝ * ↑n) + x✝¹ * (x✝ * 1)

Tactic:
mul_one

Goal state after:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * (x✝ * ↑n) + x✝¹ * x✝ = x✝¹ * (x✝ * ↑n) + x✝¹ * x✝
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FaithfulSMul R A ↔ Injective ⇑(algebraMap R A)

Tactic:
by
  rw [faithfulSMul_iff_injective_smul_one, Algebra.algebraMap_eq_smul_one']

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure.toNonUnitalSubsemiring
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
simp only [Subsemiring.mem_toNonUnitalSubsemiring, subsemiringClosure_mem] at hx

Goal state after:
case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ AddSubmonoid.closure ↑M
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝¹ : NonAssocSemiring R
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → Subsemiring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
by
  simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
    Subsemigroup.coe_iSup_of_directed dir] using! Subsemigroup.isMulCommutative_iSup dir

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

Goal state before:
pp: R : Type u
inst✝¹ : NonAssocRing R
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → Subring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
by
  simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
    Subsemigroup.coe_iSup_of_directed dir] using! Subsemigroup.isMulCommutative_iSup dir

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
u : Mˣ
⊢ x * 1 = x

Tactic:
mul_one

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : a = b
⊢ a * 1 = b

Tactic:
mul_one

Goal state after:
M : Type u_1
inst✝ : Monoid M
a b : M
h : a = b
⊢ a = b