mathlib-initiative/mathlib-tactics huggingface dataset:
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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
surj : Set.SurjOn ⇑g ↑S ↑T
hg : Surjective ⇑g
y t : P
ht : t ∈ T
⊢ ∃ a, (f.map hy k) a = k.mk' y ⟨t, ht⟩

Tactic:
obtain ⟨s, hs, rfl⟩ := surj ht

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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
surj : Set.SurjOn ⇑g ↑S ↑T
hg : Surjective ⇑g
y : P
s : M
hs : s ∈ ↑S
ht : g s ∈ T
⊢ ∃ a, (f.map hy k) a = k.mk' y ⟨g s, ht⟩
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (f ms₁.1 * f ↑ms₂.2) = f m * (n₂ * f ↑ms₂.2 * f ↑ms₁.2)
⊢ f ms₁.1 * f ↑ms₂.2 = n₂ * f ↑ms₂.2 * f ↑ms₁.2

Tactic:
eq₂

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (f ms₁.1 * f ↑ms₂.2) = f m * (f ms₂.1 * f ↑ms₁.2)
⊢ f ms₁.1 * f ↑ms₂.2 = f ms₂.1 * f ↑ms₁.2
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
x : OreLocalization S X
⊢ (r • 1) • x = r • x

Tactic:
by
  cases x
  simp only [smul_oreDiv, smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
hn : 0 < 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 < y 0

Tactic:
exact hn.false.elim

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
⊢ False

Tactic:
suffices ∀ b, f a₀ ≤ b → ∃ a, b < f a by
    obtain ⟨a, ha⟩ : ∃ a, m < f a := this m (hm' a₀)
    exact ha.not_ge (hm' a)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
⊢ ∀ (b : β), f a₀ ≤ b → ∃ a, b < f a
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
this : ¬⟨b, ⋯⟩ ⋖ a
⊢ ⟨b, ⋯⟩ < a

Tactic:
· exact hb.lt

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b

Tactic:
← Ici_inter_Iio,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ici (succ a) ∩ Iio b = Ioo a b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : ¬IsMax a
⊢ f (succ a) = succ (f a)

Tactic:
· exact ((apply_covBy_apply_iff f).2 <| covBy_succ_of_not_isMax h).succ_eq.symm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ico a (succ b) = Icc a b

Tactic:
← Ici_inter_Iio,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ici a ∩ Iio (succ b) = Icc a b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ici a ∩ Iic b = Icc a b

Tactic:
Ici_inter_Iic

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Icc a b = Icc a b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ioo a (succ b) = Ioc a b

Tactic:
← Ioi_inter_Iio,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ioi a ∩ Iio (succ b) = Ioc a b
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
⊢ x + ↑n + 1 = x + (↑n + ↑1)

Tactic:
Nat.cast_one,

Goal state after:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + ↑n
⊢ x + ↑n + 1 = x + (↑n + 1)
Module: Mathlib.Algebra.Order.SuccPred

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

Tactic:
Nat.cast_one,

Goal state after:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - ↑n
⊢ x - ↑n - 1 = x - (↑n + 1)
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : SuccAddOrder α
⊢ 1 ≤ x ↔ 0 < x

Tactic:
← succ_le_iff_of_not_isMax not_isMax_zero,

Goal state after:
α : Type u_1
x : α
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : SuccAddOrder α
⊢ 1 ≤ x ↔ succ 0 ≤ x
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : y = 1 ∧ z = 1
x_z : ↑z = x.inv
x_y : ↑x = ↑1
⊢ x = default

Tactic:
Nat.cast_one,

Goal state after:
a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : y = 1 ∧ z = 1
x_z : ↑z = x.inv
x_y : ↑x = 1
⊢ x = default
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ i ∈ s.attach, f i = ∏ i, if h : i ∈ s then f ⟨i, h⟩ else 1

Tactic:
rw [Finset.prod_dite, Finset.univ_eq_attach, Finset.prod_const_one, mul_one]

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ∀ i ∈ s, ¬p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1

Tactic:
rw [prod_eq_one]

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ∀ i ∈ s, ¬p i
⊢ ∀ x ∈ s, (if p x then a else 1) = 1
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_3
n : ℕ
s : Sym α n
⊢ map id s = s

Tactic:
by
  ext; simp only [map, id_eq, Multiset.map_id', ← val_eq_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_6
f : β → α → β
b : β
⊢ scanl f b nil = b ::ᵥ nil

Tactic:
ext; simp [scanl, get]

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

Goal state before:
pp: α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b v = b ::ᵥ f b v.head ::ᵥ nil

Tactic:
by
  rw [← cons_head_tail v]
  simp only [scanl_cons, scanl_nil, head_cons, singleton_tail]

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x ↦ ¬a = x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m

Tactic:
rw [count_add, count_filter, Sym.coe_replicate, count_replicate]

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List α
⊢ map (⇑e.symm) (map (⇑e) l) = l

Tactic:
rw [List.map_map, e.symm_comp_self, List.map_id]

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

Goal state before:
pp: α : Type u
⊢ ¬univ.Countable ↔ Uncountable α

Tactic:
by
  rw [countable_univ_iff, not_countable_iff]

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

Goal state before:
pp: α : Type u_1
x✝ : α
⊢ x✝ ∈ fixedPoints id ↔ x✝ ∈ Set.univ

Tactic:
simpa using isFixedPt_id _

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
b : β
h✝ : t (g.toRelEmbedding b) (g (f a))
h : s b (f a)
⊢ g.toRelEmbedding b ∈ Set.range (⇑g ∘ ⇑f)

Tactic:
rcases f.2 _ _ h with ⟨a', rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a a' : α
h✝ : t (g.toRelEmbedding (f.toRelEmbedding a')) (g (f a))
h : s (f.toRelEmbedding a') (f a)
⊢ g.toRelEmbedding (f.toRelEmbedding a') ∈ Set.range (⇑g ∘ ⇑f)
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : WellFoundedLT α
h : IsLowerSet s
⊢ sᶜ = univᶜ ∨ ∃ a, sᶜ = (Iio a)ᶜ

Tactic:
simpa using h.compl.eq_empty_or_Ici

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (f y)
b : β
hb : s b (f a)
⊢ Acc s b

Tactic:
obtain ⟨a', rfl⟩ := f.mem_range_of_rel hb

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a✝ : α
h : Acc r a✝
a : α
x✝ : ∀ (y : α), r y a → Acc r y
ha : ∀ (y : α), r y a → Acc s (f y)
a' : α
hb : s (f a') (f a)
⊢ Acc s (f a')
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
⊢ p (lfp f)

Tactic:
suffices sSup s = f.lfp from this ▸ hSup

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
⊢ sSup s = lfp f
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case succ
α : 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 : SuccChain r c₂ ⊆ c₃ ∨ c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
obtain ih | ih := ih
    · exact Or.inl (ih.trans subset_succChain)
    · exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsLeast {y | IsExtremePt x f y} x

pp: case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ f '' {y | IsExtremePt x f y} ⊆ {y | IsExtremePt x f y}

pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ {y | IsExtremePt x f y} → cSup c ∈ {y | IsExtremePt x f y}

Tactic:
· constructor
    · refine ⟨(bot_isAdmissible le_map).base_isLeast.1, ?_⟩
      intro y hy hyx
      exfalso
      exact lt_irrefl x (lt_of_le_of_lt ((bot_isAdmissible le_map).base_isLeast.2 hy) hyx)
    · exact fun y h ↦ (bot_isAdmissible le_map).base_isLeast.2 h.1

Goal state after:
case image_self_subset_self
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ f '' {y | IsExtremePt x f y} ⊆ {y | IsExtremePt x f y}

case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ {y | IsExtremePt x f y} → cSup c ∈ {y | IsExtremePt x f y}
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), ωScottContinuous (f i)
c : Chain α
a : β
⊢ (⨆ i, f i) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := ⨆ i, f i, monotone' := ⋯ }) ≤ a

Tactic:
simp +contextual [ωSup_le_iff, (hf _).map_ωSup, @forall_comm ι]

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
⊢ ωScottContinuous (SupSet.sSup s)

Tactic:
rw [sSup_eq_iSup]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
⊢ ωScottContinuous (⨆ a ∈ s, a)
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
⊢ CharZero Cardinal.{u_1}

Tactic:
refine ⟨fun a b h ↦ ?_⟩
  rwa [← lift_mk_fin, ← lift_mk_fin, lift_inj, Cardinal.eq, ← Fintype.card_eq,
    Fintype.card_fin, Fintype.card_fin] at h

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

Goal state before:
pp: case inr
hx : ℵ₀ ≤ ℵ₀
⊢ ℵ₀ ∈ range ofENat

Tactic:
exact mem_range_self (⊤ : ℕ∞)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : a • s • c = a • s • d
⊢ c = d

Tactic:
rw [← smul_assoc, ← smul_assoc] at cd

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : (a • s) • c = (a • s) • d
⊢ c = d
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
S : Set α
h : #↑S < #α
⊢ Sᶜ.Nonempty

Tactic:
rw [← mk_univ (α := α)] at h

Goal state after:
α : Type u
S : Set α
h : #↑S < #↑univ
⊢ Sᶜ.Nonempty
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mp
α : Type u
x a b : α
hne : a ≠ b
h : {a, b} = univ
⊢ ∃! y, y ≠ x

Tactic:
simp only [eq_univ_iff_forall, mem_insert_iff, mem_singleton_iff] at h

Goal state after:
case mp
α : Type u
x a b : α
hne : a ≠ b
h : ∀ (x : α), x = a ∨ x = b
⊢ ∃! y, y ≠ x
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : R
x y : A
⊢ x * s • y = s • (x * y)

Tactic:
rw [smul_def, smul_def, left_comm]

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

Goal state before:
pp: G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
⊢ (g / h) • (a / b) = g • a / h • b

Tactic:
have (x : G) : x • (0 : G₀) = 0 := by simpa using (smul_assoc x (0 : G₀) (0 : G₀)).symm
  by_cases hb : b = 0
  · simp [hb, this]
  have : h • b ≠ 0 := by
    refine (ne_of_apply_ne (h⁻¹ • ·) ?_)
    simpa [this]
  rw [eq_div_iff_mul_eq this, smul_mul_smul_comm]
  simp [hb]

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R₁
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M
inst✝¹ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst✝ : Nontrivial M₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective ⇑f
x : M
ne : f x ≠ 0
⊢ f ≠ 0

Tactic:
exact fun h ↦ ne congr($h x)

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

Goal state before:
pp: M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
x✝ : Y
⊢ (f.comp (f.inverse' g k₂ h₁ h₂)) x✝ = (MulActionHom.id N) x✝

Tactic:
simpa using h₂.eq _

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : M
inst✝¹ : IsCancelMulZero R
inst✝ : IsTorsionFree R M
hm : m ≠ 0
r₁ r₂ : R
hr : r₁ • m - r₂ • m = 0
⊢ r₁ = r₂

Tactic:
← sub_smul,

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : M
inst✝¹ : IsCancelMulZero R
inst✝ : IsTorsionFree R M
hm : m ≠ 0
r₁ r₂ : R
hr : (r₁ - r₂) • m = 0
⊢ r₁ = r₂
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✝⁴ : Monoid R
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulDistribMulAction R M
inst✝ : MulDistribMulAction R N
x✝² : R
x✝¹ x✝ : M × N
⊢ x✝² • (x✝¹ * x✝) = x✝² • x✝¹ * x✝² • x✝

Tactic:
by ext <;> exact smul_mul' ..

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
⊢ ⅟r • r • x ∈ p

Tactic:
exact p.smul_mem _ h

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

Goal state before:
pp: S : Type u'
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ (s • 1) • x ∈ p

Tactic:
exact p.smul_mem _ h

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M
inst✝ : Module R M₂
e : M ≃+ M₂
c : ℕ
a : M
⊢ e (c • a) = c • e a

Tactic:
by rw [map_nsmul]

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

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
s t : Submodule R M
⊢ restrictScalars S (s ⊔ t) = restrictScalars S s ⊔ restrictScalars S t

Tactic:
simpa [Set.image_insert_eq] using restrictScalars_sSup S (s := {s, t})

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

Goal state before:
pp: case H
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 : Surjective ⇑f
p q : Submodule R₂ M₂
⊢ comap f q ≤ comap f p ↔ q ≤ p

Tactic:
exact comap_le_comap_iff_of_surjective hf

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

Goal state before:
pp: case H'
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 : Surjective ⇑f
p q : Submodule R₂ M₂
⊢ comap f p ≤ comap f q ↔ p ≤ q

Tactic:
exact comap_le_comap_iff_of_surjective hf

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

Goal state before:
pp: α : Type u_1
R : Type u_2
S : Type u_3
n : ℕ
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ 2 ≠ 0

Tactic:
rw [← Nat.cast_two, Nat.cast_ne_zero]; decide

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

Goal state before:
pp: K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V₂
a : K
h : a ≠ 0
⊢ comap (a • f) p = comap f p

Tactic:
by
  ext b; simp only [Submodule.mem_comap, p.smul_mem_iff h, LinearMap.smul_apply]

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

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0⁻¹ ∈ s.centralizer

Tactic:
rw [inv_zero]

Goal state after:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0 ∈ s.centralizer
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(↑n + ↑1) * (x✝¹ * x✝) = -(↑n + ↑1) * x✝¹ * x✝

Tactic:
Nat.cast_one,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(↑n + 1) * (x✝¹ * x✝) = -(↑n + 1) * x✝¹ * x✝
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
⊢ x✝¹ * x✝ * a + x✝¹ * x✝ * b = x✝¹ * (x✝ * (a + b))

Tactic:
ha.right_assoc,

Goal state after:
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * (x✝ * a) + x✝¹ * x✝ * b = x✝¹ * (x✝ * (a + b))
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -(x✝¹ * x✝ * a) = x✝¹ * (x✝ * -a)

Tactic:
ha.right_assoc,

Goal state after:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -(x✝¹ * (x✝ * a)) = x✝¹ * (x✝ * -a)
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: case mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ y✝ : R
hx : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
induction hx, hy using AddSubgroup.closure_induction₂ with

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

Goal state before:
pp: case mul
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝ y✝ : R
hx : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
induction hx, hy using AddSubgroup.closure_induction₂ with

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
t : Subring S
h : t ≤ f.range
⊢ map f (comap f t) = t

Tactic:
simpa only [inf_of_le_left h] using Subring.map_comap_eq f t

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : DvdNotUnit p q
u : Mˣ
⊢ DvdNotUnit p (q * ↑u)

Tactic:
obtain ⟨hp, x, hx⟩ := h

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
u : Mˣ
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ q = p * x
⊢ DvdNotUnit p (q * ↑u)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h : DvdNotUnit (q * ↑u) r
h' : q * ↑u ~ᵤ q
⊢ DvdNotUnit q r

Tactic:
obtain ⟨hp, x, hx⟩ := h

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h' : q * ↑u ~ᵤ q
hp : q * ↑u ≠ 0
x : M
hx : ¬IsUnit x ∧ r = q * ↑u * x
⊢ DvdNotUnit q r