mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : M →ₗ[R] M
n : ℕ
h : map f id ^ n = map (f ^ n) (id ^ n)
⊢ rTensor N f ^ n = rTensor N (f ^ n)

Tactic:
Module.End.id_pow

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
f : M →ₗ[R] M
n : ℕ
h : map f id ^ n = map (f ^ n) id
⊢ rTensor N f ^ n = rTensor N (f ^ n)
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
f : N →ₗ[R] N
n : ℕ
h : map id f ^ n = map (id ^ n) (f ^ n)
⊢ lTensor M f ^ n = lTensor M (f ^ n)

Tactic:
Module.End.id_pow

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
f : N →ₗ[R] N
n : ℕ
h : map id f ^ n = map id (f ^ n)
⊢ lTensor M f ^ n = lTensor M (f ^ n)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: A : Type u
inst✝¹ : CommRing A
inst✝ : Nontrivial A
a b : ℕ
h : a.Coprime b
⊢ IsCoprime ↑a ↑b

Tactic:
by
    simpa only [map_natCast] using IsCoprime.map (Nat.Coprime.isCoprime h) (Int.castRingHom A)

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

Goal state before:
pp: case singleton
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t : Finset I
inst✝ : DecidableEq I
a✝ : I
⊢ (∃ μ, ∑ i ∈ {a✝}, μ i * ∏ j ∈ {a✝} \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)

Tactic:
| singleton =>

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

Goal state before:
pp: case e'_3.e'_5
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
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j ∈ t \ {x}, s j

Tactic:
by_cases hx : x = h.choose

Goal state after:
case pos
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
hx : x = Exists.choose h
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j ∈ t \ {x}, s j

case neg
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
hx : ¬x = Exists.choose h
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j ∈ t \ {x}, s j
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S P
ι : Type u_6
inst✝ : Finite ι
⊢ ∀ {M : ι → Submodule R N} [∀ (i : ι), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)

Tactic:
by
  apply Finite.induction_empty_option _ _ _ ι
  · intro _ _ e h _ _; rw [← e.iSup_comp]; apply h
  · intros; rw [iSup_of_empty]; infer_instance
  · intro _ _ ih _ _; rw [iSup_option]; infer_instance

Goal state after:
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:
| add _ _ _ _ ihr ihs =>

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommGroup M
a : M
⊢ (ℤ ∙ a).toAddSubgroup = AddSubgroup.zmultiples a

Tactic:
ext i

Goal state after:
M : Type u_1
inst✝ : AddCommGroup M
a i : M
⊢ i ∈ (ℤ ∙ a).toAddSubgroup ↔ i ∈ AddSubgroup.zmultiples a
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : EuclideanDomain R
x z : R
hz : ¬z = 0
p : R
⊢ x * (z * p) / z = x * p

Tactic:
mul_left_comm,

Goal state after:
case neg
R : Type u
inst✝ : EuclideanDomain R
x z : R
hz : ¬z = 0
p : R
⊢ z * (x * p) / z = x * p
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mpr
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
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i c ↦ c • f i) ∈ I • span R (Set.range f)

Tactic:
exact Submodule.sum_mem _ fun c _ => smul_mem_smul (ha c) <| subset_span <| Set.mem_range_self _

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

Goal state before:
pp: case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ z = x * (g * s) / g * p

Tactic:
mul_left_comm,

Goal state after:
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ z = g * (x * s) / g * p
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ x * (g * s) * p = x * s * p * g

Tactic:
rw [← mul_assoc]

Goal state after:
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ x * g * s * p = x * s * p * g
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case h₂
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 * (y * gcdB x y)

Tactic:
mul_left_comm,

Goal state after:
case h₂
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 ∣ y * (z * gcdB x y)
Module: Mathlib.RingTheory.Ideal.Maps

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

Tactic:
ext i

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
r : R
h : ∀ (m : M), r • m = 0
m : ι →₀ M
i : ι
⊢ (r • m) i = 0 i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n x✝¹ : ℕ
x✝ : (I ^ x✝¹).IsTwoSided
⊢ (I ^ x✝¹.succ).IsTwoSided

Tactic:
rw [Submodule.pow_succ]; infer_instance

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

Goal state before:
pp: case mpr
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 : ∀ (i : ι) (m : M i), r • m = 0
m : Π₀ (i : ι), M i
⊢ r • m = 0

Tactic:
ext i

Goal state after:
case mpr
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 : ∀ (i : ι) (m : M i), r • m = 0
m : Π₀ (i : ι), M i
i : ι
⊢ (r • m) i = 0 i
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
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 : ∀ (i : ι) (m : M i), r • m = 0
m : (i : ι) → M i
⊢ r • m = 0

Tactic:
ext i

Goal state after:
case mpr
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 : ∀ (i : ι) (m : M i), r • m = 0
m : (i : ι) → M i
i : ι
⊢ (r • m) i = 0 i
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ y / z = x ↔ z * x = y

Tactic:
div_eq_iff_eq_mul_of_dvd _ _ _ h1 h2,

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ y = z * x ↔ z * x = y
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : M
⊢ (R ∙ g).annihilator = (toSpanSingleton R M g).ker

Tactic:
simp [annihilator_span]

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

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

Tactic:
simp_rw [map_zero, gcd_zero, mul_zero, Associated.of_eq]

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

Goal state before:
pp: case refine_2
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
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : f a = x
b : R
hxy : f (a * b) ∈ map f I
hb : f b = y
⊢ x ∈ map f I ∨ y ∈ map f I

Tactic:
mem_map_iff_of_surjective _ hf

Goal state after:
case refine_2
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
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : f a = x
b : R
hxy : ∃ x ∈ I, f x = f (a * b)
hb : f b = y
⊢ x ∈ map f I ∨ y ∈ map f I
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
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
⊢ (map f I).IsPrime

Tactic:
by
  refine ⟨fun h => H.ne_top (eq_top_iff.2 ?_), fun {x y} => ?_⟩
  · replace h := congr_arg (comap f) h
    rw [comap_map_of_surjective _ hf, comap_top] at h
    exact h ▸ sup_le (le_of_eq rfl) hk
  · refine fun hxy => (hf x).recOn fun a ha => (hf y).recOn fun b hb => ?_
    rw [← ha, ← hb, ← map_mul f, mem_map_iff_of_surjective _ hf] at hxy
    rcases hxy with ⟨c, hc, hc'⟩
    rw [← sub_eq_zero, ← map_sub] at hc'
    have : a * b ∈ I := by
      convert! I.sub_mem hc (hk (hc' : c - a * b ∈ RingHom.ker f)) using 1
      abel
    exact
      (H.mem_or_mem this).imp (fun h => ha ▸ mem_map_of_mem f h) fun h => hb ▸ mem_map_of_mem f h

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

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

Tactic:
top_pow

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

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

Tactic:
classical
    trans ({x ∈ s | f x = 0} ∪ {x ∈ s | f x ≠ 0}).gcd f
    · rw [filter_union_filter_not_eq]
    rw [gcd_union]
    refine Eq.trans (?_ : _ = GCDMonoid.gcd (0 : α) ?_) (?_ : GCDMonoid.gcd (0 : α) _ = _)
    · exact gcd {x ∈ s | f x ≠ 0} f
    · refine congr (congr rfl <| s.induction_on ?_ ?_) (by simp)
      · simp
      · intro a s _ h
        rw [filter_insert]
        split_ifs with h1 <;> simp [h, h1]
    simp only [gcd_zero_left, normalize_gcd]

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

Goal state before:
pp: α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : Ideal.span {a} = ⊤
⊢ False

Tactic:
Ideal.span_singleton_eq_top

Goal state after:
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : IsUnit a
⊢ False
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case zero
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
a b : ι
h : I ≤ f a ∨ I ≤ f b
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ ∅, I ≤ f i

Tactic:
simpa only [exists_prop, Finset.notMem_empty, false_and, exists_false, or_false]

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := (Finsupp.linearEquivFunOnFinite R R α).symm
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
exact card_le_of_injective R (P.toLinearMap ∘ₗ f ∘ₗ Q) (P.injective.comp (i.comp Q.injective))

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
h : IsRelPrime x y
⊢ Ideal.span {gcd x y} = ⊤

Tactic:
Ideal.span_singleton_eq_top

Goal state after:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
h : IsRelPrime x y
⊢ IsUnit (gcd x y)
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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)

Tactic:
rw [mul_comm a, ← mul_assoc, mul_dvd_mul_iff_right h_1.1]

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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (d * a) ∣ c * d
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ g, s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * ↑u + s.gcd f * y * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
⊢ ∃ g, (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a

Tactic:
obtain ⟨g, hg⟩ := ih

Goal state after:
case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * ↑u + s.gcd f * y * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
⊢ ∃ g, (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
h : z ∈ S
y : R
hz : generator S * 1 = generator T * (generator S * y)
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T

Tactic:
mul_left_comm,

Goal state after:
case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
h : z ∈ S
y : R
hz : generator S * 1 = generator S * (generator T * y)
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : R ∙ p < R ∙ a
⊢ Ideal.span {a} = ⊤

Tactic:
Ideal.span_singleton_eq_top

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : R ∙ p < R ∙ a
⊢ IsUnit a
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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)

Tactic:
rw [mul_comm a, ← mul_assoc, mul_dvd_mul_iff_right h_1.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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (d * a) ∣ c * d
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
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : IsEmpty m
M N : Matrix m n α
⊢ M = N

Tactic:
ext i

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝ : IsEmpty m
M N : Matrix m n α
i : m
j✝ : n
⊢ M i j✝ = N i j✝
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case i
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
f g : ι →₀ R
h : (linearCombination R fun b ↦ v b) f = (linearCombination R fun b ↦ v b) g
⊢ f = g

Tactic:
exact i h

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
⊢ (∀ (i j : n), (if i = j then d i else 0) ∈ S) ↔ ∀ (i : n), d i ∈ S

Tactic:
conv_lhs => intro _ _; rw [ite_mem]

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
⊢ (∀ (i j : n), (i = j → d i ∈ S) ∧ (¬i = j → 0 ∈ S)) ↔ ∀ (i : n), d i ∈ S
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
f g : ι →₀ R
h : (linearCombination R fun b ↦ v b) f = (linearCombination R fun b ↦ v b) g
⊢ f = g

Tactic:
exact i h

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
⊢ LinearIndepOn R id (range ⇑v)

Tactic:
by
          rw [LinearIndepOn]
          convert! v.reindexRange.linearIndependent
          simp

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
inst✝ : Free R M
⊢ 0 < Module.rank R M ↔ Nontrivial M

Tactic:
by
  refine ⟨fun h ↦ ?_, fun _ ↦ rank_pos_of_free⟩
  rw [← not_subsingleton_iff_nontrivial]
  intro h'
  simp only [rank_subsingleton', lt_self_iff_false] at h

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSemiring α
u : m → α
w : n → α
v : Matrix m n α
⊢ (fun j ↦ u ⬝ᵥ fun i ↦ v i j) ⬝ᵥ w = u ⬝ᵥ fun i ↦ v i ⬝ᵥ w

Tactic:
by
  simpa [dotProduct, Finset.mul_sum, Finset.sum_mul, mul_assoc] using Finset.sum_comm

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
⊢ (∀ (i_1 : m) (j_1 : n), (if i = i_1 ∧ j = j_1 then a else 0) ∈ S) ↔ a ∈ S

Tactic:
conv_lhs => intro _ _; rw [ite_mem]

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
⊢ (∀ (i_1 : m) (j_1 : n), (i = i_1 ∧ j = j_1 → a ∈ S) ∧ (¬(i = i_1 ∧ j = j_1) → 0 ∈ S)) ↔ a ∈ S
Module: Mathlib.Data.Matrix.Mul

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

Tactic:
diagonal_mul,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
i✝ : m
j✝ : n
⊢ 1 * M i✝ j✝ = M i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
⊢ diagonal v *ᵥ Pi.single j x = Pi.single j (v j * x)

Tactic:
ext i

Goal state after:
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ (diagonal v *ᵥ Pi.single j x) i = Pi.single j (v j * x) i