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

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
h_base : base = Group.conjugatesOfSet base
⊢ (closure (Group.conjugatesOfSet base)).Normal

Tactic:
exact Subgroup.normalClosure_normal

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 : M
h : f x = f y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ ↑((IsUnit.liftRight (g.domRestrict S) hg) c)⁻¹ * (g ↑c * g x) = g y

Tactic:
← g.map_mul,

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 : M
h : f x = f y
c : ↥S
hc : ↑c * x = ↑c * y
⊢ ↑((IsUnit.liftRight (g.domRestrict S) hg) c)⁻¹ * g (↑c * x) = g y
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
⊢ StrictMono ⇑f ↔ ∀ (a : α), 0 < a → 0 < f a

Tactic:
by
  refine ⟨fun h a => ?_, fun h a b hl => ?_⟩
  · rw [← map_zero f]
    apply h
  · rw [← sub_add_cancel b a, map_add f]
    exact lt_add_of_pos_left _ (h _ <| sub_pos.2 hl)

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case h
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)
H : Surjective ⇑(f.lift hg)
v : P
z : N
hz : (f.lift hg) z = v
x : M × ↥S
hx : z * f ↑x.2 = f x.1
⊢ (f.lift hg) z * g ↑x.2 = g x.1

Tactic:
f.eq_mk'_iff_mul_eq.2 hx,

Goal state after:
case h
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)
H : Surjective ⇑(f.lift hg)
v : P
z : N
hz : (f.lift hg) z = v
x : M × ↥S
hx : z * f ↑x.2 = f x.1
⊢ (f.lift hg) (f.mk' x.1 x.2) * g ↑x.2 = g x.1
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mpr
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)
H : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
w✝ : M × ↥S
h✝ : z * f ↑w✝.2 = f w✝.1
⊢ z = w

Tactic:
obtain ⟨_, _⟩ := f.surj w

Goal state after:
case mpr
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)
H : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
w✝¹ : M × ↥S
h✝¹ : z * f ↑w✝¹.2 = f w✝¹.1
w✝ : M × ↥S
h✝ : w * f ↑w✝.2 = f w✝.1
⊢ z = w
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

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

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

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›
  lift a₁ to α using ha.lt_top.ne
  lift b₁ to α using hb.lt_top.ne
  obtain rfl | ha₂ := eq_or_ne a₂ ⊤
  · rw [top_mul (by simpa [bot_eq_zero] using hb.bot_lt.ne')]
    exact coe_lt_top _
  obtain rfl | hb₂ := eq_or_ne b₂ ⊤
  · rw [mul_top (by simpa [bot_eq_zero] using ha.bot_lt.ne')]
    exact coe_lt_top _
  lift a₂ to α using ha₂
  lift b₂ to α using hb₂
  norm_cast at *
  exact CanonicallyOrderedAdd.mul_lt_mul_of_lt_of_lt ha hb

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b < b
⊢ ∃ n, pred^[n] b = a

Tactic:
obtain ⟨k, hk⟩ := ih (pred b) hb (le_pred_of_lt hab)

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b < b
k : ℕ
hk : pred^[k] (pred b) = a
⊢ ∃ n, pred^[n] b = a
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: a n : ℕ
⊢ (pred ∘ pred^[n]) a = (a - n).pred

Tactic:
exact congr_arg _ (Nat.pred_iterate a n)

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
x : α
⊢ x ∈ Ioo a b ↔ x ∈ ∅

Tactic:
suffices a < x → b ≤ x by simpa

Goal state after:
case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : b ≤ succ a
x : α
⊢ a < x → b ≤ x
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + ↑n
⊢ succ^[n + 1] x = x + ↑(n + 1)

Tactic:
rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ succ a = sInf (Ioi a)

Tactic:
apply (le_sInf fun b => succ_le_of_lt).antisymm
  obtain rfl | ha := eq_or_ne a ⊤
  · rw [succ_top]
    exact le_top
  · exact sInf_le (lt_succ_iff_ne_top.2 ha)

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
h_sub_le : succ^[n] i ≤ succ^[n.succ] i
⊢ ¬IsMax (succ^[n] i)

Tactic:
refine fun h_max => hin fun j hj => ?_

Goal state after:
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
h_sub_le : succ^[n] i ≤ succ^[n.succ] i
h_max : IsMax (succ^[n] i)
j : α
hj : succ^[n + 1] i ≤ j
⊢ j ≤ succ^[n + 1] i
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
ha :
  ⊤ ≤
    match ⊤ with
    | none => ↑⊤
    | Option.some a => ↑(pred a)
⊢ IsMin ⊤

Tactic:
exact ((coe_lt_top (⊤ : α)).not_ge ha).elim

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

Goal state before:
pp: α : Type v
h : ¬Small.{w, v} α
⊢ Uncountable α

Tactic:
uncountable_iff_not_countable

Goal state after:
α : Type v
h : ¬Small.{w, v} α
⊢ ¬Countable α
Module: Mathlib.Data.ENat.Basic

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

Tactic:
rw [WithBot.coe_le_coe, natCast_add, natCast_one, ENat.add_one_le_iff (natCast_ne_top n),
      ← WithBot.coe_lt_coe, WithBot.coe_natCast]

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
p2 : {α : Type u} → α → F α
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
⊢ p1 = p2

Tactic:
by
      funext α x
      apply H1

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type u
β : Type v
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ ∀ (x : α ⊕ β), x ∈ univ.disjSum univ

Tactic:
rintro (_ | _) <;> simp

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

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

Tactic:
by rw [decodeList]; exact ⟨_, rfl, rfl⟩

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

Goal state before:
pp: β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∏ i, c i = ∏ i ∈ range n, if h : i < n then c ⟨i, h⟩ else 1

Tactic:
← Fin.prod_univ_eq_prod_range,

Goal state after:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∏ i, c i = ∏ i, if h : ↑i < n then c ⟨↑i, h⟩ else 1
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
s : Set α
h : s.Countable
⊢ ∃ f, s ⊆ range f

Tactic:
inhabit α
    exact ⟨enumerateCountable h default, subset_range_enumerate _ _⟩

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

Goal state before:
pp: n : ℕ
α : Type u
⊢ ∀ (x : Vector α n), Vector.traverse pure x = pure x

Tactic:
rintro ⟨x, rfl⟩; dsimp [Vector.traverse, cast]
  induction x with | nil => rfl | cons x xs IH => simp! [IH]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a : α
⊢ ∃ b, a < b

Tactic:
by
        obtain ⟨b | b, h⟩ := exists_gt (inl a : α ⊕ β)
        · exact ⟨b, inl_lt_inl_iff.1 h⟩
        · exact (not_inl_lt_inr h).elim

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:
simpa only [h.comp_eq] using bijOn_fixedPoints_comp g f

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : Set α
h : IsUpperSet sᶜ
⊢ IsLowerSet s

Tactic:
by
    convert! h.compl
    rw [compl_compl]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case h.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
m : α
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}, ¬r x m
gt : s (↑(collapseF f m)) b
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = b

Tactic:
exact (hm gt).elim

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
o : Part α
a : α
h : a ∈ o
f : α → Part β
⊢ o.bind f = f a

Tactic:
rw [eq_some_iff.2 h, bind_some]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ (a * b).get ⋯ = ma * mb

Tactic:
by simp only [← ha.2, ← hb.2]; rfl

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
c : Set ↑s
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
p : { x // x ∈ s }
hpc : p ∈ c
q : { x // x ∈ s }
hqc : q ∈ c
hpq : ↑p ≠ ↑q
⊢ (fun x1 x2 ↦ x1 ≤ x2) ↑p ↑q ∨ (fun x1 x2 ↦ x1 ≤ x2) ↑q ↑p

Tactic:
exact hc hpc hqc fun t => hpq (Subtype.ext_iff.1 t)

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
i j : ℕ
⊢ (c₀ i) (c₁ j) ≤ (c₀ i) (c₁ (max i j))

Tactic:
apply (c₀ i).monotone

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
i j : ℕ
⊢ c₁ j ≤ c₁ (max i j)
Module: Mathlib.SetTheory.Cardinal.ENat

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

Tactic:
wlog hle : x ≤ y

Goal state after:
case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x * y).toENatAux = x.toENatAux * y.toENatAux
hle : ¬x ≤ y
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

x y : Cardinal.{u}
hle : x ≤ y
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
x y : ℕ
hle : ↑x ≤ ↑y
⊢ (↑x * ↑y).toENatAux = (↑x).toENatAux * (↑y).toENatAux

Tactic:
simp only [← Nat.cast_mul, toENatAux_nat]

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

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

Tactic:
wlog hle : x ≤ y

Goal state after:
case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x + y).toENatAux = x.toENatAux + y.toENatAux
hle : ¬x ≤ y
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux

x y : Cardinal.{u}
hle : x ≤ y
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: case mp
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
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃ → φ₁₂.CompTriple φ₃ φ₁₂₃

Tactic:
rintro ⟨h⟩

Goal state after:
case mp
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 φ₁ = φ₁₂₃
⊢ φ₁₂.CompTriple φ₃ φ₁₂₃
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: case mpr
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
⊢ φ₁₂.CompTriple φ₃ φ₁₂₃ → φ₁.CompTriple φ₂₃ φ₁₂₃

Tactic:
rintro ⟨h⟩

Goal state after:
case mpr
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 φ₁₂ = φ₁₂₃
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ lift.{0, u} #α ≤ lift.{u, 0} #ℕ ↔ Nonempty (α ↪ ℕ)

Tactic:
lift_mk_le'

Goal state after:
α : Type u
⊢ Nonempty (α ↪ ℕ) ↔ Nonempty (α ↪ ℕ)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ #α ≤ ℵ₀ ↔ Countable α

Tactic:
by
  rw [countable_iff_nonempty_embedding, aleph0, ← lift_uzero #α, lift_mk_le']

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

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b ↔ ¬a = 0 ∧ ¬b = 0 ∧ (ℵ₀ ≤ a ∨ ¬b < ℵ₀)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)

Tactic:
not_lt

Goal state after:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b ↔ ¬a = 0 ∧ ¬b = 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ lift.{v, u} #↑(f ⁻¹' s) ≤ lift.{u, v} #↑s

Tactic:
lift_mk_le.{0}

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Nonempty (↑(f ⁻¹' s) ↪ ↑s)
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a

Tactic:
(conv_rhs => rw [← hN.one_smul a])

Goal state after:
case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (1 • a)
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_2
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ (fun x ↦ SMulCommClass M N α) = fun x ↦ SMulCommClass M N α

Tactic:
funext

Goal state after:
case e_4.e_2
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
⊢ SMulCommClass M N α = SMulCommClass M N α
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_2.e_4.e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a

Tactic:
(conv_rhs => rw [← hN.one_smul a])

Goal state after:
case e_4.e_2.e_4.e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (1 • a)
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 R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝³ : DistribSMul S M₂
inst✝² : SMulCommClass R₂ S M₂
inst✝¹ : DistribSMul 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 [Pi.smul_apply, f.map_add, smul_add]

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
m : M
k l : ℕ
hk : k ≤ l
hm : (f ^ k) m = 0
⊢ (f ^ l) m = 0

Tactic:
rw [← Nat.sub_add_cancel hk, pow_add, mul_apply, hm, map_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
⊢ (0 ∘ₗ N.subtype) m = 0

Tactic:
zero_comp,

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
⊢ 0 m = 0
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₂
τ₂₁ : R₂ →+* R
inst✝ : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₁] M
h : g ∘ₛₗ f = id
m : M
hm : f m = 0
⊢ id m = 0

Tactic:
← h,

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₂
τ₂₁ : R₂ →+* R
inst✝ : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₁] M
h : g ∘ₛₗ f = id
m : M
hm : f m = 0
⊢ (g ∘ₛₗ f) m = 0
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:
by rintro ⟨⟨_, _⟩, h, ⟨⟩⟩; exact h

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
⊢ a * ↑u = ↑u * a

Tactic:
obtain rfl | ha := eq_or_ne a 0

Goal state after:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ 0 * ↑u = ↑u * 0

case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
ha : a ≠ 0
⊢ a * ↑u = ↑u * a
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

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

Tactic:
forall_exists_index

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

Goal state before:
pp: M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ (a + b) * (x✝¹ * x✝) = (a + b) * x✝¹ * x✝

Tactic:
rw [add_mul, ha.left_assoc, hb.left_assoc, ← add_mul, ← add_mul]

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

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

Tactic:
forall_exists_index

Goal state after:
R : Type u
inst✝¹ : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : R) (x : ι), a ∈ S x → ∀ (b : R) (x : ι), b ∈ S x → a * b = b * a
Module: Mathlib.Algebra.Prime.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p : M
hp : Irreducible p
q' : M
hq : Irreducible (p * q')
⊢ p * q' ∣ p

Tactic:
IsUnit.mul_right_dvd (Or.resolve_left (of_irreducible_mul hq) hp.not_isUnit)

Goal state after:
M : Type u_1
inst✝ : Monoid M
p : M
hp : Irreducible p
q' : M
hq : Irreducible (p * q')
⊢ p ∣ p