mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
j : ι
v : π j
hs : j ∉ s
⊢ update (s.piecewise f g) j v j = s.piecewise (update f j v) (update g j v) j

Tactic:
simp [*]

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

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
hs : j ∈ s
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j

Tactic:
simp [*]

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

Goal state before:
pp: case neg
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
hs : j ∉ s
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j

Tactic:
simp [*]

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

Goal state before:
pp: case pos
ι : Type u_1
s : Finset ι
inst✝¹ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst✝ : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
hx : x ∈ s
⊢ s.piecewise f g x ≤ s.piecewise f' g' x

Tactic:
simp [*]

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

Goal state before:
pp: case neg
ι : Type u_1
s : Finset ι
inst✝¹ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst✝ : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
hx : x ∉ s
⊢ s.piecewise f g x ≤ s.piecewise f' g' x

Tactic:
simp [*]

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ (if h : a = a then b a h else 1) = b a ⋯

pp: case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ a → (if h : a = b_1 then b b_1 h else 1) = 1

pp: case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1

Tactic:
dif_pos rfl

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ b a ⋯ = b a ⋯

case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ a → (if h : a = b_1 then b b_1 h else 1) = 1

case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n✝ : ℕ
p : α → Prop
n m : ℕ
l₁ : List α
h₁ : l₁.length = n
l₂ : List α
h₂ : l₂.length = m
⊢ (l₁ ++ l₂).length = n + m

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → β
l : List α
h : l.length = n
⊢ (List.map f l).length = n

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
f : α → β → φ
x : List α
property✝¹ : x.length = n
y : List β
property✝ : y.length = n
⊢ (zipWith f x y).length = n

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : ℕ
l : List α
p : l.length = n
⊢ (List.drop i l).length = n - i

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : ℕ
l : List α
p : l.length = n
⊢ (List.take i l).length = min i n

Tactic:
simp [*]

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ (if h : a = a then b a h else 1) = b a ⋯

pp: case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ a → (if h : b_1 = a then b b_1 h else 1) = 1

pp: case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1

Tactic:
dif_pos rfl

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ b a ⋯ = b a ⋯

case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ a → (if h : b_1 = a then b b_1 h else 1) = 1

case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i ↦ b ↑i) univ = (image b univ).erase k

Tactic:
apply subset_antisymm

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i ↦ b ↑i) univ ⊆ (image b univ).erase k

case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ (image b univ).erase k ⊆ image (fun i ↦ b ↑i) univ
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } ≤ card { x // p x } + card { x // q x }

Tactic:
convert! Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)

Goal state after:
α : Type u_1
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x } + card { x // q x } = card ({ x // p x } ⊕ { x // q x })
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ ↑(map g (map f s)) = ↑(map (g ∘ f) s)

Tactic:
by dsimp only [Sym.map]; simp

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

Goal state before:
pp: case inl
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
j : ι
a : α j
ha : a ∈ s j
⊢ #(Function.update s j {a} j) = Function.update (fun j ↦ #(s j)) j 1 j

Tactic:
simp [*]

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

Goal state before:
pp: case inr
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
j : ι
hji : j ≠ i
⊢ #(Function.update s i {a} j) = Function.update (fun j ↦ #(s j)) i 1 j

Tactic:
simp [*]

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

Goal state before:
pp: case neg
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∉ s i
⊢ #({f ∈ piFinset s | f i = a}) = 0

Tactic:
rw [filter_piFinset_of_notMem _ _ _ h, Finset.card_empty]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
j : Fin s
⊢ ↑j < a.length

Tactic:
by simp [hlen]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := mem_filter.mp ha
⊢ (List.ofFn fun j ↦ a.get ⟨↑j, ⋯⟩).length = a.length

Tactic:
by simp [hlen]

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

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v).insertIdx j.succ a).eraseIdx ↑⟨i, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j.succ, hj⟩.pred ⋯)) a

Tactic:
rw [← List.insertIdx_eraseIdx_of_ge]

Goal state after:
case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v).eraseIdx ↑⟨i, ⋯⟩).insertIdx j a =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j.succ, hj⟩.pred ⋯)) a

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, ⋯⟩ < (↑v).length

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
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : i = j
⊢ (v.set i a).get j = a

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ (v.set i a).get j = v.get j

Tactic:
simp [*]

Goal state after:
case neg
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ (v.set i a).get j = v.get j
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
x✝² : α
x✝¹ x✝ : Part α
ho : x✝¹.Dom
h✝¹ : x✝¹.get ho = x✝²
hp : x✝.Dom
h✝ : x✝.get hp = x✝²
⊢ ∀ (h₁ : x✝¹.Dom) (h₂ : x✝.Dom), x✝¹.get h₁ = x✝.get h₂

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ y ≤ x

Tactic:
intro b'

Goal state after:
case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
⊢ b' ∈ y → b' ∈ x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
⊢ Set.range ⇑(pair a b hab) = {a, b}

Tactic:
by
  ext; exact Nat.or_exists_add_one.symm.trans (by aesop)

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma % mb ∈ a % b

Tactic:
simp [mod_def]; aesop

Goal state after:
Module: Mathlib.Data.Part

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

Tactic:
simp [mod_def]; aesop

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

Goal state before:
pp: a : Cardinal.{u}
⊢ lift.{v, u} (succ a) = succ (lift.{v, u} a)

Tactic:
apply (succ_le_of_lt <| lift_lt.2 <| lt_succ a).antisymm'

Goal state after:
a : Cardinal.{u}
⊢ lift.{v, u} (succ a) ≤ succ (lift.{v, u} a)
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x : (i : ι) → β i
hx : x ∈ insert f s
y : (i : ι) → β i
hy : y ∈ insert f s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
rcases hx with hx | hx

Goal state after:
case inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

case inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
subst y
              exact fun e => (hf i x hx e).elim

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

Goal state before:
pp: case zero
⊢ lift.{u, v} ↑0 = ↑0

Tactic:
simp [*]

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

Goal state before:
pp: case succ
n✝ : ℕ
a✝ : lift.{u, v} ↑n✝ = ↑n✝
⊢ lift.{u, v} ↑(n✝ + 1) = ↑(n✝ + 1)

Tactic:
simp [*]

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

Goal state before:
pp: a : Cardinal.{u}
b : Cardinal.{v}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ toNat (lift.{v, u} a + lift.{u, v} b) = toNat a + toNat b

Tactic:
simp [*]

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

Goal state before:
pp: case succ
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a * a ^ n)

Tactic:
exact (ra.smul_iff (a ^ n)).mpr hn

Goal state after:
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}
⊢ (lift.{u, v} (f none) * prod fun i ↦ lift.{v, v} (f (some i))) = lift.{u, v} (f none) * prod fun a ↦ f (some a)

Tactic:
simp only [lift_id]

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

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

Tactic:
bddAbove_iff_small

Goal state after:
f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ Small.{max u v, (max u v) + 1} ↑(f '' s)
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : f.toNatLinearMap = g.toNatLinearMap
x : M
⊢ f x = g x

Tactic:
exact LinearMap.congr_fun h x

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

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : f.toIntLinearMap = g.toIntLinearMap
x : M
⊢ f x = g x

Tactic:
exact LinearMap.congr_fun h x

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
hr : r ≠ 0
hm : m ≠ 0
⊢ r • m ≠ 0

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
hm : m ≠ 0
⊢ r • m = 0 ↔ r = 0

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
hm : m ≠ 0
⊢ r • m ≠ 0 ↔ r ≠ 0

Tactic:
simp [*]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M × N
⊢ 0 • x✝ = 0

Tactic:
ext <;> exact zero_smul ..

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst✝⁴ : Zero R
inst✝³ : Zero M
inst✝² : Zero N
inst✝¹ : SMulWithZero R M
inst✝ : SMulWithZero R N
x✝ : M × N
⊢ 0 • x✝ = 0

Tactic:
ext <;> exact zero_smul ..

Goal state after:
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 α
⊢ Function.RightInverse
    (fun _insts ↦
      have this := ⋯;
      prodOfSMulCommClass M N α)
    fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩

Tactic:
by
    rintro ⟨_, x, _⟩
    dsimp only; congr 1
    · ext m a; (conv_rhs => rw [← one_smul N a]); rfl
    congr 1
    · funext i; congr; ext m a; clear i; (conv_rhs => rw [← one_smul N a]); rfl
    · ext n a; (conv_rhs => rw [← one_smul M (SMul.smul n a)]); rfl
    · exact proof_irrel_heq ..

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 : Bijective ⇑f'
n : ℕ
⊢ Bijective ⇑(f' ^ (n + 1))

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

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

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 R M
inst✝³ : Module S M
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R M
p q : Submodule R M
inst✝ : Subsingleton R
⊢ Unique (Submodule R M)

Tactic:
haveI := Module.subsingleton R M; infer_instance

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✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
f : F
a b : α
⊢ sSup (⇑f '' {a, b}) = f a ⊔ f b

Tactic:
simp only [Set.image_pair, sSup_insert, sSup_singleton]

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 α β
e : α ≃ β
a✝ b✝ : Set α
h :
  { toFun := fun s ↦ ⇑e '' s, invFun := fun s ↦ ⇑e.symm '' s, left_inv := ⋯, right_inv := ⋯ } a✝ ⊆
    { toFun := fun s ↦ ⇑e '' s, invFun := fun s ↦ ⇑e.symm '' s, left_inv := ⋯, right_inv := ⋯ } b✝
⊢ a✝ ⊆ b✝

Tactic:
simpa using @monotone_image _ _ e.symm _ _ h

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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
⊢ (↑0).1 = ↑0

Tactic:
simp [*]

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

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n✝ : ℕ
a✝ : (↑n✝).1 = ↑n✝
⊢ (↑(n✝ + 1)).1 = ↑(n✝ + 1)

Tactic:
simp [*]

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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
⊢ (↑0).2 = ↑0

Tactic:
simp [*]

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

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n✝ : ℕ
a✝ : (↑n✝).2 = ↑n✝
⊢ (↑(n✝ + 1)).2 = ↑(n✝ + 1)

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup N
x : M × N
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (MulHom.snd M N) s

Tactic:
simp [mem_prod, MulHom.coe_snd]

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
hbdiv : p ∣ b ^ n
⊢ p ∣ a

Tactic:
obtain ⟨x, rfl⟩ := hp.dvd_of_dvd_pow hbdiv

Goal state after:
case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hpow : p ^ n.succ ∣ a ^ n.succ * (p * x) ^ n
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
⊢ p ∣ a
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
r x : M₀
hr : r ∈ nonZeroDivisorsLeft M₀
⊢ x = 0 → r * x = 0

Tactic:
by simp +contextual

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
r x : M₀
hr : r ∈ nonZeroDivisorsRight M₀
⊢ x = 0 → x * r = 0

Tactic:
by simp +contextual

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

Goal state before:
pp: case refine_1.inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
h : Prime (x * y)
hx : IsUnit x
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

pp: case refine_1.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
h : Prime (x * y)
hy : IsUnit y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
· exact Or.inr ⟨hx, (associated_unit_mul_left y x hx).prime h⟩

Goal state after:
case refine_1.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
h : Prime (x * y)
hy : IsUnit y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.range = ⊥ ↔ f = 0

Tactic:
by
  rw [← range_le_bot_iff, le_bot_iff]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : SMulZeroClass α β
s : Set α
t : Set β
a x✝ : α
⊢ {0} = 0

Tactic:
singleton_zero

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : SMulZeroClass α β
s : Set α
t : Set β
a x✝ : α
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : GroupWithZero α
⊢ (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : GroupWithZero α
⊢ (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

Tactic:
simp [*]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
⊢ (inclusion h).range = comap q.subtype p

Tactic:
← map_top,

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
⊢ map (inclusion h) ⊤ = comap q.subtype p
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: R : Type u_4
G : Type u_5
M : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Group G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
S : Submodule R M
x✝ : G
⊢ x✝ ∈ stabilizer G S ↔ x✝ ∈ stabilizer G ↑S

Tactic:
mem_stabilizer_iff,

Goal state after:
R : Type u_4
G : Type u_5
M : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Group G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
S : Submodule R M
x✝ : G
⊢ x✝ • S = S ↔ x✝ ∈ stabilizer G ↑S