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

Goal state before:
pp: case neg
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
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : ¬x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0

Tactic:
hp hps h1,

Goal state after:
case neg
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
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : ¬x.coeff p.1 = 0
⊢ x.coeff p.1 * 0 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : MulOneClass M
⊢ ∀ (n : ℕ), single 1 ↑(n + 1) = single 1 ↑n + 1

Tactic:
by simp [one_def]

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
m : M
r : R
⊢ single m r ^ 0 = single (m ^ 0) (r ^ 0)

Tactic:
by simp [one_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
r : α → α → Prop
inst✝⁷ : DecidableRel r
inst✝⁶ : IsTrans α r
inst✝⁵ : Std.Antisymm r
inst✝⁴ : Std.Total r
r' : β → β → Prop
inst✝³ : DecidableRel r'
inst✝² : IsTrans β r'
inst✝¹ : Std.Antisymm r'
inst✝ : Std.Total r'
l : List α
h : ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) l → ∀ (b : α), b ∈ Quot.mk (⇑(isSetoid α)) l → (r a b ↔ r' (f a) (f b))
⊢ ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → decide (r a b) = decide (r' (f a) (f b))

Tactic:
by simpa using h

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

Goal state before:
pp: R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst✝ : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
he : ∀ (x : M'), e x = (Finsupp.mapRange.addEquiv e₁.toAddEquiv) (e₃ (e₂.symm x))
⊢ Free R' M'

Tactic:
let e' : M' ≃ₗ[R'] (I →₀ R') :=
    { __ := e, map_smul' := fun m x ↦ Finsupp.ext fun i ↦ by simp [e₁, he, map_smulₛₗ] }

Goal state after:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst✝ : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
he : ∀ (x : M'), e x = (Finsupp.mapRange.addEquiv e₁.toAddEquiv) (e₃ (e₂.symm x))
e' : M' ≃ₗ[R'] I →₀ R' :=
  let __spread.0 := e;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Free R' M'
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
⊢ (∃ α, ∃ (h : ∀ (g : R), g * α = α * g), ∀ (x : M), f x = (smulLeft α ⋯) x) →
    ∀ (g : End R M) (x : M), g (f x) = f (g x)

Tactic:
by simp_all

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

Goal state before:
pp: case refine_1
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
a0 : G
ha0 : a0 ∈ A
hc : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ∈ C
b0 : G
hb0 : b0 ∈ B
hd : { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ∈ D
hne : { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0 ≠ 1 ∨ { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0 ≠ 1
hu' : UniqueMul C D ({ toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } a0) ({ toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } b0)
⊢ (a0, b0) ≠ (a, b)

Tactic:
simp_rw [Function.Embedding.coeFn_mk, Ne, inv_mul_eq_one, mul_inv_eq_one] at hne
        rwa [Ne, Prod.mk_inj, not_and_or, eq_comm]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).support = p.support.erase n

Tactic:
by
  simp [support]

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
q : Submodule R E
F : Type u_7
inst✝¹ : AddCommGroup F
inst✝ : Module R F
i : F →ₗ[R] E
hi : Function.Injective ⇑i
h : IsCompl i.range q
x : E
hx : x ∈ q
⊢ (linearProjOfIsCompl q i hi h) x = 0

Tactic:
by
  simpa [LinearMap.linearProjOfIsCompl]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
ha : a ∈ s
hst : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → x = y
hb : a ∈ t
⊢ ∃ x, x ∈ s ∧ (∀ (x_1 : α), x_1 ∈ s → x_1 = x) ∧ x ∈ t ∧ ∀ (x_1 : α), x_1 ∈ t → x_1 = x

Tactic:
exact ⟨a, ha, (hst · · _ hb), hb, (hst _ ha · · |>.symm)⟩

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mp
α : 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

Tactic:
rintro ⟨i, rfl⟩
    exact Fin.lastCases (Or.inr <| Fin.append_right _ _ 0) (fun i => Or.inl ⟨⟨i.1, i.2⟩,
      (Fin.append_left _ _ _).symm⟩) i

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
⊢ p.length ≠ 0

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case pos
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : i.succ = Fin.last p.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length 0) = p.toFun i.succ

Tactic:
Fin.addCases_right,

Goal state after:
case pos
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : i.succ = Fin.last p.length
⊢ q.toFun 0 = p.toFun i.succ
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr.inl.mp
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ n ≤ (LTSeries.longestOf α).length → ∃ l, l.length = n

Tactic:
exact fun H ↦ ⟨(LTSeries.longestOf α).take ⟨_, Nat.lt_succ_of_le H⟩, rfl⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

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

Tactic:
apply iSup_le
    intro p
    suffices p.length ≤ ⨆ (a : α), height a from (WithBot.unbotD_le_iff fun _ => this).mp this
    apply le_iSup_of_le p.last (length_le_height_last (p := p))

Goal state after:
Module: Mathlib.Order.RelSeries

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

Tactic:
wlog h₁ : s.head = ⊥
  · obtain ⟨t, i, hi, ht⟩ := this (s.cons ⊥ (bot_lt_iff_ne_bot.mpr h₁)) rfl
    exact ⟨t, ⟨fun j ↦ i (j.succ.cast (by simp)), fun _ _ ↦ by simp⟩,
      funext fun j ↦ (congr_fun hi _).trans (RelSeries.cons_cast_succ _ _ _ _), ht⟩
  wlog h₂ : s.last = ⊤
  · obtain ⟨t, i, hi, ht⟩ := this (s.snoc ⊤ (lt_top_iff_ne_top.mpr h₂)) (by simp [h₁]) (by simp)
    exact ⟨t, ⟨fun j ↦ i (.cast (by simp) j.castSucc), fun _ _ ↦ by simp⟩,
      funext fun j ↦ (congr_fun hi _).trans (RelSeries.snoc_cast_castSucc _ _ _ _), ht⟩
  obtain ⟨t, i, hit, hi₁, hi₂⟩ := s.exists_relSeries_covBy
  refine ⟨t, i, hit, ?_, ?_⟩
  · rw [← h₁, RelSeries.head, RelSeries.head, ← hi₁, ← hit, Function.comp]
  · rw [← h₂, RelSeries.last, RelSeries.last, ← hi₂, ← hit, Function.comp]

Goal state after:
Module: Mathlib.Order.KrullDimension

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

Tactic:
by
  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.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
r s : R
m : M
n : N
⊢ (r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n

Tactic:
simp_rw [smul_tmul, tmul_smul, mul_smul]

Goal state after:
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 : ℕ
⊢ 1 = id

Tactic:
Module.End.one_eq_id

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 : ℕ
⊢ id = id
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✝ : IsScalarTower R A A
a : A
n : ℕ
⊢ 1 = id

Tactic:
Module.End.one_eq_id

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n : ℕ
⊢ id = id
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: 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
⊢ sR • N = map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)

Tactic:
apply set_smul_eq_of_le
  · intro r n hr hn
    exact ⟨Finsupp.single r ⟨n, hn⟩, Finsupp.single_mem_supported _ _ hr, by simp⟩
  · intro x hx
    obtain ⟨c, hc, rfl⟩ := hx
    simp only [LinearMap.coe_comp, coe_subtype, Finsupp.coe_lsum, Finsupp.sum, Function.comp_apply]
    rw [AddSubmonoid.coe_finsetSum]
    refine Submodule.sum_mem (p := sR • N) (t := c.support) ?_ _ ⟨sR • N, ?_⟩
    · rintro r hr
      rw [mem_set_smul_def, Submodule.mem_sInf]
      rintro p hp
      exact hp (hc hr) (c r).2
    · ext x : 1
      simp only [Set.mem_iInter, SetLike.mem_coe]
      fconstructor
      · refine fun h ↦ h fun r n hr hn ↦ ?_
        rw [mem_set_smul_def, mem_sInf]
        exact fun p hp ↦ hp hr hn
      · simp_all

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

Goal state before:
pp: case zero
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
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n
⊢ ∃ m n, 0 = m ⊗ₜ[R] n

Tactic:
use 0, 0
    rw [TensorProduct.zero_tmul]

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

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
m : M
hr : r ∈ s
hm : m ∈ t • x
⊢ r • m ∈ (s * t) • x

Tactic:
by
      have : SMulCommClass R R x := ⟨fun r s m => Subtype.ext <| smul_comm _ _ _⟩
      obtain ⟨c, hc1, rfl⟩ := mem_set_smul _ _ _ |>.mp hm
      rw [Finsupp.sum, AddSubmonoid.coe_finsetSum]
      simp only [SetLike.val_smul, Finset.smul_sum, smul_smul]
      exact Submodule.sum_mem _ fun r' hr' ↦
        mem_set_smul_of_mem_mem (Set.mul_mem_mul hr (hc1 hr')) (c _).2

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

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
M₂ : Type u_12
N₂ : Type u_14
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R₂ M₂
inst✝ : Module R₂ N₂
f₁ f₂ : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
⊢ map (f₁ + f₂) g = map f₁ g + map f₂ g

Tactic:
by
  ext
  simp only [add_tmul, compr₂ₛₗ_apply, mk_apply, map_tmul, add_apply]

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

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

Tactic:
rwa [mul_comm, add_mul]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : IsCoprime x z
⊢ IsCoprime x (y * z)

Tactic:
rw [isCoprime_comm] at H1 H2 ⊢
  exact H1.mul_left H2

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 (z * y + x) y

Tactic:
rw [add_comm]
  exact h.add_mul_right_left z

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semifield R
m : R
⊢ IsCoprime m 0 ↔ m ≠ 0 ∨ 0 ≠ 0

pp: case inr
R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Tactic:
· simp [isCoprime_zero_right]

Goal state after:
case inr
R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsNoetherian R M
inst✝ : Nontrivial R
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
i : ι
x✝ : R ∙ v i = ⊥
⊢ v i = 0

Tactic:
by simp_all

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

Goal state before:
pp: case add
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x✝ y✝ : R'
hx✝ : x✝ ∈ span R' s
hy✝ : y✝ ∈ span R' s
ihr : x✝ • n ∈ s • N
ihs : y✝ • n ∈ s • N
⊢ (x✝ + y✝) • n ∈ s • N

Tactic:
rw [add_smul]; exact Submodule.add_mem _ ihr ihs

Goal state after:
Module: Mathlib.Algebra.Ring.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : HasDistribNeg M
a b : M
h : Associated a b
u : Mˣ
hu : a * ↑u = b
⊢ -a * ↑(-u) = b

Tactic:
simp [hu]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p / q ∣ p

Tactic:
use q

Goal state after:
case h
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p = p / q * q
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i j : ι
this : DecidableEq ι := Classical.decEq ι
h✝ : ¬i = j
⊢ 0 ∈ I

Tactic:
· exact I.zero_mem

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : J ⊔ K = ⊤
⊢ I * K ⊔ J = I ⊔ J

Tactic:
rw [sup_comm, sup_mul_eq_of_coprime_right h, sup_comm]

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ s₂.lcm f = GCDMonoid.lcm 1 (s₂.lcm f)

Tactic:
lcm_one_left,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ s₂.lcm f = normalize (s₂.lcm f)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
⊢ x ∈ Ideal.span {1 - Pi.single i 1}

Tactic:
simp only [RingHom.mem_ker, Pi.evalRingHom_apply] at hx

Goal state after:
ι : Type u_1
inst✝¹ : DecidableEq ι
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx : x i = 0
⊢ x ∈ Ideal.span {1 - Pi.single i 1}
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case h
ι : Type u_1
inst✝¹ : DecidableEq ι
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx : x i = 0
⊢ x = (1 - Pi.single i 1) * (x + Pi.single i 1)

Tactic:
simp [mul_add, sub_mul, one_mul, ← Pi.single_mul_left, hx]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
x y x' y' : α
ex : x = gcd x y * x'
ey : y = gcd x y * y'
h : gcd x y ≠ 0
⊢ IsUnit (gcd x' y')

Tactic:
by
  rw [← associated_one_iff_isUnit]
  refine Associated.of_mul_left ?_ (Associated.refl <| gcd x y) h
  convert (gcd_mul_left' (gcd x y) x' y').symm
  rw [← ex, ← ey, mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
⊢ (if a = 0 then b else if b = 0 then a else Classical.choose ⋯) ∣ a

Tactic:
by
      split_ifs with h h_1
      · rw [h]
        apply dvd_zero
      · exact dvd_rfl
      have h0 : lcm a b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹a = 0› h
        · exact absurd ‹b = 0› h_1
      rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b), mul_comm,
        mul_dvd_mul_iff_right h]
      apply dvd_lcm_right

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝ : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
f : ι ↪ ι'
this : Infinite ι'
w₂ : lift.{w, w'} #ι' ≤ lift.{w', w} #ι
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
exact le_antisymm w₁ w₂

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

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b c : G₀
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ if c = 0 ∧ b = 0 then 0 else 1

Tactic:
by simp_all

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
⊢ v ⬝ᵥ 0 = 0

Tactic:
by simp [dotProduct]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
⊢ 0 ⬝ᵥ v = 0

Tactic:
by simp [dotProduct]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocRing α
v w : m → α
⊢ -v ⬝ᵥ w = -(v ⬝ᵥ w)

Tactic:
by simp [dotProduct]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocRing α
v w : m → α
⊢ v ⬝ᵥ -w = -(v ⬝ᵥ w)

Tactic:
by simp [dotProduct]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
x : M
inst✝ : Module.Finite K ↥(span K s)
⊢ x ∈ span K s ↔ ∃ c, c.support.card ≤ finrank K ↥(span K s) ∧ ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x

Tactic:
by
  constructor
  · intro h
    rcases exists_finset_span_eq_linearIndepOn K s with ⟨t, ht_sub, ht_card, ht_span, ht_indep⟩
    rcases mem_span_set.mp (ht_span ▸ h) with ⟨c, hct, hx⟩
    refine ⟨c, ?_, hct.trans ht_sub, hx⟩
    exact ht_card ▸ Finset.card_mono hct
  · rintro ⟨c, -, hcs, hx⟩
    exact mem_span_set.mpr ⟨c, hcs, hx⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ z * i * x + i * i ^ n + y * x = 1

Tactic:
· rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]
        simpa

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
M : Matrix l m α
x : m → α
y : n → α
⊢ M * vecMulVec x y = vecMulVec (M *ᵥ x) y

Tactic:
by
  ext
  simp_rw [mul_apply, vecMulVec_apply, mulVec, dotProduct, Finset.sum_mul, mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
⊢ LinearIndependent R fun p ↦ b p.1 • c p.2

Tactic:
by
  rw [← linearIndependent_equiv' (.prodComm ..) (g := fun p : ι' × ι ↦ b p.2 • c p.1) rfl,
    LinearIndependent, linearCombination_smul]
  simpa using! Function.Injective.comp hc
    ((mapRange_injective _ (map_zero _) hb).comp <| Equiv.injective _)

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
this : x = inclusion ⋯ ⟨↑x, hi⟩
| iUnionLift S f hf (iUnion S) ⋯ (u x)

Tactic:
rw [this, hui, iUnionLift_inclusion]

Goal state after:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
this : x = inclusion ⋯ ⟨↑x, hi⟩
| f i (ui i ⟨↑x, hi⟩)
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_4
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
x✝ : R
h : x✝ ∈ I
⊢ x✝ - 0 ∈ I

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
inst✝ : Subsingleton (Subalgebra R B)
f g : A ≃ₐ[R] B
⊢ f = g

Tactic:
by rw [← f.symm_symm, Subsingleton.elim f.symm g.symm, g.symm_symm]

Goal state after: