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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Function.Bijective f
⊢ Function.Bijective ⇑(map f)

Tactic:
exact ⟨map_injective hf.injective, map_surjective hf.surjective⟩

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
⊢ FG G ↔ ∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ

Tactic:
refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeGroup.lift Subtype.val, ?_⟩, ?_⟩
  · rwa [← MonoidHom.range_eq_top, ← FreeGroup.closure_eq_range]
  · rintro ⟨S, hfin : Finite S, φ, hφ⟩
    exact Group.fg_of_surjective hφ

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
⊢ 0 = 0 <*> pure p

Tactic:
zero_seq

Goal state after:
case pure.zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
⊢ 0 = 0
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
inst✝ : Subsingleton ι
f : ι → M
a : ι
this : Unique ι
⊢ ∏ x, f x = f a

Tactic:
prod_unique f,

Goal state after:
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
inst✝ : Subsingleton ι
f : ι → M
a : ι
this : Unique ι
⊢ f default = f a
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
p₁ : G
p₂ : G'
hp₁ : (p₁, p₂).1 ∈ ↑H₁.toSubmonoid
hp₂ : (p₁, p₂).2 ∈ ↑K₁.toSubmonoid
q₁ : G
q₂ : G'
hq₁ : (q₁, q₂).1 ∈ ↑H₂.toSubmonoid
hq₂ : (q₁, q₂).2 ∈ ↑K₂.toSubmonoid
⊢ ⁅(p₁, p₂), (q₁, q₂)⁆ ∈ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

Tactic:
exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩

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

Tactic:
exact mul_inv_left hg _ _ _

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R ≃+* S
x : R
⊢ f x = -1 ↔ x = -1

Tactic:
by
  rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, RingEquiv.map_eq_one_iff]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
rcases Decidable.eq_or_ne x 0 with (rfl | hx)

Goal state after:
case inl
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (0 * y) = map (⇑f) 0 * map (⇑f) y

case inr
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
WithTop.lt_top_iff_ne_top,

Goal state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : MonoidWithZero α
inst✝² : NoZeroDivisors α
inst✝¹ : Nontrivial α
x : WithTop α
n : ℕ
inst✝ : Preorder α
⊢ x ^ n ≠ ⊤ ↔ x ≠ ⊤ ∨ n = 0
Module: Mathlib.Order.Iterate

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

Tactic:
by
  simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt hg hf hn)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
h_le : n + 1 ≤ m
⊢ succ^[n.succ] a ≤ succ^[m] a

Tactic:
exact Monotone.monotone_iterate_of_le_map succ_mono (le_succ a) h_le

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ succ a ≤ succ b ↔ a ≤ b

Tactic:
rw [succ_le_iff_of_not_isMax ha, lt_succ_iff_of_not_isMax hb]

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

Goal state before:
pp: case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hm : ∀ x ∈ S, x ≤ succ m
hn : n ∈ S
hm' : succ m ∉ S
⊢ ∃ x, IsGreatest S x

Tactic:
simp_rw [Order.le_succ_iff_eq_or_le] at hm

Goal state after:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
⊢ ∃ x, IsGreatest S x
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) < f a) → StrictMonoOn f s

Tactic:
simpa [Order.pred_eq_sub_one] using strictMonoOn_of_pred_lt hs (f := f)

Goal state after:
Module: Mathlib.Logic.Small.Defs

Goal state before:
pp: S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × e✝.symm α)
e :
  (fun a ↦ ⟨e✝.toFun (Set ((α : S) × e✝.symm α)), cast ⋯ a⟩) a =
    (fun a ↦ ⟨e✝.toFun (Set ((α : S) × e✝.symm α)), cast ⋯ a⟩) b
⊢ a = b

Tactic:
dsimp at e

Goal state after:
S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × e✝.symm α)
e : ⟨e✝ (Set ((α : S) × e✝.symm α)), cast ⋯ a⟩ = ⟨e✝ (Set ((α : S) × e✝.symm α)), cast ⋯ b⟩
⊢ a = b
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: c a : ℕ∞
hc : c ≠ 0
⊢ a ≤ c * a

Tactic:
rw [mul_comm]
  exact ENat.self_le_mul_right a hc

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

Goal state before:
pp: a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
x y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
rcases Decidable.eq_or_ne x 0 with (rfl | hx)

Goal state after:
case inl
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (0 * y) = map (⇑f) 0 * map (⇑f) y

case inr
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
x y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
p q : α → Prop
h : Disjoint p q
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_congr (subtypeOrEquiv p q h)
    simp

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

Goal state before:
pp: case succ.succ.refine_2
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ ∀ (i : Fin (n + 1)),
    (scanl f (f b v.head) v.tail).get i.succ =
      f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.succ.castSucc) ((v.head ::ᵥ v.tail).get i.succ)

Tactic:
intro i'

Goal state after:
case succ.succ.refine_2
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
i' : Fin (n + 1)
⊢ (scanl f (f b v.head) v.tail).get i'.succ =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get i'.succ.castSucc) ((v.head ::ᵥ v.tail).get i'.succ)
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
⊢ n - (↑m₂.snd).card = ↑m₂.fst

Tactic:
← val_eq_coe,

Goal state after:
α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ n - (↑m₂.snd).card = ↑m₂.fst
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑⟨⟨count a ↑m, ⋯⟩, ⟨filter (fun x ↦ a ≠ x) ↑m, ⋯⟩⟩.snd +
      ↑(replicate (↑⟨⟨count a ↑m, ⋯⟩, ⟨filter (fun x ↦ a ≠ x) ↑m, ⋯⟩⟩.fst) a) =
    ↑m

Tactic:
← val_eq_coe,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ↑⟨⟨count a ↑m, ⋯⟩, ⟨filter (fun x ↦ a ≠ x) ↑m, ⋯⟩⟩.snd +
      ↑(replicate (↑⟨⟨count a ↑m, ⋯⟩, ⟨filter (fun x ↦ a ≠ x) ↑m, ⋯⟩⟩.fst) a) =
    ↑m
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
⊢ ↑⟨⟨count a ↑(fill a m.fst m.snd), ⋯⟩, ⟨filter (fun x ↦ a ≠ x) ↑(fill a m.fst m.snd), ⋯⟩⟩.snd = ↑m.snd

Tactic:
← val_eq_coe,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ↑⟨⟨count a ↑(fill a m.fst m.snd), ⋯⟩, ⟨filter (fun x ↦ a ≠ x) ↑(fill a m.fst m.snd), ⋯⟩⟩.snd = ↑m.snd
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
⊢ Std.Trichotomous (Lex r s)

Tactic:
grind [Std.Trichotomous, Lex]

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

Goal state before:
pp: ι : Type u
c : ι → Cardinal.{v}
⊢ lift.{w, max v u} (prod c) = prod fun i ↦ lift.{w, v} (c i)

Tactic:
lift c to ι → Type v using fun _ => trivial
  simp only [← mk_pi, ← mk_uLift]
  exact mk_congr (Equiv.ulift.trans <| Equiv.piCongrRight fun i => Equiv.ulift.symm)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁸ : LE α
inst✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a : α
b : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
⊢ ∀ {a b : α₁ ⊕ₗ β₁},
    (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) a ≤ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) b ↔ a ≤ b

Tactic:
simp_rw [Lex.forall]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁸ : LE α
inst✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a : α
b : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
⊢ ∀ (a a_1 : α₁ ⊕ β₁),
    (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex a) ≤
        (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex a_1) ↔
      toLex a ≤ toLex a_1
Module: Mathlib.Data.Part

Goal state before:
pp: case refl
α : Type u_1
od : Prop
o p : od → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := od, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := od, get := p }.Dom),
    { Dom := od, get := o }.get h₁ = { Dom := od, get := p }.get h₂
⊢ { Dom := od, get := o } = { Dom := od, get := p }

Tactic:
rw [show o = p from funext fun p => H2 p p]

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

Goal state before:
pp: case succ.inr
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl

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

Goal state before:
pp: n : ℕ
⊢ #(ULift.{u, 0} (Fin (n + 1))) = #(ULift.{u, 0} (Fin n)) + 1

Tactic:
← mk_option

Goal state after:
n : ℕ
⊢ #(ULift.{u, 0} (Fin (n + 1))) = #(Option (ULift.{u, 0} (Fin n)))
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case mk
α β : Type u_1
h : #α < #β
f : α ↪ β
b : β
hb : ¬∃ a, f a = b
⊢ #α + 1 ≤ #β

Tactic:
← mk_option

Goal state after:
case mk
α β : Type u_1
h : #α < #β
f : α ↪ β
b : β
hb : ¬∃ a, f a = b
⊢ #(Option α) ≤ #β
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
⊢ ↑n < ↑n.succ

Tactic:
exact Nat.cast_lt.2 (Nat.lt_succ_self _)

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

Goal state before:
pp: n : ℕ
c : Cardinal.{u_1}
⊢ ↑n + 1 ≤ c ↔ ↑n < c

Tactic:
by
  rw [← Order.succ_le_iff, succ_natCast]

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

Goal state before:
pp: α : Type u
h : #α = ℵ₀
⊢ Nonempty (Denumerable α)

Tactic:
obtain ⟨f⟩ := Quotient.exact h

Goal state after:
α : Type u
h : #α = ℵ₀
f : α ≃ ULift.{u, 0} ℕ
⊢ Nonempty (Denumerable α)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
s : Set α
a : α
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u
s : Set α
a : α
h : a ∈ s
⊢ #↑(insert a s) ≤ #↑s + 1

case neg
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) ≤ #↑s + 1
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✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommGroup N₂
inst✝⁶ : AddCommGroup N₃
inst✝⁵ : Module R₁ M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f g : M →ₛₗ[σ₁₂] N₂
x y : M
⊢ (⇑f - ⇑g) (x + y) = (⇑f - ⇑g) x + (⇑f - ⇑g) y

Tactic:
by simp only [Pi.sub_apply, map_add, add_sub_add_comm]

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
n : ℕ
hn : n ≠ 0
h : Surjective (⇑f' ∘ ⇑(f' ^ n.pred))
⊢ Surjective ⇑f'

Tactic:
exact Surjective.of_comp h

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst✝ : Invertible r
h : r • x ∈ p
⊢ x ∈ p

Tactic:
← invOf_smul_smul r x

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst✝ : Invertible r
h : r • x ∈ p
⊢ ⅟r • r • x ∈ p
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
inst✝ : RingHomSurjective σ₁₂
f g : M →ₛₗ[σ₁₂] M₂
⊢ map (f + g) p ≤ map f p ⊔ map g p

Tactic:
rintro x ⟨m, hm, rfl⟩

Goal state after:
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
inst✝ : RingHomSurjective σ₁₂
f g : M →ₛₗ[σ₁₂] M₂
m : M
hm : m ∈ ↑p
⊢ (f + g) m ∈ map f p ⊔ map g p
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₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
h : p ⋖ q
⊢ ∀ ⦃c : Submodule R₂ M₂⦄, map f p < c → ¬c < map f q

Tactic:
intro P

Goal state after:
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₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
⊢ map f p < P → ¬P < map f q
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: α : Type u_1
R : Type u_2
S : Type u_3
n✝ : ℕ
inst✝² : Semiring R
inst✝¹ : CharZero R
inst✝ : IsCancelMulZero R
n : ℕ
hn : n ≠ 0
a b : R
hab : (fun a ↦ n • a) a = (fun a ↦ n • a) b
⊢ a = b

Tactic:
by simpa [hn] using hab

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
z : R
⊢ z ∈ center R ↔ ∀ (g : R), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]

Goal state after:
R : Type u_1
inst✝ : NonUnitalSemiring R
z : R
⊢ z ∈ center R ↔ z ∈ Set.center R
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
hf : f 1 = 1
r : R
h : Invertible ((algebraMap R A) r)
⊢ (algebraMap R B) r * f ⅟((algebraMap R A) r) = 1

Tactic:
by rw [← Algebra.smul_def, ← map_smul, Algebra.smul_def, mul_invOf_self, hf]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
hx : x ∈ closure s
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
rw [mem_closure_iff] at hx

Goal state after:
case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
hx : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x y : R
hx✝ : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hy✝ : y ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
hM : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
HL2 : (List.map List.prod L).sum = x
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s
HM2 : (List.map List.prod M).sum = y
⊢ (List.map List.prod L ++ List.map List.prod M).sum = x + y

Tactic:
List.sum_append,

Goal state after:
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x y : R
hx✝ : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hy✝ : y ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
hM : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
HL2 : (List.map List.prod L).sum = x
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s
HM2 : (List.map List.prod M).sum = y
⊢ (List.map List.prod L).sum + (List.map List.prod M).sum = x + y
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
x : R
hx : x ∈ closure s
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x

Tactic:
rw [mem_closure_iff] at hx

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
x : R
hx : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝
hM : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = y✝
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1
HL2 : (List.map List.prod L).sum = x✝
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s ∨ y = -1
HM2 : (List.map List.prod M).sum = y✝
⊢ (List.map List.prod L ++ List.map List.prod M).sum = x✝ + y✝

Tactic:
List.sum_append,

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝
hM : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = y✝
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1
HL2 : (List.map List.prod L).sum = x✝
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s ∨ y = -1
HM2 : (List.map List.prod M).sum = y✝
⊢ (List.map List.prod L).sum + (List.map List.prod M).sum = x✝ + y✝
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit z
⊢ IsUnit y ∨ x ~ᵤ y

Tactic:
rw [hz]
      exact Or.inr (associated_mul_unit_left _ _ h)

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

Goal state before:
pp: case mp
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∃ x, x * Associates.mk a = 0 ∧ x ≠ 0) → ∃ x, x * a = 0 ∧ x ≠ 0

Tactic:
rintro ⟨⟨x⟩, hx₁, hx₂⟩

Goal state after:
case mp.mk
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ ∃ x, x * a = 0 ∧ x ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
⊢ DecompositionMonoid (Associates M) ↔ DecompositionMonoid M

Tactic:
_root_.decompositionMonoid_iff,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
⊢ (∀ (a : Associates M), IsPrimal a) ↔ ∀ (a : M), IsPrimal a
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : SMulZeroClass α β
s : Set α
⊢ s • 0 ⊆ 0

Tactic:
by simp [subset_def, mem_smul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
t : Set β
⊢ 0 • t ⊆ 0

Tactic:
by simp [subset_def, mem_smul]

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

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
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
⊢ ↥(map p.subtype q) → ↥q

Tactic:
by
      rintro ⟨x, hx⟩
      refine ⟨⟨x, ?_⟩, ?_⟩ <;> rcases hx with ⟨⟨_, h⟩, _, rfl⟩ <;> assumption

Goal state after: