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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
⊢ ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'

Tactic:
rw [mul_assoc, ← h₁, ← mul_assoc, h₃, mul_assoc, h₂]

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
⊢ r₃' * (r₂' * ↑⟨r₂ * ↑s', hs⟩) = r₃' * r₂' * r₂ * ↑s'
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ c • mk a b = mk (c • a) b

Tactic:
mk,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ c • (a /ₒ b) = mk (c • a) b
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ c • (a /ₒ b) = mk (c • a) b

Tactic:
mk,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ c • (a /ₒ b) = c • a /ₒ b
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z : N
⊢ f (f.sec z).1 = f ↑(f.sec z).2 * z

Tactic:
by rw [mul_comm, sec_spec]

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ rc * (↑sb * r₂) = rc * rb * ↑s₃

Tactic:
hb,

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ rc * (rb * ↑s₃) = rc * rb * ↑s₃
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * ↑s ∈ S
this : ↑(fS ⟨t * ↑s, ht⟩) = f t * ↑(fS s)
| ↑(fS ⟨t * ↑s, ht⟩)⁻¹ * (f t * (↑1 * f r))

Tactic:
← mul_inv_cancel (fS s)

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * ↑s ∈ S
this : ↑(fS ⟨t * ↑s, ht⟩) = f t * ↑(fS s)
| ↑(fS ⟨t * ↑s, ht⟩)⁻¹ * (f t * (↑(fS s * (fS s)⁻¹) * f r))
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
hb,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untopD 0 (a * 0) = untopD 0 a * untopD 0 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
hb,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ unbotD 0 (a * 0) = unbotD 0 a * unbotD 0 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ⊥ * ↑x < ↑a✝ * ↑x

Tactic:
simp_rw [bot_mul x0.ne.symm, ← coe_mul, bot_lt_coe]

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

Goal state before:
pp: case succ
α : 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₀ : α
h : ∀ (a : α), ∃ a', f a < f a'
⊢ ∀ (n : β), f a₀ ≤ n → (∃ a, n < f a) → ∃ a, succ n < f a

Tactic:
rintro b _ ⟨a, hba⟩

Goal state after:
case succ
α : 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₀ : α
h : ∀ (a : α), ∃ a', f a < f a'
b : β
hmn✝ : f a₀ ≤ b
a : α
hba : b < f a
⊢ ∃ a, succ b < f a
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 α
f : α → β
⊢ (∀ (a : α), ¬IsMin a → f a ≤ f (a - 1)) → Antitone f

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

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

Goal state before:
pp: n : ℕ∞
hn : n ≠ ⊤
⊢ ∃ m, ¬↑m ≤ n

Tactic:
exact not_forall.mp <| eq_top_iff_forall_ge.2.mt hn

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

Goal state before:
pp: case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∈ s
h : ⟨x, hx⟩ ≤ ⟨pred x, h'⟩
⊢ IsMin ⟨x, hx⟩

Tactic:
simp only [Subtype.mk_le_mk, Order.le_pred_iff_isMin] at h

Goal state after:
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∈ s
h : IsMin x
⊢ IsMin ⟨x, hx⟩
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
⊢ ↑(if h : pred ↑(ofDual a) ∈ ⇑ofDual ⁻¹' s then ⟨pred ↑(ofDual a), h⟩ else ofDual a) = succ ↑a

Tactic:
split_ifs <;> trivial

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

Goal state before:
pp: α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
⊢ (if h : pred ↑(ofDual a) ∈ ⇑ofDual ⁻¹' s then ⟨pred ↑(ofDual a), h⟩ else ofDual a) = a

Tactic:
split_ifs <;> trivial

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
⊢ F1 = F2

Tactic:
apply Functor.ext
      intros
      exact (pure_seq1 _ _).symm.trans (pure_seq2 _ _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ n < n + 1

Tactic:
Nat.lt_succ_iff

Goal state after:
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ n ≤ n
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ β
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
refine ⟨fun hab => ⟨hab.mono (fun _ _ => le_of_lt) fun _ _ => le_of_lt, ?_⟩, ?_⟩
      · rintro (⟨hba⟩ | ⟨hba⟩)
        · exact hba.not_gt (inl_lt_inl_iff.1 hab)
        · exact hba.not_gt (inr_lt_inr_iff.1 hab)
      · rintro ⟨⟨hab⟩ | ⟨hab⟩, hba⟩
        · exact LiftRel.inl (hab.lt_of_not_ge fun h => hba <| LiftRel.inl h)
        · exact LiftRel.inr (hab.lt_of_not_ge fun h => hba <| LiftRel.inr h)

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

Goal state before:
pp: α : Type u_1
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f^[n]) s

Tactic:
rw [Set.preimage_iterate_eq]

Goal state after:
α : Type u_1
f : α → α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f)^[n] s
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b < f a → ∃ a' < a, f a' = b

pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ (∃ a' < a, f a' = b) → b < f a

Tactic:
· intro h
    obtain ⟨c, hc⟩ := f.mem_range_of_rel h
    refine ⟨c, ?_, hc⟩
    rwa [← hc, f.lt_iff_lt] at h

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ (∃ a' < a, f a' = b) → b < f a
Module: Mathlib.Data.Part

Goal state before:
pp: case none
α : Type u_4
h₁ : (↑Option.none).Dom
h₂ : { Dom := Option.none.isSome = true, get := Option.none.get }.Dom
⊢ (↑Option.none).get h₁ = { Dom := Option.none.isSome = true, get := Option.none.get }.get h₂

pp: case some
α : Type u_4
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := (Option.some val✝).isSome = true, get := (Option.some val✝).get }.Dom
⊢ (↑(Option.some val✝)).get h₁ = { Dom := (Option.some val✝).isSome = true, get := (Option.some val✝).get }.get h₂

Tactic:
· simp at h₂

Goal state after:
case some
α : Type u_4
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := (Option.some val✝).isSome = true, get := (Option.some val✝).get }.Dom
⊢ (↑(Option.some val✝)).get h₁ = { Dom := (Option.some val✝).isSome = true, get := (Option.some val✝).get }.get h₂
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous (SupSet.sSup {f, g})

Tactic:
apply ωScottContinuous.sSup

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ∀ f_1 ∈ {f, g}, ωScottContinuous f_1
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
⊢ False

Tactic:
have : Inhabited (∀ i : ι, (g i).out) := by
      refine ⟨fun i => Classical.choice <| mk_ne_zero_iff.1 ?_⟩
      rw [mk_out]
      exact (H i).ne_bot

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
⊢ False
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

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

Tactic:
rcases hx with hx | hx <;> rcases hy with hy | hy; · simp [hx, hy]
            · subst x
              exact fun e => (hf i y hy e.symm).elim
            · subst y
              exact fun e => (hf i x hx e).elim
            · exact hs.prop i hx hy

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

Goal state before:
pp: M : Type u_1
N✝ : Type u_2
P✝ : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N✝
inst✝³ : Monoid P✝
N : Type u_4
P : Type u_5
inst✝² : Monoid N
inst✝¹ : Monoid P
φ : N →* N
inst✝ : IsId φ
ψ : N →* P
⊢ ψ.comp φ = ψ

Tactic:
simp only [IsId.eq_id, MonoidHom.comp_id]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M α
inst✝¹ : MulAction N α
inst✝ : SMulCommClass M N α
x y : M × N
a : α
⊢ x.1 • y.1 • x.2 • y.2 • a = x.1 • x.2 • y.1 • y.2 • a

Tactic:
smul_comm y.1 x.2

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M α
inst✝¹ : MulAction N α
inst✝ : SMulCommClass M N α
x y : M × N
a : α
⊢ x.1 • x.2 • y.1 • y.2 • a = x.1 • x.2 • y.1 • y.2 • a
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case fst
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✝ • 1).1 = 1.1

Tactic:
exact smul_one _

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

Goal state before:
pp: case snd
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✝ • 1).2 = 1.2

Tactic:
exact smul_one _

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Surjective ⇑f'
n : ℕ
⊢ Surjective ⇑(f' ^ (n + 1))

Tactic:
rw [iterate_succ]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Surjective ⇑f'
n : ℕ
⊢ Surjective ⇑((f' ^ n) ∘ₗ f')
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Injective ⇑f'
n : ℕ
⊢ Injective ⇑(f' ^ (n + 1))

Tactic:
rw [iterate_succ]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Injective ⇑f'
n : ℕ
⊢ Injective ⇑((f' ^ n) ∘ₗ f')
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Bijective ⇑f'
n : ℕ
⊢ Bijective ⇑(f' ^ (n + 1))

Tactic:
rw [iterate_succ]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Bijective ⇑f'
n : ℕ
⊢ Bijective ⇑((f' ^ n) ∘ₗ f')
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✝¹⁰ : Semiring R₃
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : Module R M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x✝ : M
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
S : Submodule R M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S

Tactic:
simp only [mem_comap, mem_map, forall_exists_index, and_imp]
    intro y hy hxy
    rw [hf.eq_iff] at hxy
    rwa [← hxy]

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₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p : Submodule R M
q : Submodule R₂ M₂
h : q < map f p
⊢ map f (comap f q) < map f p

Tactic:
exact (map_comap_le _ _).trans_lt h

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✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ comap f q ≤ comap (c • f) q

Tactic:
by
  simp only [SetLike.le_def, mem_comap, LinearMap.smul_apply]
  exact fun _ h ↦ smul_mem _ _ h

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

Goal state before:
pp: case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
c : G₀
hc : c ∈ s
⊢ c * a⁻¹ = a⁻¹ * c

Tactic:
mul_inv_eq_iff_eq_mul₀ ha₀,

Goal state after:
case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
c : G₀
hc : c ∈ s
⊢ c = a⁻¹ * c * a
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
have : S ≤ S ⊔ T := le_sup_left
  tauto

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
a : R
⊢ a ∈ Set.center R ↔
    AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧
      AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧
        AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)

Tactic:
Set.mem_center_iff,

Goal state after:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
a : R
⊢ IsMulCentral a ↔
    AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧
      AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧
        AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit m' = ↑h.unit (↑h.unit⁻¹ (x • m'))

Tactic:
simpa using isUnit_apply_inv_apply_of_isUnit h (x • m') |>.symm

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : FaithfulSMul R A
inst✝⁴ : Semiring S
inst✝³ : Module S R
inst✝² : Module S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsTorsionFree S A
⊢ ∀ (r : S) (m : R), (algebraMap R A) (r • m) = r • (algebraMap R A) m

Tactic:
by simp [Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) → ∀ ⦃a_2 b : M⦄, a = a_2 * b → IsUnit a_2 ∨ IsUnit b

Tactic:
rintro h x y rfl

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
x y : M
h : ∀ (a a_1 : M), a * a_1 ~ᵤ x * y → IsUnit a ∨ IsUnit a_1
⊢ IsUnit x ∨ IsUnit y
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: 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 S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ {a} • N), p m ⋯ → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ {a} • N) (hy : y ∈ {a} • N), p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → x ∈ {a} • N → Prop := fun x hx ↦ p x ⋯
r : S
n : M
hr : r ∈ {a}
hn : n ∈ N
⊢ p' (r • n) ⋯

Tactic:
push _ ∈ _ at hr
    subst hr
    exact smul₀ n hn

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ ¬a ≤ b ∧ IsEmpty ↑(Ioo (a ⊓ b) a) → ¬a ≤ b ∧ IsEmpty ↑(Ioo b (a ⊔ b))

Tactic:
(infIooOrderIsoIooSup a b).toEquiv.isEmpty_congr

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ ¬a ≤ b ∧ IsEmpty ↑(Ioo b (a ⊔ b)) → ¬a ≤ b ∧ IsEmpty ↑(Ioo b (a ⊔ b))
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ s ⊆ ↑(AddSubmonoid.toNatSubmodule.symm.symm (AddSubmonoid.closure s))

Tactic:
exact AddSubmonoid.subset_closure

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
s : Set (Submodule R M)
⊢ span R (⋂ S ∈ s, ↑S) = sInf s

Tactic:
by
  rw [← Submodule.coe_sInf, span_eq]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ∃ b', b ⊓ b' = a ∧ b ⊔ b' = ⊤

Tactic:
apply exists_inf_eq_and_sup_eq h (by simp)

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsAtomistic α
b : αᵒᵈ
⊢ ∃ s, IsGLB s b ∧ ∀ a ∈ s, IsCoatom a

Tactic:
apply h.isLUB_atoms

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : IsAtomistic αᵒᵈ
b : α
⊢ ∃ s, IsGLB s b ∧ ∀ a ∈ s, IsCoatom a

Tactic:
apply h.isLUB_atoms

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
x y z : M
hxy : x ∈ R ∙ y
hyz : y ∈ R ∙ z
⊢ x ∈ R ∙ z

Tactic:
rw [← SetLike.mem_coe, ← singleton_subset_iff] at *

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : {x} ⊆ ↑(R ∙ y)
hyz : {y} ⊆ ↑(R ∙ z)
⊢ {x} ⊆ ↑(R ∙ z)
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ a, b ⊓ bif g a then a else aᶜ
⊢ (c < bif g c then c else cᶜ) → c = ⊥

Tactic:
nontriviality α

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ a, b ⊓ bif g a then a else aᶜ
a✝ : Nontrivial α
⊢ (c < bif g c then c else cᶜ) → c = ⊥