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

Goal state before:
pp: R : Type u
S : Type u₁
T : Type u_1
inst✝¹⁰ : Monoid R
inst✝⁹ : Monoid S
inst✝⁸ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : DistribMulAction R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction S B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring B₁
inst✝ : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse ⇑φ' ⇑φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ g 0 = 0

Tactic:
← f.map_zero,

Goal state after:
R : Type u
S : Type u₁
T : Type u_1
inst✝¹⁰ : Monoid R
inst✝⁹ : Monoid S
inst✝⁸ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : DistribMulAction R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction S B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring B₁
inst✝ : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse ⇑φ' ⇑φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ g (f 0) = 0
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
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
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_2_to_3 : (Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
e : N ≃ₗ[R] M × P
e₁ : f = ↑e.symm ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ ↑e
this : Injective ⇑f
⊢ Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id

Tactic:
exact ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 = ↑m
⊢ y = p.toFun i.succ

Tactic:
change Fin.insertNth _ _ _ _ = _
          rw [Fin.insertNth_apply_above]
          swap
          · change i.1 + 1 < m.1 + 1; lia
          simp only [Fin.pred_succ, eq_rec_constant]
          congr; ext; exact hm.symm

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ span R (image2 (fun m n ↦ (f m) n) s t) ≤ map₂ f (span R s) (span R t)

Tactic:
span_le,

Goal state after:
case a
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ image2 (fun m n ↦ (f m) n) s t ⊆ ↑(map₂ f (span R s) (span R t))
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ (p.take i).last = p.toFun i

Tactic:
by simp [take, last, Fin.last]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℕ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : i ≤ j
⊢ p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, hj⟩ + i

Tactic:
induction j, hij using Nat.le_induction with
  | base => simp
  | succ j _hij ih =>
    specialize ih (Nat.lt_of_succ_lt hj)
    have step : p ⟨j, _⟩ < p ⟨j + 1, _⟩ := p.step ⟨j, by lia⟩
    lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: p : LTSeries ℤ
i✝ j✝ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j : ℕ
hj : j < p.length + 1
hij : i ≤ j
⊢ p.toFun ⟨i, hi⟩ + ↑j ≤ p.toFun ⟨j, hj⟩ + ↑i

Tactic:
induction j, hij using Nat.le_induction with
  | base => simp
  | succ j _hij ih =>
    specialize ih (Nat.lt_of_succ_lt hj)
    have step : p ⟨j, _⟩ < p ⟨j + 1, _⟩ := p.step ⟨j, by lia⟩
    lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ height ⊤ ≤ ⨆ p, ↑p.length

pp: case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ ⨆ p, ↑p.length ≤ height ⊤

Tactic:
· exact height_le fun p _ ↦ le_iSup_of_le p le_rfl

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ ⨆ p, ↑p.length ≤ height ⊤
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
φ ψ : M ⊗[R] N ⊗[R] (P ⊗[R] Q) →ₛₗ[σ₁₂] P₂
H : ∀ (w : M) (x : N) (y : P) (z : Q), φ (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) = ψ (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z))
m : M
n : N
p : P
q : Q
⊢ (((mk R P Q).compr₂ₛₗ ((((mk R M N).compr₂ₛₗ ((mk R (M ⊗[R] N) (P ⊗[R] Q)).compr₂ₛₗ φ)) m) n)) p) q =
    (((mk R P Q).compr₂ₛₗ ((((mk R M N).compr₂ₛₗ ((mk R (M ⊗[R] N) (P ⊗[R] Q)).compr₂ₛₗ ψ)) m) n)) p) q

Tactic:
exact H m n p q

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
φ ψ : M ⊗[R] (N ⊗[R] P) ⊗[R] Q →ₛₗ[σ₁₂] P₂
H : ∀ (w : M) (x : N) (y : P) (z : Q), φ (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z) = ψ (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z)
m : M
n : N
p : P
q : Q
⊢ ((((mk R N P).compr₂ₛₗ (((mk R M (N ⊗[R] P)).compr₂ₛₗ ((mk R (M ⊗[R] (N ⊗[R] P)) Q).compr₂ₛₗ φ)) m)) n) p) q =
    ((((mk R N P).compr₂ₛₗ (((mk R M (N ⊗[R] P)).compr₂ₛₗ ((mk R (M ⊗[R] (N ⊗[R] P)) Q).compr₂ₛₗ ψ)) m)) n) p) q

Tactic:
exact H m n p q

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
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : CommSemiring A
inst✝⁸ : Module A M
inst✝⁷ : Module A N
inst✝⁶ : SMulCommClass R A M
inst✝⁵ : CommSemiring S
inst✝⁴ : Module S M
inst✝³ : SMulCommClass R S M
inst✝² : SMulCommClass A S M
inst✝¹ : CompatibleSMul R A M N
inst✝ : CompatibleSMul A R M N
x x✝¹ x✝ : M ⊗[A] N
h : (mapOfCompatibleSMul A R S M N) ((mapOfCompatibleSMul R A S M N).toFun x✝¹) = x✝¹
h' : (mapOfCompatibleSMul A R S M N) ((mapOfCompatibleSMul R A S M N).toFun x✝) = x✝
⊢ (mapOfCompatibleSMul A R S M N) ((mapOfCompatibleSMul R A S M N).toFun (x✝¹ + x✝)) = x✝¹ + x✝

Tactic:
simpa using congr($h + $h')

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
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : CommSemiring A
inst✝⁸ : Module A M
inst✝⁷ : Module A N
inst✝⁶ : SMulCommClass R A M
inst✝⁵ : CommSemiring S
inst✝⁴ : Module S M
inst✝³ : SMulCommClass R S M
inst✝² : SMulCommClass A S M
inst✝¹ : CompatibleSMul R A M N
inst✝ : CompatibleSMul A R M N
x x✝¹ x✝ : M ⊗[R] N
h : (mapOfCompatibleSMul R A S M N).toFun ((mapOfCompatibleSMul A R S M N) x✝¹) = x✝¹
h' : (mapOfCompatibleSMul R A S M N).toFun ((mapOfCompatibleSMul A R S M N) x✝) = x✝
⊢ (mapOfCompatibleSMul R A S M N).toFun ((mapOfCompatibleSMul A R S M N) (x✝¹ + x✝)) = x✝¹ + x✝

Tactic:
simpa using congr($h + $h')

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
⊢ False

Tactic:
suffices h'' : f (p i) < f x by
      obtain ⟨n', hn'⟩ : ∃ (n' : ℕ), n' = height (f (p i)) := ENat.ne_top_iff_exists.mp
        ((height_mono h''.le).trans_lt (h' ▸ ENat.natCast_lt_top _)).ne
      have h_lt : n' < n := ENat.natCast_lt_natCast.mp
        (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.natCast_lt_top _))
      have := (length_le_height_last (p := p.take i)).trans <| ih n' h_lt (p i) hn'.symm
      rw [RelSeries.take_length, ENat.natCast_sub, Nat.cast_add, Nat.cast_one, tsub_le_iff_right,
        add_assoc, add_comm _ (_ + 1), ← add_assoc, ← mul_add_one] at this
      refine not_lt_of_ge ?_ (h_len.trans_le this)
      gcongr
      rwa [← ENat.natCast_one, ← ENat.natCast_add, ENat.natCast_le_natCast]

Goal state after:
case coe.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
⊢ f (p.toFun i) < f x
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case mp
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
x : M
inst✝ : SMulCommClass R R ↥N
h : x ∈ sR • N
⊢ ∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m ↦ r • m)

Tactic:
set_smul_eq_map

Goal state after:
case mp
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
x : M
inst✝ : SMulCommClass R R ↥N
h : x ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)
⊢ ∃ c, ↑c.support ⊆ sR ∧ x = ↑(c.sum fun r m ↦ r • m)
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
⊢ Submodule.map₂ (mk R M N) ⊤ ⊤ = ⊤

Tactic:
← top_le_iff,

Goal state after:
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
⊢ ⊤ ≤ Submodule.map₂ (mk R M N) ⊤ ⊤
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ IsCoprime ↑a ↑b

Tactic:
use u, v

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ ↑u * ↑a + ↑v * ↑b = 1
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
neg_right_iff

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

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

Tactic:
neg_right_iff

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime x y ↔ IsRelPrime x y
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: case h
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
i : Fin n
⊢ ∀ (j : Fin n), val i ≤ val j ↔ (fun i ↦ ↑↑⋯.choose) i ≤ (fun i ↦ ↑↑⋯.choose) j

Tactic:
j

Goal state after:
case h
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
⊢ val i ≤ val j ↔ (fun i ↦ ↑↑⋯.choose) i ≤ (fun i ↦ ↑↑⋯.choose) j
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ (r • 1) • m ∈ N

Tactic:
smul_one_smul

Goal state after:
case refine_1
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ r • m ∈ N
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ span s ≤ comap f (Submodule.span S (⇑f '' s))

Tactic:
span_le,

Goal state after:
case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ s ⊆ ↑(comap f (Submodule.span S (⇑f '' s)))
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ b * c = b * (b * c / b)

Tactic:
have := Classical.dec

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
⊢ b * c = b * (b * c / b)
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s : Multiset α
⊢ (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd

Tactic:
by
  refine s.induction_on ?_ fun b s ih ↦ ?_
  · simp_rw [map_zero, gcd_zero, mul_zero]
  · simp_rw [map_cons, gcd_cons, ← gcd_mul_left]
    rw [ih]
    apply ((normalize_associated a).mul_right _).gcd_eq_right

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

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ α

Tactic:
exact gcd {x ∈ s | f x ≠ 0} f

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ (s.inf f).radical = (f i).radical

Tactic:
rw [← radicalInfTopHom_apply, map_finset_inf, ← Finset.inf'_eq_inf ⟨_, hi⟩]

Goal state after:
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ s.inf' ⋯ (⇑radicalInfTopHom ∘ f) = (f i).radical
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case mk.mk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a✝ : Associates α
a : α
b✝ : Associates α
b : α
⊢ Associated
    (Quotient.map₂ gcd ⋯ (Quot.mk (⇑(Associated.setoid α)) a) (Quot.mk (⇑(Associated.setoid α)) b) *
      Quotient.map₂ lcm ⋯ (Quot.mk (⇑(Associated.setoid α)) a) (Quot.mk (⇑(Associated.setoid α)) b))
    (Quot.mk (⇑(Associated.setoid α)) a * Quot.mk (⇑(Associated.setoid α)) b)

Tactic:
associated_iff_eq

Goal state after:
case mk.mk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a✝ : Associates α
a : α
b✝ : Associates α
b : α
⊢ Quotient.map₂ gcd ⋯ (Quot.mk (⇑(Associated.setoid α)) a) (Quot.mk (⇑(Associated.setoid α)) b) *
      Quotient.map₂ lcm ⋯ (Quot.mk (⇑(Associated.setoid α)) a) (Quot.mk (⇑(Associated.setoid α)) b) =
    Quot.mk (⇑(Associated.setoid α)) a * Quot.mk (⇑(Associated.setoid α)) b
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
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j ↦ ↑(v.repr ↑j).support
S' : ↑J → Set M := fun j ↦ ⇑v '' S j
b : M
hb : b ∈ range ⇑v
i : ι
hi : v i = b
this : ⊤ ≤ comap (↑v.repr) (Finsupp.supported R R (⋃ j, S j))
⊢ b ∈ ⋃ j, S' j

Tactic:
replace : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j) := this trivial

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j ↦ ↑(v.repr ↑j).support
S' : ↑J → Set M := fun j ↦ ⇑v '' S j
b : M
hb : b ∈ range ⇑v
i : ι
hi : v i = b
this : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j)
⊢ b ∈ ⋃ j, S' j
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
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Infinite ↑J
⊢ #↑(range ⇑v) ≤ #↑J

Tactic:
let S : J → Set ι := fun j => ↑(v.repr j).support
    let S' : J → Set M := fun j => v '' S j
    have hs : range v ⊆ ⋃ j, S' j := by
      intro b hb
      rcases mem_range.1 hb with ⟨i, hi⟩
      have : span R J ≤ comap v.repr.toLinearMap (Finsupp.supported R R (⋃ j, S j)) :=
        span_le.2 fun j hj x hx => ⟨_, ⟨⟨j, hj⟩, rfl⟩, hx⟩
      rw [hJ] at this
      replace : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j) := this trivial
      rw [v.repr_self, Finsupp.mem_supported, Finsupp.support_single _ one_ne_zero] at this
      · subst b
        rcases mem_iUnion.1 (this (Finset.mem_singleton_self _)) with ⟨j, hj⟩
        exact mem_iUnion.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩
    refine le_of_not_gt fun IJ => ?_
    suffices #(⋃ j, S' j) < #(range v) by exact not_le_of_gt this ⟨Set.embeddingOfSubset _ _ hs⟩
    refine lt_of_le_of_lt (le_trans Cardinal.mk_iUnion_le_sum_mk
      (Cardinal.sum_le_sum _ (fun _ => ℵ₀) ?_)) ?_
    · exact fun j => (Cardinal.lt_aleph0_of_finite _).le
    · simpa

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

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

Tactic:
rw [diagonal_transpose]

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
⊢ 0 < Module.rank R M ↔ Nontrivial M

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ rank_pos_of_free⟩
  rw [← not_subsingleton_iff_nontrivial]
  intro h'
  simp only [rank_subsingleton', lt_self_iff_false] at h

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

Goal state before:
pp: case hd
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank R M < ℵ₀

Tactic:
· exact Module.rank_lt_aleph0 _ _

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (∃ n, ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, toNat (Module.rank R (Fin n → R)) ≤ 0

Tactic:
Nat.le_zero,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (∃ n, ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, toNat (Module.rank R (Fin n → R)) = 0
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
R : Type u_7
α : Type v
inst✝⁴ : Fintype m
inst✝³ : Mul α
inst✝² : AddCommMonoid α
inst✝¹ : DistribSMul R α
inst✝ : SMulCommClass R α α
x : R
v w : m → α
⊢ v ⬝ᵥ x • w = x • (v ⬝ᵥ w)

Tactic:
by simp [dotProduct, Finset.smul_sum, mul_smul_comm]

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

Goal state before:
pp: case succ
n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
m : ℕ
ih : ∀ (i j : n), 0 ≤ (A ^ m) i j
i : n
⊢ ∀ (j : n), 0 ≤ (A ^ (m + 1)) i j

Tactic:
j

Goal state after:
case succ
n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
m : ℕ
ih : ∀ (i j : n), 0 ≤ (A ^ m) i j
i j : n
⊢ 0 ≤ (A ^ (m + 1)) i j
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Nontrivial R
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero, mem_nonZeroDivisors_iff_ne_zero, ne_eq, zero_eq_bot,
      span_singleton_eq_bot]

Goal state after: