mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Tactic:
← lcm_dedup,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).dedup.lcm = GCDMonoid.lcm s₁.lcm s₂.lcm
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Tactic:
← lcm_dedup,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).dedup.lcm = GCDMonoid.lcm s₁.lcm s₂.lcm
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).lcm = GCDMonoid.lcm a s.lcm

Tactic:
← lcm_dedup,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).dedup.lcm = GCDMonoid.lcm a s.lcm
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:
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.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsPrime}
hJ' : map f J = j
⊢ j ∈ {J | map f I ≤ J ∧ J.IsPrime}

Tactic:
have : J.IsPrime := hJ.right

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this✝ : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsPrime}
hJ' : map f J = j
this : J.IsPrime
⊢ j ∈ {J | map f I ≤ J ∧ J.IsPrime}
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
⊢ (∅ ∪ s₂).gcd f = GCDMonoid.gcd (∅.gcd f) (s₂.gcd f)

Tactic:
rw [empty_union, gcd_empty, gcd_zero_left, normalize_gcd]

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ Multiset.inf 0

Tactic:
rw [Multiset.inf_zero]

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ ⊤
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
ha : a ≠ 0
⊢ Associated (gcd (a * b) (a * c)) (a * gcd b c)

Tactic:
obtain ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c)

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : gcd (a * b) (a * c) = a * d
⊢ Associated (gcd (a * b) (a * c)) (a * gcd b c)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg.succ
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b ^ (k + 1)) ∣ gcd a b ^ (k + 1)

Tactic:
pow_succ',

Goal state after:
case neg.succ
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b * b ^ k) ∣ gcd a b ^ (k + 1)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Multiset R
⊢ s.prod ∈ I ↔ ∃ p ∈ s, p ∈ I

Tactic:
by
  simpa using (hI.multiset_prod_map_le (span {·}))

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hI : IsPrincipal I
⊢ Ideal.map f I = Ideal.span (⇑f '' {generator I})

Tactic:
← Ideal.map_span,

Goal state after:
R : Type u
S : Type u_1
F : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I : Ideal R
hI : IsPrincipal I
⊢ Ideal.map f I = Ideal.map f (Ideal.span {generator I})
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a : G₀
h0 : a ≠ 0
⊢ normalize a = 1

Tactic:
by simp [normalize_apply, h0]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq m
a : α
⊢ MulOpposite.op a • 1 = diagonal fun x ↦ a

Tactic:
simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, op_smul_eq_mul, one_mul]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
u : m → α
v w : n → α
⊢ vecMulVec u v *ᵥ w = MulOpposite.op (v ⬝ᵥ w) • u

Tactic:
by
  ext i
  simp [mulVec, dotProduct, vecMulVec, Finset.mul_sum, mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι × ι'
⊢ (b.smulTower c) ij = b ij.1 • c ij.2

Tactic:
by
  classical
  obtain ⟨i, j⟩ := ij
  rw [Basis.apply_eq_iff]
  ext ⟨i', j'⟩
  rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]
  dsimp only
  split_ifs with hi
  · simp [hi, Finsupp.single_apply]
  · simp [hi]

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

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

Tactic:
by
  ext; simp [vecMul_diagonal]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset

Tactic:
· rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (iUnionLift S f hf (iUnion S) ⋯ x)

Tactic:
iUnionLift_of_mem x hi,

Goal state after:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (f i ⟨↑x, hi⟩)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ a + b ∈ {x | ∃ m ∈ M, m * x ∈ s}

Tactic:
refine ⟨_, mul_mem hn hm, ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ n * m * (a + b) ∈ s
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p✝ p : Submodule R A
h_one : 1 ∈ p
h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p
r : R
⊢ (algebraMap R A) r ∈ p.carrier

Tactic:
by
      rw [Algebra.algebraMap_eq_smul_one]
      exact p.smul_mem _ h_one

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_11
inst✝¹ : Semiring S
inst✝ : Algebra R S
m : R ⊗[R] M
this :
  ∀ (m : M), (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) m = 1 ⊗ₜ[R] m
⊢ 1 ⊗ₜ[R] (TensorProduct.lid R M) m = (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap) m

Tactic:
simp [← this]

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

Goal state before:
pp: case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ ↑(Submonoid.closure s) ⊆ ↑(Subalgebra.toSubmodule (adjoin R s))

Tactic:
change Submonoid.closure s ≤ (adjoin R s).toSubsemiring.toSubmonoid

Goal state after:
case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Submonoid.closure s ≤ (adjoin R s).toSubmonoid
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
s : Set A
x : A
⊢ x ∈ (adjoin R s).toSubring ↔ x ∈ Subring.closure (Set.range ⇑(algebraMap R A) ∪ s)

Tactic:
adjoin_eq_ring_closure

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
s : Set A
x : A
⊢ x ∈ Subring.closure (Set.range ⇑(algebraMap R A) ∪ s) ↔ x ∈ Subring.closure (Set.range ⇑(algebraMap R A) ∪ s)
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
⊢ ((finsuppTensorFinsupp R S M N ι κ) (f ⊗ₜ[R] g)) (i, k) = f i ⊗ₜ[R] g k

Tactic:
induction f using Finsupp.induction_linear with

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddMonoid (R i)
inst✝ : (i : ι) → StarAddMonoid (R i)
i : ι
r : R i
⊢ star (single i r) = single i (star r)

Tactic:
by
  ext; exact apply_single (fun _ ↦ star) (fun _ ↦ star_zero _) ..

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

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝³ : DivisionSemiring R
inst✝² : MulAction R M
inst✝¹ : MulAction ℚ≥0 M
inst✝ : IsScalarTower ℚ≥0 R M
q : ℚ≥0
x : M
⊢ ↑q • x = q • x

Tactic:
← one_smul R x,

Goal state after:
M : Type u_1
R : Type u_3
inst✝³ : DivisionSemiring R
inst✝² : MulAction R M
inst✝¹ : MulAction ℚ≥0 M
inst✝ : IsScalarTower ℚ≥0 R M
q : ℚ≥0
x : M
⊢ ↑q • 1 • x = q • 1 • x
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝³ : DivisionRing R
inst✝² : MulAction R M
inst✝¹ : MulAction ℚ M
inst✝ : IsScalarTower ℚ R M
q : ℚ
x : M
⊢ ↑q • x = q • x

Tactic:
← one_smul R x,

Goal state after:
M : Type u_1
R : Type u_3
inst✝³ : DivisionRing R
inst✝² : MulAction R M
inst✝¹ : MulAction ℚ M
inst✝ : IsScalarTower ℚ R M
q : ℚ
x : M
⊢ ↑q • 1 • x = q • 1 • x
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝ : InvolutiveStar R
x : R
⊢ IsSelfAdjoint (star x) ↔ IsSelfAdjoint x

Tactic:
simpa only [IsSelfAdjoint, star_star] using eq_comm

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:
diagonal_updateCol_single,

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : DecidableEq n
A : Matrix m n α
j j' : n
h : j ≠ j'
x y : m → α
⊢ (A.updateCol j x).updateCol j' y = (A.updateCol j' y).updateCol j x

Tactic:
simpa only [updateRow_transpose] using! congr_arg transpose <| updateRow_comm Aᵀ h x y

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) α
k : o
i : m' k
k' : o
j : p' k'
⊢ ∀ (x : o),
    x ≠ k → (∑ x_1, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0) = 0

Tactic:
· 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
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬⊥ < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr ⟨x, ⋯⟩) i ∈ (Finsupp.lapply i ∘ₗ ↑b.repr).submoduleImage N

Tactic:
exact (LinearMap.mem_submoduleImage_of_le hNO).mpr ⟨x, hx, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
x : R
hx : x ∈ I
| R ∙ generator I ≤ Ideal.span {x}

Tactic:
Submodule.span_singleton_le_iff_mem

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
x : R
hx : x ∈ I
| generator I ∈ Ideal.span {x}
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
x✝¹ : A ⊗[R] ↥p
x✝ : x✝¹ ∈ {t | ∃ m n, m ⊗ₜ[R] n = t}
a : A
m : ↥p
h : a ⊗ₜ[R] m = x✝¹
⊢ a • 1 ⊗ₜ[R] p.subtype m ∈ span A ↑(map ((TensorProduct.mk R A M) 1) p)

Tactic:
exact smul_mem _ a (subset_span ⟨m, m.2, rfl⟩)

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

Goal state before:
pp: case neg.intro.refine_1.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c✝ : ι → R
hc✝ : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c✝ i
val✝ : Fintype ι
y' : O := ∑ i, c✝ i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c✝ i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
c : R
z : O
zN' : z ∈ N'
hc : c • y + z = 0
⊢ c • a • y' + z = 0

Tactic:
← a_smul_y'

Goal state after:
case neg.intro.refine_1.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c✝ : ι → R
hc✝ : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c✝ i
val✝ : Fintype ι
y' : O := ∑ i, c✝ i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c✝ i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
c : R
z : O
zN' : z ∈ N'
hc : c • a • y' + z = 0
⊢ c • a • y' + z = 0
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c
R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
r₁ : R
s₁ : ↥S
⊢ (algebraMap R₀ R) r /ₒ 1 * (r₁ /ₒ s₁) = r₁ * (algebraMap R₀ R) r /ₒ s₁

Tactic:
oreDiv_mul_char _ _ _ _ (algebraMap R₀ R r) s₁ (Algebra.commutes _ _).symm,

Goal state after:
case c
R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
r₁ : R
s₁ : ↥S
⊢ (algebraMap R₀ R) r * r₁ /ₒ (s₁ * 1) = r₁ * (algebraMap R₀ R) r /ₒ s₁
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_5
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
R : Type u_8
M : Type u_9
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis ι R M
a : ι → R
s : End R M
hs : ∀ (k : ι), s (b k) = a k • b k
i j : ι
⊢ ⁅s, b.end (i, j)⁆ = (a i - a j) • b.end (i, j)

Tactic:
refine b.ext fun k ↦ ?_

Goal state after:
ι : Type u_5
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
R : Type u_8
M : Type u_9
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis ι R M
a : ι → R
s : End R M
hs : ∀ (k : ι), s (b k) = a k • b k
i j k : ι
⊢ ⁅s, b.end (i, j)⁆ (b k) = ((a i - a j) • b.end (i, j)) (b k)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
x₁ x₂ : Localization (Submonoid.comap (Pi.evalRingHom R i) S)
eq : (mapPiEvalRingHom S) x₁ = (mapPiEvalRingHom S) x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨r₁, s₁, rfl⟩ := exists_mk'_eq T x₁

Goal state after:
case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
x₂ : Localization (Submonoid.comap (Pi.evalRingHom R i) S)
r₁ : (i : ι) → R i
s₁ : ↥T
eq : (mapPiEvalRingHom S) (mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁) = (mapPiEvalRingHom S) x₂
⊢ mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁ = x₂
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst✝¹⁰ : CommSemiring F
inst✝⁹ : CommSemiring L
inst✝⁸ : CommSemiring L'
inst✝⁷ : Semiring E
inst✝⁶ : Algebra F L
inst✝⁵ : Algebra L E
inst✝⁴ : Algebra F L'
inst✝³ : Algebra L' E
inst✝² : Algebra F E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
K K' : Subalgebra F E
h : K.toSubsemiring = K'.toSubsemiring
⊢ K = K'

Tactic:
by rwa [SetLike.ext'_iff] at h ⊢

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroupWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
n : ℕ
⊢ ↑(Int.negSucc n) ⊗ₜ[R] 1 = -↑(n + 1)

Tactic:
by simp [natCast_def, add_tmul, neg_tmul, one_def]

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
x y z : PreQuasiregular R
⊢ equiv.symm (x * y * z) = equiv.symm (x * (y * z))

Tactic:
simp [mul_add, add_mul, mul_assoc]; abel

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : StarOrderedRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module R A
inst✝⁵ : StarModule R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : IsDomain R
inst✝¹ : IsCancelAdd A
inst✝ : Module.IsTorsionFree R A
r : R
a✝ a : A
ha₀ : a ≠ 0
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hr₀ : r ≠ 0
hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ r • (a✝ + a) = r • a✝ + p

Tactic:
exact ⟨r • a, smul_ne_zero hr₀ ha₀, smul_mem_closure_star_mul hr ha, smul_add ..⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
hf : ∃ x, ¬f x = 0 x
⊢ ∃ w, f w = 1

Tactic:
rcases hf with ⟨w, hw⟩

Goal state after:
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : ¬f w = 0 w
⊢ ∃ w, f w = 1
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
⊢ Module.Finite R (ι →₀ M) → IsEmpty ι ∨ Subsingleton M ∨ Module.Finite R M ∧ Finite ι

Tactic:
simp only [or_iff_not_imp_left, not_subsingleton_iff_nontrivial, not_isEmpty_iff]

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
⊢ Module.Finite R (ι →₀ M) → Nonempty ι → Nontrivial M → Module.Finite R M ∧ Finite ι