mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ Sum.inr (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach) = Sum.inr s

Tactic:
refine congr_arg Sum.inr ?_

Goal state after:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach = s
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a, a ∈ o ∧ b ∈ f a) ↔ b ∈ f (o.get h)

Tactic:
refine ⟨?_, fun hb => ⟨o.get h, Part.get_mem _, hb⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a, a ∈ o ∧ b ∈ f a) → b ∈ f (o.get h)
Module: Mathlib.Data.Part

Goal state before:
pp: case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
⊢ x >>= f ≤ y

Tactic:
intro b h'

Goal state after:
case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : b ∈ x >>= f
⊢ b ∈ y
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)
hSup : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sSup s)
⊢ p (lfp f)

Tactic:
set s := { a | a ≤ f.lfp ∧ p a }
  specialize hSup s fun a => And.right
  suffices sSup s = f.lfp from this ▸ hSup
  have h : sSup s ≤ f.lfp := sSup_le fun b => And.left
  have hmem : f (sSup s) ∈ s := ⟨f.map_le_lfp h, step _ hSup h⟩
  exact h.antisymm (f.lfp_le <| le_sSup hmem)

Goal state after:
Module: Mathlib.Data.Part

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

Tactic:
by simp [inter_def]; aesop

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

Goal state before:
pp: case union.inr.inr
α : 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 α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : c₁ ⊆ c₃
h' : SuccChain r c₁ ⊆ c₃
⊢ False

Tactic:
· exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (Classical.choose h') ∈ c
⊢ x ∈ some (Classical.choose h')

Tactic:
rw [eq_of_chain hh h]

Goal state after:
case mpr
α : Type u_2
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (Classical.choose h') ∈ c
⊢ x ∈ some x
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
⊢ Surjective h

Tactic:
rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]

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

Goal state before:
pp: α β : Type u
⊢ ∀ (a : Cardinal.{u}), a ≤ a

Tactic:
rintro ⟨α⟩
    exact ⟨Embedding.refl _⟩

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

Goal state before:
pp: c : Cardinal.{u_1}
n : ℕ
h : c ≤ ↑n
⊢ ∃ m ≤ n, c = ↑m

Tactic:
by
  lift c to ℕ using h.trans_lt natCast_lt_aleph0
  exact ⟨c, mod_cast h, rfl⟩

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

Goal state before:
pp: α : Type u
s : Set α
⊢ Subsingleton ↑s ∧ Nonempty ↑s ↔ ∃ x, s = {x}

Tactic:
Set.exists_eq_singleton_iff_nonempty_subsingleton,

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

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

pp: case neg
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
· simp only [insert_eq_of_mem h, self_le_add_right]

Goal state after:
case neg
α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) ≤ #↑s + 1
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ #↑t ≤ #↑{x | x ∈ s ∧ f x ∈ t}

Tactic:
by
  rw [image_eq_range] at h
  convert! mk_preimage_of_subset_range _ _ h using 1
  rw [mk_sep]
  rfl

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

Goal state before:
pp: a b c : Cardinal.{u}
⊢ a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c

Tactic:
rw [powerlt, ciSup_le_iff']

Goal state after:
a b c : Cardinal.{u}
⊢ (∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ x < b, a ^ x ≤ c

case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c ↦ a ^ ↑c)
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:
by
  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.GroupTheory.GroupAction.Hom

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

Tactic:
rw [← mul_one (m • x), ← smul_eq_mul, map_smul, smul_assoc, ← map_smul,
      smul_eq_mul, mul_one, id_eq]

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

Goal state before:
pp: I : Type u
f : I → Type v
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * (b✝ + c✝)) x✝ = (a✝ * b✝ + a✝ * c✝) x✝

Tactic:
exact mul_add _ _ _

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹² : Semiring R
inst✝¹¹ : Semiring R'
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁶ : Monoid S'
inst✝⁵ : DistribMulAction S' M
inst✝⁴ : SMulCommClass R S' M
inst✝³ : Monoid T'
inst✝² : DistribMulAction T' M
inst✝¹ : SMulCommClass R T' M
inst✝ : SMulCommClass S' T' M
s : S'ᵈᵐᵃ
t : T'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
m : M
⊢ (s • t • f) m = (t • s • f) m

Tactic:
by simp_rw [DomMulAct.smul_linearMap_apply, smul_comm]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ Subtype.val ⁻¹' MulAction.orbit R ↑m = MulAction.orbit R m

Tactic:
← val_image_orbit,

Goal state after:
R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ Subtype.val ⁻¹' Subtype.val '' MulAction.orbit R m = MulAction.orbit R m
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ x ∈ ↑(⨅ i, p i) ↔ ∀ (i : ι), x ∈ p i

Tactic:
coe_iInf,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ x ∈ ⋂ i, ↑(p i) ↔ ∀ (i : ι), x ∈ p i
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ ↑⟨p.toAddSubmonoid, ⋯⟩
this : p.toAddSubmonoid ≤ ⨆ q, ↑q
⊢ t • x ∈ ⨆ a, ↑a

Tactic:
exact this (smul_mem p t hx)

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

Goal state before:
pp: case mem
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ ↑⟨p.toAddSubmonoid, ⋯⟩
⊢ p.toAddSubmonoid ≤ ⨆ q, ↑q

Tactic:
apply le_sSup

Goal state after:
case mem
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ ↑⟨p.toAddSubmonoid, ⋯⟩
⊢ p.toAddSubmonoid ∈ Set.range fun q ↦ ↑q
Module: Mathlib.Algebra.Module.Equiv.Basic

Goal state before:
pp: R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_12
R₂' : Type u_13
R₁'' : Type u_15
R₂'' : Type u_16
M₁ : Type u_17
M₂ : Type u_18
M₁' : Type u_20
M₂' : Type u_21
M₁'' : Type u_23
M₂'' : Type u_24
inst✝³⁷ : Semiring R₁
inst✝³⁶ : Semiring R₂
inst✝³⁵ : CommSemiring R₁'
inst✝³⁴ : CommSemiring R₂'
inst✝³³ : CommSemiring R₁''
inst✝³² : CommSemiring R₂''
inst✝³¹ : AddCommMonoid M₁
inst✝³⁰ : AddCommMonoid M₂
inst✝²⁹ : AddCommMonoid M₁'
inst✝²⁸ : AddCommMonoid M₂'
inst✝²⁷ : AddCommMonoid M₁''
inst✝²⁶ : AddCommMonoid M₂''
inst✝²⁵ : Module R₁ M₁
inst✝²⁴ : Module R₂ M₂
inst✝²³ : Module R₁' M₁'
inst✝²² : Module R₂' M₂'
inst✝²¹ : Module R₁'' M₁''
inst✝²⁰ : Module R₂'' M₂''
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁''₂'' : R₁'' →+* R₂''
σ₂''₁'' : R₂'' →+* R₁''
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₁'₁'' : R₁' →+* R₁''
σ₂'₂'' : R₂' →+* R₂''
σ₁₁'' : R₁ →+* R₁''
σ₂₂'' : R₂ →+* R₂''
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
σ₂'₁'' : R₂' →+* R₁''
σ₁'₂'' : R₁' →+* R₂''
σ₂₁'' : R₂ →+* R₁''
σ₁₂'' : R₁ →+* R₂''
inst✝¹⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹⁷ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝¹⁶ : RingHomInvPair σ₂'₁' σ₁'₂'
inst✝¹⁵ : RingHomInvPair σ₁''₂'' σ₂''₁''
inst✝¹⁴ : RingHomInvPair σ₂''₁'' σ₁''₂''
inst✝¹³ : RingHomCompTriple σ₁₁' σ₁'₁'' σ₁₁''
inst✝¹² : RingHomCompTriple σ₂₂' σ₂'₂'' σ₂₂''
inst✝¹¹ : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst✝¹⁰ : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst✝⁹ : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst✝⁸ : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
inst✝⁷ : RingHomCompTriple σ₁₁'' σ₁''₂'' σ₁₂''
inst✝⁶ : RingHomCompTriple σ₂₁ σ₁₂'' σ₂₂''
inst✝⁵ : RingHomCompTriple σ₂₂'' σ₂''₁'' σ₂₁''
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₁'' σ₁₁''
inst✝³ : RingHomCompTriple σ₁'₁'' σ₁''₂'' σ₁'₂''
inst✝² : RingHomCompTriple σ₂'₁' σ₁'₂'' σ₂'₂''
inst✝¹ : RingHomCompTriple σ₂'₂'' σ₂''₁'' σ₂'₁''
inst✝ : RingHomCompTriple σ₁'₂' σ₂'₁'' σ₁'₁''
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
e₃ : M₁'' ≃ₛₗ[σ₁''₂''] M₂''
f : M₁ →ₛₗ[σ₁₁'] M₁'
g : M₁' →ₛₗ[σ₁'₁''] M₁''
x✝ : M₂
⊢ ((e₁.arrowCongr e₃) (g ∘ₛₗ f)) x✝ = ((e₂.arrowCongr e₃) g ∘ₛₗ (e₁.arrowCongr e₂) f) x✝

Tactic:
simp only [symm_apply_apply, arrowCongr_apply, LinearMap.comp_apply]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
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₂
p : Submodule R M
⊢ p ≤ f.ker ↔ map f p = ⊥

Tactic:
rw [ker, eq_bot_iff, map_le_iff_le_comap]

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
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

Tactic:
by
  by_cases h : a = 0 <;> simp [h, comap_smul]

Goal state after:
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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ x ∈ map (↑e) p ↔ e.symm x ∈ p

Tactic:
Submodule.mem_map

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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y ∈ p, ↑e y = x) ↔ e.symm x ∈ p
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝³ : Semiring R
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy : y' ∈ Submodule.map (↑e) p
⊢ ↑e.symm ↑⟨y', hy⟩ ∈ p

