mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case mk.mk
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ (sumZeroHom fun i ↦ ↑(φ i)).toFun
      ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨sf, hf⟩ } +
        { toFun := g, support' := Quot.mk ⇑trueSetoid ⟨sg, hg⟩ }) =
    (sumZeroHom fun i ↦ ↑(φ i)).toFun { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨sf, hf⟩ } +
      (sumZeroHom fun i ↦ ↑(φ i)).toFun { toFun := g, support' := Quot.mk ⇑trueSetoid ⟨sg, hg⟩ }

Tactic:
change (∑ i ∈ _, _) = (∑ i ∈ _, _) + ∑ i ∈ _, _

Goal state after:
case mk.mk
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ ∑ i ∈ (↑((fun ys ↦ ⟨↑⟨sf, hf⟩ + ↑ys, ⋯⟩) ⟨sg, hg⟩)).toFinset,
      ((fun i ↦ ↑(φ i)) i)
        (({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨sf, hf⟩ } +
            { toFun := g, support' := Quot.mk ⇑trueSetoid ⟨sg, hg⟩ })
          i) =
    ∑ i ∈ (↑⟨sf, hf⟩).toFinset, ((fun i ↦ ↑(φ i)) i) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨sf, hf⟩ } i) +
      ∑ i ∈ (↑⟨sg, hg⟩).toFinset, ((fun i ↦ ↑(φ i)) i) ({ toFun := g, support' := Quot.mk ⇑trueSetoid ⟨sg, hg⟩ } i)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
f : Dual R M
⊢ (∀ w ∈ span R s, w ∈ LinearMap.ker f) ↔ s ⊆ ↑(LinearMap.ker f)

Tactic:
exact span_le

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Dual R M)
x : M
this : ∀ (φ : M →ₗ[R] R), x ∈ φ.ker ↔ φ ∈ LinearMap.ker ((Dual.eval R M) x)
⊢ (∀ φ ∈ span R s, φ ∈ LinearMap.ker ((Dual.eval R M) x)) ↔ ∀ f ∈ s, f ∈ LinearMap.ker ((Dual.eval R M) x)

Tactic:
exact span_le

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
i : ι
hm : ((lsum ℕ) fun i ↦ (p i).subtype) (erase i m) + (p i).subtype (m i) = 0
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) (erase i m) = ↑(-m i)

Tactic:
Submodule.subtype_apply,

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
i : ι
hm : ((lsum ℕ) fun i ↦ (p i).subtype) (erase i m) + ↑(m i) = 0
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) (erase i m) = ↑(-m i)
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support) → (if True then f.coeff a0 * g.coeff b0 else 0) = 0

Tactic:
refine fun hnotMem ↦ ite_eq_right_iff.mpr (fun _ ↦ ?_)

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
⊢ f.coeff a0 * g.coeff b0 = 0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a b : G
ha : a ∈ A.preimage ⇑f ⋯
hb : b ∈ B.preimage ⇑f ⋯
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
simp only [← hf.eq_iff, map_mul] at ab ⊢

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
a b : G
ha : a ∈ A.preimage ⇑f ⋯
hb : b ∈ B.preimage ⇑f ⋯
ab : f a * f b = f a0 * f b0
⊢ f a = f a0 ∧ f b = f b0
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⨅ a, (lapply a).ker ≤ ⊥

Tactic:
by
  simp only [SetLike.le_def, mem_iInf, mem_ker, mem_bot, lapply_apply]
  exact fun a h => Finsupp.ext h

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
a : R[ℕ]
⊢ { toFinsupp := a ^ 0 } = npowRec 0 { toFinsupp := a }

Tactic:
| zero        =>

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

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : SMulZeroClass S R
inst✝¹ : SMulZeroClass Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
⊢ ∀ (m : S) (a : R[X]), MulOpposite.op m • a = m • a

Tactic:
by
    rintro _ ⟨⟩
    simp_rw [← ofFinsupp_smul, op_smul_eq_smul]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
a : R
⊢ (monomial n) 0 = 0

Tactic:
monomial_zero_right

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
a : R
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
⊢ ((Finsupp.basis b).repr (single ⟨i, x⟩.fst ((b ⟨i, x⟩.fst) ⟨i, x⟩.snd))) ⟨j, y⟩ = (single ⟨i, x⟩ 1) ⟨j, y⟩

Tactic:
by_cases h : i = j

Goal state after:
case pos
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : i = j
⊢ ((Finsupp.basis b).repr (single ⟨i, x⟩.fst ((b ⟨i, x⟩.fst) ⟨i, x⟩.snd))) ⟨j, y⟩ = (single ⟨i, x⟩ 1) ⟨j, y⟩

case neg
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : ¬i = j
⊢ ((Finsupp.basis b).repr (single ⟨i, x⟩.fst ((b ⟨i, x⟩.fst) ⟨i, x⟩.snd))) ⟨j, y⟩ = (single ⟨i, x⟩ 1) ⟨j, y⟩
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
y : ℕ∞
h : y ≤ ↑x
hy : y ∈ s
⊢ y ∈ (fun n ↦ ↑n) '' {n | n ≤ x}

Tactic:
have hxt : y < ⊤ := lt_of_le_of_lt h hx

Goal state after:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
y : ℕ∞
h : y ≤ ↑x
hy : y ∈ s
hxt : y < ⊤
⊢ y ∈ (fun n ↦ ↑n) '' {n | n ≤ x}
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ι₂ → ℕ∞
inst✝¹ : Nonempty ι₁
inst✝ : Nonempty ι₂
h : ⨆ i, ⨆ j, f i j < ⊤
⊢ ∃ i j, f i j = ⨆ i, ⨆ j, f i j

