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

Goal state before:
pp: α : 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), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
⊢ False

Tactic:
have := (length_le_height_last (p := p.take i)).trans <| ih n' h_lt (p i) hn'.symm

Goal state after:
α : 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), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑(RelSeries.take p i).length ≤ (↑m + 1) * ↑n' + ↑m
⊢ False
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocCommSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
⊢ mul' R A ∘ₗ ↑(TensorProduct.comm R A A) = mul' R A

Tactic:
simp [mul', lift_comp_comm_eq]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f : N →ₗ[R] P
⊢ lTensor M (g ∘ₗ f) = lTensor M g ∘ₗ lTensor M f

Tactic:
by
  ext m n
  simp only [compr₂ₛₗ_apply, mk_apply, comp_apply, lTensor_tmul]

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

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m ∈ ⊥
n : R
x✝ : n ∈ S
⊢ m * n ∈ ⊥

Tactic:
rw [AddSubmonoid.mem_bot] at hm ⊢; rw [hm, zero_mul]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
⊢ f (a * x + b * y) = 1

Tactic:
h,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
⊢ f 1 = 1
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons.mp.refine_1
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
⊢ ∑ i ∈ t, (Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) + μ * fun x ↦ s a) i * ∏ j ∈ t \ {i}, s j = 1

Tactic:
prod_eq_mul_prod_sdiff_singleton_of_mem h.choose_spec,

Goal state after:
case cons.mp.refine_1
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 * (s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
⊢ ∑ i ∈ t, (Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) + μ * fun x ↦ s a) i * ∏ j ∈ t \ {i}, s j = 1
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case e'_2.e'_6
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 * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ ∏ j ∈ insert a t \ {x}, s j = (fun x ↦ s a) x * ∏ j ∈ t \ {x}, s j

Tactic:
prod_eq_prod_sdiff_singleton_mul (mem x hx),

Goal state after:
case e'_2.e'_6
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 * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ (∏ x ∈ (insert a t \ {x}) \ {a}, s x) * s a = (fun x ↦ s a) x * ∏ j ∈ t \ {x}, s j
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬(I.prod ⊤).IsPrime

Tactic:
h,

Goal state after:
case ne_top'
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I = ⊤
⊢ ¬(⊤.prod ⊤).IsPrime
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: 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
I : Ideal S
h : I = ⊤
⊢ comap f I = ⊤

Tactic:
h,

Goal state after:
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
I : Ideal S
h : I = ⊤
⊢ comap f ⊤ = ⊤
Module: Mathlib.Algebra.EuclideanDomain.Field

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b : K
⊢ b * (a / b) + (a - a * b / b) = a

Tactic:
by
    by_cases h : b = 0 <;> simp [h, mul_div_cancel₀]

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ b * (a / b) + a % b

Tactic:
h,

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ b * (a / b) + 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ a b : R
x✝¹ : a ≠ 0
x✝ : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd a b ∣ a ∧ gcd a b ∣ b

Tactic:
rw [gcd_val]

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ a b : R
x✝¹ : a ≠ 0
x✝ : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd (b % a) a ∣ a ∧ gcd (b % a) a ∣ b
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ c a b : R
x✝ : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd a b

Tactic:
rw [gcd_val]

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ c a b : R
x✝ : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd (b % a) a
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R✝ : Type u
inst✝¹ : EuclideanDomain R✝
inst✝ : DecidableEq R✝
R : Type u_1
e : EuclideanDomain R
this : DecidableEq R
a b : R
h : a * b = 0
h0 : ¬a = 0 ∧ ¬b = 0
⊢ a * b / b = 0

Tactic:
h,

Goal state after:
R✝ : Type u
inst✝¹ : EuclideanDomain R✝
inst✝ : DecidableEq R✝
R : Type u_1
e : EuclideanDomain R
this : DecidableEq R
a b : R
h : a * b = 0
h0 : ¬a = 0 ∧ ¬b = 0
⊢ 0 / b = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
e : S ≃+* T
⊢ ker (e.toRingHom.comp f) = ker f

Tactic:
rw [← RingHom.comap_ker, RingEquiv.toRingHom_eq_coe, RingHom.ker_coe_equiv, RingHom.ker]

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

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

Tactic:
h,

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

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

Tactic:
h,

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : FaithfulSMul R M
a : R
ha : a ∈ annihilator R M
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ ∀ (a_1 : M), a • a_1 = 0 • a_1

Tactic:
by simp [Module.mem_annihilator.mp ha]

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y

Tactic:
h,

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ 0 * (x * y / 0) = x * y
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
⊢ i' + (i1 + j) * k = i' + k

Tactic:
h,

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
⊢ i' + 1 * k = i' + k
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
i1 : R
hi1 : i1 ∈ I
k : R
hk : k ∈ K
h : i1 + k = 1
i' : R
hi' : i' ∈ I
j : R
hj : j ∈ J
⊢ i' + j * (i1 + k) = i' + j

Tactic:
h,

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
i1 : R
hi1 : i1 ∈ I
k : R
hk : k ∈ K
h : i1 + k = 1
i' : R
hi' : i' ∈ I
j : R
hj : j ∈ J
⊢ i' + j * 1 = i' + j
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

Tactic:
· simp [IH, h]

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : FunLike F R S
rc : RingHomClass F R S
F' : Type u_4
inst✝² : EquivLike F' R S
inst✝¹ : RingEquivClass F' R S
f : F'
I : Ideal R
inst✝ : I.IsPrime
h : map f I = map (↑↑f) I
⊢ (map f I).IsPrime

Tactic:
h,

Goal state after:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : FunLike F R S
rc : RingHomClass F R S
F' : Type u_4
inst✝² : EquivLike F' R S
inst✝¹ : RingEquivClass F' R S
f : F'
I : Ideal R
inst✝ : I.IsPrime
h : map f I = map (↑↑f) I
⊢ (map (↑↑f) I).IsPrime
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
⊢ I ⊔ ⨅ i ∈ s, J i = ⊤

Tactic:
by
  classical
  exact s.induction_on' (by simp) fun {i t} his hts hit eq_top ↦ top_unique <| by
    rw [Finset.iInf_insert, inf_comm]
    refine le_trans ?_ (sup_le_sup_left mul_le_inf _)
    simpa only [sup_mul_eq_of_coprime_right (h _ his)] using eq_top.ge

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

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

pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

Tactic:
· simp [IH, h]

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.gcd = s.gcd
h : a ∈ s
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
w x y z : R
inst✝ : (span {w, x}).IsTwoSided
⊢ span {w, x} * span {y, z} = span {w * y, w * z, x * y, x * z}

Tactic:
span_mul_span'

Goal state after:
R : Type u
inst✝¹ : Semiring R
w x y z : R
inst✝ : (span {w, x}).IsTwoSided
⊢ span ({w, x} * {y, z}) = span {w * y, w * z, x * y, x * z}
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : I = ⊤
⊢ I ^ n = ⊤

Tactic:
h,

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : I = ⊤
⊢ ⊤ ^ n = ⊤
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : n = 0
⊢ I ^ n = ⊤

Tactic:
h,

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : n = 0
⊢ I ^ 0 = ⊤
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: a : ℤ
⊢ ∃ u x, ↑a.natAbs = u * a

Tactic:
rcases natAbs_eq a with h | h

Goal state after:
case inl
a : ℤ
h : a = ↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a

case inr
a : ℤ
h : a = -↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

Tactic:
rw [insert_eq_of_mem h,
      (gcd_eq_right_iff (f b) (s.gcd f) (Multiset.normalize_gcd (s.1.map f))).2 (gcd_dvd h)]

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

Goal state before:
pp: case refine_2
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
h : (t.gcd fun x ↦ a * f x) = normalize a * t.gcd f
⊢ GCDMonoid.gcd (a * f b) (t.gcd fun x ↦ a * f x) = normalize a * GCDMonoid.gcd (f b) (t.gcd f)

Tactic:
h,

Goal state after:
case refine_2
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
h : (t.gcd fun x ↦ a * f x) = normalize a * t.gcd f
⊢ GCDMonoid.gcd (a * f b) (normalize a * t.gcd f) = normalize a * GCDMonoid.gcd (f b) (t.gcd f)
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : Group α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ ¬IsUnit a ↔ (↑a)⁻¹ ∉ S

Tactic:
isUnit_iff

Goal state after:
α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : Group α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ (↑a)⁻¹ ∉ S ↔ (↑a)⁻¹ ∉ S
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = gcd a b * ca
cb : α
hb : b = gcd a b * cb
⊢ a = 0 ∧ b = 0

Tactic:
h,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = 0 * ca
cb : α
hb : b = 0 * cb
⊢ a = 0 ∧ b = 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
a✝ : GCDMonoid α
h0 : gcd k m = 0
⊢ ∃ a₁ a₂, a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂

Tactic:
rw [gcd_eq_zero_iff] at h0

Goal state after:
case pos
α : Type u_1
inst✝ : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
a✝ : GCDMonoid α
h0 : k = 0 ∧ m = 0
⊢ ∃ a₁ a₂, a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
Module: Mathlib.Algebra.GCDMonoid.Basic

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

Tactic:
h,

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ c ^ k = d₁ ^ k * d₂ ^ k
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ
⊢ Set.univ.WellFoundedOn (Function.onFun (fun x1 x2 ↦ x1 > x2) fun a ↦ span {a})

Tactic:
Set.wellFoundedOn_univ

Goal state after:
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ
⊢ WellFounded (Function.onFun (fun x1 x2 ↦ x1 > x2) fun a ↦ span {a})
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
h : gcd 0 0 = 0
⊢ 0 = gcd 0 0 * 1

Tactic:
h,

Goal state after:
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
h : gcd 0 0 = 0
⊢ 0 = 0 * 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : lcm a b = 0
⊢ Associated (gcd a b * lcm a b) 0

Tactic:
h,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : lcm a b = 0
⊢ Associated (gcd a b * 0) 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
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
a : α
a0 : ¬a = 0
h : gcd a 0 * Classical.choose ⋯ = a * 0
a0' : gcd a 0 ≠ 0
⊢ gcd a 0 * Classical.choose ⋯ = 0

Tactic:
h,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
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
a : α
a0 : ¬a = 0
h : gcd a 0 * Classical.choose ⋯ = a * 0
a0' : gcd a 0 ≠ 0
⊢ a * 0 = 0
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective ⇑f
⊢ Fintype.card β ≤ Fintype.card α

Tactic:
let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
  let Q := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
  exact le_of_fin_surjective R
    (Q.symm.toLinearMap ∘ₗ f ∘ₗ P) (Q.symm.surjective.comp (i.comp P.surjective))

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
h : a = 0
⊢ Associated (b * lcm a b) (a * b)

Tactic:
h,

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
h : a = 0
⊢ Associated (b * lcm 0 b) (0 * b)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : a = 0
⊢ Associated (normalize b * lcm a b) (a * b)

Tactic:
h,

Goal state after:
case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : a = 0
⊢ Associated (normalize b * lcm 0 b) (0 * b)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case inl.intro
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✝¹ : Fintype ι
this : Finite ι'
val✝ : Fintype ι'
⊢ lift.{w', w} ↑(Fintype.card ι) = lift.{w, w'} #ι'

Tactic:
Cardinal.mk_fintype

Goal state after:
case inl.intro
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✝¹ : Fintype ι
this : Finite ι'
val✝ : Fintype ι'
⊢ lift.{w', w} ↑(Fintype.card ι) = lift.{w, w'} ↑(Fintype.card ι')
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
hs : range ⇑v ⊆ ⋃ j, S' j
IJ : #↑J < #↑(range ⇑v)
this : #↑(⋃ j, S' j) < #↑(range ⇑v)
⊢ False

Tactic:
by exact not_le_of_gt this ⟨Set.embeddingOfSubset _ _ hs⟩

Goal state after: