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

Goal state before:
pp: case h
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ ∀ (i : ℕ) (h₁ : i < (p.append q connect).toList.length) (h₂ : i < (p.toList ++ q.toList).length),
    (p.append q connect).toList[i] = (p.toList ++ q.toList)[i]

Tactic:
simp [List.getElem_append, Fin.append, Fin.addCases]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
hne : Nonempty { p // RelSeries.last p = a }
⊢ (⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length) + n = ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length + n

Tactic:
iSup_subtype',

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
hne : Nonempty { p // RelSeries.last p = a }
⊢ (⨆ x, ↑(↑x).length) + n = ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length + n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
hne : Nonempty { p // RelSeries.last p = a }
⊢ (⨆ x, ↑(↑x).length) + n = ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length + n

Tactic:
iSup_subtype',

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
hne : Nonempty { p // RelSeries.last p = a }
⊢ (⨆ x, ↑(↑x).length) + n = ⨆ x, ↑(↑x).length + n
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✝⁶ : Ring 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 : Function.Exact ⇑f ⇑g
⊢ f.range = ⊥ ↔ f = 0

Tactic:
LinearMap.range_eq_bot

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring 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 : Function.Exact ⇑f ⇑g
⊢ f = 0 ↔ f = 0
Module: Mathlib.Order.KrullDimension

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

Tactic:
iSup_subtype',

Goal state after:
case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ⨆ x, ↑(↑x).length = ⊤
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = x), ↑p.length = ⊤

Tactic:
iSup_subtype',

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ ⨆ x_1, ↑(↑x_1).length = ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.right
α : 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
⊢ height (p.toFun ⟨n, ⋯⟩) = ↑n

Tactic:
exact height_eq_index_of_length_eq_height_last (by simp [hlen, hp, hx]) ⟨n, by lia⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
motive : M ⊗[R] N → Prop
z : M ⊗[R] N
zero : motive 0
tmul : ∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)
add : ∀ (x y : M ⊗[R] N), motive x → motive y → motive (x + y)
x : FreeAddMonoid (M × N)
x✝ : M × N
y : FreeAddMonoid (M × N)
ih : motive ↑y
m : M
n : N
⊢ motive (↑(FreeAddMonoid.of (m, n)) + ↑y)

Tactic:
exact add _ _ (tmul ..) ih

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
this :
  ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
    (s : LTSeries α), RelSeries.head s = ⊥ → ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤
h₁ : ¬RelSeries.head s = ⊥
t : RelSeries {(a, b) | a ⋖ b}
i : Fin ((RelSeries.cons s ⊥ ⋯).length + 1) ↪ Fin (t.length + 1)
hi : t.toFun ∘ ⇑i = (RelSeries.cons s ⊥ ⋯).toFun
ht : t.head = ⊥ ∧ t.last = ⊤
⊢ ∃ t i, t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

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

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₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
s : R
m : M
n : N
⊢ (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (s • m, n)) =
    (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m, s • n))

Tactic:
by rw [FreeAddMonoid.lift_eval_of, FreeAddMonoid.lift_eval_of, hf]

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

Goal state before:
pp: case negSucc
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
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ congr f g ^ Int.negSucc n = congr (f ^ Int.negSucc n) (g ^ Int.negSucc n)

Tactic:
simp_rw [zpow_negSucc, congr_pow]

Goal state after:
case negSucc
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
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℕ
⊢ (congr (f ^ (n + 1)) (g ^ (n + 1)))⁻¹ = congr (f ^ (n + 1))⁻¹ (g ^ (n + 1))⁻¹
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
x✝¹ x✝ : R
⊢ x✝¹ * t ∈ ⨆ i, S i * T → x✝ * t ∈ ⨆ i, S i * T → (x✝¹ + x✝) * t ∈ ⨆ i, S i * T

Tactic:
simp_rw [right_distrib]; apply add_mem

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
s : Set R
n : ℕ
⊢ closure s ^ (n + 1) = closure (s ^ (n + 1))

Tactic:
by rw [pow_succ, pow_succ, closure_pow s n, closure_mul_closure]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x + b * y)

Tactic:
mul_add

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x) + z * (b * y)
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
rw [isCoprime_comm]
  exact h.symm.add_mul_right_left z

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

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

Tactic:
by
  rw [add_comm]
  exact h.add_mul_right_left z

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
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
⊢ (m + n) • p ∈ I • N ⊔ J • N

Tactic:
rw [add_smul]

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
I J : Submodule R A
N : Submodule R M
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
⊢ m • p + n • p ∈ I • N ⊔ J • N
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
p q : Submodule R Aᵐᵒᵖ
⊢ op (comap (↑(opLinearEquiv R)) (p + q)) = op (comap (↑(opLinearEquiv R)) p) + op (comap (↑(opLinearEquiv R)) q)

Tactic:
by simp [comap_equiv_eq_map_symm, ← op_add]

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 × S)
r : R
s : S
⊢ (r, s) ∈ I ↔ (r, s) ∈ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)

Tactic:
mem_prod,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
r : R
s : S
⊢ (r, s) ∈ I ↔ (r, s).1 ∈ map (RingHom.fst R S) I ∧ (r, s).2 ∈ map (RingHom.snd R S) I
Module: Mathlib.RingTheory.Ideal.Operations

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

Tactic:
rw [add_smul]

Goal state after:
case add
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x✝ y✝ : R'
hx✝ : x✝ ∈ span R' s
hy✝ : y✝ ∈ span R' s
ihr : x✝ • n ∈ s • N
ihs : y✝ • n ∈ s • N
⊢ x✝ • n + y✝ • n ∈ s • N
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (⇑(algebraMap R S) '' ↑I • N) = I • Submodule.restrictScalars R N

Tactic:
← Submodule.coe_set_smul,

Goal state after:
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (⇑(algebraMap R S) '' ↑I • N) = ↑I • Submodule.restrictScalars R N
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
this : (p : Prop) → Decidable p
⊢ b * c = b * (b * c / b)

Tactic:
by_cases b0 : b = 0

Goal state after:
case pos
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : b = 0
⊢ b * c = b * (b * c / b)

case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)
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:
by
    rintro ⟨rfl, rfl⟩
    exact gcd_zero_right _

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
m : M
hm : m ∈ T
r : R
hr : r ∈ Ideal.span S
x✝³ x✝² : R
x✝¹ : x✝³ ∈ span R S
x✝ : x✝² ∈ span R S
h₁ : x✝³ • m ∈ span R (S • T)
h₂ : x✝² • m ∈ span R (S • T)
⊢ (x✝³ + x✝²) • m ∈ span R (S • T)

Tactic:
rw [add_smul]

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
m : M
hm : m ∈ T
r : R
hr : r ∈ Ideal.span S
x✝³ x✝² : R
x✝¹ : x✝³ ∈ span R S
x✝ : x✝² ∈ span R S
h₁ : x✝³ • m ∈ span R (S • T)
h₂ : x✝² • m ∈ span R (S • T)
⊢ x✝³ • m + x✝² • m ∈ span R (S • T)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case H0
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b n s t s' t' : R
p : P a b (0, s, t)
p' : P a b (n, s', t')
⊢ P a b (xgcdAux 0 s t n s' t')

Tactic:
| H0 n =>

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (x * gcdA x y + y * gcdB x y)

Tactic:
mul_add

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (x * gcdA x y) + z * (y * gcdB x y)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : Π₀ (i : ι), M i), r • m = 0
⊢ ∀ (i : ι) (m : M i), r • m = 0

Tactic:
intro i m

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : Π₀ (i : ι), M i), r • m = 0
i : ι
m : M i
⊢ r • m = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
by
  constructor
  · intro hxy
    rw [lcm, mul_div_assoc _ (gcd_dvd_right _ _), mul_eq_zero] at hxy
    apply Or.imp_right _ hxy
    intro hy
    by_cases hgxy : gcd x y = 0
    · rw [EuclideanDomain.gcd_eq_zero_iff] at hgxy
      exact hgxy.2
    · rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
      generalize gcd x y = g at hr hs hy hgxy ⊢
      subst hs
      rw [mul_div_cancel_left₀ _ hgxy] at hy
      rw [hy, mul_zero]
  rintro (hx | hy)
  · rw [hx, lcm_zero_left]
  · rw [hy, lcm_zero_right]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ gcd x y * lcm x y = x * y

Tactic:
rw [lcm]; by_cases h : gcd x y = 0
  · rw [h, zero_mul]
    rw [EuclideanDomain.gcd_eq_zero_iff] at h
    rw [h.1, zero_mul]
  rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
  generalize gcd x y = g at h hr ⊢; subst hr
  rw [mul_assoc, mul_div_cancel_left₀ _ h]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : (i : ι) → M i), r • m = 0
⊢ ∀ (i : ι) (m : M i), r • m = 0

Tactic:
intro i m

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (m : (i : ι) → M i), r • m = 0
i : ι
m : M i
⊢ r • m = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N P : Submodule R M
⊢ (⨆ a ∈ {N, P}, a).annihilator = N.annihilator ⊓ P.annihilator

Tactic:
iSup_subtype',

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N P : Submodule R M
⊢ (⨆ x, ↑x).annihilator = N.annihilator ⊓ P.annihilator
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
I : Ideal S
N : Submodule R M
⊢ restrictScalars S (Ideal.map (algebraMap S R) I • N) = I • restrictScalars S N

Tactic:
have := N.restrictScalars_image_smul_eq (I : Set S)

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
I : Ideal S
N : Submodule R M
this : restrictScalars S (⇑(algebraMap S R) '' ↑I • N) = ↑I • restrictScalars S N
⊢ restrictScalars S (Ideal.map (algebraMap S R) I • N) = I • restrictScalars S N
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

Tactic:
by
    by_cases h : a ∈ s; swap; · simp [IH, h]
    simp only [h, dedup_cons_of_mem, IH, gcd_cons]
    unfold gcd
    rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]
    apply (associated_normalize _).gcd_eq_left

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
m : Ideal R
inst✝ : m.IsMaximal
hk : RingHom.ker f ≤ m
h : m ⊔ RingHom.ker f = ⊤
⊢ False

Tactic:
sup_of_le_left hk

Goal state after:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
m : Ideal R
inst✝ : m.IsMaximal
hk : RingHom.ker f ≤ m
h : m = ⊤
⊢ False
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

Tactic:
rcases hna.lt_or_gt with ha | ha

Goal state after:
case inl
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : a < 0
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1

case inr
a b : ℤ
hna : a ≠ 0
hnb : b ≠ 0
ha : 0 < a
⊢ (if 0 ≤ a * b then 1 else -1) = (if 0 ≤ a then 1 else -1) * if 0 ≤ b then 1 else -1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ [IsCoprime I J, IsCoprime I J, IsCoprime I J, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE

Tactic:
← isCoprime_iff_exists,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ [IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J, I ⊔ J = ⊤].TFAE
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case mk.mk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
toIsCancelMulZero✝¹ : IsCancelMulZero α
gcd✝¹ lcm✝¹ : α → α → α
gcd_dvd_left✝¹ : ∀ (a b : α), gcd✝¹ a b ∣ a
gcd_dvd_right✝¹ : ∀ (a b : α), gcd✝¹ a b ∣ b
dvd_gcd✝¹ : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd✝¹ c b
gcd_mul_lcm✝¹ : ∀ (a b : α), Associated (gcd✝¹ a b * lcm✝¹ a b) (a * b)
lcm_zero_left✝¹ : ∀ (a : α), lcm✝¹ 0 a = 0
lcm_zero_right✝¹ : ∀ (a : α), lcm✝¹ a 0 = 0
toIsCancelMulZero✝ : IsCancelMulZero α
gcd✝ lcm✝ : α → α → α
gcd_dvd_left✝ : ∀ (a b : α), gcd✝ a b ∣ a
gcd_dvd_right✝ : ∀ (a b : α), gcd✝ a b ∣ b
dvd_gcd✝ : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd✝ c b
gcd_mul_lcm✝ : ∀ (a b : α), Associated (gcd✝ a b * lcm✝ a b) (a * b)
lcm_zero_left✝ : ∀ (a : α), lcm✝ 0 a = 0
lcm_zero_right✝ : ∀ (a : α), lcm✝ a 0 = 0
hgcd : gcd = gcd
hlcm : lcm = lcm
⊢ { toIsCancelMulZero := toIsCancelMulZero✝¹, gcd := gcd✝¹, lcm := lcm✝¹, gcd_dvd_left := gcd_dvd_left✝¹,
      gcd_dvd_right := gcd_dvd_right✝¹, dvd_gcd := dvd_gcd✝¹, gcd_mul_lcm := gcd_mul_lcm✝¹,
      lcm_zero_left := lcm_zero_left✝¹, lcm_zero_right := lcm_zero_right✝¹ } =
    { toIsCancelMulZero := toIsCancelMulZero✝, gcd := gcd✝, lcm := lcm✝, gcd_dvd_left := gcd_dvd_left✝,
      gcd_dvd_right := gcd_dvd_right✝, dvd_gcd := dvd_gcd✝, gcd_mul_lcm := gcd_mul_lcm✝,
      lcm_zero_left := lcm_zero_left✝, lcm_zero_right := lcm_zero_right✝ }

Tactic:
dsimp only at hgcd hlcm

Goal state after:
case mk.mk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
toIsCancelMulZero✝¹ : IsCancelMulZero α
gcd✝¹ lcm✝¹ : α → α → α
gcd_dvd_left✝¹ : ∀ (a b : α), gcd✝¹ a b ∣ a
gcd_dvd_right✝¹ : ∀ (a b : α), gcd✝¹ a b ∣ b
dvd_gcd✝¹ : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd✝¹ c b
gcd_mul_lcm✝¹ : ∀ (a b : α), Associated (gcd✝¹ a b * lcm✝¹ a b) (a * b)
lcm_zero_left✝¹ : ∀ (a : α), lcm✝¹ 0 a = 0
lcm_zero_right✝¹ : ∀ (a : α), lcm✝¹ a 0 = 0
toIsCancelMulZero✝ : IsCancelMulZero α
gcd✝ lcm✝ : α → α → α
gcd_dvd_left✝ : ∀ (a b : α), gcd✝ a b ∣ a
gcd_dvd_right✝ : ∀ (a b : α), gcd✝ a b ∣ b
dvd_gcd✝ : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd✝ c b
gcd_mul_lcm✝ : ∀ (a b : α), Associated (gcd✝ a b * lcm✝ a b) (a * b)
lcm_zero_left✝ : ∀ (a : α), lcm✝ 0 a = 0
lcm_zero_right✝ : ∀ (a : α), lcm✝ a 0 = 0
hgcd : gcd✝¹ = gcd✝
hlcm : lcm✝¹ = lcm✝
⊢ { toIsCancelMulZero := toIsCancelMulZero✝¹, gcd := gcd✝¹, lcm := lcm✝¹, gcd_dvd_left := gcd_dvd_left✝¹,
      gcd_dvd_right := gcd_dvd_right✝¹, dvd_gcd := dvd_gcd✝¹, gcd_mul_lcm := gcd_mul_lcm✝¹,
      lcm_zero_left := lcm_zero_left✝¹, lcm_zero_right := lcm_zero_right✝¹ } =
    { toIsCancelMulZero := toIsCancelMulZero✝, gcd := gcd✝, lcm := lcm✝, gcd_dvd_left := gcd_dvd_left✝,
      gcd_dvd_right := gcd_dvd_right✝, dvd_gcd := dvd_gcd✝, gcd_mul_lcm := gcd_mul_lcm✝,
      lcm_zero_left := lcm_zero_left✝, lcm_zero_right := lcm_zero_right✝ }
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : Associated (c ^ k) (a * b)
⊢ ∃ d, Associated (d ^ k) a

Tactic:
obtain ⟨u, hu⟩ := h.symm

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : Associated (c ^ k) (a * b)
u : Rˣ
hu : a * b * ↑u = c ^ k
⊢ ∃ d, Associated (d ^ k) a
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
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Infinite ι
⊢ #κ ≤ #ι

Tactic:
exact linearIndependent_le_infinite_basis b v i

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
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ?m.29 ≤ ⨆ ι, #↑↑ι

Tactic:
apply le_ciSup Cardinal.bddAbove_of_small
      exact
        ⟨Set.range v, by
          rw [LinearIndepOn]
          convert! v.reindexRange.linearIndependent
          simp⟩

Goal state after: