mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : FaithfulSMul R A
r : R
h : R ∙ (algebraMap R A) r = 1
r' : R
eq : (algebraMap R A) r' * (algebraMap R A) r = (algebraMap R A) 1
⊢ ∃ r_1, (algebraMap R A) r = (algebraMap R A) ↑r_1

Tactic:
← map_mul,

Goal state after:
R : Type u
inst✝³ : CommSemiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
r : R
h : R ∙ (algebraMap R A) r = 1
r' : R
eq : (algebraMap R A) (r' * r) = (algebraMap R A) 1
⊢ ∃ r_1, (algebraMap R A) r = (algebraMap R A) ↑r_1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
⊢ ⊥ = 0

Tactic:
bot_eq_zero

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective ⇑l
e : Submodule R M ≃o Submodule S P := orderIsoMapComapOfBijective l hl
⊢ WellFoundedGT (Submodule R M) ↔ WellFoundedGT (Submodule S P)

Tactic:
exact ⟨fun _ ↦ e.symm.strictMono.wellFoundedGT, fun _ ↦ e.strictMono.wellFoundedGT⟩

Goal state after:
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 (span (⇑(algebraMap R S) '' ↑I) • N) = I • Submodule.restrictScalars R N

Tactic:
Submodule.span_smul_eq,

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.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
⊢ 0 ∈ span R (S • T)

Tactic:
exact zero_mem _

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
x✝¹ : R
x✝ : x✝¹ ∈ Ideal.span S
⊢ 0 ∈ span R (S • T)

Tactic:
exact zero_mem _

Goal state after:
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 :
  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
⊢ b✝ % a✝ = b✝ - a * (b✝ / a✝ * s) - b * (b✝ / a✝ * t)

Tactic:
sub_sub,

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
⊢ b✝ % a✝ = b✝ - (a * (b✝ / a✝ * s) + b * (b✝ / a✝ * t))
Module: Mathlib.Algebra.EuclideanDomain.Basic

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

Tactic:
rw [mul_sub, EuclideanDomain.mul_div_cancel' h1 h2]

Goal state after:
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
⊢ z * (x - y / z) = z * x - y

Tactic:
rw [mul_sub, EuclideanDomain.mul_div_cancel' h1 h2]

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

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

Tactic:
div_eq_iff_eq_mul_of_dvd _ _ _ h1 h3,

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z t : R
h1 : y ≠ 0
h2 : t ≠ 0
h3 : y ∣ x
h4 : t ∣ z
⊢ x = y * (z / t) ↔ t * x = y * z
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.lcm = s.lcm
⊢ (a ::ₘ s).dedup.lcm = (a ::ₘ s).lcm

Tactic:
by
    by_cases h : a ∈ s; swap; · simp [IH, h]
    simp only [h, dedup_cons_of_mem, IH, lcm_cons]
    unfold lcm
    rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_same]
    apply lcm_eq_of_associated_left (associated_normalize _)

Goal state after:
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, J i ⊔ I = ⊤
⊢ I ⊔ ⨅ i ∈ s, J i = ⊤

Tactic:
sup_iInf_eq_top

Goal state after:
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, J i ⊔ I = ⊤
⊢ ⊤ = ⊤

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, J i ⊔ I = ⊤
⊢ ∀ i ∈ s, I ⊔ J i = ⊤
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
h : Associated a b
ha : normalize a = a
hb : normalize b = b
⊢ normalize b = b

Tactic:
hb

Goal state after:
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
h : Associated a b
ha : normalize a = a
hb : normalize b = b
⊢ b = b
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y * ↑(normUnit (x * y)) = x * ↑(normUnit x) * (y * ↑(normUnit y))

Tactic:
normUnit_mul hx hy

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y * ↑(normUnit x * normUnit y) = x * ↑(normUnit x) * (y * ↑(normUnit y))
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℤ
⊢ 0 ≤ s.gcd f

Tactic:
by
  induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s has ih =>
    rw [gcd_cons, ← Int.coe_gcd]
    grind

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

Goal state before:
pp: case h
α : 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
⊢ Associated (gcd a b) a

Tactic:
hb

Goal state after:
case h
α : 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
⊢ Associated (gcd a 0) a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
a : α
ha : a ∈ b * ↑u ::ₘ f.erase b
⊢ Irreducible a

Tactic:
obtain rfl | ha := Multiset.mem_cons.1 ha
        exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)]

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✝ : 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
b : M
⊢ b ∈ range ⇑v → b ∈ ⋃ j, S' j

Tactic:
hb

Goal state after:
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
b : M
hb : b ∈ range ⇑v
⊢ b ∈ ⋃ j, S' j
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
α : Type u_7
inst✝¹ : DecidableEq m
inst✝ : Zero α
i : m
r : α
⊢ diagonal (Pi.single i r) = single i i r

Tactic:
ext j k

Goal state after:
m : Type u_2
α : Type u_7
inst✝¹ : DecidableEq m
inst✝ : Zero α
i : m
r : α
j k : m
⊢ diagonal (Pi.single i r) j k = single i i r j k
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
α : Type u_7
inst✝¹ : DecidableEq m
inst✝ : Zero α
i : m
r : α
⊢ diagonal (Pi.single i r) = single i i r

Tactic:
by
  ext j k
  dsimp [diagonal, single]
  grind

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

Goal state before:
pp: m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
⊢ ∑ i, single i i (f i) = diagonal f

Tactic:
ext j k

Goal state after:
m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ (∑ i, single i i (f i)) j k = diagonal f j k
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
i : n
⊢ (diagonal v *ᵥ Pi.single j x) i = Pi.single j (v j * x) i

Tactic:
rw [mulVec_diagonal]

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
⊢ v i * Pi.single j x i = Pi.single j (v j * x) i
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case inl
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : IsEmpty m
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec

pp: case inr
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : Nonempty m
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec

Tactic:
· simp [IsLeftRegular, Function.injective_of_subsingleton]

Goal state after:
case inr
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : Nonempty m
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
h : 0 ≠ 0
⊢ (0 • s).toFinset = s.toFinset

Tactic:
by contradiction

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
⊢ M * submatrix 1 (⇑e₁) e₂ = M.submatrix id (⇑e₁.symm ∘ e₂)

Tactic:
cases nonempty_fintype o
  let A := M.submatrix id e₁.symm
  have : M = A.submatrix id e₁ := by
    simp only [A, submatrix_submatrix, Function.comp_id, submatrix_id_id, Equiv.symm_comp_self]
  rw [this, submatrix_mul_equiv]
  simp only [A, Matrix.mul_one, submatrix_submatrix, Function.comp_id, submatrix_id_id,
    Equiv.symm_comp_self]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → x ∈ I ⊔ J

Tactic:
· rintro ⟨y, ⟨hy, ⟨z, ⟨hz, rfl⟩⟩⟩⟩; exact add_mem _ (mem_sup_left hy) (mem_sup_right hz)

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
constructor
  · let s : TwoSidedIdeal R := .mk'
      {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}
      ⟨0, ⟨zero_mem _, ⟨0, ⟨zero_mem _, zero_add _⟩⟩⟩⟩
      (by rintro _ _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩ ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩;
          exact ⟨x + a, ⟨add_mem _ hx ha, ⟨y + b, ⟨add_mem _ hy hb, by abel⟩⟩⟩⟩)
      (by rintro _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨-x, ⟨neg_mem _ hx, ⟨-y, ⟨neg_mem _ hy, by abel⟩⟩⟩⟩)
      (by rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨_, ⟨mul_mem_left _ _ _ hx, ⟨_, ⟨mul_mem_left _ _ _ hy, mul_add _ _ _ |>.symm⟩⟩⟩⟩)
      (by rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨_, ⟨mul_mem_right _ _ _ hx, ⟨_, ⟨mul_mem_right _ _ _ hy, add_mul _ _ _ |>.symm⟩⟩⟩⟩)
    suffices (I.ringCon ⊔ J.ringCon) ≤ s.ringCon by
      intro h; convert! this h; rw [rel_iff, sub_zero, mem_mk']; rfl
    refine sup_le (fun x y h => ?_) (fun x y h => ?_) <;> rw [rel_iff] at h ⊢ <;> rw [mem_mk']
    exacts [⟨_, ⟨h, ⟨0, ⟨zero_mem _, add_zero _⟩⟩⟩⟩, ⟨0, ⟨zero_mem _, ⟨_, ⟨h, zero_add _⟩⟩⟩⟩]
  · rintro ⟨y, ⟨hy, ⟨z, ⟨hz, rfl⟩⟩⟩⟩; exact add_mem _ (mem_sup_left hy) (mem_sup_right hz)

Goal state after:
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
S T : Subalgebra R A
x : R
⊢ (algebraMap R A) x ∈ ↑S ∪ ↑T

Tactic:
exact Set.mem_union_left _ (algebraMap_mem S x)

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

Goal state before:
pp: case a.zero
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
s : Set A
x : A
⊢ 0 ∈ span R ↑(Subsemigroup.closure s)

Tactic:
exact zero_mem _

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

Goal state before:
pp: F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : NonUnitalNonAssocSemiring A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : FunLike F A B
inst✝⁴ : NonUnitalAlgHomClass F R A B
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : F
x : A
⊢ map f (adjoin R {x}) = adjoin R {f x}

Tactic:
simp [NonUnitalAlgHom.map_adjoin]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a.nil
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
HL : ∀ t ∈ [], ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod []).sum ∈ span R ↑(Submonoid.closure s)

Tactic:
exact zero_mem _

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

Goal state before:
pp: F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : NonUnitalNonAssocSemiring A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : FunLike F A B
inst✝⁴ : NonUnitalAlgHomClass F R A B
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : F
x : A
⊢ map f (adjoin R {x}) = adjoin R {f x}

Tactic:
by
  simp [NonUnitalAlgHom.map_adjoin]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a.cons.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
HL : hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
⊢ ∃ z_1 r_1, ∃ (_ : r_1 ∈ Submonoid.closure s), z_1 • r_1 = hd * z • r

Tactic:
rcases HL.1 with (⟨hd, rfl⟩ | hs)

Goal state after:
case a.cons.cons.inl
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
hd : R
HL : (algebraMap R A) hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ ∃ z_1 r_1, ∃ (_ : r_1 ∈ Submonoid.closure s), z_1 • r_1 = (algebraMap R A) hd * z • r

case a.cons.cons.inr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
HL : hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
hs : hd ∈ s
⊢ ∃ z_1 r_1, ∃ (_ : r_1 ∈ Submonoid.closure s), z_1 • r_1 = hd * z • r
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ℬ : Basis ι R M
x : M ⊗[R] N
⊢ ∃ c, (c.sum fun i n ↦ ℬ i ⊗ₜ[R] n) = x

Tactic:
obtain ⟨c, rfl⟩ := (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.surjective x

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ℬ : Basis ι R M
c : ι →₀ N
⊢ ∃ c_1, (c_1.sum fun i n ↦ ℬ i ⊗ₜ[R] n) = (equivFinsuppOfBasisLeft ℬ).symm c
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ Commute (star x) y ↔ Commute x (star y)

Tactic:
← commute_star_star,

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ Commute (star (star x)) (star y) ↔ Commute x (star y)
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
inst✝² : StarMul R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
⊢ star ⅟r * 1 = ⅟(star r)

Tactic:
← mul_invOf_self (star r),

Goal state after:
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarMul R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
⊢ star ⅟r * (star r * ⅟(star r)) = ⅟(star r)
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ≥0
x : M
⊢ f (↑c • x) = ↑c • f x

Tactic:
rw [NNRat.cast_def, NNRat.cast_def, div_eq_mul_inv, div_eq_mul_inv, mul_smul, mul_smul,
    map_natCast_smul f R S, map_inv_natCast_smul f R S]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Ring α
inst✝ : StarRing α
M : Matrix n n α
d : ℤ
⊢ M = (↑d).map star ↔ M = ↑d

Tactic:
map_intCast_star

Goal state after:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Ring α
inst✝ : StarRing α
M : Matrix n n α
d : ℤ
⊢ M = ↑d ↔ M = ↑d
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : MulOneClass R
x : n → R
i✝ : n
j✝ : m
⊢ vecMulVec x 1 i✝ j✝ = replicateCol m x i✝ j✝

Tactic:
simp [vecMulVec_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : MulOneClass R
x : n → R
i✝ : m
j✝ : n
⊢ vecMulVec 1 x i✝ j✝ = replicateRow m x i✝ j✝

Tactic:
simp [vecMulVec_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
⊢ (diagonal v).updateCol i (Pi.single i x) = diagonal (Function.update v i x)

Tactic:
ext j k

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
⊢ (diagonal v).updateCol i (Pi.single i x) j k = diagonal (Function.update v i x) j k
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq m
inst✝ : Mul α
u : m → α
v : n → α
a : α
i' : m
j : n
⊢ vecMulVec (Function.update u i' a) v i' j = (vecMulVec u v).updateRow i' (a • v) i' j

Tactic:
simp [vecMulVec_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Mul α
u : m → α
v : n → α
a : α
i : m
j' : n
⊢ vecMulVec u (Function.update v j' a) i j' = (vecMulVec u v).updateCol j' (MulOpposite.op a • u) i j'

Tactic:
simp [vecMulVec_apply]

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

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
⊢ (blockDiagonal' fun k ↦ M k * N k) = blockDiagonal' M * blockDiagonal' N

Tactic:
by
  ext ⟨k, i⟩ ⟨k', j⟩
  simp only [blockDiagonal'_apply, mul_apply, ← Finset.univ_sigma_univ, Finset.sum_sigma]
  rw [Fintype.sum_eq_single k]
  · simp only [dif_pos]
    split_ifs <;> simp
  · intro j' hj'
    exact Finset.sum_eq_zero fun _ _ => by rw [dif_neg hj'.symm, zero_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ ∃ y, ∃ (yN : y ∈ N), ψ' ⟨y, ⋯⟩ = d

Tactic:
refine ⟨y, yN, ?_⟩

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ ψ' ⟨y, ⋯⟩ = d
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f g : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (f + g))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A f + baseChange A g)) 1) x✝

Tactic:
simp [baseChange_eq_ltensor, -baseChange_tmul]

Goal state after:
Module: Mathlib.Algebra.Field.Equiv

Goal state before:
pp: A : Type u_1
B : Type u_2
F : Type u_3
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : FunLike F A B
inst✝¹ : MonoidWithZeroHomClass F A B
f : F
inst✝ : IsLocalHom f
inj : Function.Injective ⇑f
hB : IsField B
x y : A
⊢ f (x * y) = f (y * x)

Tactic:
by rw [map_mul, map_mul, hB.mul_comm]

Goal state after: