mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_1
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ ↑n < height x ↔ ∃ y < x, height y = ↑n

Tactic:
exact coe_lt_height_iff hfin

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ height x = ↑n + 1 ↔ (∃ y < x, height y = ↑n + 1 - 1) ∧ ∀ y < x, height y < ↑n + 1

Tactic:
rw [height_eq_coe_add_one_iff]

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ (height x < ⊤ ∧ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n) ↔
    (∃ y < x, height y = ↑n + 1 - 1) ∧ ∀ y < x, height y < ↑n + 1
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_2
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
⊢ ((t₁.smash t₃ H).toFun ∘ ⇑{ toFun := Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length), inj' := ⋯ })
      (Fin.last { length := n + 1, toFun := s, step := h }.length) =
    t₂ m

Tactic:
simpa using! RelSeries.last_smash ..

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:
by
  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.RelSeries

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
⊢ s.length < Fintype.card α

Tactic:
by_contra! h

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
⊢ False
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocCommSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
x✝¹ x✝ : A
⊢ ((mul R A).flip x✝¹) x✝ = ((mul R A) x✝¹) x✝

Tactic:
simp [mul_comm]

Goal state after:
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
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ (map f g).range = Submodule.map₂ (mk R P Q) f.range g.range

Tactic:
by
  simp_rw [← Submodule.map_top, Submodule.map₂_map_map, ← map₂_mk_top_top_eq_top,
    Submodule.map_map₂]
  rfl

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

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

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

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

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 + a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ ≤ 1 + a * a∗

Tactic:
by
    rw [add_le_iff] at this
    nth_rw 1 [← mul_one a∗]
    exact (mul_right_mono this.1).trans (kstar_mul_le_self this.2)

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

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

Tactic:
rwa [mul_zero, zero_add, mul_comm] at H

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

Goal state before:
pp: R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
⊢ Pairwise (IsCoprime on fun i ↦ s ↑i) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)

Tactic:
by
  rw [Finset.pairwise_subtype_iff_pairwise_finset']
  refine ⟨fun hp i hi ↦ IsCoprime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
  · rw [Finset.mem_sdiff, Finset.mem_singleton] at hj
    exact (hp hj.1 hi hj.2).symm
  · rintro i hi j hj h
    apply IsCoprime.prod_right_iff.mp (hp i hi)
    exact Finset.mem_sdiff.mpr ⟨hj, fun f ↦ h (Finset.mem_singleton.mp f).symm⟩

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
r : R
h : R ∙ (algebraMap R A) r = 1
r' : R
eq : r' • (algebraMap R A) r = (algebraMap R A) 1
⊢ ∃ r_1, (algebraMap R A) r = (algebraMap R A) ↑r_1

Tactic:
rw [Algebra.smul_def, ← map_mul, (FaithfulSMul.algebraMap_injective R A).eq_iff] at eq

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
h : R ∙ (algebraMap R A) r = 1
r' : R
eq : r' * r = 1
⊢ ∃ r_1, (algebraMap R A) r = (algebraMap R A) ↑r_1
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
h : R ∙ x = 1
⊢ ∃ r, x = (algebraMap R A) ↑r

Tactic:
obtain ⟨r, rfl⟩ := mem_one.mp (h ▸ mem_span_singleton_self x)
    have ⟨r', eq⟩ := mem_span_singleton.mp (h ▸ algebraMap_mem 1)
    rw [Algebra.smul_def, ← map_mul, (FaithfulSMul.algebraMap_injective R A).eq_iff] at eq
    exact ⟨.mkOfMulEqOne _ _ (mul_comm _ r ▸ eq), rfl⟩

Goal state after:
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
x : R
⊢ (∃ x_1 ∈ I.prod J, (RingHom.fst R S) x_1 = x) → x ∈ I

Tactic:
rintro ⟨x, ⟨h, rfl⟩⟩

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ I.prod J
⊢ (RingHom.fst R S) x ∈ I
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
x : S
⊢ (∃ x_1 ∈ I.prod J, (RingHom.snd R S) x_1 = x) → x ∈ J

Tactic:
rintro ⟨x, ⟨h, rfl⟩⟩

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ I.prod J
⊢ (RingHom.snd R S) x ∈ J
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1.refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
r : R
y : M
h : y ∈ ⇑(algebraMap S R) '' s • N
h' : y ∈ s • restrictScalars S N
c : R →₀ ↥N
c_supp : ↑c.support ⊆ ⇑(algebraMap S R) '' s
hc : r • y = ↑(c.sum fun r m ↦ r • m)
⊢ ∑ x ∈ c.support, x • ↑(c x) ∈ s • restrictScalars S N

Tactic:
refine sum_mem fun u u_in ↦ ?_

Goal state after:
case refine_1.refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
r : R
y : M
h : y ∈ ⇑(algebraMap S R) '' s • N
h' : y ∈ s • restrictScalars S N
c : R →₀ ↥N
c_supp : ↑c.support ⊆ ⇑(algebraMap S R) '' s
hc : r • y = ↑(c.sum fun r m ↦ r • m)
u : R
u_in : u ∈ c.support
⊢ u • ↑(c u) ∈ s • restrictScalars S N
Module: Mathlib.RingTheory.OrzechProperty

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
⊢ Injective ⇑f

Tactic:
have := small_of_surjective hg

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this : Small.{max u ?u.51, v} M
⊢ Injective ⇑f
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
rw [hpq]

Goal state after:
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ 0 / q ∣ 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
⊢ b ∣ c / a

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)
  · simp only [div_zero, dvd_zero]
  rcases h with ⟨d, rfl⟩
  refine ⟨d, ?_⟩
  rw [mul_assoc, mul_div_cancel_left₀ _ ha]

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

Goal state before:
pp: case mp.refine_3
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)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
⊢ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • f i) = (ax.sum fun i c ↦ c • f i) + ay.sum fun i c ↦ c • f i

Tactic:
refine ⟨ax + ay, fun i => I.add_mem (hax i) (hay i), Finsupp.sum_add_index' ?_ ?_⟩

Goal state after:
case mp.refine_3.refine_1
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)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
⊢ ∀ (a : ι), 0 • f a = 0

case mp.refine_3.refine_2
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)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
⊢ ∀ (a : ι) (b₁ b₂ : R), (b₁ + b₂) • f a = b₁ • f a + b₂ • f a
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f
x : R
h : ∀ (m : M), x • m = 0
m : M
⊢ x • f m = 0

Tactic:
← map_smul,

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f
x : R
h : ∀ (m : M), x • m = 0
m : M
⊢ f (x • m) = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : EuclideanDomain R
inst✝ : CommRing S
e : S ≃+* R
a b : S
hb : b ≠ 0
⊢ ¬EuclideanDomain.r (e (a * b)) (e a)

Tactic:
by
    have hb' : e b ≠ 0 := by simpa using hb
    simpa using! EuclideanDomain.mul_left_not_lt (e a) hb'

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

Goal state before:
pp: a b : ℕ
⊢ Associated (a.gcd b * a.lcm b) (a * b)

Tactic:
Nat.gcd_mul_lcm

Goal state after:
a b : ℕ
⊢ Associated (a * b) (a * b)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ (image g s).lcm f = s.lcm (f ∘ g)

Tactic:
classical induction s using Finset.induction <;> simp [*]

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₂.gcd f = GCDMonoid.gcd (∅.gcd f) (s₂.gcd f)

Tactic:
gcd_empty,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ s₂.gcd f = GCDMonoid.gcd 0 (s₂.gcd f)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ (image g s).gcd f = s.gcd (f ∘ g)

Tactic:
classical induction s using Finset.induction <;> simp [*]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
a✝ : GCDMonoid α
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
⊢ a ∣ n

Tactic:
rw [← mul_dvd_mul_iff_left h0, ← ha]

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
a✝ : GCDMonoid α
h0 : ¬gcd k m = 0
a : α
ha : k = gcd k m * a
⊢ k ∣ gcd k m * n
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : 0 ∣ a
hdk : d₁ ^ k = 0
⊢ False

Tactic:
apply absurd (zero_dvd_iff.mp h3) ha

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
⊢ gcd x y * 1 = gcd x (gcd x y * y')

Tactic:
← ey,

Goal state after:
α : 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
⊢ gcd x y * 1 = gcd x y
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
⊢ Nontrivial R

Tactic:
by_contra! h

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : Subsingleton R
⊢ False
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
n m : R
⊢ Ideal.span {n} ⊓ Ideal.span {m} = Ideal.span {lcm n m}

Tactic:
rw [Ideal.ext_iff]
  intro x
  rw [Ideal.mem_inf]
  simp only [Ideal.mem_span_singleton]
  exact lcm_dvd_iff.symm

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ 0 < finrank R M ↔ Nontrivial M

Tactic:
by
  rw [← not_subsingleton_iff_nontrivial, ← iff_not_comm]
  simp [Module.finrank_eq_zero_iff_of_free]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
ι : Type u_10
s : Finset ι
u : ι → m → α
v : m → α
⊢ (∑ i ∈ s, u i) ⬝ᵥ v = ∑ i ∈ s, u i ⬝ᵥ v

Tactic:
by
  simp only [dotProduct, Finset.sum_apply, Finset.sum_mul]
  rw [Finset.sum_comm]

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

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

pp: case mpr
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)
⊢ (∃ c, c.support.card ≤ finrank K ↥(span K s) ∧ ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x) → x ∈ span K s

Tactic:
· 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

Goal state after:
case mpr
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)
⊢ (∃ c, c.support.card ≤ finrank K ↥(span K s) ∧ ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x) → x ∈ span K s
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
i✝ : m
j✝ : n
⊢ (a • M) i✝ j✝ = (M * diagonal fun x ↦ a) i✝ j✝

Tactic:
simp [mul_comm]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec

Tactic:
cases isEmpty_or_nonempty m
  · simp [IsLeftRegular, Function.injective_of_subsingleton]
  exact mul_right_injective_iff_mulVec_injective

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
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι' × ι
⊢ ((b.smulTower' c).repr x) ij = (b.repr ((c.repr x) ij.1)) ij.2

Tactic:
rw [smulTower', repr_reindex_apply, smulTower_repr]

Goal state after:
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
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι' × ι
⊢ (b.repr ((c.repr x) ((Equiv.prodComm ι ι').symm ij).2)) ((Equiv.prodComm ι ι').symm ij).1 =
    (b.repr ((c.repr x) ij.1)) ij.2
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
x : Matrix n n α
⊢ (∀ (g : Matrix n n α), g * x = x * g) ↔ ∃ x_1, (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n) x_1 = x

Tactic:
refine ⟨fun hx ↦ ?_, fun ⟨x, hx, eq⟩ y ↦ eq ▸ scalar_commute x (hx · |>.symm) y |>.symm⟩

Goal state after:
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
x : Matrix n n α
hx : ∀ (g : Matrix n n α), g * x = x * g
⊢ ∃ x_1, (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n) x_1 = x
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
inst✝⁴ : Semiring α
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
r : α
M : Matrix m n α
⊢ (scalar m) r * M = M * (scalar n) r ↔ r • M = MulOpposite.op r • M

Tactic:
scalar_apply,

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_11
inst✝⁴ : Semiring α
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
r : α
M : Matrix m n α
⊢ ((diagonal fun x ↦ r) * M = M * diagonal fun x ↦ r) ↔ r • M = MulOpposite.op r • M
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
⊢ Module.rank R M < ℵ₀ ↔ Module.Finite R M

Tactic:
rw [Free.rank_eq_card_chooseBasisIndex, mk_lt_aleph0_iff]

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
⊢ Finite (ChooseBasisIndex R M) ↔ Module.Finite R M
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
S : Subalgebra R A
inst✝³ : CommSemiring R'
inst✝² : SMul R' R
inst✝¹ : Algebra R' A
inst✝ : IsScalarTower R' R A
x : R'
⊢ x • 1 ∈ S

Tactic:
← smul_one_smul R x (1 : A),

Goal state after:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
S : Subalgebra R A
inst✝³ : CommSemiring R'
inst✝² : SMul R' R
inst✝¹ : Algebra R' A
inst✝ : IsScalarTower R' R A
x : R'
⊢ (x • 1) • 1 ∈ S
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case refine_2
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ 0 * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

Tactic:
exact (zero_mul b).symm ▸ Submodule.zero_mem _

Goal state after: