mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Function.Surjective ⇑(quotientInfToSupQuotient p p')

Tactic:
← range_eq_top,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ (quotientInfToSupQuotient p p').range = ⊤
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ (a * d) • s = d • a • s

Tactic:
rw [mul_comm, mul_smul]

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case mk
A : Type u_1
B : Type u_2
M : Type u_3
N : Type u_4
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ✝ ψ : AddChar A M
toFun✝ : A → M
map_zero_eq_one'✝ : toFun✝ 0 = 1
map_add_eq_mul'✝ : ∀ (a b : A), toFun✝ (a + b) = toFun✝ a * toFun✝ b
h : { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ }.toFun = ψ.toFun
⊢ { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ } = ψ

Tactic:
cases ψ

Goal state after:
case mk.mk
A : Type u_1
B : Type u_2
M : Type u_3
N : Type u_4
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
ψ : AddChar A M
toFun✝¹ : A → M
map_zero_eq_one'✝¹ : toFun✝¹ 0 = 1
map_add_eq_mul'✝¹ : ∀ (a b : A), toFun✝¹ (a + b) = toFun✝¹ a * toFun✝¹ b
toFun✝ : A → M
map_zero_eq_one'✝ : toFun✝ 0 = 1
map_add_eq_mul'✝ : ∀ (a b : A), toFun✝ (a + b) = toFun✝ a * toFun✝ b
h :
  { toFun := toFun✝¹, map_zero_eq_one' := map_zero_eq_one'✝¹, map_add_eq_mul' := map_add_eq_mul'✝¹ }.toFun =
    { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_zero_eq_one' := map_zero_eq_one'✝¹, map_add_eq_mul' := map_add_eq_mul'✝¹ } =
    { toFun := toFun✝, map_zero_eq_one' := map_zero_eq_one'✝, map_add_eq_mul' := map_add_eq_mul'✝ }
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
⊢ Set.range (map f) = ⇑coeffEquiv ⁻¹' Set.range (mapRange ⇑f ⋯ ∘ ⇑coeffEquiv)

Tactic:
simp_rw [comp_def, Equiv.eq_preimage_iff_image_eq, ← Set.range_comp', coeffEquiv_apply,
        coeff_map]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
⊢ ∑ m₁ ∈ x.coeff.support, ∑ m₂ ∈ y.coeff.support, F (m₁, m₂) =
    ∑ p ∈ x.coeff.support ×ˢ y.coeff.support with p.1 * p.2 = m, x.coeff p.1 * y.coeff p.2

Tactic:
rw [Finset.sum_filter, Finset.sum_product]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Subsingleton M
r : R
⊢ (uniqueRingEquiv M).symm r = single 1 r

Tactic:
ext; simp [uniqueRingEquiv]

Goal state after:
Module: Mathlib.Data.Multiset.Sort

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ a ∈ ↑(s.sort r) ↔ a ∈ s

Tactic:
sort_eq

Goal state after:
α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ a ∈ s ↔ a ∈ s
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ (↑(s.sort r)).Nodup

Tactic:
sort_eq

Goal state after:
α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ s.val.Nodup
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
n : ℕ
i : Fin (n + 1)
⊢ #{i}ᶜ = n

Tactic:
by simp [card_compl]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
j : Fin k
⊢ #{i}ᶜ = n

Tactic:
by simp [card_compl]

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:
classical 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✝ : Group α
a : α
⊢ preimage 1 (fun x ↦ a⁻¹ * x) ⋯ = {a}

Tactic:
preimage_mul_left_one,

Goal state after:
α : Type u_2
inst✝ : Group α
a : α
⊢ {a⁻¹⁻¹} = {a}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ (C a).coeff n = if n = 0 then a else 0

Tactic:
convert! coeff_monomial (a := a) (m := n) (n := 0) using 2
  simp [eq_comm]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : GeneralLinearGroup R M
⊢ (x * y).toLinearEquiv = x.toLinearEquiv * y.toLinearEquiv

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
⊢ ↑((generalLinearEquiv R M) f) = ↑f

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive ((Polynomial.monomial n) a)
n : ℕ
a : R
_h : motive (C a * X ^ n)
⊢ motive (C a * X ^ (n + 1))

Tactic:
rw [C_mul_X_pow_eq_monomial]

Goal state after:
R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive ((Polynomial.monomial n) a)
n : ℕ
a : R
_h : motive (C a * X ^ n)
⊢ motive ((Polynomial.monomial (n + 1)) a)
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
⊢ ∃ s, φ (Pi.single s 1) ≠ 0

Tactic:
by_contra

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this✝ : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
this : ¬∃ s, φ (Pi.single s 1) ≠ 0
⊢ False
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
⊢ φ (Pi.single s 1 * Pi.single x✝¹ 1) = 0

Tactic:
convert! map_zero φ

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
this : Fintype G
h1 : ∑ x, φ (Pi.single x 1) = 1
s : G
hs : φ (Pi.single s 1) ≠ 0
x✝¹ : G
x✝ : x✝¹ ≠ s
⊢ Pi.single s 1 * Pi.single x✝¹ 1 = 0
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case refine_2
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
inst✝ : Module.Finite R M
s : Finset M
span_s : Submodule.span R ↑s = ⊤
x : M →ₗ[R] ι →₀ N
⊢ (finsuppLinearMap S) (onFinset (s.sup fun m ↦ (x m).support) (fun x_1 ↦ lapply x_1 ∘ₗ x) ⋯) = x

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case right
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
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Function.Surjective ⇑(p.subtype.coprod q.subtype)

Tactic:
← range_eq_top,

Goal state after:
case right
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
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ (p.subtype.coprod q.subtype).range = ⊤
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ f.range ∈ Module.End.invtSubmodule T ↔ map T f.range ≤ f.range

Tactic:
Module.End.mem_invtSubmodule_iff_map_le

Goal state after:
E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ map T f.range ≤ f.range ↔ map T f.range ≤ f.range
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A : Finset ((i : ι) → G i)
⊢ ∀ {B : Finset ((i : ι) → G i)},
    1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
let _ := isWellFounded_ssubset (α := ∀ i, G i) -- why need this?
    apply IsWellFounded.induction (· ⊂ ·) A; intro A ihA B
    apply IsWellFounded.induction (· ⊂ ·) B; intro B ihB hc
    obtain ⟨hA, hB, hc⟩ := Nat.one_lt_mul_iff.mp hc
    rw [card_pos] at hA hB
    obtain ⟨i, hc⟩ := exists_or.mpr (hc.imp exists_of_one_lt_card_pi exists_of_one_lt_card_pi)
    obtain ⟨p1, h1, p2, h2, hne, hi1, hi2⟩ := uniqueMul_of_one_lt_card (Nat.one_lt_mul_iff.mpr
      ⟨card_pos.2 (hA.image _), card_pos.2 (hB.image _), hc.imp And.left And.left⟩)
    simp_rw [mem_product, mem_image, ← filter_nonempty_iff] at h1 h2
    replace h1 := uniqueMul_of_twoUniqueMul ?_ h1.1 h1.2
    on_goal 1 => replace h2 := uniqueMul_of_twoUniqueMul ?_ h2.1 h2.2
    · obtain ⟨a1, ha1, b1, hb1, hu1⟩ := h1
      obtain ⟨a2, ha2, b2, hb2, hu2⟩ := h2
      rw [mem_filter] at ha1 hb1 ha2 hb2
      simp_rw [mem_product]
      refine ⟨(a1, b1), ⟨ha1.1, hb1.1⟩, (a2, b2), ⟨ha2.1, hb2.1⟩, ?_,
        UniqueMul.of_image_filter (Pi.evalMulHom G i) ha1.2 hb1.2 hi1 hu1,
        UniqueMul.of_image_filter (Pi.evalMulHom G i) ha2.2 hb2.2 hi2 hu2⟩
      grind
    all_goals rcases hc with hc | hc; · exact ihA _ (hc.2 _)
    · by_cases hA : {a ∈ A | a i = p2.1} = A
      · rw [hA]
        exact ihB _ (hc.2 _)
      · exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)
    · by_cases hA : {a ∈ A | a i = p1.1} = A
      · rw [hA]
        exact ihB _ (hc.2 _)
      · exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)

Goal state after:
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, ⋯⟩
⊢ (Fin.append p.toFun q.toFun x, Fin.append p.toFun q.toFun y) ∈ r

Tactic:
rw [hx, Fin.append_right, hy, Fin.append_right]

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), ⋯⟩, q.toFun ⟨↑i - p.length, ⋯⟩) ∈ r
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : (a0, b0) = (a1, b1)
⊢ False

Tactic:
rw [Prod.mk_inj] at he; rw [he.1, he.2, he1] at he0
      obtain ⟨⟨a2, b2⟩, h2, hne⟩ := exists_mem_ne hc (a0, b0)
      rw [mem_product] at h2
      refine (min'_lt_max' _ (mul_mem_mul ha0 hb0) (mul_mem_mul h2.1 h2.2) fun he ↦ hne ?_).ne he0
      exact Prod.ext_iff.mpr (this h2.1 h2.2 he.symm)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ height a
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
ha : height a = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
| coe m =>

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✝
x y : FreeAddMonoid (M × N)
⊢ (SMul.aux r) (x + y) = (SMul.aux r) (y + x)

Tactic:
simp_rw [map_add, add_comm]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe.coe
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
⊢ ↑n + ↑m ≤ ⨆ p, ↑p.length

Tactic:
| coe m =>

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
h : IsEmpty α
⊢ ⊥ = ⨆ a, ↑(height a)

Tactic:
ciSup_of_empty

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
h : IsEmpty α
⊢ ⊥ = ⊥
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

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₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x✝ y✝ : FreeAddMonoid (M × N)
hxy : Eqv R M N x✝ y✝
x y : FreeAddMonoid (M × N)
⊢ (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (x + y) = (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (y + x)

Tactic:
simp_rw [map_add, add_comm]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
h : IsEmpty α
⊢ ⊥ = ⨆ a, ↑(coheight a)

Tactic:
ciSup_of_empty

Goal state after:
case inl
α : Type u_1
inst✝ : Preorder α
h : IsEmpty α
⊢ ⊥ = ⊥
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

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
f✝ : M →ₗ[R] N →ₗ[R] P
f' f g : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
⊢ lift (f + g) = lift f + lift g

Tactic:
ext; rfl

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

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
f : M →ₗ[R] N →ₗ[R] P
f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
x✝¹ : R₂
x✝ : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
⊢ lift (x✝¹ • x✝) = (RingHom.id R₂) x✝¹ • lift x✝

Tactic:
ext; rfl

Goal state after:
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) = ⇑f '' a * (List.map (fun s ↦ ⇑f '' s) as).prod

Tactic:
image_mul,

Goal state after:
α : 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 * ⇑f '' as.prod = ⇑f '' a * (List.map (fun s ↦ ⇑f '' s) as).prod
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case closed_under_smul
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
r : R
n : M
⊢ r ∈ sR →
    n ∈ N → r • n ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)

Tactic:
hr

Goal state after:
case closed_under_smul
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
r : R
n : M
hr : r ∈ sR
⊢ n ∈ N → r • n ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)
Module: Mathlib.LinearAlgebra.TensorProduct.Map

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 : N ⊗[R] M
⊢ (rTensor M id) x = x

Tactic:
rw [rTensor_id, id_coe, _root_.id]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
ι : Sort u_4
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
⊢ t • 0 ∈ ⨆ i, T • S i

Tactic:
simp_rw [smul_zero]

Goal state after:
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
ι : Sort u_4
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
⊢ 0 ∈ ⨆ i, T • S i
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
add_mul_right_left_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 + -z * y) y ↔ IsRelPrime x y

Tactic:
add_mul_right_left_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 : ℤ
⊢ IsCoprime m n → m.gcd n = 1

Tactic:
rintro ⟨a, b, h⟩
    refine Nat.dvd_one.mp (Int.gcd_dvd_iff.mpr ⟨a, b, ?_⟩)
    rwa [mul_comm m, mul_comm n, eq_comm]

Goal state after: