mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ (mapRingHom M ↑e.symm).comp (mapRingHom M ↑e) = RingHom.id R[M]

Tactic:
apply MonoidAlgebra.ringHom_ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
b : α
⊢ preimage 1 (fun x ↦ x * b) ⋯ = {b⁻¹}

Tactic:
rw [← image_mul_right', image_one, one_mul]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s t : Finset α
⊢ s.Nontrivial → t.Nonempty → (s * t).Nontrivial

Tactic:
rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩
  exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s : Finset α
⊢ #s ≤ #(s * s)

Tactic:
by
  cases s.eq_empty_or_nonempty <;> simp [card_le_card_mul_right, *]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ X * (monomial n) r = (monomial (n + 1)) r

Tactic:
rw [X_mul, monomial_mul_X]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
x✝¹ x✝ : ι →₀ M →ₗ[R] N
eq : (finsuppLinearMap S) x✝¹ = (finsuppLinearMap S) x✝
⊢ x✝¹ = x✝

Tactic:
ext i m; exact congr($eq m i)

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.right
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ x - (linearCombination R id) ((lmapDomain R R g) l) ∈ f.ker

Tactic:
rw [LinearMap.mem_ker, f.map_sub, ← hl2]
    rw [Finsupp.linearCombination_apply, Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply]
    rw [Finsupp.sum_mapDomain_index, Finsupp.sum, Finsupp.sum, map_sum]
    · rw [sub_eq_zero]
      refine Finset.sum_congr rfl fun y hy => ?_
      unfold id
      rw [f.map_smul, (hg y (hl1 hy)).2]
    · exact zero_smul _
    · exact fun _ _ _ => add_smul _ _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
⊢ ofIsCompl ⋯ ψ φ = ofIsCompl hpq φ ψ

Tactic:
by
  simp [ofIsCompl_eq_add, add_comm]

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

Goal state before:
pp: s : Set ℕ∞
⊢ sInf s < 1 ↔ 0 ∈ s

Tactic:
sInf_lt_iff

Goal state after:
s : Set ℕ∞
⊢ (∃ a ∈ s, a < 1) ↔ 0 ∈ s
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case mpr.mp
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f' ⇑g'
x₂ : M₂
⊢ g x₂ = 1 → x₂ ∈ Set.range ⇑f

pp: case mpr.mpr
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f' ⇑g'
x₂ : M₂
⊢ x₂ ∈ Set.range ⇑f → g x₂ = 1

Tactic:
· intro hx₂
      obtain ⟨y₁, hy₁⟩ := (h (τ₂ x₂)).1 (by simp only [comm₂₃, hx₂, map_one])
      obtain ⟨x₁, rfl⟩ := h₁ y₁
      exact ⟨x₁, h₂.1 (by simpa only [comm₁₂] using hy₁)⟩

Goal state after:
case mpr.mpr
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f' ⇑g'
x₂ : M₂
⊢ x₂ ∈ Set.range ⇑f → g x₂ = 1
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
hy : y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩
⊢ (q.toFun ⟨↑i - (p.length + 1), ⋯⟩, Fin.append p.toFun q.toFun y) ∈ r

Tactic:
hy,

Goal state after:
case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
hy : y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩
⊢ (q.toFun ⟨↑i - (p.length + 1), ⋯⟩, Fin.append p.toFun q.toFun (Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩)) ∈ r
Module: Mathlib.Algebra.Algebra.NonUnitalHom

Goal state before:
pp: R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
⊢ Function.Injective DFunLike.coe

Tactic:
by
  rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h; congr

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
x : α
⊢ x ∈ p.snoc newLast rel ↔ x ∈ p ∨ x = newLast

Tactic:
simp only [snoc, append, mem_def, Set.mem_range]

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
x : α
⊢ (∃ y, (Fin.append p.toFun (singleton r newLast).toFun ∘ Fin.cast ⋯) y = x) ↔ (∃ y, p.toFun y = x) ∨ x = newLast
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
x : α
h : 2 ≤ height x
⊢ ∃ y, ∃ z < y, y < x

pp: case refine_2
α : Type u_1
inst✝ : Preorder α
x : α
⊢ (∃ y, ∃ z < y, y < x) → 2 ≤ height x

Tactic:
· obtain ⟨p, hp, hlen⟩ := Order.exists_series_of_le_height x (n := 2) h
    refine ⟨p 1, p 0, p.rel_of_lt ?_, hp ▸ p.rel_of_lt ?_⟩ <;> simp [Fin.lt_def, hlen]

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
x : α
⊢ (∃ y, ∃ z < y, y < x) → 2 ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ ⊥ < krullDim α ↔ Nonempty α

Tactic:
rw [bot_lt_iff_ne_bot, krullDim_ne_bot_iff]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁸ : CommSemiring R
inst✝³⁷ : CommSemiring R₂
inst✝³⁶ : CommSemiring R₃
inst✝³⁵ : Monoid R'
inst✝³⁴ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : AddCommMonoid P
inst✝³⁰ : AddCommMonoid Q
inst✝²⁹ : AddCommMonoid S
inst✝²⁸ : AddCommMonoid P'
inst✝²⁷ : AddCommMonoid Q'
inst✝²⁶ : AddCommMonoid M₂
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid P₂
inst✝²³ : AddCommMonoid Q₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid N₃
inst✝²⁰ : AddCommMonoid P₃
inst✝¹⁹ : AddCommMonoid Q₃
inst✝¹⁸ : DistribMulAction R' M
inst✝¹⁷ : Module R'' M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module R N
inst✝¹⁴ : Module R S
inst✝¹³ : Module R P'
inst✝¹² : Module R Q'
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₂ N₂
inst✝⁹ : Module R₂ P₂
inst✝⁸ : Module R₂ Q₂
inst✝⁷ : Module R₃ M₃
inst✝⁶ : Module R₃ N₃
inst✝⁵ : Module R₃ P₃
inst✝⁴ : Module R₃ Q₃
inst✝³ : SMul R' R
inst✝² : IsScalarTower R' R M
inst✝¹ : DistribMulAction R' N
inst✝ : IsScalarTower R' R N
r : R'
m : M
n : N
| (r • m) ⊗ₜ[R] n

Tactic:
rw [← one_smul R m]

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁸ : CommSemiring R
inst✝³⁷ : CommSemiring R₂
inst✝³⁶ : CommSemiring R₃
inst✝³⁵ : Monoid R'
inst✝³⁴ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : AddCommMonoid P
inst✝³⁰ : AddCommMonoid Q
inst✝²⁹ : AddCommMonoid S
inst✝²⁸ : AddCommMonoid P'
inst✝²⁷ : AddCommMonoid Q'
inst✝²⁶ : AddCommMonoid M₂
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid P₂
inst✝²³ : AddCommMonoid Q₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid N₃
inst✝²⁰ : AddCommMonoid P₃
inst✝¹⁹ : AddCommMonoid Q₃
inst✝¹⁸ : DistribMulAction R' M
inst✝¹⁷ : Module R'' M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module R N
inst✝¹⁴ : Module R S
inst✝¹³ : Module R P'
inst✝¹² : Module R Q'
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₂ N₂
inst✝⁹ : Module R₂ P₂
inst✝⁸ : Module R₂ Q₂
inst✝⁷ : Module R₃ M₃
inst✝⁶ : Module R₃ N₃
inst✝⁵ : Module R₃ P₃
inst✝⁴ : Module R₃ Q₃
inst✝³ : SMul R' R
inst✝² : IsScalarTower R' R M
inst✝¹ : DistribMulAction R' N
inst✝ : IsScalarTower R' R N
r : R'
m : M
n : N
| (r • 1 • m) ⊗ₜ[R] n
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

Tactic:
wlog h₂ : s.last = ⊤

Goal state after:
case inr
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α),
    RelSeries.head s = ⊥ → RelSeries.last s = ⊤ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₂ : ¬RelSeries.last s = ⊤
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Subsingleton α
⊢ krullDim α ≤ 0

Tactic:
rw [krullDim_nonpos_iff_forall_isMax]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Subsingleton α
⊢ ∀ (x : α), IsMax x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α = ⨆ a, ↑(height a)

Tactic:
cases isEmpty_or_nonempty α with
  | inl h => rw [krullDim_eq_bot, ciSup_of_empty]
  | inr h => rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α = ⨆ a, ↑(coheight a)

Tactic:
cases isEmpty_or_nonempty α with
  | inl h => rw [krullDim_eq_bot, ciSup_of_empty]
  | inr h => rw [krullDim_eq_iSup_coheight_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
n : N
hn : IsAddUnit n
m : M
⊢ IsAddUnit (m ⊗ₜ[R] n)

Tactic:
rw [isAddUnit_iff_exists_neg] at hn ⊢

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
n : N
hn : ∃ b, n + b = 0
m : M
⊢ ∃ b, m ⊗ₜ[R] n + b = 0
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg.mp
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α → krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
exact (fun h1 ↦ False.elim (h (LTSeries.nonempty_of_finiteDimensionalOrder α)))

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
⊢ 0 + (-y + y) = 0

Tactic:
hy,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
⊢ 0 + 0 = 0
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
n✝ n : ℕ
⊢ (mulLeft R a ^ n) ∘ₗ mulLeft R a = mulLeft R (a ^ n) ∘ₗ mulLeft R a

Tactic:
pow_mulLeft

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
n✝ n : ℕ
⊢ mulLeft R (a ^ n) ∘ₗ mulLeft R a = mulLeft R (a ^ n) ∘ₗ mulLeft R a
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case le.refine_1
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
⊢ ∀ c_1 ∈ c.support, ↑((DistribSMul.toLinearMap R (↥N) c_1) (c c_1)) ∈ sR • N

pp: case le.refine_2
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
⊢ (fun s ↦ ⋂ (_ : s ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}), ↑s) (sR • N) = ↑(sR • N)

Tactic:
· rintro r hr
      rw [mem_set_smul_def, Submodule.mem_sInf]
      rintro p hp
      exact hp (hc hr) (c r).2

Goal state after:
case le.refine_2
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
c : R →₀ ↥N
hc : c ∈ ↑(Finsupp.supported (↥N) R sR)
⊢ (fun s ↦ ⋂ (_ : s ∈ {p | ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ sR → n ∈ N → r • n ∈ p}), ↑s) (sR • N) = ↑(sR • N)
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n
⊢ ∃ m n, x = m ⊗ₜ[R] n

Tactic:
induction x with
  | zero =>
    use 0, 0
    rw [TensorProduct.zero_tmul]
  | tmul m n => use m, n
  | add x y h₁ h₂ =>
    obtain ⟨m₁, n₁, rfl⟩ := h₁
    obtain ⟨m₂, n₂, rfl⟩ := h₂
    apply h

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁶ : CommSemiring R
inst✝³⁵ : CommSemiring R₂
inst✝³⁴ : CommSemiring R₃
inst✝³³ : Monoid R'
inst✝³² : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³¹ : AddCommMonoid M
inst✝³⁰ : AddCommMonoid N
inst✝²⁹ : AddCommMonoid P
inst✝²⁸ : AddCommMonoid Q
inst✝²⁷ : AddCommMonoid S
inst✝²⁶ : AddCommMonoid P'
inst✝²⁵ : AddCommMonoid Q'
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N₂
inst✝²² : AddCommMonoid P₂
inst✝²¹ : AddCommMonoid Q₂
inst✝²⁰ : AddCommMonoid M₃
inst✝¹⁹ : AddCommMonoid N₃
inst✝¹⁸ : AddCommMonoid P₃
inst✝¹⁷ : AddCommMonoid Q₃
inst✝¹⁶ : DistribMulAction R' M
inst✝¹⁵ : Module R'' M
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module R S
inst✝¹¹ : Module R P'
inst✝¹⁰ : Module R Q'
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Module R₂ N₂
inst✝⁷ : Module R₂ P₂
inst✝⁶ : Module R₂ Q₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₃ N₃
inst✝³ : Module R₃ P₃
inst✝² : Module R₃ Q₃
inst✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f✝ : N →ₗ[R] P
r : R
f : N →ₗ[R] P
⊢ lTensor M (r • f) = (RingHom.id R) r • lTensor M f

Tactic:
dsimp
    ext x y
    simp only [compr₂ₛₗ_apply, mk_apply, tmul_smul, smul_apply, lTensor_tmul]

Goal state after:
Module: Mathlib.Data.Fintype.Lattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
⊢ ∃ x₀, ∀ (x : α), f x₀ ≤ f x

Tactic:
by
  cases nonempty_fintype α
  simpa using exists_min_image univ f univ_nonempty

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
a b : R
H : a * (x + y * z) + b * y = 1
⊢ a * x + (a * z + b) * y = 1

Tactic:
simpa only [add_mul, mul_add, add_assoc, add_comm, add_left_comm, mul_assoc, mul_comm,
      mul_left_comm] using H

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + z * y) y

Tactic:
rw [mul_comm]

Goal state after:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z) y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime x (y - z * x) ↔ IsCoprime x y

Tactic:
by
  rw [sub_eq_add_neg, ← neg_mul, add_mul_right_right_iff]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime x (y - z * x) ↔ IsRelPrime x y

Tactic:
by
  rw [sub_eq_add_neg, ← neg_mul, add_mul_right_right_iff]

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α✝ : Type u_1
inst✝ : LinearOrder α✝
n : ℕ
val : Fin n → α✝
i j k : Fin n
u : Level
α :
  let u := u;
  Q(Type u)
atoms : Array Q(«$α»)
h : ¬atoms.isEmpty = true
⊢ 0 < atoms.size

Tactic:
by simpa [Array.size_pos_iff] using h

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

Goal state before:
pp: case succ.zero
R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
ih : 0 ≠ 0 → (M ^ 0).toAddSubmonoid = M.toAddSubmonoid ^ 0
h : 0 + 1 ≠ 0
⊢ (M ^ 0).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ 0 * M.toAddSubmonoid

Tactic:
rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]

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

Goal state before:
pp: case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
m : A
hm : op m ∈ map (↑(opLinearEquiv R)) N
n : A
hn : op n ∈ map (↑(opLinearEquiv R)) M
⊢ op m * op n ∈ map (↑(opLinearEquiv R)) (M * N)

Tactic:
Submodule.mem_map_equiv

Goal state after:
case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
m : A
hm : (opLinearEquiv R).symm (op m) ∈ N
n : A
hn : (opLinearEquiv R).symm (op n) ∈ M
⊢ (opLinearEquiv R).symm (op m * op n) ∈ M * N
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
⊢ ⇑(RingHom.snd R S) '' s ×ˢ t ⊆ t

Tactic:
· exact Set.snd_image_prod_subset _ _

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ y ∈ I, n * y ∈ 1
⊢ m * n ∈ 1

Tactic:
rw [mul_comm]

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ y ∈ I, n * y ∈ 1
⊢ n * m ∈ 1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, h y_1 = y) → ∃ y_1 ∈ I, h y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h xz = x * h z
⊢ h (h.symm x * z) = h xz

Tactic:
rw [map_mul, h.apply_symm_apply, hxz]

Goal state after:
Module: Mathlib.RingTheory.OrzechProperty

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝¹ : Small.{u, v} M
this✝ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
⊢ Injective ⇑f

Tactic:
have := Module.Finite.equiv j.symm

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
⊢ Injective ⇑f
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I✝ J : Ideal R
K L : Ideal S
inst✝ : RingHomClass F R S
I : Ideal S
x y : R
hx : x ∈ ⇑f ⁻¹' ↑I
hy : y ∈ ⇑f ⁻¹' ↑I
⊢ x + y ∈ ⇑f ⁻¹' ↑I

Tactic:
simp only [Set.mem_preimage, SetLike.mem_coe, map_add f] at hx hy ⊢
    exact add_mem hx hy

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ ∀ (x s t s' t' : R), (xgcdAux 0 s t x s' t').1 = gcd 0 x

Tactic:
by
      intros
      rw [xgcd_zero_left, gcd_zero_left]

Goal state after: