mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀o γ
f₁ f₂ : α →*₀o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)

Tactic:
h,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀o γ
f₁ f₂ : α →*₀o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
⊢ Surjective ⇑mkHom

Tactic:
rintro ⟨x, y⟩; exact ⟨⟨x, y⟩, rfl⟩

Goal state after:
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 : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹
⊢ f ↑y = f ↑z

Tactic:
by
  rw [← mul_one (f y), eq_comm, ← mul_inv_left hf y (f z) 1, h]
  exact Units.inv_mul (IsUnit.liftRight (f.domRestrict S) hf z)⁻¹

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : NonAssocSemiring α
inst✝⁴ : Preorder α
inst✝³ : NonAssocSemiring β
inst✝² : Preorder β
inst✝¹ : NonAssocSemiring γ
inst✝ : Preorder γ
f : β →+*o γ
g₁ g₂ : α →+*o β
hf : Injective ⇑f
h : f.comp g₁ = f.comp g₂
a : α
⊢ (f.comp g₁) a = f (g₂ a)

Tactic:
h,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : NonAssocSemiring α
inst✝⁴ : Preorder α
inst✝³ : NonAssocSemiring β
inst✝² : Preorder β
inst✝¹ : NonAssocSemiring γ
inst✝ : Preorder γ
f : β →+*o γ
g₁ g₂ : α →+*o β
hf : Injective ⇑f
h : f.comp g₁ = f.comp g₂
a : α
⊢ (f.comp g₂) a = f (g₂ a)
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
P : Type u_4
inst✝ : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : n * f ↑s = f m
h : ∀ (a : M), j (f a) = k (f a)
⊢ j (n * f ↑s) = k n * j (f ↑s)

Tactic:
h,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
P : Type u_4
inst✝ : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : n * f ↑s = f m
h : ∀ (a : M), j (f a) = k (f a)
⊢ j (n * f ↑s) = k n * k (f ↑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)
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ 1 = 1

Tactic:
rw [OreLocalization.one_def, liftExpand_of]; simp

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

Goal state before:
pp: case c.c
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ r₂ * r₁ /ₒ (s₁ * s₂) = r₂ * r₁ /ₒ (s₂ * s₁)

Tactic:
mul_comm s₁

Goal state after:
case c.c
R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ r₂ * r₁ /ₒ (s₂ * s₁) = r₂ * r₁ /ₒ (s₂ * s₁)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : αᵒᵈ
h : a ≤ b
⊢ ∃ n, pred^[n] b = a

Tactic:
convert! exists_succ_iterate_of_le h.ofDual

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
⊢ succ^[n] x = x + ↑n

Tactic:
induction n with
  | zero =>
    rw [Function.iterate_zero_apply, Nat.cast_zero, add_zero]
  | succ n IH =>
    rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ ¬IsMax 0

Tactic:
rw [not_isMax_iff]
  exact ⟨1, one_pos⟩

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

Goal state before:
pp: motive : ℕ∞ → Prop
a : ℕ∞
zero : motive 0
succ : ∀ (n : ℕ), motive ↑n → motive ↑n.succ
top : (∀ (n : ℕ), motive ↑n) → motive ⊤
⊢ motive a

Tactic:
have A : ∀ n : ℕ, motive n := fun n => Nat.recOn n zero succ

Goal state after:
motive : ℕ∞ → Prop
a : ℕ∞
zero : motive 0
succ : ∀ (n : ℕ), motive ↑n → motive ↑n.succ
top : (∀ (n : ℕ), motive ↑n) → motive ⊤
A : ∀ (n : ℕ), motive ↑n
⊢ motive a
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g j = f j

Tactic:
simp [piecewise]

Goal state after:
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst✝ : (i : ι) → Decidable (i ∈ ∅)
i : ι
⊢ ∅.piecewise f g i = g i

Tactic:
simp [piecewise]

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

Goal state before:
pp: case bot
m : ℕ
⊢ ⊥ < ↑↑(m + 1) ↔ ⊥ ≤ ↑m

pp: case coe
m : ℕ
a✝ : ℕ∞
⊢ ↑a✝ < ↑↑(m + 1) ↔ ↑a✝ ≤ ↑m

Tactic:
· simp only [bot_le, WithBot.bot_lt_coe]

Goal state after:
case coe
m : ℕ
a✝ : ℕ∞
⊢ ↑a✝ < ↑↑(m + 1) ↔ ↑a✝ ≤ ↑m
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Decidable (i ∈ univ)
f g : (i : ι) → π i
i : ι
⊢ univ.piecewise f g i = f i

Tactic:
simp [piecewise]

Goal state after:
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
s : Finset ι
inst✝¹ : (i : ι) → Decidable (i ∈ s)
inst✝ : (i : ι) → Decidable (i ∈ sᶜ)
f g : (i : ι) → π i
i : ι
⊢ sᶜ.piecewise f g i = s.piecewise g f i

Tactic:
simp [piecewise]

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
α✝ β✝ : Type u_2
x✝¹ : α✝ → β✝
x✝ : AddConst α α✝
⊢ pure x✝¹ <*> x✝ = x✝¹ <$> x✝

Tactic:
by simp [Const.map, map, Seq.seq, pure, zero_add]

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (map f v).head = f v.head

Tactic:
h,

Goal state after:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (map f (a ::ᵥ v')).head = f (a ::ᵥ v').head
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (map f v).tail = map f v.tail

Tactic:
h,

Goal state after:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (map f (a ::ᵥ v')).tail = map f (a ::ᵥ v').tail
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f v hp).head = f v.head ⋯

Tactic:
h,

Goal state after:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f (a ::ᵥ v') ⋯).head = f (a ::ᵥ v').head ⋯
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
x : α
hx : x ∈ v.tail.toList
⊢ x ∈ v.toList

Tactic:
rw [← cons_head_tail v, toList_cons, List.mem_cons]; exact .inr hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f v hp).tail = pmap f v.tail ⋯

Tactic:
h,

Goal state after:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f (a ::ᵥ v') ⋯).tail = pmap f (a ::ᵥ v').tail ⋯
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_3
n : ℕ
s : Sym α n
⊢ map (fun x ↦ x) s = s

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

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

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

Tactic:
h,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : LT α
f : α ≤i β
⊢ IsLowerSet (Set.range ⇑f)

Tactic:
by
  rintro _ b h ⟨a, rfl⟩
  exact mem_range_of_le f h

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ (a * b).get ⋯ = ma * mb

Tactic:
simp only [← ha.2, ← hb.2]; rfl

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case neg
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
z : α
hz : z ∈ c
hzy : ¬z ≤ y
⊢ cSup c ≤ y ∨ f y ≤ cSup c

Tactic:
have h' := Or.resolve_left (hc hz).2 hzy

Goal state after:
case neg
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
z : α
hz : z ∈ c
hzy : ¬z ≤ y
h' : f y ≤ z
⊢ cSup c ≤ y ∨ f y ≤ cSup c
Module: Mathlib.Data.Part

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

Tactic:
simp [union_def]; aesop

Goal state after:
Module: Mathlib.Data.Part

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

Tactic:
simp [union_def]; aesop

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

Goal state before:
pp: case pos
c : Cardinal.{u}
h : c = 0
⊢ 0 ^ c ≤ 1

Tactic:
h,

Goal state after:
case pos
c : Cardinal.{u}
h : c = 0
⊢ 0 ^ 0 ≤ 1
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: n : ℕ∞
x : Cardinal.{u_1}
x✝ : x < ℵ₀ ∨ ℵ₀ ≤ x
⊢ ↑n ≤ x ↔ n ≤ x.toENatAux

Tactic:
cases lt_or_ge x ℵ₀ with

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

Goal state before:
pp: x : Cardinal.{u_1}
n : ℕ
x✝ : x < ℵ₀ ∨ ℵ₀ ≤ x
⊢ x.toENatAux ≤ ↑n ↔ x ≤ ↑n

Tactic:
cases lt_or_ge x ℵ₀ with

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
r s : R✝
x✝ : M✝
R : Type u_5
S : Type u_6
M : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : SMul S M
f : R →+* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
x : M
⊢ f 0 • x = 0

Tactic:
hsmul,

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
r s : R✝
x✝ : M✝
R : Type u_5
S : Type u_6
M : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : SMul S M
f : R →+* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
x : M
⊢ 0 • x = 0
Module: Mathlib.Logic.Function.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
φ : M → N
ψ : N → M
h : Function.RightInverse φ ψ
χ : M → M
inst✝ : IsId χ
⊢ ψ ∘ φ = χ

Tactic:
by simp only [IsId.eq_id, h.id]

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
⊢ sum f ≤ lift.{v, u} #ι * ⨆ i, lift.{u, v} (f i)

Tactic:
← (sum f).lift_id,

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
⊢ lift.{max u v, max u v} (sum f) ≤ lift.{v, u} #ι * ⨆ i, lift.{u, v} (f i)
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
by rw [add_comm, aleph0_add_nat]

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

Goal state before:
pp: α : Type u_1
l : List α
h : ↑l.length < #α
⊢ ∃ z, z ∉ l

Tactic:
by
  classical
  contrapose! h
  calc
    #α = #(Set.univ : Set α) := mk_univ.symm
    _ ≤ #l.toFinset := mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x)
    _ = l.toFinset.card := Cardinal.mk_coe_finset
    _ ≤ l.length := Nat.cast_le.mpr (List.toFinset_card_le l)

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

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
F : Type u_14
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module S M₃
σ : R →+* S
f : F
inst✝² : FunLike F M M₃
inst✝¹ : SemilinearMapClass F σ M M₃
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
c : S
x : M
⊢ c • f x = f (σ' c • x)

Tactic:
by simp [map_smulₛₗ _]

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst✝⁶ : Semiring R₁
inst✝⁵ : Semiring R₂
inst✝⁴ : Semiring R₃
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
hf : Injective ⇑f
g₁ g₂ : M₁ →ₛₗ[σ₁₂] M₂
h : f ∘ₛₗ g₁ = f ∘ₛₗ g₂
x : M₁
⊢ (f ∘ₛₗ g₁) x = f (g₂ x)

Tactic:
h,

Goal state after:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst✝⁶ : Semiring R₁
inst✝⁵ : Semiring R₂
inst✝⁴ : Semiring R₃
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
hf : Injective ⇑f
g₁ g₂ : M₁ →ₛₗ[σ₁₂] M₂
h : f ∘ₛₗ g₁ = f ∘ₛₗ g₂
x : M₁
⊢ (f ∘ₛₗ g₂) x = f (g₂ x)
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
⊢ Injective ⇑(g ∘ₛₗ f)

Tactic:
h,

Goal state after:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
⊢ Injective ⇑id
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
⊢ Surjective ⇑(g ∘ₛₗ f)

Tactic:
h,

Goal state after:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
⊢ Surjective ⇑id
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
X : Type u_4
Y : Type u_5
σ : M → N
inst✝ : Monoid M
f : M →ₑ[id] M
m : M
⊢ m • f 1 = f m

Tactic:
rw [← map_smul, smul_eq_mul, mul_one]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M
h : f 1 = g 1
x : R
⊢ σ (MulOpposite.op x) • f 1 = g (MulOpposite.op x • 1)

Tactic:
h,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M
h : f 1 = g 1
x : R
⊢ σ (MulOpposite.op x) • g 1 = g (MulOpposite.op x • 1)
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: case succ
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
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ (g₂ ∘ₛₗ f) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)

Tactic:
h,

Goal state after:
case succ
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
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ (f ∘ₛₗ g) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : Set M
nonempty : C.Nonempty
linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C
c : R
x : M
hx : x ∈ C
⊢ c • x ∈ C

Tactic:
by simpa using linearComb x hx x hx c 0

Goal state after:
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
p : Submodule R M
⊢ ↑p = ↑⊤ ↔ ↑p = Set.univ

Tactic:
top_coe

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ↑p = Set.univ ↔ ↑p = Set.univ
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 ∈ Set.range fun q ↦ ↑q

Tactic:
Subtype.range_coe_subtype

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 ∈ {x | x ∈ toAddSubmonoid '' s}
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✝⁴ : Semiring S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : R →ₗ[R] M
⊢ smulRight 1 ((fun f ↦ f 1) f) = f

Tactic:
by
      ext
      simp only [coe_smulRight, Module.End.one_apply, smul_eq_mul, ← map_smul f, mul_one]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : SupSet γ
g : sSupHom β γ
f₁ f₂ : sSupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)

Tactic:
h,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : SupSet γ
g : sSupHom β γ
f₁ f₂ : sSupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
g : FrameHom β γ
f₁ f₂ : FrameHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)

Tactic:
h,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
g : FrameHom β γ
f₁ f₂ : FrameHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
g : CompleteLatticeHom β γ
f₁ f₂ : CompleteLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)

Tactic:
h,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
g : CompleteLatticeHom β γ
f₁ f₂ : CompleteLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)
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✝ : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : n → M
i : n
⊢ (funLeft R M ⇑e.symm ∘ₗ funLeft R M ⇑e) x i = LinearMap.id x i

Tactic:
rw [id_apply, ← funLeft_comp, Equiv.self_comp_symm, LinearMap.funLeft_id]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
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 τ₁₂ τ₂₃ τ₁₃
f : M →ₗ[R] M
n : ℕ
x : M
h : (f ^ n) x = 0
c : ℕ
w : n ≤ n + c
⊢ (f ^ c) ((f ^ n) x) = 0

Tactic:
h,

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
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 τ₁₂ τ₂₃ τ₁₃
f : M →ₗ[R] M
n : ℕ
x : M
h : (f ^ n) x = 0
c : ℕ
w : n ≤ n + c
⊢ (f ^ c) 0 = 0
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₂
K : Submodule R₂ M₂
⊢ map (↑e.symm) K = p ↔ map (↑e) p = K

Tactic:
rw [map_equiv_eq_comap_symm]
  exact (orderIsoMapComap e).symm_apply_eq.trans eq_comm

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
ι : Type u_5
f : M →ₙ* N
hf : Function.Injective ⇑f
S : Subsemigroup M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S

Tactic:
by simp [mem_comap, mem_map, hf.eq_iff]

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

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

Tactic:
| zero_left =>

Goal state after: