mathlib-initiative/mathlib-tactics huggingface dataset:
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 t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0) ↔ LinearIndependent R ![x, y]

Tactic:
pair_iff

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ (∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0) →
    ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0

Tactic:
intro h i x hx hsup
    obtain ⟨f, hf, rfl⟩ := (Submodule.mem_iSup_iff_exists_finsupp ..).mp hsup
    contrapose! h
    use insert i f.support, fun j ↦ if j = i then -f.sum fun _ x ↦ x else f j
    refine ⟨fun j hj ↦ ?_, ?_, by grind⟩
    · beta_reduce
      split_ifs with h
      · exact (p j).neg_mem (h ▸ hx)
      · simpa [h] using hf j
    · specialize hf i
      simp at hf
      grind [Finsupp.sum, Finset.sum_congr]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl
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
inst✝ : Nontrivial R
h : a * d = b * c
⊢ ¬LinearIndependent R ![a • x + b • y, c • x + d • y]

Tactic:
pair_iff

Goal state after:
case inl
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
inst✝ : Nontrivial R
h : a * d = b * c
⊢ ¬∀ (s t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 → s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hImaximal : LinearIndepOn R v (I ∪ {i}) → I = I ∪ {i}
hi : i ∉ I
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)

Tactic:
set J := I ∪ {i} with hJ

Goal state after:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x y : V
⊢ ∀ (x_1 : K), ∀ x_2 ∈ span K s, x = x_1 • y + x_2 → x ∉ span K s → ∃ a, ∃ z ∈ span K s, y = a • x + z

Tactic:
rintro a z hz rfl h

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
y : V
a : K
z : V
hz : z ∈ span K s
h : a • y + z ∉ span K s
⊢ ∃ a_1, ∃ z_1 ∈ span K s, y = a_1 • (a • y + z) + z_1
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
⊢ LinearIndepOn K v (insert x s)

Tactic:
rw [← union_singleton]

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
⊢ LinearIndepOn K v (s ∪ {x})
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
n : ℕ
v : Fin n → V
⊢ (LinearIndependent K fun i ↦ Fin.cons x v ((finRotate (n + 1)) i)) ↔ LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
← Function.comp_def,

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K (Fin.cons x v ∘ ⇑(finRotate (n + 1))) ↔ LinearIndependent K v ∧ x ∉ span K (range v)
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
β' : Type u_4
γ' : Type u_6
δ : Type u_7
ε : Type u_9
inst✝³ : DecidableEq β'
inst✝² : DecidableEq γ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
⊢ image2 f (↑s) (image2 g ↑t ↑u) ⊆ image2 g' (image2 f₁ ↑s ↑t) (image2 f₂ ↑s ↑u)

Tactic:
exact Set.image2_distrib_subset_left h_distrib

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

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
⊢ f = g

Tactic:
convert congr(($this).comp coeffAddEquiv.toAddMonoidHom) <;> ext

Goal state after:
case e'_2
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
x✝ : R[M]
⊢ f x✝ = ((f.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom) x✝

case e'_3
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
x✝ : R[M]
⊢ g x✝ = ((g.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom) x✝
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : 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:
Nat.one_lt_mul_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : 0 < #A ∧ 0 < #B ∧ (1 < #A ∨ 1 < #B)
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
h✝ : s = ∅
⊢ #s ≤ #(s / s)

Tactic:
simp [card_le_card_div_left, *]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
h✝ : s.Nonempty
⊢ #s ≤ #(s / s)

Tactic:
simp [card_le_card_div_left, *]

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

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

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, add_assoc]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ Injective coeff

Tactic:
rintro ⟨p⟩ ⟨q⟩; simp [coeff]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).coeff = Function.update p.coeff n a

Tactic:
by ext; simp [coeff, update]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ coeffs 1 ⊆ {1}

Tactic:
by
  simp_rw [coeffs, Finset.image_subset_iff]
  simp_all [coeff_one]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d

Tactic:
classical
    let _ := Finset.mul (α := G)              -- E = D⁻¹C, F = DC⁻¹
    have := uniqueMul_of_nonempty (A := D.image (·⁻¹) * C) (B := D * C.image (·⁻¹)) ?_ ?_
    · obtain ⟨e, he, f, hf, hu⟩ := this
      clear_value C D
      simp only [UniqueMul, mem_mul, mem_image] at he hf hu
      obtain ⟨_, ⟨d1, hd1, rfl⟩, c1, hc1, rfl⟩ := he
      obtain ⟨d2, hd2, _, ⟨c2, hc2, rfl⟩, rfl⟩ := hf
      by_cases! h12 : c1 ≠ 1 ∨ d2 ≠ 1
      · refine ⟨c1, hc1, d2, hd2, h12, fun c3 d3 hc3 hd3 he => ?_⟩
        specialize hu ⟨_, ⟨_, hd1, rfl⟩, _, hc3, rfl⟩ ⟨_, hd3, _, ⟨_, hc2, rfl⟩, rfl⟩
        rw [mul_left_cancel_iff, mul_right_cancel_iff,
            mul_assoc, ← mul_assoc c3, he, mul_assoc, mul_assoc] at hu; exact hu rfl
      obtain ⟨rfl, rfl⟩ := h12
      by_cases! h21 : c2 ≠ 1 ∨ d1 ≠ 1
      · refine ⟨c2, hc2, d1, hd1, h21, fun c4 d4 hc4 hd4 he => ?_⟩
        specialize hu ⟨_, ⟨_, hd4, rfl⟩, _, hC, rfl⟩ ⟨_, hD, _, ⟨_, hc4, rfl⟩, rfl⟩
        simpa only [mul_one, one_mul, ← mul_inv_rev, he, true_imp_iff, inv_inj, and_comm] using hu
      obtain ⟨rfl, rfl⟩ := h21
      rcases hcard with hC | hD
      · obtain ⟨c, hc, hc1⟩ := exists_mem_ne hC 1
        refine (hc1 ?_).elim
        simpa using hu ⟨_, ⟨_, hD, rfl⟩, _, hc, rfl⟩ ⟨_, hD, _, ⟨_, hc, rfl⟩, rfl⟩
      · obtain ⟨d, hd, hd1⟩ := exists_mem_ne hD 1
        refine (hd1 ?_).elim
        simpa using hu ⟨_, ⟨_, hd, rfl⟩, _, hC, rfl⟩ ⟨_, hd, _, ⟨_, hC, rfl⟩, rfl⟩
    all_goals apply_rules [Nonempty.mul, Nonempty.image, Finset.Nonempty.map, hc.1, hc.2.1]

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
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ x ∈ q

Tactic:
conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ q
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
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔ x ∈ p

Tactic:
conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔ (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ p
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
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ (p.projection q hpq) x = 0 ↔ x ∈ q

Tactic:
by
  simp [projection, -coe_projectionOnto_apply]

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
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f = (↑(p.prodEquivOfIsCompl f.ker ⋯) ∘ₗ id.prodMap 0) ∘ₗ ↑(p.prodEquivOfIsCompl f.ker ⋯).symm

Tactic:
LinearEquiv.eq_comp_toLinearMap_symm

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f ∘ₗ ↑(p.prodEquivOfIsCompl f.ker ⋯) = ↑(p.prodEquivOfIsCompl f.ker ⋯) ∘ₗ id.prodMap 0
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_2.right
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm

Tactic:
LinearEquiv.eq_comp_toLinearMap_symm

Goal state after:
case refine_2.right
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ g ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯) = snd R M P
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
⊢ ↑p.length ≤ height x

Tactic:
by_cases hlen0 : p.length ≠ 0

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : p.length ≠ 0
⊢ ↑p.length ≤ height x

case neg
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
x : α
hlast : RelSeries.last p ≤ x
hlen0 : ¬p.length ≠ 0
⊢ ↑p.length ≤ height x
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

Tactic:
obtain ⟨p, hp, hlen⟩ := Order.exists_series_of_le_height x (n := 2) h

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
x : α
h : 2 ≤ height x
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = 2
⊢ ∃ y, ∃ z < y, y < x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y z : α
hzy : z < y
hyx : y < x
p : LTSeries α := RelSeries.fromListIsChain [z, y, x] ⋯ ⋯
⊢ RelSeries.last p = x

Tactic:
simp [p, ← RelSeries.getLast_toList]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α = ⊤ ↔ InfiniteDimensionalOrder α

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ krullDim_eq_top⟩
  cases isEmpty_or_nonempty α
  · simp [krullDim_eq_bot] at h
  cases finiteDimensionalOrder_or_infiniteDimensionalOrder α
  · rw [krullDim_eq_length_of_finiteDimensionalOrder] at h
    cases h
  · infer_instance

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₃
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
m : M
n₁ n₂ : N
⊢ (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m, n₁) + FreeAddMonoid.of (m, n₂)) =
    (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m, n₁ + n₂))

Tactic:
by simp_rw [map_add, FreeAddMonoid.lift_eval_of, map_add]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf : ∀ (i : Fin l), (f i.castSucc, f i.succ) ∈ {(a, b) | a < b}
bl : { length := l, toFun := f, step := mf }.length < Fintype.card α
⊢ { length := l, toFun := f, step := mf } ∈ Finset.map (injStrictMono (Fintype.card α)) Finset.univ

Tactic:
Finset.mem_map,

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf : ∀ (i : Fin l), (f i.castSucc, f i.succ) ∈ {(a, b) | a < b}
bl : { length := l, toFun := f, step := mf }.length < Fintype.card α
⊢ ∃ a ∈ Finset.univ, (injStrictMono (Fintype.card α)) a = { length := l, toFun := f, step := mf }
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case ind.a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ ∀ y < n, height y < ↑n

Tactic:
simp +contextual only [ih, Nat.cast_lt, implies_true]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
P₂ : Type u_17
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid P₂
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R₂ P₂
inst✝¹ : Module R P
inst✝ : Module R Q
g h : M ⊗[R] N ⊗[R] P ⊗[R] Q →ₛₗ[σ₁₂] P₂
H : ∀ (w : M) (x : N) (y : P) (z : Q), g (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) = h (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)
⊢ g = h

Tactic:
by
  ext w x y z
  exact H w x y z

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
P : Type u_4
Q : Type u_5
S : Type u_6
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommGroup P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
⊢ ∀ (n : ℕ) (a : M ⊗[R] N), ↑n.succ • a = ↑n • a + a

Tactic:
by simp [add_comm, TensorProduct.add_smul]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
l : Finset ι
S : ι → Set α
x✝ : α
⊢ (∃ x ∈ (↑l).pi S, ∏ i ∈ l, x i = x✝) ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x✝

Tactic:
mem_pi,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
l : Finset ι
S : ι → Set α
x✝ : α
⊢ (∃ x, (∀ i ∈ ↑l, x i ∈ S i) ∧ ∏ i ∈ l, x i = x✝) ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x✝
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
S : Type u_11
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R S
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] P
g : N →ₗ[R] Q
g' : S →ₗ[R] N
⊢ map f g ∘ₗ lTensor M g' = map f (g ∘ₗ g')

Tactic:
by
  simp only [lTensor, ← map_comp, comp_id]

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
⊢ M * N = span R (↑M * ↑N)

Tactic:
simp [← span_mul_span]

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
n : ℕ
M : Submodule R Aᵐᵒᵖ
⊢ map (↑(opLinearEquiv R).symm) (M ^ n) = map (↑(opLinearEquiv R).symm) M ^ n

Tactic:
rw [← comap_equiv_eq_map_symm, ← comap_equiv_eq_map_symm, comap_op_pow]

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

Goal state before:
pp: α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
⊢ (↑t).Pairwise (IsRelPrime on s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, s x ∣ z

Tactic:
exact Finset.induction_on t (fun _ _ ↦ one_dvd z)
    (by
      intro a r har ih Hs Hs1
      rw [Finset.prod_insert har]
      have aux1 : a ∈ (↑(insert a r) : Set I) := Finset.mem_insert_self a r
      refine
        (IsRelPrime.prod_right fun i hir ↦
              Hs aux1 (Finset.mem_insert_of_mem hir) <| by
                rintro rfl
                exact har hir).mul_dvd
          (Hs1 a aux1) (ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi)
      simp only [Finset.coe_insert, Set.subset_insert])

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
m : ℕ
H : IsRelPrime x y
⊢ IsRelPrime (x ^ m) y

Tactic:
rw [← Finset.card_range m, ← Finset.prod_const]
  exact IsRelPrime.prod_left fun _ _ ↦ H

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

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
⊢ span R (SetSemiring.down (s + t)) * P = span R (SetSemiring.down s) * P + span R (SetSemiring.down t) * P

Tactic:
SetSemiring.down_add,

Goal state after:
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
⊢ span R (SetSemiring.down s ∪ SetSemiring.down t) * P =
    span R (SetSemiring.down s) * P + span R (SetSemiring.down t) * P
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
G : Type u_2
inst✝³ : FunLike G S R✝
inst✝² : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
⊢ (r ∈ pi fun i ↦ map (Pi.evalRingHom R i) I) ↔ r ∈ I

Tactic:
mem_pi,

Goal state after:
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
G : Type u_2
inst✝³ : FunLike G S R✝
inst✝² : RingHomClass F R✝ S
ι✝ : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
inst✝ : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
⊢ (∀ (i : ι), r i ∈ map (Pi.evalRingHom R i) I) ↔ r ∈ I
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
N : Submodule R M
⊢ span R ({r} • ↑N) = r • N

Tactic:
simpa using span_eq (r • N)

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

Goal state before:
pp: case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x * y / gcd x y = 0
⊢ x = 0 ∨ y = 0

Tactic:
mul_div_assoc _ (gcd_dvd_right _ _),

Goal state after:
case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x * (y / gcd x y) = 0
⊢ x = 0 ∨ y = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ 0 = x * y

Tactic:
rw [EuclideanDomain.gcd_eq_zero_iff] at h

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : x = 0 ∧ y = 0
⊢ 0 = x * y