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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹² : KleeneAlgebra α
inst✝¹¹ : LE β
inst✝¹⁰ : LT β
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Max β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ f 1 ≤ f a∗

Tactic:
one,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹² : KleeneAlgebra α
inst✝¹¹ : LE β
inst✝¹⁰ : LT β
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Max β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ 1 ≤ f a∗
Module: Mathlib.LinearAlgebra.TensorProduct.Map

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
y : N ⊗[R] M
⊢ (rTensor M (refl R N)) y = y

Tactic:
rTensor_refl,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
y : N ⊗[R] M
⊢ (refl R (N ⊗[R] M)) y = y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
rw [mul_comm] at h

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
⊢ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
rw [mul_comm] at h

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y
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
A' : Submodule R A
M' : Submodule R M
r : R
m✝ : M
hm✝ : m✝ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
a : A
ha : a ∈ A'.toAddSubmonoid
m : M
hm : m ∈ M'.toAddSubmonoid
⊢ r • a • m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier

Tactic:
rw [← smul_assoc]

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
A' : Submodule R A
M' : Submodule R M
r : R
m✝ : M
hm✝ : m✝ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
a : A
ha : a ∈ A'.toAddSubmonoid
m : M
hm : m ∈ M'.toAddSubmonoid
⊢ (r • a) • m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Semiring C
inst✝⁵ : SMul A B
inst✝⁴ : Module A C
inst✝³ : Module B C
inst✝² : IsScalarTower A C C
inst✝¹ : IsScalarTower B C C
inst✝ : IsScalarTower A B C
I : Submodule B C
n : ℕ
x✝ : n + 2 ≠ 0
⊢ restrictScalars A (I ^ (n + 2)) = restrictScalars A I ^ (n + 2)

Tactic:
simp [Submodule.pow_succ (n := n + 1), restrictScalars_mul, restrictScalars_pow n.succ_ne_zero]

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
s : Set A
⊢ 1 = span R 1

Tactic:
one_eq_span_one_set

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ span R 1 = span R 1
Module: Mathlib.RingTheory.OrzechProperty

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : OrzechProperty R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N : Type w
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
i f : N →ₗ[R] M
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝² : Small.{u, v} M
this✝¹ : AddCommMonoid (Shrink.{u, v} M) := (equivShrink M).symm.addCommMonoid
this✝ : Module R (Shrink.{u, v} M) := Equiv.module R (equivShrink M).symm
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ i
hi : Injective ⇑i'
f' : ↥i'.range →ₗ[R] Shrink.{u, v} M := ↑j.symm ∘ₗ f ∘ₗ ↑(LinearEquiv.ofInjective i' hi).symm
hf : Surjective ⇑f'
⊢ Injective ⇑f

Tactic:
simpa [f'] using injective_of_surjective_of_submodule' f' hf

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

Goal state before:
pp: case zero
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
⊢ 0 ∈ s • N

Tactic:
exact Submodule.zero_mem _

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

Goal state before:
pp: case zero
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
⊢ 0 • n ∈ s • N

Tactic:
rw [zero_smul]; exact Submodule.zero_mem _

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = a
⊢ a ∣ b

Tactic:
rw [← h]

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = a
⊢ gcd a b ∣ b
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH : ∀ {s t s' t' : R}, P a b (b✝ % a✝, s, t) → P a b (a✝, s', t') → P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : P a b (a✝, s, t)
p' : P a b (b✝, s', t')
⊢ P a b (b✝ % a✝, s' - b✝ / a✝ * s, t' - b✝ / a✝ * t)

Tactic:
unfold P at p p' ⊢

Goal state after:
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH : ∀ {s t s' t' : R}, P a b (b✝ % a✝, s, t) → P a b (a✝, s', t') → P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ match (b✝ % a✝, s' - b✝ / a✝ * s, t' - b✝ / a✝ * t) with
  | (r, s, t) => r = a * s + b * t
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_1.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i : ι
⊢ ((Finsupp.single i y).sum fun i c ↦ c • f i) = (fun x1 x2 ↦ x1 • x2) y (f i)

Tactic:
refine @Finsupp.sum_single_index ι R M _ _ i _ (fun i y => y • f i) ?_

Goal state after:
case mp.refine_1.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i : ι
⊢ 0 • f i = 0
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 K ^ 0 ≤ comap f (K ^ 0)

Tactic:
rw [pow_zero, pow_zero, Ideal.one_eq_top, Ideal.one_eq_top]

Goal state after:
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 ⊤
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
    classical simpa using congr_fun (h (Pi.single i m)) i

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
I J : Ideal R
inst✝² : IsDomain R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
x : R
hx : x ≠ 0
⊢ I * span {x} = J * span {x} ↔ I = J

Tactic:
simp only [le_antisymm_iff, span_singleton_mul_left_mono hx]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : K ⊔ J = ⊤
⊢ I * K ⊔ J = I ⊔ J

Tactic:
by
  rw [sup_comm] at h
  rw [sup_comm, sup_mul_eq_of_coprime_right h, sup_comm]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ 0 ∣ x

Tactic:
rw [← h]

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
h : s.gcd = 0
x : α
hx : x ∈ s
⊢ s.gcd ∣ x
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
| map id s

Tactic:
← s.pmap_eq_map _ _ fun _ ↦ id

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
| pmap (fun a x ↦ id a) s ⋯
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ GCDMonoid.gcd ({x ∈ s | f x = 0}.gcd f) ({x ∈ s | f x ≠ 0}.gcd f) = GCDMonoid.gcd 0 ({x ∈ s | f x ≠ 0}.gcd f)

Tactic:
refine congr (congr rfl <| s.induction_on ?_ ?_) (by simp)
      · simp
      · intro a s _ h
        rw [filter_insert]
        split_ifs with h1 <;> simp [h, h1]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
⊢ ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
by_cases! h : ∀ x ∈ s, f x = (0 : α)

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
⊢ ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
⊢ ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : a = 0
⊢ ∃ d, Associated (d ^ k) a

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
⊢ ∃ d, Associated (d ^ k) a

Tactic:
· use 0
    obtain rfl | hk := eq_or_ne k 0
    · simp [ha] at h
    · rw [ha, zero_pow hk]

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
⊢ ∃ d, Associated (d ^ k) a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc : c ∣ a * b
⊢ ∃ d, Associated (d ^ k) a

Tactic:
obtain ⟨d₁, d₂, hd₁, hd₂, hc⟩ := exists_dvd_and_dvd_of_dvd_mul hc

Goal state after:
case neg.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₁ * d₂
⊢ ∃ d, Associated (d ^ k) a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a✝ a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
x✝ : i * a ≠ 0
s : Multiset α
hs : (∀ b ∈ s, Irreducible b) ∧ s.prod ~ᵤ a
⊢ (i ::ₘ s).prod ~ᵤ i * a

Tactic:
rw [s.prod_cons i]
      exact hs.2.mul_left i

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

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

Tactic:
rw [← h]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * b' * (d₁ ^ k * a')
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
⊢ (∀ r ∈ I, ∀ s ∈ J, r ∈ P ∨ s ∈ P) ↔ ∀ x ∈ I, x ∈ P ∨ ∀ ⦃x : R⦄, x ∈ J → x ∈ P

Tactic:
forall_or_left

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

Goal state before:
pp: case neg
α : 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
h0 : lcm c b ≠ 0
⊢ a ∣ Classical.choose ⋯

Tactic:
rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd c b)]

Goal state after:
case neg
α : 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
h0 : lcm c b ≠ 0
⊢ lcm c b * a ∣ c * b
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
⊢ a ∣ normalize (Classical.choose ⋯)

Tactic:
have h0 : lcm c b ≠ 0 := lcm_ne_zero_iff.mpr ⟨h, h_1⟩

Goal state after:
case neg
α : 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
h0 : lcm c b ≠ 0
⊢ a ∣ normalize (Classical.choose ⋯)
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Unique m
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
i j : m
⊢ diagonal d i j = of (fun x x_1 ↦ d default) i j

Tactic:
Subsingleton.elim i default,

Goal state after:
m : Type u_2
α : Type v
inst✝² : Unique m
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
i j : m
⊢ diagonal d default j = of (fun x x_1 ↦ d default) default j
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case a
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
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ #κ ≤ #ι

pp: case a
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
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ #ι ≤ #κ

Tactic:
· exact linearIndependent_le_basis b v i

Goal state after:
case a
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
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ #ι ≤ #κ
Module: Mathlib.GroupTheory.DedekindFinite

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
a b : M
hab : a * b = 1
c : M
hbc : (fun x ↦ b * x) c = 1
⊢ b * a = 1

Tactic:
rwa [left_inv_eq_right_inv hab hbc]

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
ι : Type w
inst✝ : StrongRankCondition R
v : Basis ι R M
this : Nontrivial R
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} #↑(range ⇑v)

Tactic:
Cardinal.mk_range_eq_of_injective v.injective

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
v : Basis ι R M
this : Nontrivial R
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{v, w} #ι
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n, ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
le : ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ Module.rank R (Fin (n + 1) → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin (n + 1) → R)

pp: case refine_2
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
pos : n > 0
eq : Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)

Tactic:
· exact .inr <| le.trans <| LinearMap.rank_le_of_injective
      (ExtendByZero.linearMap R _) <| extend_injective (Fin.castSucc_injective n) _

Goal state after:
case refine_2
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n > 0, Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
n : ℕ
pos : n > 0
eq : Module.rank R (Fin n → R) = 0 ∨ ℵ₀ ≤ Module.rank R (Fin n → R)
⊢ ℵ₀ ≤ Module.rank R (Fin n → R)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
M : Matrix m n α
⊢ 0 * M = 0

Tactic:
ext
  apply zero_dotProduct

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
i✝ : m
j✝ : n
⊢ (M * 1) i✝ j✝ = M i✝ j✝

Tactic:
rw [← diagonal_one, mul_diagonal, mul_one]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N N' : Matrix n o α
⊢ M * (N - N') = M * N - M * N'

Tactic:
rw [sub_eq_add_neg, Matrix.mul_add, Matrix.mul_neg, sub_eq_add_neg]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I

Tactic:
rw [mul_comm] at h

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ (v ᵥ* diagonal fun x ↦ 1) x✝ = v x✝

Tactic:
vecMul_diagonal,

Goal state after:
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ v x✝ * 1 = v x✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
⊢ -A *ᵥ -v = A *ᵥ v

Tactic:
mulVec_neg,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
⊢ -(-A *ᵥ v) = A *ᵥ v
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
H : ¬I = ⊥
⊢ 1 ∈ I

Tactic:
obtain ⟨x, hx1, hx2 : x ≠ 0⟩ := SetLike.exists_of_lt (bot_lt_iff_ne_bot.mpr H : ⊥ < I)

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
H : ¬I = ⊥
x : A
hx1 : x ∈ I
hx2 : x ≠ 0
⊢ 1 ∈ I
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : (x : A) → x ∈ ⨆ i, S i → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯
add : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r) ⋯
⊢ ∃ (x_1 : x ∈ ⨆ i, S i), motive x x_1

Tactic:
exact iSup_induction S (motive := fun x' ↦ ∃ h, motive x' h) mem
    (fun _ _ h ↦ ⟨_, basic _ _ h⟩) (fun _ _ h h' ↦ ⟨_, add _ _ _ _ h.2 h'.2⟩)
    (fun _ _ h h' ↦ ⟨_, mul _ _ _ _ h.2 h'.2⟩) fun _ ↦ ⟨_, algebraMap _⟩

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
⊢ x ∈ Submodule.span R ↑⊥ ↔ x = 0

Tactic:
NonUnitalSubsemiring.coe_bot,

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
⊢ x ∈ R ∙ 0 ↔ x = 0
Module: Mathlib.Algebra.Field.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
q : ℚ≥0
⊢ ↑q = (↑q.den)⁻¹ * ↑q.num

Tactic:
NNRat.cast_def,

Goal state after:
α : Type u_1
inst✝ : DivisionSemiring α
q : ℚ≥0
⊢ ↑q.num / ↑q.den = (↑q.den)⁻¹ * ↑q.num