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

Goal state before:
pp: case succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : succ^[n] a ∈ s → f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
this : succ^[n] a ∈ s
⊢ f a ≤ f (succ (succ^[n] a))

Tactic:
by_cases hb' : IsMax (succ^[n] a)

Goal state after:
case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : succ^[n] a ∈ s → f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
this : succ^[n] a ∈ s
hb' : IsMax (succ^[n] a)
⊢ f a ≤ f (succ (succ^[n] a))

case neg
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : succ^[n] a ∈ s → f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
this : succ^[n] a ∈ s
hb' : ¬IsMax (succ^[n] a)
⊢ f a ≤ f (succ (succ^[n] a))
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a ≤ f (succ a)
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f a ≤ f (succ a)

Tactic:
simpa using hf

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) ≤ f a
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f (succ a) ≤ f a

Tactic:
simpa using hf

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a < f (succ a)
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f a < f (succ a)

Tactic:
simpa using hf

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) < f a
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f (succ a) < f a

Tactic:
simpa using hf

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) ≤ f a
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f (pred a) ≤ f a

Tactic:
simpa using hf

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

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

Tactic:
rw [← WithBot.coe_one, ← ENat.natCast_one, WithBot.coe_natCast, ← Nat.cast_add,
    ← WithBot.coe_natCast]

Goal state after:
n : WithBot ℕ∞
m : ℕ
⊢ n < ↑↑(m + 1) ↔ n ≤ ↑m
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a ≤ f (pred a)
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f a ≤ f (pred a)

Tactic:
simpa using hf

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) < f a
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f (pred a) < f a

Tactic:
simpa using hf

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a < f (pred a)
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f a < f (pred a)

Tactic:
simpa using hf

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

Goal state before:
pp: α : Type u_1
f : Fin 0 → α
⊢ nil.toList = List.ofFn f

Tactic:
List.ofFn_zero,

Goal state after:
α : Type u_1
f : Fin 0 → α
⊢ nil.toList = []
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
⊢ ∀ (a b : Sym α (n✝ + 1)), a = b

Tactic:
· intro s s'
      obtain ⟨b, -⟩ := exists_mem s
      rw [eq_replicate_of_subsingleton b s', eq_replicate_of_subsingleton b s]

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.get 0 = v.get (Fin.last n)

Tactic:
get_eq_get_toList,

Goal state after:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.toList.get (Fin.cast ⋯ 0) = v.get (Fin.last n)
Module: Mathlib.Logic.Small.Set

Goal state before:
pp: α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Small.{u, u1} ↑s
inst✝ : Small.{u, u2} ↑t
⊢ Small.{u, u3} ↑(Set.image2 f s t)

Tactic:
← Set.image_uncurry_prod

Goal state after:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Small.{u, u1} ↑s
inst✝ : Small.{u, u2} ↑t
⊢ Small.{u, u3} ↑(Function.uncurry f '' s ×ˢ t)
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x < y
⊢ (sumLexIicIoi x).symm y = toLex (Sum.inr ⟨y, h⟩)

Tactic:
by
  rw [symm_apply_eq, sumLexIicIoi_apply_inr]

Goal state after:
Module: Mathlib.Data.Part

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

Tactic:
bind_some

Goal state after:
α : Type u_1
β : Type u_2
o : Part α
a : α
h : a ∈ o
f : α → Part β
⊢ f a = f a
Module: Mathlib.Data.Part

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

Tactic:
simp [append_def]

Goal state after:
α : Type u_1
inst✝ : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1, a_1 ∈ a ∧ ∃ a, a ∈ b ∧ a_1 ++ a = ma ++ mb
Module: Mathlib.Data.Part

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

Tactic:
simp [append_def]

Goal state after:
α : Type u_1
inst✝ : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ (a.bind fun y ↦ map (fun x ↦ y ++ x) b).get ⋯ = a.get ⋯ ++ b.get ⋯
Module: Mathlib.Data.Part

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

Tactic:
simp [append_def]

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

Goal state before:
pp: case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
⊢ ∀ x ∈ s✝, ¬x ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s✝ → False

Tactic:
intro c₃

Goal state after:
case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
⊢ c₃ ∈ s✝ → ¬c₃ ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s✝ → False
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case mk
α : Type u
⊢ #α < 2 ^ #α

Tactic:
← mk_set

Goal state after:
case mk
α : Type u
⊢ #α < #(Set α)
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case mk
α β : Type u_1
h : #α < #β
f : α ↪ β
hf : ¬Surjective ⇑f
⊢ #α + 1 ≤ #β

Tactic:
Surjective,

Goal state after:
case mk
α β : Type u_1
h : #α < #β
f : α ↪ β
hf : ¬∀ (b : β), ∃ a, f a = b
⊢ #α + 1 ≤ #β
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: ⊢ StrictMonoOn (⇑toNat) (Iio ℵ₀)

Tactic:
simp only [← range_natCast, StrictMonoOn, forall_mem_range, toNat_natCast, Nat.cast_lt]
  exact fun _ _ ↦ id

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

Goal state before:
pp: m : ℕ∞
⊢ ℵ₀ + ↑m = ℵ₀

Tactic:
aleph0_add_ofENat

Goal state after:
m : ℕ∞
⊢ ℵ₀ = ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
h : IsSuccLimit ↑n.succ
⊢ False

Tactic:
Nat.cast_succ,

Goal state after:
n : ℕ
h : IsSuccLimit (↑n + 1)
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]
  exact mk_preimage_of_injective_lift f s h

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ x * r • 1 = r • x

