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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
h : b ≤ succ a
x : α
this : a < x → b ≤ x
⊢ x ∈ Ioo a b ↔ x ∈ ∅

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ y + ↑0 < x

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
⊢ x < y - ↑0

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
h : pred x < y
⊢ x ≤ y

Tactic:
exact le_of_pred_lt h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst✝² : Preorder X
inst✝¹ : Preorder Y
inst✝ : SuccOrder X
f : X ≃o Y
a✝ : Y
h : f (succ (f.symm a✝)) ≤ a✝
⊢ succ (f.symm a✝) ≤ f.symm a✝

Tactic:
simp [f.le_symm_apply, h]

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

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

Tactic:
by
  simp [piecewise, hi]

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

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

Tactic:
by
  simp [piecewise, hi]

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

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

Tactic:
rw [← WithBot.coe_one, ← natCast_one, WithBot.coe_natCast, ← Nat.cast_add, ← WithBot.coe_natCast]
  cases m
  · simp
  · 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.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i, g ↑i ⋯

Tactic:
refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_

Goal state after:
case refine_1
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s), ⟨a, ha⟩ ∈ univ

case refine_2
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ a ∈ univ, ↑a ∈ s

case refine_3
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s), ↑⟨a, ha⟩ = a

case refine_4
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ↥s) (ha : a ∈ univ), ⟨↑a, ⋯⟩ = a

case refine_5
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s), (if hi : p a then f a hi else g a hi) = g ↑⟨a, ha⟩ ⋯
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i, f ↑i ⋯

Tactic:
refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_

Goal state after:
case refine_1
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s), ⟨a, ha⟩ ∈ univ

case refine_2
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ a ∈ univ, ↑a ∈ s

case refine_3
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s), ↑⟨a, ha⟩ = a

case refine_4
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ↥s) (ha : a ∈ univ), ⟨↑a, ⋯⟩ = a

case refine_5
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s), (if hi : p a then f a hi else g a hi) = f ↑⟨a, ha⟩ ⋯
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
hi : i < n
⊢ i < v.toList.length

Tactic:
by simpa

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ ∀ x ∈ s \ {i}, f x = ?m.47 x

Tactic:
by simpa

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
x : Comp F G α
f : Comp F G (α → β)
g : Comp F G (β → γ)
⊢ (g <*> (f <*> x)).run = (Function.comp <$> g <*> f <*> x).run

Tactic:
by simp [comp_def, functor_norm]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ ↑univ.powerset = ↑univ

Tactic:
by simp [-coe_eq_univ]

Goal state after:
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.Sum.Order

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ₗ β
hab : a < b
⊢ ¬b ≤ a

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ₗ β
⊢ a ≤ b ∧ ¬b ≤ a → a < b

Tactic:
· rintro (⟨hba⟩ | ⟨hba⟩ | ⟨b, a⟩)
        · exact hba.not_gt (inl_lt_inl_iff.1 hab)
        · exact hba.not_gt (inr_lt_inr_iff.1 hab)
        · exact not_inr_lt_inl hab

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ₗ β
⊢ a ≤ b ∧ ¬b ≤ a → a < b
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ ScottContinuous _root_.id

Tactic:
simp [ScottContinuous]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
o : Part α
h : ∀ (a : α), ¬a ∈ o
⊢ ∀ (a : α), a ∈ o ↔ a ∈ none

Tactic:
by simpa

Goal state after:
Module: Mathlib.Order.BourbakiWitt

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

Tactic:
rcases le_iff_lt_or_eq.1 hzy with (hzy | rfl)
        · left; exact hy.map_le_of_mem_of_lt hz hzy
        · right; exact le_refl _

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
⊢ f (ωSup₀ c) ≤ f x

Tactic:
rw [h']; apply ωSup_le; intro i; apply f.monotone (hx i)

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Inter α
a b : α
⊢ some a ∩ some b = some (a ∩ b)

Tactic:
by
  simp [inter_def]

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
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (Subtype.val '' c)

Tactic:
rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq

Goal state after:
α : 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
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α →o β
⊢ (∃ (hf : Monotone ⇑f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := ⇑f, monotone' := hf })) ↔
    ∀ (c : Chain α), f (ωSup c) = ωSup (c.map f)

Tactic:
exact exists_prop_of_true f.monotone'

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 : β
⊢ (∀ (i j : ℕ), (c₀ i) (c₁ j) ≤ z) ↔ ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z

Tactic:
by
  constructor <;> introv h
  · apply h
  · apply le_trans _ (h (max i j))
    trans c₀ i (c₁ (max i j))
    · apply (c₀ i).monotone
      apply c₁.monotone
      apply le_max_right
    · apply c₀.monotone
      apply le_max_left

Goal state after:
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 := fun x ↦ (f x) (g x), monotone' := ⋯ }) ≤
    ωSup
      (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ }))))

Tactic:
simp only [ωSup_le_iff]
      intro i
      apply le_ωSup_of_le i
      apply (f (c i)).monotone
      apply le_ωSup_of_le i
      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 : ι
this : Quot.mk (⇑isEquivalent) (Quot.out (f i)) ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))

Tactic:
← Quot.out_eq (g i)

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

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a < lift.{v, u} ↑n ↔ a < ↑n

Tactic:
lift_lt

Goal state after:
a : Cardinal.{u}
n : ℕ
⊢ a < ↑n ↔ a < ↑n
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: n : ℕ
a : Cardinal.{u}
⊢ lift.{v, u} ↑n < lift.{v, u} a ↔ ↑n < a

Tactic:
lift_lt

Goal state after:
n : ℕ
a : Cardinal.{u}
⊢ ↑n < a ↔ ↑n < a
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ toNat a ≤ n ↔ a ≤ ↑n

Tactic:
← Cardinal.toNat_natCast.{u} n,

Goal state after:
a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ toNat a ≤ toNat ↑n ↔ a ≤ ↑n
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} x < lift.{u, v} ↑m ↔ x < ↑m

Tactic:
lift_lt

Goal state after:
x : Cardinal.{v}
m : ℕ∞
⊢ x < ↑m ↔ x < ↑m
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} ↑m < lift.{u, v} x ↔ ↑m < x

Tactic:
lift_lt

Goal state after:
x : Cardinal.{v}
m : ℕ∞
⊢ ↑m < x ↔ ↑m < x
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: c c' : Cardinal.{u}
hc' : c' < ℵ₀
⊢ toENat c ≤ toENat c' ↔ c ≤ c'

Tactic:
by
  lift c' to ℕ using hc'; simp_rw [toENat_nat, ← toENat_le_natCast]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s

Tactic:
let f : ULift.down ⁻¹' s → ULift s := fun x ↦ ULift.up (restrictPreimage s ULift.down x)

Goal state after:
α : Type u
s : Set α
f : ↑(ULift.down ⁻¹' s) → ULift.{?u.29, u} ↑s := fun x ↦ { down := s.restrictPreimage ULift.down x }
⊢ ↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ lift.{u, w} (iSup f) = ⨆ i, lift.{u, w} (f i)

Tactic:
rw [iSup, iSup, lift_sSup hf, ← range_comp]

Goal state after:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ sSup (range (lift.{u, w} ∘ f)) = sSup (range fun i ↦ lift.{u, w} (f i))
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
hb : 1 < b
⊢ a < b ^ a

Tactic:
rw [← succ_le_iff, (by norm_cast : succ (1 : Cardinal) = 2)] at hb
  exact (cantor a).trans_le (power_le_power_right hb)

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

Goal state before:
pp: α : Type u
s : Set α
⊢ #↑s ≠ 0 ↔ s.Nonempty

Tactic:
mk_ne_zero_iff,

Goal state after:
α : Type u
s : Set α
⊢ Nonempty ↑s ↔ s.Nonempty
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mpr
α : Type u
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}

Tactic:
rintro ⟨x, y, hne, h⟩

Goal state after:
case mpr
α : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : CompatibleSMul M M₂ R S
inst✝ : IsScalarTower R S M₂
f : M →ₗ[S] M₂
hf : Injective ⇑f
r : R
s : S
x✝ : M
⊢ f ((r • s) • x✝) = r • f (s • x✝)

Tactic:
map_smul,

Goal state after:
M : Type u_8
M₂ : Type u_10
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : CompatibleSMul M M₂ R S
inst✝ : IsScalarTower R S M₂
f : M →ₗ[S] M₂
hf : Injective ⇑f
r : R
s : S
x✝ : M
⊢ (r • s) • f x✝ = r • f (s • x✝)
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : CompatibleSMul M M₂ R S
inst✝ : IsScalarTower R S M₂
f : M →ₗ[S] M₂
hf : Injective ⇑f
r : R
s : S
x✝ : M
⊢ (r • s) • f x✝ = r • f (s • x✝)

Tactic:
map_smul,

Goal state after:
M : Type u_8
M₂ : Type u_10
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : CompatibleSMul M M₂ R S
inst✝ : IsScalarTower R S M₂
f : M →ₗ[S] M₂
hf : Injective ⇑f
r : R
s : S
x✝ : M
⊢ (r • s) • f x✝ = r • s • f x✝
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
X : Type u_5
inst✝⁶ : SMul M' X
Y : Type u_6
inst✝⁵ : SMul M' Y
F : Type u_8
inst✝⁴ : FunLike F X Y
inst✝³ : MulOneClass X
inst✝² : SMul X Y
inst✝¹ : IsScalarTower M' X Y
inst✝ : MulActionHomClass F X X Y
f : F
m : M'
x : X
⊢ f ((m • x) • 1) = id m • f x

Tactic:
map_smul,

Goal state after:
M' : Type u_1
X : Type u_5
inst✝⁶ : SMul M' X
Y : Type u_6
inst✝⁵ : SMul M' Y
F : Type u_8
inst✝⁴ : FunLike F X Y
inst✝³ : MulOneClass X
inst✝² : SMul X Y
inst✝¹ : IsScalarTower M' X Y
inst✝ : MulActionHomClass F X X Y
f : F
m : M'
x : X
⊢ (m • x) • f 1 = id m • f x
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
X : Type u_5
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul M' Y
F : Type u_8
inst✝² : FunLike F X Y
inst✝¹ : FaithfulSMul M' X
inst✝ : MulActionHomClass F M' X Y
f : F
hf : Function.Injective ⇑f
x✝¹ x✝ : M'
h : ∀ (a : Y), x✝¹ • a = x✝ • a
m : X
⊢ f (x✝¹ • m) = f (x✝ • m)

Tactic:
map_smul,

Goal state after:
M' : Type u_1
X : Type u_5
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul M' Y
F : Type u_8
inst✝² : FunLike F X Y
inst✝¹ : FaithfulSMul M' X
inst✝ : MulActionHomClass F M' X Y
f : F
hf : Function.Injective ⇑f
x✝¹ x✝ : M'
h : ∀ (a : Y), x✝¹ • a = x✝ • a
m : X
⊢ x✝¹ • f m = x✝ • f m
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : AddMonoid α
inst✝² : DistribMulAction M α
inst✝¹ : DistribMulAction N α
inst✝ : SMulCommClass M N α
mn : M × N
⊢ mn • 0 = 0

Tactic:
change mn.1 • mn.2 • 0 = (0 : α); rw [smul_zero, smul_zero]

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

Goal state before:
pp: R : Type u_6
A : Type u_7
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a b x✝ : A
⊢ (mulLeft R (a * b)) x✝ = (mulLeft R a ∘ₗ mulLeft R b) x✝

Tactic:
simp only [mulLeft_apply, comp_apply, mul_assoc]

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

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

Tactic:
map_smul,

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Zero R
⊢ ∀ (a : R), a • 0 = 0

Tactic:
subsingleton

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Zero R
⊢ ∀ (m : PUnit), 0 • m = 0

Tactic:
subsingleton

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (x y : R) (b : PUnit), (x * y) • b = x • y • b

Tactic:
subsingleton

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (b : PUnit), 1 • b = b

Tactic:
subsingleton

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (a : R), a • 0 = 0

Tactic:
subsingleton

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (a : R) (x y : PUnit), a • (x + y) = a • x + a • y

Tactic:
subsingleton

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (r : R), r • 1 = 1

Tactic:
subsingleton

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (r : R) (x y : PUnit), r • (x * y) = r • x * r • y

Tactic:
subsingleton

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Semiring R
⊢ ∀ (r s : R) (x : PUnit), (r + s) • x = r • x + s • x

Tactic:
subsingleton

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Semiring R
⊢ ∀ (x : PUnit), 0 • x = 0

Tactic:
subsingleton

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
x y : ↥⊥
⊢ x = y

Tactic:
subsingleton

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
ι : Sort u_4
p : ι → Submodule R M
⊢ ↑(⨅ i, p i) = ⋂ i, ↑(p i)

Tactic:
rw [iInf, coe_sInf]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
⊢ ⋂ p_1 ∈ Set.range fun i ↦ p i, ↑p_1 = ⋂ i, ↑(p i)
Module: Mathlib.Algebra.Module.Submodule.LinearMap

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
ι : Type u_9
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
r : R
c : M
⊢ p (Exists.choose ⋯) = p (σ₁₂ r • Exists.choose ⋯)

Tactic:
map_smul,

Goal state after:
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
ι : Type u_9
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
r : R
c : M
⊢ p (Exists.choose ⋯) = σ₁₂ r • p (Exists.choose ⋯)
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: case inr
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 α
x✝ : CompleteLattice β
s : Set α
hs : s.Nonempty
⊢ ⊥ = sSup {⊥}

Tactic:
sSup_singleton

Goal state after:
case inr
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 α
x✝ : CompleteLattice β
s : Set α
hs : s.Nonempty
⊢ ⊥ = ⊥
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
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
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y : ↥(Submodule.map (↑e) p)
⊢ ↑((LinearMap.codRestrict (Submodule.map (↑e) p) ((↑e).domRestrict p) ⋯).toFun ((fun y ↦ ⟨↑e.symm ↑y, ⋯⟩) y)) = ↑y

Tactic:
simp only [LinearMap.domRestrict_apply, LinearMap.codRestrict_apply, LinearMap.toFun_eq_coe,
        LinearEquiv.coe_coe, LinearEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.Data.Int.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
x✝ : ℕ
⊢ (↑↑x✝, ↑↑x✝) = ↑x✝

Tactic:
by ext <;> simp

Goal state after: