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

Goal state before:
pp: case pos
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : j = j'
⊢ ((Pi.basis s).repr (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

pp: case neg
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ((Pi.basis s).repr (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

Tactic:
· subst hj
    simp only [Pi.basis, LinearEquiv.trans_apply,
      LinearEquiv.piCongrRight, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
      Basis.repr_symm_apply, LinearEquiv.coe_mk]
    symm
    simp [Finsupp.single_apply]

Goal state after:
case neg
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ((Pi.basis s).repr (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : i = j
⊢ ((Finsupp.basis b).repr (single ⟨i, x⟩.fst ((b ⟨i, x⟩.fst) ⟨i, x⟩.snd))) ⟨j, y⟩ = (single ⟨i, x⟩ 1) ⟨j, y⟩

Tactic:
cases h
        simp [Finsupp.single_apply_left sigma_mk_injective]

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
h : sSup s < ⊤
⊢ s.Finite

Tactic:
by
  contrapose! h
  simp only [top_le_iff]
  exact sSup_eq_top_of_infinite h

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝⁴ : Semiring S
M : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst✝¹ : AddCommMonoid E
inst✝ : Module S E
p : E →ₗ[S] M
⊢ (∀ (x : E), q (p x) = p x) ↔ p.range ≤ q.range

Tactic:
← hq.mem_range_iff,

Goal state after:
S : Type u_5
inst✝⁴ : Semiring S
M : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst✝¹ : AddCommMonoid E
inst✝ : Module S E
p : E →ₗ[S] M
⊢ (∀ (x : E), p x ∈ q.range) ↔ p.range ≤ q.range
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝⁴ : Semiring S
M : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst✝¹ : AddCommMonoid E
inst✝ : Module S E
p : E →ₗ[S] M
⊢ (∀ (x : E), ∃ y, q y = p x) ↔ ∀ ⦃x : M⦄ (x_1 : E), p x_1 = x → ∃ y, q y = x

Tactic:
forall_apply_eq_imp_iff

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ ∀ (i : ℕ) (_hi : i + 1 < x.length + 1), (x.toList[i], x.toList[i + 1]) ∈ r

Tactic:
add_lt_add_iff_right

Goal state after:
α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ ∀ (i : ℕ) (_hi : i < x.length), (x.toList[i], x.toList[i + 1]) ∈ r
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_2.left
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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
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
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ f = ↑(LinearEquiv.ofBijective ((↑l).prod g) ⋯).symm ∘ₗ inl R M P

Tactic:
LinearEquiv.eq_toLinearMap_symm_comp

Goal state after:
case refine_2.left
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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
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
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ ↑(LinearEquiv.ofBijective ((↑l).prod g) ⋯) ∘ₗ f = inl R M P
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4.h
α : 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 : ↑m < ↑i
⊢ ↑m + 1 < ↑i + 1

Tactic:
add_lt_add_iff_right

Goal state after:
case e'_4.h
α : 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 : ↑m < ↑i
⊢ ↑m < ↑i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case zero
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
snoc : (p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)
p : RelSeries r
heq : p.length = 0
⊢ motive p

Tactic:
convert! singleton p.head
      ext n
      · exact heq
      · simp [show n = 0 by lia, apply_zero]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case zero
α : Type u_1
r : SetRel α α
q : RelSeries r
toFun✝ : Fin (0 + 1) → α
step✝ : ∀ (i : Fin 0), (toFun✝ i.castSucc, toFun✝ i.succ) ∈ r
h : { length := 0, toFun := toFun✝, step := step✝ }.last = q.head
⊢ ({ length := 0, toFun := toFun✝, step := step✝ }.smash q h).head =
    { length := 0, toFun := toFun✝, step := step✝ }.head

pp: case succ
α : Type u_1
r : SetRel α α
q : RelSeries r
n✝ : ℕ
toFun✝ : Fin (n✝ + 1 + 1) → α
step✝ : ∀ (i : Fin (n✝ + 1)), (toFun✝ i.castSucc, toFun✝ i.succ) ∈ r
h : { length := n✝ + 1, toFun := toFun✝, step := step✝ }.last = q.head
⊢ ({ length := n✝ + 1, toFun := toFun✝, step := step✝ }.smash q h).head =
    { length := n✝ + 1, toFun := toFun✝, step := step✝ }.head

Tactic:
· simpa [Fin.addCases] using! h.symm

Goal state after:
case succ
α : Type u_1
r : SetRel α α
q : RelSeries r
n✝ : ℕ
toFun✝ : Fin (n✝ + 1 + 1) → α
step✝ : ∀ (i : Fin (n✝ + 1)), (toFun✝ i.castSucc, toFun✝ i.succ) ∈ r
h : { length := n✝ + 1, toFun := toFun✝, step := step✝ }.last = q.head
⊢ ({ length := n✝ + 1, toFun := toFun✝, step := step✝ }.smash q h).head =
    { length := n✝ + 1, toFun := toFun✝, step := step✝ }.head
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ ↑(height ⊤) = krullDim α

Tactic:
by
  rw [krullDim_eq_iSup_length]
  simp only [WithBot.coe_inj]
  apply le_antisymm
  · exact height_le fun p _ ↦ le_iSup_of_le p le_rfl
  · exact iSup_le fun _ => length_le_height le_top

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b : A
⊢ Commute (mulLeft R a) (mulRight R b)

Tactic:
ext c

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b c : A
⊢ (mulLeft R a * mulRight R b) c = (mulRight R b * mulLeft R a) c
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
x : A ⊗[R] A
⊢ ∀ (x y : A ⊗[R] A),
    (mul' R A).toFun (a • x) = (RingHom.id A) a • (mul' R A).toFun x →
      (mul' R A).toFun (a • y) = (RingHom.id A) a • (mul' R A).toFun y →
        (mul' R A).toFun (a • (x + y)) = (RingHom.id A) a • (mul' R A).toFun (x + y)

Tactic:
by simp +contextual [mul_add]

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

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

Tactic:
by
  rw [sub_eq_add_neg, ← mul_neg, add_mul_left_right_iff]

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

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

Tactic:
by
  rw [sub_eq_add_neg, ← mul_neg, add_mul_left_right_iff]

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : 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
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
| val i ≤ val j

Tactic:
rw [← hi.choose_spec, ← hj.choose_spec]

Goal state after:
α : 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
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
| sli[↑hi.choose] ≤ sli[↑hj.choose]
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: 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✝¹
inst✝¹ : IsScalarTower R A A
S T : Set A
M✝ N P Q : Submodule R A
m n : A
ι : Sort uι
inst✝ : IsReduced A
M : Submodule R A
hM : IsNilpotent M
⊢ M = ⊥

Tactic:
Submodule.eq_bot_iff

Goal state after:
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✝¹
inst✝¹ : IsScalarTower R A A
S T : Set A
M✝ N P Q : Submodule R A
m n : A
ι : Sort uι
inst✝ : IsReduced A
M : Submodule R A
hM : IsNilpotent M
⊢ ∀ x ∈ M, x = 0
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons.mp.refine_2.refine_1.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ (∏ j ∈ t \ {x}, s j) * s a = ∏ j ∈ insert a t \ {x}, s j

Tactic:
rw [prod_eq_prod_sdiff_singleton_mul (mem x hx) _]

Goal state after:
case cons.mp.refine_2.refine_1.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ (∏ j ∈ t \ {x}, s j) * s a = (∏ x ∈ (insert a t \ {x}) \ {a}, s x) * s a
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case h.e_a.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ ∏ j ∈ insert a t \ {x}, s j = (∏ j ∈ t \ {x}, s j) * s a

Tactic:
rw [prod_eq_prod_sdiff_singleton_mul (mem x hx) _]

Goal state after:
case h.e_a.e_a
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ (∏ x ∈ (insert a t \ {x}) \ {a}, s x) * s a = (∏ j ∈ t \ {x}, s j) * s a
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
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective ⇑l
⊢ IsNoetherian R M ↔ IsNoetherian S P

Tactic:
simp_rw [isNoetherian_iff']
  let e := Submodule.orderIsoMapComapOfBijective l hl
  exact ⟨fun _ ↦ e.symm.strictMono.wellFoundedGT, fun _ ↦ e.strictMono.wellFoundedGT⟩

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

Goal state before:
pp: 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'
hr : r ∈ ↑(Ideal.span s)
hn : n ∈ N
⊢ r • n ∈ s • N

Tactic:
induction hr using Submodule.span_induction with
        | mem _ h => exact mem_set_smul_of_mem_mem h hn
        | zero => rw [zero_smul]; exact Submodule.zero_mem _
        | add _ _ _ _ ihr ihs => rw [add_smul]; exact Submodule.add_mem _ ihr ihs
        | smul _ _ hr =>
          rw [mem_span_set] at hr
          obtain ⟨c, hc, rfl⟩ := hr
          rw [Finsupp.sum, Finset.smul_sum, Finset.sum_smul]
          refine Submodule.sum_mem _ fun i hi => ?_
          rw [← mul_smul, smul_eq_mul, mul_comm, mul_smul]
          exact mem_set_smul_of_mem_mem (hc hi) <| Submodule.smul_mem _ _ hn

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = 0 ∧ b = 0 → gcd a b = 0

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
⊢ gcd 0 0 = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map f.symm.toRingHom (map f.toRingHom I) = I

Tactic:
map_map,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map (f.symm.toRingHom.comp f.toRingHom) I = I
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 (∅.lcm f) (s₂.lcm f)

Tactic:
empty_union,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ s₂.lcm f = GCDMonoid.lcm (∅.lcm f) (s₂.lcm f)
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:
empty_union,

Goal state after:
α : 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)
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
x : M
⊢ x ∈ S ↔ ∃ s, x = s • generator S

Tactic:
@eq_comm _ x,

Goal state after:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
x : M
⊢ x ∈ S ↔ ∃ s, s • generator S = x
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
p n : R
hp : Irreducible p
⊢ IsCoprime p n ↔ ¬p ∣ n

Tactic:
by rw [← isRelPrime_iff_isCoprime, hp.isRelPrime_iff_not_dvd]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ Ideal.span {gcd x y} = Ideal.span {IsBezout.gcd x y}

Tactic:
IsBezout.span_gcd_eq_span_gcd

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ Ideal.span {IsBezout.gcd x y} = Ideal.span {IsBezout.gcd x y}
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommMonoidWithZero α
x✝ : IsGCDMonoid α
a✝ : GCDMonoid α
this : NormalizationMonoid α
⊢ Nonempty (NormalizedGCDMonoid α)

Tactic:
classical exact ⟨normalizedGCDMonoidOfExistsGCD fun _ _ ↦ ⟨_, fun _ ↦ (dvd_gcd_iff ..).symm⟩⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : CommMonoidWithZero α
x✝ : IsCancelMulZero α ∧ ∀ (a b : α), ∃ c, ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c
left✝ : IsCancelMulZero α
h : ∀ (a b : α), ∃ c, ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c
⊢ IsGCDMonoid α

Tactic:
by classical exact ⟨gcdMonoidOfExistsGCD h⟩

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddGroupWithOne α
i j : n
d : ℤ
⊢ ↑d i j = ↑(if i = j then d else 0)

Tactic:
rw [Int.cast_ite, Int.cast_zero, ← diagonal_intCast, diagonal_apply]

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

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∉ t
j : ι
hj : j ∈ t
⊢ (f j).IsPrime

Tactic:
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_

Goal state after:
case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∉ t
j : ι
hj : j ∈ t
⊢ j ≠ a

case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∉ t
j : ι
hj : j ∈ t
⊢ j ≠ b
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:
simp only [dotProduct, Finset.sum_apply, Finset.sum_mul]
  rw [Finset.sum_comm]

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

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
⊢ (f j).IsPrime

Tactic:
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_

Goal state after:
case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
⊢ j ≠ a

case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
⊢ j ≠ b
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
i : m
j : n
a : α
⊢ r • single i j a = single i j (r • a)

Tactic:
by
  unfold single
  ext
  simp [smul_ite]

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

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
j : ι
hj : j ∈ t
⊢ (f j).IsPrime

Tactic:
refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_

Goal state after:
case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
j : ι
hj : j ∈ t
⊢ j ≠ a

case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
j : ι
hj : j ∈ t
⊢ j ≠ b
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j k : n
⊢ diagonal (fun x ↦ M i i) j k = M j k

Tactic:
obtain rfl | hkl := Decidable.eq_or_ne j k

Goal state after:
case inr.inl
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j : n
⊢ diagonal (fun x ↦ M i i) j j = M j j

case inr.inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j k : n
hkl : j ≠ k
⊢ diagonal (fun x ↦ M i i) j k = M j k
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:
smulTower',

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.smulTower c).reindex (Equiv.prodComm ι ι')).repr x) ij = (b.repr ((c.repr x) ij.1)) ij.2