Tactic:
rw [h₂, mul_one]

Goal state after:
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:
by
  rw [smul_def, smul_def, left_comm]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic

Goal state before:
pp: M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
⊢ mk.symm c₁ • a = mk.symm c₂ • a

Tactic:
rcases exists_pair_ne β with ⟨x, y, hne⟩

Goal state after:
M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
x y : β
hne : x ≠ y
⊢ mk.symm c₁ • a = mk.symm c₂ • a
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
⊢ (m • x) • f 1 = id m • f x

Tactic:
smul_assoc,

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.Algebra.Module.LinearMap.End

Goal state before:
pp: case zero
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
⊢ (g₂ ^ 0) ∘ₛₗ f = f ∘ₛₗ (g ^ 0)

Tactic:
simp [one_eq_id]

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝² x✝¹ : S
x✝ : ↥t
⊢ ↑((x✝² * x✝¹) • x✝) = ↑(x✝² • x✝¹ • x✝)

Tactic:
simp [mul_smul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_3
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : SetLike S M
inst✝ : SMulMemClass S R M
N : S
x : M
h : ∀ (a : R), a • x ∈ N
⊢ x ∈ N

Tactic:
simpa using h 1

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ x ∈ map p.subtype (comap p.subtype p') → x ∈ p ⊓ p'

Tactic:
rintro ⟨⟨_, h₁⟩, h₂, rfl⟩; exact ⟨h₁, h₂⟩

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ x✝¹ * x✝ * 0 = x✝¹ * (x✝ * 0)

Tactic:
mul_zero,

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ 0 = x✝¹ * (x✝ * 0)
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ 0 = x✝¹ * (x✝ * 0)

Tactic:
mul_zero,

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ 0 = x✝¹ * 0
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝
⊢ ↑(n + 1) * (x✝¹ * x✝) = ↑(n + 1) * x✝¹ * x✝

Tactic:
Nat.cast_succ,

Goal state after:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝
⊢ (↑n + 1) * (x✝¹ * x✝) = (↑n + 1) * x✝¹ * x✝
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * 0 = x✝¹ * (x✝ * 0)

Tactic:
mul_zero,

Goal state after:
case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ 0 = x✝¹ * (x✝ * 0)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ 0 = x✝¹ * (x✝ * 0)

Tactic:
mul_zero,

Goal state after:
case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ 0 = x✝¹ * 0
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * x✝ * ↑(n + 1) = x✝¹ * (x✝ * ↑(n + 1))

Tactic:
Nat.cast_succ,

Goal state after:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * x✝ * (↑n + 1) = x✝¹ * (x✝ * (↑n + 1))
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * x✝ * (↑n + 1) = x✝¹ * (x✝ * (↑n + 1))

Tactic:
mul_add,

Goal state after:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * x✝ * ↑n + x✝¹ * x✝ * 1 = x✝¹ * (x✝ * (↑n + 1))
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * (x✝ * ↑n) + x✝¹ * x✝ * 1 = x✝¹ * (x✝ * (↑n + 1))

Tactic:
mul_add,

Goal state after:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * (x✝ * ↑n) + x✝¹ * x✝ * 1 = x✝¹ * (x✝ * ↑n + x✝ * 1)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * (x✝ * ↑n) + x✝¹ * x✝ * 1 = x✝¹ * (x✝ * ↑n + x✝ * 1)

Tactic:
mul_add,

Goal state after:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * (x✝ * ↑n) + x✝¹ * x✝ * 1 = x✝¹ * (x✝ * ↑n) + x✝¹ * (x✝ * 1)
Module: Mathlib.Algebra.Ring.Center

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

Tactic:
mul_add,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * x✝ * -1 + x✝¹ * x✝ * -↑n = x✝¹ * (x✝ * (-1 + -↑n))
Module: Mathlib.Algebra.Ring.Center

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

Tactic:
mul_add,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * x✝ * -1 + x✝¹ * x✝ * -↑n = x✝¹ * (x✝ * -1 + x✝ * -↑n)
Module: Mathlib.Algebra.Ring.Center

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

Tactic:
mul_add,

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

Tactic:
mul_add,

Goal state after:
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝ : M
⊢ a * x✝ + b * x✝ = x✝ * a + x✝ * b
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 + b) = x✝¹ * (x✝ * (a + b))

Tactic:
mul_add,

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.Centralizer

Goal state before:
pp: M : Type u_1
S : Set M
a b : M
inst✝ : Distrib M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
c : M
hc : c ∈ S
⊢ c * (a + b) = a * c + b * c

Tactic:
mul_add,

Goal state after:
M : Type u_1
S : Set M
a b : M
inst✝ : Distrib M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
c : M
hc : c ∈ S
⊢ c * a + c * b = a * c + b * c
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : NonUnitalNonAssocRing S
f : R →ₙ+* S
⊢ ↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
by rw [coe_range, coe_top]

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Group

Goal state before:
pp: G : Type u_1
inst✝² : Group G
R : Type u_2
inst✝¹ : Semiring R
inst✝ : MulSemiringAction G R
x y : G
x✝ : R
⊢ (let __src := DistribMulAction.toAddEquiv R (x * y);
      let __src_1 := toRingHom G R (x * y);
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ })
      x✝ =
    ((let __src := DistribMulAction.toAddEquiv R x;
        let __src_1 := toRingHom G R x;
        { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ }) *
        let __src := DistribMulAction.toAddEquiv R y;
        let __src_1 := toRingHom G R y;
        { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯ })
      x✝

Tactic:
simp [mul_smul]

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
⊢ ↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
by rw [coe_range, coe_top]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ a ^ n.succ * x ^ n = p * y

Tactic:
refine mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) ?_

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = p ^ n * (p * y)
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
y z : M
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y
this : a ^ n.succ * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p ^ 2 ∣ p * (p * z)

Tactic:
rw [pow_two, ← mul_assoc]

Goal state after:
case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
y z : M
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y
this : a ^ n.succ * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p * p ∣ p * p * z
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case succ.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
obtain ⟨i, hi, hq⟩ := ih.mp hno

Goal state after:
case succ.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
hno : q ∣ p ^ n
i : ℕ
hi : i ≤ n
hq : q ~ᵤ p ^ i
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: K : Type u_4
V : Type u_8
V₂ : Type u_9
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
a : K
⊢ (a • f).range = ⨆ (_ : a ≠ 0), f.range

Tactic:
by
  simpa only [range_eq_map] using Submodule.map_smul' f _ a

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
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
hNO : N ≤ O
⊢ Submodule.map ϕ (Submodule.comap O.subtype N) = Submodule.map ϕ (Submodule.inclusion hNO).range

Tactic:
Submodule.range_inclusion

Goal state after:
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
hNO : N ≤ O
⊢ Submodule.map ϕ (Submodule.comap O.subtype N) = Submodule.map ϕ (Submodule.comap O.subtype N)
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case mp.smul₁
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x : M
t : R
n : M
mem : n ∈ {r} • N
h : ∃ m ∈ N, n = r • m
⊢ ∃ m ∈ N, t • n = r • m

Tactic:
rcases h with ⟨n, hn, rfl⟩
      exact ⟨t • n, by aesop, smul_comm _ _ _⟩

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint b c
hsup : Disjoint a (b ⊔ c)
⊢ Disjoint (a ⊔ b) c

Tactic:
rw [disjoint_comm, sup_comm]
  apply Disjoint.disjoint_sup_right_of_disjoint_sup_left h.symm
  rwa [sup_comm, disjoint_comm] at hsup

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
b : α
a : ↑(Iic b)
⊢ IsCoatom a ↔ ↑a ⋖ b

Tactic:
by
  rw [← covBy_top_iff]
  refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => c ≤ b) ?_).symm
  simpa only [OrderEmbedding.coe_subtype, Subtype.range_coe_subtype] using! Set.ordConnected_Iic

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
← span_singleton_le_iff_mem,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
m : M
⊢ R ∙ m ≤ ⨆ i, p i ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2.inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊥ ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ ⊥

Tactic:
rw [if_neg]
          intro con
          exact bot_ne_top (eq_top_iff.2 (h con))

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
s : Set α
⊢ IsCoatom s ↔ ∃ x, s = {x}ᶜ

Tactic:
rw [isCompl_compl.isCoatom_iff_isAtom, isAtom_iff]

Goal state after:
α : Type u_2
s : Set α
⊢ (∃ x, sᶜ = {x}) ↔ ∃ x, s = {x}ᶜ