Tactic:
Submodule.mem_map

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝³ : Semiring R
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
p : Submodule R M
y' : M₂
hy✝ : y' ∈ Submodule.map (↑e) p
hy : ∃ y ∈ p, ↑e y = y'
⊢ ↑e.symm ↑⟨y', hy✝⟩ ∈ p
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, exists_prop]

Goal state after:
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:
by rw [mul_add, ha.right_assoc, hb.right_assoc, ← mul_add, ← mul_add]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
r : R
x : A
⊢ f (r • x) = (RingHom.id R) r • f x

Tactic:
by
      simp only [Algebra.smul_def, map_mul, commutes, RingHom.id_apply]

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
n : ℕ
s : Set R
⊢ closure ({↑n} ∪ s) = closure s

Tactic:
closure_union

Goal state after:
R : Type u
inst✝ : NonAssocSemiring R
n : ℕ
s : Set R
⊢ closure {↑n} ⊔ closure s = closure s
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
S : Set (Subsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, exists_prop]

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
n : ℤ
s : Set R
⊢ closure ({↑n} ∪ s) = closure s

Tactic:
closure_union

Goal state after:
R : Type u
inst✝ : NonAssocRing R
n : ℤ
s : Set R
⊢ closure {↑n} ⊔ closure s = closure s
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : Set (Subring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, exists_prop]

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

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
b c a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
u : Mˣ
h :
  ∀ (a a_1 : M),
    a₁ * a₂ * ↑u ∣ a * a_1 → ∃ x x_1, x ∣ a ∧ x_1 ∣ a_1 ∧ Associates.mk (a₁ * a₂ * ↑u) = Associates.mk (x * x_1)
dvd : a₁ * a₂ * ↑u ∣ b * c
eq : Associates.mk (a₁ * a₂ * ↑u) = Associates.mk (a₁ * a₂)
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ b ∧ a₂_1 ∣ c ∧ a₁ * a₂ * ↑u = a₁_1 * a₂_1

Tactic:
exact ⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
e : R ≃ₗ[R] A
x : A
⊢ (algebraMap R A) (e.symm (e 1 * x)) * e (e.symm 1 • 1) = x

Tactic:
by rw [map_smul, Algebra.smul_def, mul_left_comm, ← Algebra.smul_def _ (e 1),
          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, ← mul_assoc, ← Algebra.smul_def,
          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, one_mul]

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

Goal state before:
pp: case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ g • g ^ n • a ≤ a

Tactic:
exact (smul_mono_right g hn).trans h

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

Goal state before:
pp: case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ g ^ (n + 1) • a ≤ a

Tactic:
rw [pow_succ', mul_smul]
    exact (smul_mono_right g hn).trans h

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
⊢ (s ×ˢ t).sup (Prod.map f g) ≤ i ↔ (s.sup f, t.sup g) ≤ i

Tactic:
obtain ⟨a, ha⟩ := hs
    obtain ⟨b, hb⟩ := ht
    simp only [Prod.map, Finset.sup_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]
    exact ⟨fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩, by simp_all⟩

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 a (b ⊔ c)
h₂ : Disjoint b (a ⊔ c)
⊢ Disjoint (b ⊔ a) c

Tactic:
exact (h₁.mono_right le_sup_right).disjoint_sup_left_of_disjoint_sup_right h₂

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
ha : IsAtom a
hba : b ≤ a
⊢ b = ⊥ → b ≠ a

Tactic:
by rintro rfl; exact ha.ne_bot.symm

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
⊢ R ∙ 0 = ⊥

Tactic:
ext
  simp [mem_span_singleton, eq_comm]

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w x y z : M
a : R
⊢ (∃ z_1, (∃ a b, a • y + b • z = z_1) ∧ w = a • x + z_1) → ∃ b c, a • x + b • y + c • z = w

Tactic:
rintro ⟨u, ⟨b, c, rfl⟩, rfl⟩

Goal state after:
case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
a b c : R
⊢ ∃ b_1 c_1, a • x + b_1 • y + c_1 • z = a • x + (b • y + c • z)
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ t.inf' ht id ⊔ u.inf' hu id ∈ infClosure s

Tactic:
rw [inf'_sup_inf']

Goal state after:
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ((t ×ˢ u).inf' ⋯ fun i ↦ id i.1 ⊔ id i.2) ∈ infClosure s
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
⊢ k ≤ sSup (range Subtype.val)

Tactic:
rwa [Subtype.range_coe]

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ (↑↑↑f).toFun ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
algebraMap_apply R S A,

Goal state after:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ (↑↑↑f).toFun ((algebraMap S A) ((algebraMap R S) r)) = (algebraMap R B) r
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A ≃ₐ[S] B
r : R
⊢ f.toRingEquiv.toFun ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
algebraMap_apply R S A,

Goal state after:
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A ≃ₐ[S] B
r : R
⊢ f.toRingEquiv.toFun ((algebraMap S A) ((algebraMap R S) r)) = (algebraMap R B) r
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
this : map q.subtype (span S (range ⇑(inclusion h₁))) = q
⊢ q = map q.subtype ⊤

Tactic:
q.map_subtype_top

Goal state after:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
q : Submodule S M
h₁ : p ≤ restrictScalars R q
h₂ : q ≤ span S ↑p
this : map q.subtype (span S (range ⇑(inclusion h₁))) = q
⊢ q = q
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
α : Type u_8
inst✝² : Monoid α
inst✝¹ : DistribMulAction α M
inst✝ : SMulCommClass α R M
s : Set α
t : Set M
⊢ span R (⋃ i ∈ s, i • t) = span R (s • t)

Tactic:
Set.iUnion_smul_set

Goal state after: