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

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a✝ : ι
s✝ : Finset ι
⊢ a✝ ∉ s✝ →
    ∏ i ∈ s✝, span R (M i) = span R (∏ i ∈ s✝, M i) →
      ∏ i ∈ insert a✝ s✝, span R (M i) = span R (∏ i ∈ insert a✝ s✝, M i)

Tactic:
H

Goal state after:
case refine_2
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a✝ : ι
s✝ : Finset ι
H : a✝ ∉ s✝
⊢ ∏ i ∈ s✝, span R (M i) = span R (∏ i ∈ s✝, M i) → ∏ i ∈ insert a✝ s✝, span R (M i) = span R (∏ i ∈ insert a✝ s✝, M i)
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
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝ : Small.{max u ?u.51, v} M
this : AddCommMonoid (Shrink.{max u ?u.51, v} M) := (equivShrink M).symm.addCommMonoid
⊢ Injective ⇑f

Tactic:
let := Equiv.module R (equivShrink M).symm

Goal state after:
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
hi : Injective ⇑i
hf : Surjective ⇑f
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective ⇑g
this✝¹ : Small.{max u ?u.51, v} M
this✝ : AddCommMonoid (Shrink.{max u ?u.51, v} M) := (equivShrink M).symm.addCommMonoid
this : Module R (Shrink.{max u ?u.51, v} M) := Equiv.module R (equivShrink M).symm
⊢ Injective ⇑f
Module: Mathlib.RingTheory.Ideal.Operations

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

Tactic:
refine ⟨_, add_mem hi' (mul_mem_left _ j hi1), _, mul_mem_mul hj hk, ?_⟩

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ r • n = 0

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hn

Goal state after:
case mpr.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ x ∈ s, r • x = 0

case mpr.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ r • 0 = 0

case mpr.refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (x y : M), x ∈ span R s → y ∈ span R s → r • x = 0 → r • y = 0 → r • (x + y) = 0

case mpr.refine_4
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
h : ∀ (n : ↑s), r • ↑n = 0
n : M
hn : n ∈ span R s
⊢ ∀ (a : R), ∀ x ∈ span R s, r • x = 0 → r • a • x = 0
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
s : Multiset α
⊢ s.lcm = 0 ↔ 0 ∈ s

Tactic:
induction s using Multiset.induction_on with

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
IH : s.dedup.lcm = s.lcm
h : a ∈ s
⊢ GCDMonoid.lcm a (fold GCDMonoid.lcm 1 (s.erase a)) = GCDMonoid.lcm (normalize a) (fold GCDMonoid.lcm 1 (s.erase a))

Tactic:
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 ∈ s, J i) ⊔ I = ⊤

Tactic:
rw [sup_comm, sup_iInf_eq_top]; intro i hi; rw [sup_comm, h i hi]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
⊢ ∃ t, s = map (fun x ↦ s.gcd * x) t ∧ t.gcd = 1

Tactic:
· choose f hf using @gcd_dvd _ _ _ s
      refine ⟨s.pmap @f fun _ ↦ id, ?_, extract_gcd' s _ h ?_⟩ <;>
      · rw [map_pmap]
        conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
        congr with (x hx)
        rw [id, ← hf hx]

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

Goal state before:
pp: z : ℤ
⊢ |z| = normalize z

Tactic:
cases le_total 0 z <;>
  simp [abs_of_nonneg, abs_of_nonpos, normalize_of_nonneg, normalize_of_nonpos, *]

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

Goal state before:
pp: a b : ℤ
⊢ Associated (↑(a.gcd b * a.lcm b)) (a * b)

Tactic:
gcd_mul_lcm,

Goal state after:
a b : ℤ
⊢ Associated (↑(a.natAbs * b.natAbs)) (a * b)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
s : Multiset (Ideal R)
h : ∀ p ∈ s, I ⊔ p = ⊤
⊢ I ⊔ 1 = ⊤

Tactic:
by simp only [one_eq_top, le_top, sup_of_le_right]

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ a * ↑u * ↑(Exists.choose ⋯) = out (Associates.mk a)

Tactic:
(assoc _).choose_spec,

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
out : Associates α → α
mk_out : ∀ (a : Associates α), Associates.mk (out a) = a
out_one : out 1 = 1
assoc : ∀ (a : α), Associated a (out (Associates.mk a))
this : (p : Prop) → Decidable p := Classical.dec
a : α
u : αˣ
ha : a ≠ 0
⊢ out (Associates.mk (a * ↑u)) = out (Associates.mk a)
Module: Mathlib.Algebra.GCDMonoid.Basic

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

Tactic:
by
  simp only [mul_comm, gcd_mul_left']

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
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)

Goal state after:
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 : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
⊢ Fintype.card α ≤ Fintype.card β
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

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

Tactic:
let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective ⇑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
⊢ Fintype.card β ≤ Fintype.card α
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Ideal R
inst✝ : IsPrincipal S
is_prime : S.IsPrime
ne_bot : S ≠ ⊥
x✝¹ x✝ : R
⊢ generator S ∣ x✝¹ * x✝ → generator S ∣ x✝¹ ∨ generator S ∣ x✝

Tactic:
by
    simpa only [← mem_iff_generator_dvd S] using is_prime.2

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Subsingleton

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
⊢ ⨆ ι, Cardinal.mk ↑↑ι = 0

Tactic:
← bot_eq_zero,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
⊢ ⨆ ι, Cardinal.mk ↑↑ι = ⊥
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
⊢ lcm c b * a ∣ lcm c b * Classical.choose ⋯

Tactic:
← 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
h0 : lcm c b ≠ 0
⊢ lcm c b * a ∣ lcm c b * Classical.choose ⋯

Tactic:
← Classical.choose_spec (exists_gcd c b)

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
⊢ lcm c b * a ∣ c * b
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
N : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
S : Submodule R N
hI : (comap f S).IsPrincipal
⊢ S.IsPrincipal

Tactic:
rw [← Submodule.map_comap_eq_of_surjective hf S]
  exact hI.map f

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
p n : R
hp : Irreducible p
⊢ IsCoprime p n ↔ ¬p ∣ n

Tactic:
rw [← isRelPrime_iff_isCoprime, hp.isRelPrime_iff_not_dvd]

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : Associated (c ^ k) (a * b)
u : Rˣ
hu : a * b * ↑u = c ^ k
⊢ ∃ d, Associated (d ^ k) a

Tactic:
exact exists_associated_pow_of_mul_eq_pow'
    ((isCoprime_mul_unit_right_right u.isUnit a b).mpr hab) <| mul_assoc a _ _ ▸ hu

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this✝ : Nontrivial R
this : Finite ι
val✝ : Fintype ι
⊢ #ι ≤ ↑(Fintype.card ↑w)

Tactic:
rw [Cardinal.mk_fintype ι]

Goal state after:
case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this✝ : Nontrivial R
this : Finite ι
val✝ : Fintype ι
⊢ ↑(Fintype.card ι) ≤ ↑(Fintype.card ↑w)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case inl
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
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
⊢ #κ ≤ #ι

Tactic:
rw [Cardinal.mk_fintype ι]

Goal state after:
case inl
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
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
⊢ #κ ≤ ↑(Fintype.card ι)
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
i j : n
b : α
w : n → α
x✝ : n
⊢ (single i j b *ᵥ w) x✝ = ((b * w j) • Pi.single i 1) x✝

Tactic:
simp [Matrix.single_mulVec, Function.update_apply, Pi.single_apply]

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✝² : AddCommMonoid α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : m → n → α
i : m
j : n
⊢ (∑ x_1, single x_1.1 x_1.2 (x x_1.1 x_1.2)) i j = of x i j

Tactic:
simp [single, Matrix.sum_apply, Matrix.of_apply, ← Prod.mk_inj]

Goal state after:
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:
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.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Finite ι₁
inst✝ : Finite ι₂
⊢ Module.Finite R (Matrix ι₁ ι₂ M)

Tactic:
cases nonempty_fintype ι₁
  cases nonempty_fintype ι₂
  exact Module.Finite.of_basis <| (Free.chooseBasis _ _).matrix _ _

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
x : A
ij : ι' × ι
⊢ (((b.smulTower c).reindex (Equiv.prodComm ι ι')).repr x) ij = (b.repr ((c.repr x) ij.1)) ij.2

Tactic:
repr_reindex_apply,

Goal state after:
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
x : A
ij : ι' × ι
⊢ ((b.smulTower c).repr x) ((Equiv.prodComm ι ι').symm ij) = (b.repr ((c.repr x) ij.1)) ij.2
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ Multiset.toFinset 0 = support 0

Tactic:
Multiset.toFinset_zero,

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ ∅ = support 0
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: n : Type u_3
R : Type u_7
α : Type u_11
β : Type u_12
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
⊢ ((algebraMap R (Matrix n n α)) r).map f = (algebraMap R (Matrix n n β)) r

Tactic:
by
  rw [algebraMap_eq_diagonal, algebraMap_eq_diagonal, diagonal_map hf]
  simp [hf₂]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
α : Type u_11
β : Type u_12
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module R α
inst✝² : Module S β
σᵣₛ : R →+* S
σₛᵣ : S →+* R
inst✝¹ : RingHomInvPair σᵣₛ σₛᵣ
inst✝ : RingHomInvPair σₛᵣ σᵣₛ
f : α ≃ₛₗ[σᵣₛ] β
i : m
j : n
⊢ entryLinearMap S β i j ∘ₛₗ ↑f.mapMatrix = ↑f ∘ₛₗ entryLinearMap R α i j

Tactic:
by
  simp only [mapMatrix_toLinearMap, LinearMap.entryLinearMap_comp_mapMatrix]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
N' : Type v'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
cnd : lift.{v', v} (Module.rank R M) < lift.{v, v'} (Module.rank R N')
⊢ ∃ f, Injective ⇑f

Tactic:
rcases exists_set_linearIndependent_of_lt_lift_rank cnd with ⟨s, hs, hs₂⟩
  exact exists_linearMap_injective_of_linearIndependent_of_lift_rank_le
    hs₂.linearIndependent hs.symm.le

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 : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ (adjoin R (⋃₀ (SetLike.coe '' S))).toSubsemiring = Subsemiring.closure (⋃₀ (SetLike.coe '' S))

Tactic:
adjoin_toSubsemiring

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ ⋃₀ (SetLike.coe '' S)) =
    Subsemiring.closure (⋃₀ (SetLike.coe '' S))
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
hi : IsInternal A
⊢ iSup A = A i ⊔ A j

Tactic:
rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]

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

Goal state before:
pp: case refine_1
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
a : A
ha : a ∈ s
⊢ ⟨a, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Tactic:
exact subset_adjoin ha

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

Goal state before:
pp: 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✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
⊢ (iSupLift K dir f hf T hT).comp (inclusion h) = f i

Tactic:
by
  ext
  simp only [NonUnitalAlgHom.comp_apply, iSupLift_inclusion]

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

Goal state before:
pp: case mul
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
y z : A
hx✝ : y ∈ adjoin R s
hy✝ : z ∈ adjoin R s
hy : Commute a y
hz : Commute a z
⊢ Commute a (y * z)

Tactic:
exact hy.mul_right hz

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

Goal state before:
pp: case inr.inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
hk : k ≠ k'
⊢ single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')

Tactic:
rw [single_apply_of_row_ne hk,
      single_apply_of_row_ne (ne_of_apply_ne Prod.snd hk)]

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
s : Finset ι
x : ι → R
h : ∀ i ∈ s, IsSelfAdjoint (x i)
⊢ IsSelfAdjoint (∑ i ∈ s, x i)

Tactic:
simpa [IsSelfAdjoint, star_sum] using Finset.sum_congr rfl fun _ hi => h _ hi

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a u : R
hu : IsUnit u
⊢ IsSelfAdjoint (u * a * star u) ↔ IsSelfAdjoint a

Tactic:
simp [IsSelfAdjoint, mul_assoc, hu.mul_right_inj, hu.star.mul_left_inj]

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

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst✝⁶ : Mul R
inst✝⁵ : Star R
inst✝⁴ : Mul S
inst✝³ : Star S
inst✝² : FunLike F R S
inst✝¹ : MulHomClass F R S
inst✝ : StarHomClass F R S
f : F
r : R
hr : IsStarNormal r
⊢ Commute (star (f r)) (f r)

Tactic:
by simpa [map_star] using! congr(f $(hr.star_comm_self))

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x✝ y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
span_b : N = span R (Set.range (⇑N.subtype ∘ ⇑b))
c : R
x : M
hx : x ∈ span R (Set.range (⇑N.subtype ∘ ⇑b))
hc : c • y + x = 0
⊢ c = 0

Tactic:
rw [← span_b] at hx

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x✝ y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
span_b : N = span R (Set.range (⇑N.subtype ∘ ⇑b))
c : R
x : M
hx : x ∈ N
hc : c • y + x = 0
⊢ c = 0