Tactic:
by
  rw [iSup_prod'] at h ⊢
  exact Prod.exists'.mp (exists_eq_iSup_of_lt_top h)

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

Goal state before:
pp: a : ℕ∞
s : Set ℕ∞
⊢ a + sInf s = ⨅ b ∈ s, a + b

Tactic:
sInf_eq_iInf,

Goal state after:
a : ℕ∞
s : Set ℕ∞
⊢ a + ⨅ a ∈ s, a = ⨅ b ∈ s, a + b
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
hf : IsProj ⊤ f
⊢ f = id

pp: case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m id
⊢ m = ⊤

Tactic:
· ext
    simp [hf.map_id]

Goal state after:
case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m id
⊢ m = ⊤
Module: Mathlib.Order.RelSeries

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

Tactic:
by
  delta snoc; rw [head_append]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
x✝ : ℕ
hlen : p.length = x✝
⊢ ↑x✝ ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
cases hlen : p.length with

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ y, ⨆ (_ : y < x), height y + 1 ≤ height x

Tactic:
· apply iSup₂_le; intro y hyx
    rw [height_add_const]
    apply iSup₂_le; intro p hp
    apply le_iSup₂_of_le (p.snoc x (hp ▸ hyx)) (by simp) (by simp)

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✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
r : R'
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
n : N
⊢ (SMul.aux r) (FreeAddMonoid.of (0, n)) = (SMul.aux r) 0

Tactic:
simp_rw [map_zero, SMul.aux_of, smul_zero, zero_tmul]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
⊢ (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 1 ≤ krullDim α ↔ IsSimpleOrder α

Tactic:
WithBot.one_le_iff_pos,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
⊢ (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 0 < krullDim α ↔ IsSimpleOrder α
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : FunLike F α β
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
⊢ ⇑f '' (a :: as).prod = (List.map (fun s ↦ ⇑f '' s) (a :: as)).prod

Tactic:
rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
⊢ x ⊗ₜ[R] Pi.single i m j = Pi.single i (x ⊗ₜ[R] m) j

Tactic:
by_cases h : i = j

Goal state after:
case pos
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
h : i = j
⊢ x ⊗ₜ[R] Pi.single i m j = Pi.single i (x ⊗ₜ[R] m) j

case neg
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
h : ¬i = j
⊢ x ⊗ₜ[R] Pi.single i m j = Pi.single i (x ⊗ₜ[R] m) j
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
⊢ Pi.single i m j ⊗ₜ[R] x = Pi.single i (m ⊗ₜ[R] x) j

Tactic:
by_cases h : i = j

Goal state after:
case pos
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
h : i = j
⊢ Pi.single i m j ⊗ₜ[R] x = Pi.single i (m ⊗ₜ[R] x) j

case neg
R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
h : ¬i = j
⊢ Pi.single i m j ⊗ₜ[R] x = Pi.single i (m ⊗ₜ[R] x) j
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b : α
hbc : a ≤ b
c : α
⊢ a + c ≤ b + c

Tactic:
by
    simp_rw [add_eq_sup]
    grw [hbc]

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

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 + a∗ * a = a∗

Tactic:
have h : 1 + a∗ * a ≤ a∗ := by
    rw [add_le_iff]
    exact ⟨one_le_kstar, kstar_mul_le_kstar⟩

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
⊢ 1 + a∗ * a = a∗
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : N ⊗[R] M
⊢ (rTensor M (g ∘ₗ f)) x = (rTensor M g) ((rTensor M f) x)

Tactic:
by rw [rTensor_comp, coe_comp]; rfl

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

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

Tactic:
add_mul_left_right_iff

Goal state after:
R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime x y ↔ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
add_mul_left_right_iff

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime x y ↔ IsRelPrime x y
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case mp
m n a b : ℤ
h : a * m + b * n = 1
⊢ ↑1 = m * a + n * b

Tactic:
rwa [mul_comm m, mul_comm n, eq_comm]

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
⊢ max (toInt val i) (toInt val j) = toInt val k ↔ max (val i) (val j) = val k

Tactic:
simp [le_antisymm_iff, sup_le_iff, le_sup_iff, toInt_le_toInt]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
⊢ map (↑(opLinearEquiv R)) (M * N) = map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M

Tactic:
by
  apply le_antisymm
  · simp_rw [map_le_iff_le_comap]
    refine mul_le.2 fun m hm n hn => ?_
    rw [mem_comap, map_equiv_eq_comap_symm, map_equiv_eq_comap_symm]
    change op n * op m ∈ _
    exact mul_mem_mul hn hm
  · refine mul_le.2 (MulOpposite.rec' fun m hm => MulOpposite.rec' fun n hn => ?_)
    rw [Submodule.mem_map_equiv] at hm hn ⊢
    exact mul_mem_mul hn hm

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x : A
⊢ (∃ r, x = (algebraMap R A) ↑r) → R ∙ x = 1

Tactic:
rintro ⟨r, rfl⟩

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
r : Rˣ
⊢ R ∙ (algebraMap R A) ↑r = 1
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I✝ : Ideal R
J✝ : Ideal S
I J : Ideal (R × S)
⊢ { toFun := fun I ↦ (map (RingHom.fst R S) I, map (RingHom.snd R S) I), invFun := fun I ↦ I.1.prod I.2, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun I ↦ (map (RingHom.fst R S) I, map (RingHom.snd R S) I), invFun := fun I ↦ I.1.prod I.2,
          left_inv := ⋯, right_inv := ⋯ }
        J ↔
    I ≤ J

Tactic:
simp only [Equiv.coe_fn_mk, Prod.mk_le_mk]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I✝ : Ideal R
J✝ : Ideal S
I J : Ideal (R × S)
⊢ map (RingHom.fst R S) I ≤ map (RingHom.fst R S) J ∧ map (RingHom.snd R S) I ≤ map (RingHom.snd R S) J ↔ I ≤ J
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : EuclideanDomain R
x z : R
hz : ¬z = 0
p : R
⊢ z * (x * p) / z = x * p

Tactic:
mul_div_cancel_left₀ _ hz

Goal state after:
case neg
R : Type u
inst✝ : EuclideanDomain R
x z : R
hz : ¬z = 0
p : R
⊢ x * p = x * p
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x r s g : R
hr : x = g * r
hgxy : ¬g = 0
hxy : x = 0 ∨ g * s / gcd x (g * s) = 0
hy : s = 0
⊢ g * s = 0

Tactic:
rw [hy, mul_zero]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n x✝¹ : ℕ
x✝ : (I ^ x✝¹).IsTwoSided
⊢ (I ^ x✝¹.succ).IsTwoSided

Tactic:
rw [Submodule.pow_succ]

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n x✝¹ : ℕ
x✝ : (I ^ x✝¹).IsTwoSided
⊢ IsTwoSided (I ^ x✝¹ * I)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
this : ∀ I ∈ A, y ∈ map f I
⊢ x ∈ sInf A

Tactic:
rw [Submodule.mem_sInf]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : y ∈ sInf (map f '' A)
x : R
hx : f x = y
this : ∀ I ∈ A, y ∈ map f I
⊢ ∀ p ∈ A, x ∈ p
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

Tactic:
by
    rcases hna.lt_or_gt with ha | ha <;> rcases hnb.lt_or_gt with hb | hb <;>
      simp [Int.mul_nonneg_iff, ha.le, ha.not_ge, hb.le, hb.not_ge]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
A : Type u_2
inst✝³ : CommSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a : A
⊢ ((LinearMap.mul R A) a).range = Submodule.restrictScalars R (span {a})

Tactic:
aesop (add simp Ideal.mem_span_singleton) (add simp dvd_def)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : DivisionMonoid α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
ha : IsUnit a
⊢ (↑a)⁻¹ ∈ S

Tactic:
obtain ⟨u, rfl⟩ := ha
  convert! u⁻¹.1.2
  exact (map_inv ((subtype <| ofClass S).comp <| Units.coeHom S) u).symm

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
s : Finset ι
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
hn : s.card = n + 1
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

Tactic:
replace hn : ∃ (i : ι) (t : Finset ι), i ∉ t ∧ insert i t = s ∧ t.card = n :=
      Finset.card_eq_succ.1 hn

Goal state after:
case succ
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
s : Finset ι
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i)
hn : ∃ i t, i ∉ t ∧ insert i t = s ∧ t.card = n
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
⊢ map 0 f = 0

Tactic:
by
  ext
  simp [h]

Goal state after:
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
⊢ (diagonal v)ᵀ i j = diagonal v i j

Tactic:
by_cases h : i = j

Goal state after:
case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j

case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : ¬i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i ↦ d₁ i + d₂ i) i j

Tactic:
by_cases h : i = j

Goal state after:
case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i ↦ d₁ i + d₂ i) i j

case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i ↦ d₁ i + d₂ i) i j
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
i j : n
⊢ diagonal (r • d) i j = (r • diagonal d) i j

Tactic:
by_cases h : i = j

Goal state after:
case pos
n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
i j : n
h : i = j
⊢ diagonal (r • d) i j = (r • diagonal d) i j

case neg
n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
i j : n
h : ¬i = j
⊢ diagonal (r • d) i j = (r • diagonal d) i j
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
d : n → α
i j : n
⊢ (-diagonal d) i j = diagonal (fun i ↦ -d i) i j

Tactic:
by_cases h : i = j

Goal state after:
case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
d : n → α
i j : n
h : i = j
⊢ (-diagonal d) i j = diagonal (fun i ↦ -d i) i j

case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
d : n → α
i j : n
h : ¬i = j
⊢ (-diagonal d) i j = diagonal (fun i ↦ -d i) i j