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

Goal state before:
pp: 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✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid N'
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid P'
inst✝⁵ : Module R M
inst✝⁴ : Module R M'
inst✝³ : Module R N
inst✝² : Module R N'
inst✝¹ : Module R P
inst✝ : Module R P'
f₁₂ : M →ₗ[R] N
f₂₃ : N →ₗ[R] P
g₁₂ : M' →ₗ[R] N'
g₂₃ : N' →ₗ[R] P'
e₁ : M ≃ₗ[R] M'
e₂ : N ≃ₗ[R] N'
e₃ : P ≃ₗ[R] P'
h₁₂ : g₁₂ ∘ₗ ↑e₁ = ↑e₂ ∘ₗ f₁₂
h₂₃ : g₂₃ ∘ₗ ↑e₂ = ↑e₃ ∘ₗ f₂₃
H : Exact ⇑f₁₂ ⇑f₂₃
⊢ Exact ⇑g₁₂ ⇑g₂₃

Tactic:
by
  rwa [iff_of_ladder_linearEquiv h₁₂ h₂₃]

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
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ T = T.range.projection T.ker ⋯

Tactic:
by
  convert! ofIsCompl_subtype_zero_eq hT.isCompl
  exact ofIsCompl_eq _ (by simp [hT.isProj_range.map_id]) (by simp) |>.symm

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝⁴ : Semiring S
M : Type u_7
inst✝³ : AddCommGroup M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_8
inst✝¹ : AddCommGroup E
inst✝ : Module S E
p : M →ₗ[S] E
⊢ p ∘ₗ q = p ↔ q.ker ≤ p.ker

Tactic:
by
  simp [hq.ker_eq_range, range_le_ker_iff, comp_sub, sub_eq_zero, eq_comm]

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

Goal state before:
pp: G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #A * #B
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
by
    obtain ⟨hA, hB, -⟩ := Nat.one_lt_mul_iff.mp hc
    rw [card_pos] at hA hB
    rw [← card_product] at hc
    obtain ⟨a0, ha0, b0, hb0, he0⟩ := mem_mul.mp (max'_mem _ <| hA.mul hB)
    obtain ⟨a1, ha1, b1, hb1, he1⟩ := mem_mul.mp (min'_mem _ <| hA.mul hB)
    have : UniqueMul A B a0 b0 := by
      intro a b ha hb he
      obtain hl | rfl | hl := lt_trichotomy b b0
      · exact ((he0 ▸ he ▸ mul_lt_mul_right hl a).not_ge <| le_max' _ _ <| mul_mem_mul ha hb0).elim
      · exact ⟨mul_right_cancel he, rfl⟩
      · exact ((he0 ▸ mul_lt_mul_right hl a0).not_ge <| le_max' _ _ <| mul_mem_mul ha0 hb).elim
    refine ⟨_, mk_mem_product ha0 hb0, _, mk_mem_product ha1 hb1, fun he ↦ ?_, this, ?_⟩
    · rw [Prod.mk_inj] at he; rw [he.1, he.2, he1] at he0
      obtain ⟨⟨a2, b2⟩, h2, hne⟩ := exists_mem_ne hc (a0, b0)
      rw [mem_product] at h2
      refine (min'_lt_max' _ (mul_mem_mul ha0 hb0) (mul_mem_mul h2.1 h2.2) fun he ↦ hne ?_).ne he0
      exact Prod.ext_iff.mpr (this h2.1 h2.2 he.symm)
    · intro a b ha hb he
      obtain hl | rfl | hl := lt_trichotomy b b1
      · exact ((he1 ▸ mul_lt_mul_right hl a1).not_ge <| min'_le _ _ <| mul_mem_mul ha1 hb).elim
      · exact ⟨mul_right_cancel he, rfl⟩
      · exact ((he1 ▸ he ▸ mul_lt_mul_right hl a).not_ge <| min'_le _ _ <| mul_mem_mul ha hb1).elim

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

Goal state before:
pp: R : Type u_1
inst✝¹² : Ring R
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[R] N₂
g' : N₂ →ₗ[R] N₃
τ₁ : M₁ →ₗ[R] N₁
τ₂ : M₂ →ₗ[R] N₂
τ₃ : M₃ →ₗ[R] N₃
comm₁₂ : f' ∘ₗ τ₁ = τ₂ ∘ₗ f
comm₂₃ : g' ∘ₗ τ₂ = τ₃ ∘ₗ g
h₁ : Function.Surjective ⇑τ₁
h₂ : Function.Bijective ⇑τ₂
h₃ : Function.Injective ⇑τ₃
⊢ f'.toAddMonoidHom.comp τ₁.toAddMonoidHom = τ₂.toAddMonoidHom.comp f.toAddMonoidHom

Tactic:
by ext; apply DFunLike.congr_fun comm₁₂

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
h : ∀ (a : α) (b : β), f a < b → ∃ a', a < a' ∧ f a' = b
a : α
⊢ coheight a = coheight (f a)

Tactic:
by
  refine le_antisymm (Order.coheight_le_coheight_apply_of_strictMono _ hf _) ?_
  refine coheight_le_iff'.mpr fun p hp ↦ ?_
  induction p using RelSeries.inductionOn generalizing a with
  | singleton x => simp
  | cons p x hx ih =>
    simp only [RelSeries.head_cons] at hp
    obtain ⟨a', haa', ha'⟩ := h a p.head (by grind)
    grw [RelSeries.cons_length, Nat.cast_add, Nat.cast_one, ih a' ha'.symm]
    exact coheight_add_one_le haa'

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
obtain ⟨⟨p, hlast⟩, hlen⟩ := exists_eq_iSup_of_iSup_eq_coe ha

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : ↑(↑⟨p, hlast⟩).length = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ
α : 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 := ⋯ }
⊢ ∃ t i,
    t.toFun ∘ ⇑i = { length := n + 1, toFun := s, step := h }.toFun ∧
      i 0 = 0 ∧ i (Fin.last { length := n + 1, toFun := s, step := h }.length) = Fin.last t.length

Tactic:
have H : t₁.last = t₂ 0 := (congr(t₁ $hi₂.symm).trans (congr_fun ht _)).trans h₁.symm

Goal state after:
case succ
α : 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 i,
    t.toFun ∘ ⇑i = { length := n + 1, toFun := s, step := h }.toFun ∧
      i 0 = 0 ∧ i (Fin.last { length := n + 1, toFun := s, step := h }.length) = Fin.last t.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last < x

Tactic:
← hp

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last < RelSeries.last p
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < x

Tactic:
← hp

Goal state after:
case h.left
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ p.toFun ⟨n, ⋯⟩ < RelSeries.last p
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m✝ : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝
m : WithBot ℕ∞
hm : ∀ (i : LTSeries α), ↑i.length ≤ m
⊢ ⊤ ≤ m

Tactic:
by
    rw [top_le_iff, ENat.WithBot.eq_top_iff_forall_ge]
    intro n
    simpa using hm (LTSeries.withLength _ n)

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

Goal state before:
pp: case cons
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
h : ι
tl : List ι
ih : (∀ i ∈ tl, g i ∈ f i) → (List.map g tl).prod ∈ (List.map f tl).prod
hg : ∀ i ∈ h :: tl, g i ∈ f i
⊢ g h * (List.map g tl).prod ∈ f h * (List.map f tl).prod

Tactic:
exact mul_mem_mul (hg h List.mem_cons_self)
      (ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi)

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

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : a * c ≤ c
⊢ a∗ * c ≤ c

Tactic:
kstar_mul_le_self ha

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : a * c ≤ c
⊢ c ≤ c
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure S * closure T ≤ closure (S * T)

pp: case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure (S * T) ≤ closure S * closure T

Tactic:
· refine mul_le.2 fun a ha b hb => ?_
    rw [← AddMonoidHom.mulRight_apply, ← AddSubmonoid.mem_comap]
    refine (closure_le.2 fun a' ha' => ?_) ha
    change b ∈ (closure (S * T)).comap (AddMonoidHom.mulLeft a')
    refine (closure_le.2 fun b' hb' => ?_) hb
    change a' * b' ∈ closure (S * T)
    exact subset_closure (Set.mul_mem_mul ha' hb')

Goal state after:
case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ closure (S * T) ≤ closure S * closure T
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]
⊢ ∀ (a b : α), (decide (a ≤ b) || decide (b ≤ a)) = true

Tactic:
simpa using le_total

Goal state after:
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
⊢ 1 ≤ toAddSubmonoid 1

Tactic:
rintro x ⟨n, rfl⟩
  exact ⟨n, show (n : R) • (1 : A) = n by rw [Nat.cast_smul_eq_nsmul, nsmul_one]⟩

Goal state after:
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
I J : Submodule R A
N : Submodule R M
mn : A
hmn : mn ∈ I ⊔ J
p : M
hp : p ∈ N
⊢ mn • p ∈ I • N ⊔ J • N

Tactic:
by
    obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn
    rw [add_smul]; exact add_mem_sup (smul_mem_smul hm hp) <| smul_mem_smul hn hp

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ ⨆ i, map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N) = map f.toLinearMap M * map f.toLinearMap N

Tactic:
rw [mul_eq_map₂]
      apply congr_arg sSup
      ext S
      constructor <;> rintro ⟨y, hy⟩
      · use ⟨f y, mem_map.mpr ⟨y.1, y.2, rfl⟩⟩
        refine Eq.trans ?_ hy
        ext
        simp
      · obtain ⟨y', hy', fy_eq⟩ := mem_map.mp y.2
        use ⟨y', hy'⟩
        refine Eq.trans ?_ hy
        rw [f.toLinearMap_apply] at fy_eq
        ext
        simp [fy_eq]

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

Goal state before:
pp: case zero
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
x : A
hx✝ : x ∈ M ^ 0
hx : x ∈ 1
⊢ C 0 x hx✝

Tactic:
obtain ⟨r, rfl⟩ := mem_one.mp hx

Goal state after:
case zero
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
r : R
hx✝ : (Algebra.algebraMap R A) r ∈ M ^ 0
hx : (Algebra.algebraMap R A) r ∈ 1
⊢ C 0 ((Algebra.algebraMap R A) r) hx✝
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case zero
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
x : A
hx✝ : x ∈ M ^ 0
hx : x ∈ 1
⊢ C 0 x hx✝

Tactic:
obtain ⟨r, rfl⟩ := mem_one.mp hx

Goal state after:
case zero
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
r : R
hx✝ : (Algebra.algebraMap R A) r ∈ M ^ 0
hx : (Algebra.algebraMap R A) r ∈ 1
⊢ C 0 ((Algebra.algebraMap R A) r) hx✝
Module: Mathlib.RingTheory.Coprime.Lemmas

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

Tactic:
refine Finset.induction_on t (iff_of_true isRelPrime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_
  rw [Finset.prod_insert hbt, IsRelPrime.mul_left_iff, ih, Finset.forall_mem_insert]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
T : Type u_1
U : Type u_2
inst✝¹ : Semiring T
inst✝ : Semiring U
f : R →+* S
g : T →+* U
⊢ RingHom.ker (f.prodMap g) = (RingHom.ker f).prod (RingHom.ker g)

Tactic:
ext ⟨⟩

Goal state after:
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
T : Type u_1
U : Type u_2
inst✝¹ : Semiring T
inst✝ : Semiring U
f : R →+* S
g : T →+* U
fst✝ : R
snd✝ : T
⊢ (fst✝, snd✝) ∈ RingHom.ker (f.prodMap g) ↔ (fst✝, snd✝) ∈ (RingHom.ker f).prod (RingHom.ker g)
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1.refine_1
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
x : M
r : S
r_in : r ∈ s
x_in : x ∈ N
⊢ r • x ∈ s • restrictScalars S N

Tactic:
exact mem_set_smul_of_mem_mem r_in x_in

Goal state after:
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
P : Type u_5
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj✝ : Injective ⇑f
p : P
x✝ : ¬p = 0
g : (ℕ →₀ P) →ₗ[R] M
inj : Injective ⇑g
i : ℕ
⊢ g ((Finsupp.lsingle i) p) ≠ 0

Tactic:
simpa [inj]

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

Goal state before:
pp: case zero
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ ⊤ ≤ comap f ⊤

Tactic:
exact rfl.le

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

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

Tactic:
rw [lcm, mul_div_assoc _ (gcd_dvd_right _ _), mul_eq_zero] at hxy

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

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

Tactic:
apply Or.imp_right _ hxy

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
⊢ y / gcd x y = 0 → y = 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).lcm = GCDMonoid.lcm a s.lcm

Tactic:
by
  rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_cons]
  simp

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : Associated (map (fun x ↦ a * x) s).gcd (a * s.gcd)
⊢ Associated (GCDMonoid.gcd (a * b) (map (fun x ↦ a * x) s).gcd) (a * GCDMonoid.gcd b s.gcd)

Tactic:
exact .trans (.gcd .rfl ih) (gcd_mul_left' ..)

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

Goal state before:
pp: a b : ℤ
⊢ a ∣ b ∧ b ∣ a ↔ a.natAbs = b.natAbs

Tactic:
← Int.natAbs_dvd_natAbs,

Goal state after:
a b : ℤ
⊢ a.natAbs ∣ b.natAbs ∧ b ∣ a ↔ a.natAbs = b.natAbs
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ∣ b.natAbs ∧ b ∣ a ↔ a.natAbs = b.natAbs

Tactic:
← Int.natAbs_dvd_natAbs,

Goal state after:
a b : ℤ
⊢ a.natAbs ∣ b.natAbs ∧ b.natAbs ∣ a.natAbs ↔ a.natAbs = b.natAbs
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a✝ : Nontrivial α
⊢ (if 1 = 0 then 1 else Exists.choose ⋯) = 1

Tactic:
← Units.val_inj

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a✝ : Nontrivial α
⊢ ↑(if 1 = 0 then 1 else Exists.choose ⋯) = ↑1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ u * Exists.choose ⋯ = Exists.choose ⋯

Tactic:
← Units.val_inj

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ ↑(u * Exists.choose ⋯) = ↑(Exists.choose ⋯)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
hIJ✝ : ¬I ⊔ J = ⊤
P : Ideal R
hP : P.IsMaximal
hIJ : I ⊔ J ≤ P
⊢ False

Tactic:
exact h P (le_trans le_sup_left hIJ) (le_trans le_sup_right hIJ) hP.isPrime

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ a b, y ∣ b ∧ a * x + b = 1

Tactic:
rintro ⟨a, b, e⟩

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
x y a b : R
e : a * x + b * y = 1
⊢ ∃ a b, y ∣ b ∧ a * x + b = 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a b c : α
⊢ gcd (b * a) (c * a) = gcd b c * normalize a

Tactic:
simp only [mul_comm, gcd_mul_left]

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

Goal state before:
pp: case insert
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : ∏ i ∈ s, J i = ⨅ i ∈ s, J i
hp1 : (↑s).Pairwise (IsCoprime on J)
hp2 : ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
⊢ J a * ⨅ i ∈ s, J i = J a ⊓ ⨅ x ∈ s, J x

Tactic:
Ideal.mul_eq_inf_of_isCoprime (isCoprime_biInf (by grind))

Goal state after:
case insert
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : ∏ i ∈ s, J i = ⨅ i ∈ s, J i
hp1 : (↑s).Pairwise (IsCoprime on J)
hp2 : ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
⊢ J a ⊓ ⨅ j ∈ s, J j = J a ⊓ ⨅ x ∈ s, J x
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionSemiring K
⊢ IsPrincipal ⊥

pp: case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionSemiring K
⊢ IsPrincipal ⊤

Tactic:
· apply bot_isPrincipal

Goal state after:
case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionSemiring K
⊢ IsPrincipal ⊤
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'} #ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
rcases Cardinal.lift_mk_le'.mp w₁ with ⟨f⟩

Goal state after:
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 : ι ↪ ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
S : Set α
M : Matrix m n α
r : l → m
c : o → n
hM : M ∈ S.matrix
⊢ M.submatrix r c ∈ S.matrix

Tactic:
simp_all [Set.mem_matrix]

Goal state after: