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✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
x : ι → A
⊢ ∏ i ∈ s, R ∙ x i = R ∙ ∏ i ∈ s, x i

Tactic:
rw [prod_span, Set.finsetProd_singleton]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module S P
σ : R →+* S
inst✝¹ : RingHomSurjective σ
s : Submodule R M
f : M →ₛₗ[σ] P
inst✝ : IsNoetherian R ↥s
⊢ (f.submoduleMap s).range = ⊤

Tactic:
by simp [LinearMap.submoduleMap]

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
I : Ideal R
N : Submodule R M
x : ↥N
⊢ x ∈ I • ⊤ ↔ ↑x ∈ I • N

Tactic:
by
  have : Submodule.map N.subtype (I • ⊤) = I • N := by
    rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]
  simp [← this, -map_smul'']

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

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

Tactic:
let := Classical.decEq ι

Goal state after:
case mp.refine_1.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
y : R
hy : y ∈ ↑I
i j : ι
this : DecidableEq ι := Classical.decEq ι
⊢ (Finsupp.single i y) j ∈ I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
rcf : RingHomClass F R S
inst✝ : Nontrivial S
f : F
⊢ 1 ∉ ker f

Tactic:
rw [mem_ker, map_one]
  exact one_ne_zero

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

Tactic:
rw [eq_comm]
  apply eq_div_of_mul_eq_right h1
  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 = x - y / z

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

Goal state after:
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.gcd = s.gcd
⊢ (a ::ₘ s).dedup.gcd = (a ::ₘ s).gcd

Tactic:
by_cases h : a ∈ s; swap; · simp [IH, h]
    simp only [h, dedup_cons_of_mem, IH, gcd_cons]
    unfold gcd
    rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]
    apply (associated_normalize _).gcd_eq_left

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

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

Tactic:
normalize_eq_one,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x, x ∈ s ∧ x ≠ 0
ht : s = map (fun x ↦ s.gcd * x) t
⊢ IsUnit t.gcd
Module: Mathlib.Algebra.GCDMonoid.Finset

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

Tactic:
normalize_eq_one,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hs : ∃ x ∈ s, f x ≠ 0
hg : ∀ b ∈ s, f b = s.gcd f * g b
⊢ IsUnit (s.gcd g)
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
ha : ↑a ≠ 0
⊢ IsUnit a ↔ (↑a)⁻¹ ∈ S

Tactic:
rw [isUnit_iff_and, and_iff_right ha]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ Associates.out 0 = 0

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ
⊢ {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2

Tactic:
rw [this, Set.wellFoundedOn_image, Set.wellFoundedOn_univ]

Goal state after:
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ
⊢ WellFounded (Function.onFun (fun x1 x2 ↦ x1 > x2) fun a ↦ span {a})
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ
x✝¹ x✝ : α
⊢ Function.onFun (fun x1 x2 ↦ x1 > x2) (fun a ↦ span {a}) x✝¹ x✝ ↔ DvdNotUnit x✝¹ x✝

Tactic:
exact Ideal.span_singleton_lt_span_singleton

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (factors a).prod ~ᵤ a

Tactic:
factors,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (if h : a = 0 then 0 else Classical.choose ⋯).prod ~ᵤ a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a x : α
hx : x ∈ factors a
ane0 : a ≠ 0
⊢ Prime x

Tactic:
factors,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a x : α
hx : x ∈ if h : a = 0 then 0 else Classical.choose ⋯
ane0 : a ≠ 0
⊢ Prime x
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
⊢ lcm a b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a b : α
⊢ Associated (gcd a b * if a = 0 then 0 else normalize (Classical.choose ⋯)) (a * b)

Tactic:
split_ifs with a0
      · rw [mul_zero, a0, zero_mul]
      · exact .trans ((normalize_associated _).mul_left _)
          (.of_eq (Classical.choose_spec (_ : _ ∣ a * b)).symm)

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

Goal state before:
pp: case pos
α : 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 : α
h : a = 0
⊢ Associated (b * lcm 0 b) (0 * b)

Tactic:
eq_zero_of_zero_dvd (dvd_lcm_left _ _),

Goal state after:
case pos
α : 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 : α
h : a = 0
⊢ Associated (b * 0) (0 * b)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : 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 : α
h : a = 0
⊢ Associated (normalize b * lcm 0 b) (0 * b)

Tactic:
eq_zero_of_zero_dvd (dvd_lcm_left _ _),

Goal state after:
case pos
α : 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 : α
h : a = 0
⊢ Associated (normalize b * 0) (0 * b)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : MulOneClass α
inst✝ : AddCommMonoid α
v : n → α
⊢ v ⬝ᵥ 1 = ∑ i, v i

Tactic:
simp [(· ⬝ᵥ ·)]

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : MulOneClass α
inst✝ : AddCommMonoid α
v : n → α
⊢ 1 ⬝ᵥ v = ∑ i, v i

Tactic:
simp [(· ⬝ᵥ ·)]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
⊢ ∃ b, b ≠ 0 ∧ b ⬝ᵥ a = 0

Tactic:
by
  obtain ⟨i, j, hij⟩ : ∃ i j : m, i ≠ j := nontrivial_iff.mp ‹_›
  classical
  use if a i = 0 then Pi.single i 1 else if a j = 0 then Pi.single j 1 else
    fun k => if k = i then a j else if k = j then - a i else 0
  split_ifs with h h2
  · simp [h]
  · simp [h2]
  · refine ⟨Function.ne_iff.mpr ⟨i, by simp [h2]⟩, ?_⟩
    simp [dotProduct, Finset.sum_ite, Finset.sum_eq_ite i, hij.symm, mul_comm (a i)]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst✝¹¹ : DecidableEq m
inst✝¹⁰ : DecidableEq n
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : Module S β
inst✝ : SMulCommClass R S β
f : m → n → α →ₗ[R] β
i : m
j : n
a : α
⊢ ((liftLinear S) f) (single i j a) = (f i j) a

Tactic:
dsimp [liftLinear, -LinearMap.lsum_apply, LinearEquiv.congrLeft, LinearEquiv.piCongrRight]
  simp_rw [of_symm_single, LinearMap.lsum_piSingle]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Nontrivial R
⊢ ¬span {r} = 0 ↔ r ≠ 0

Tactic:
zero_eq_bot,

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Nontrivial R
⊢ ¬span {r} = ⊥ ↔ r ≠ 0
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
h' : x ∈ s
⊢ x = a

Tactic:
rwa [← mem_toFinset, H, Finset.mem_singleton] at h'

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

Goal state before:
pp: case a.h
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ a ≤ s.sup' hs fun i ↦ f i + a

Tactic:
exact Finset.le_sup'_of_le _ hs.choose_spec le_add_self

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

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{v, w} #(Free.ChooseBasisIndex K A))

Tactic:
lift_mul,

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K)) *
      lift.{w, max v w} (lift.{v, w} #(Free.ChooseBasisIndex K A))
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Free R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : Free R M'
inst✝ : StrongRankCondition R
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
⊢ Nonempty (M ≃ₗ[R] M')

Tactic:
by
  obtain ⟨⟨α, B⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  obtain ⟨⟨β, B'⟩⟩ := Module.Free.exists_basis (R := R) (M := M')
  have : Cardinal.lift.{v', v} #α = Cardinal.lift.{v, v'} #β := by
    rw [B.mk_eq_rank'', cnd, B'.mk_eq_rank'']
  exact (Cardinal.lift_mk_eq.{v, v', 0}.1 this).map (B.equiv B')

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S✝ T U : Subalgebra R A
h : S✝ ≤ T
α : Type u_1
β : Type u_2
inst✝ : IsDomain A
S : Subalgebra R A
⊢ ∀ (r : ↥S) (m : A), ↑r • m = r • m

Tactic:
simp [smul_def]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
𝒞 : Basis κ R N
x : M ⊗[R] N
⊢ ∃ b, (b.sum fun i m ↦ m ⊗ₜ[R] 𝒞 i) = x

Tactic:
simpa using (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.surjective x

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ⇑f
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg : ∀ (i : ι), f ∘ₗ g i = DFinsupp.lsingle i
⊢ ∃ h, f ∘ₗ h = LinearMap.id

Tactic:
replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ DFunLike.congr_fun (hg i)

Goal state after:
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ⇑f
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg : ∀ (i : ι) (x : A i), f ((g i) x) = DFinsupp.single i x
⊢ ∃ h, f ∘ₗ h = LinearMap.id
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
s : S
t : (ι →₀ M) ⊗[R] N
⊢ (finsuppLeft R S M N ι) (s • t) = s • (finsuppLeft R S M N ι) t

Tactic:
by
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : Algebra R S
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
ι : Type u_5
inst✝ : DecidableEq ι
s : S
t : M ⊗[R] (ι →₀ R)
⊢ (finsuppScalarRight R S M ι) (s • t) = s • (finsuppScalarRight R S M ι) t

Tactic:
by
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
i : ι × κ
r : R
⊢ (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r

Tactic:
by
  nth_rw 1 [← one_mul r]
  exact finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
⊢ finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ

Tactic:
by
  rw [finsuppTensorFinsupp', finsuppTensorFinsuppLid, finsuppTensorFinsuppRid,
    TensorProduct.lid_eq_rid]

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

Goal state before:
pp: case inr.inr
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
⊢ single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')

Tactic:
obtain hk | rfl := ne_or_eq k k'

Goal state after:
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')

case inr.inr.inr
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
l' : L
⊢ single k l r k l' = single (i, k) (j, l) r (i, k) (j, l')
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (z * x * star z)

Tactic:
simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (star z * x * z)

Tactic:
simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
i : m
j : n
a : α
⊢ (single i j a)ᴴ = single j i (star a)

Tactic:
by
  change (single i j a).transpose.map starAddEquiv = single j i (star a)
  simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : AddCommMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : Module R A
inst✝ : StarModule R A
x : A
⊢ (starLinearEquiv R).symm x = starAddEquiv.invFun x

Tactic:
by
  simp

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

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

Tactic:
rw [map_natCast_star]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
c : ℕ
M : Matrix m n α
⊢ (c • M)ᴴ = c • Mᴴ

Tactic:
by
  simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
c : ℤ
M : Matrix m n α
⊢ (c • M)ᴴ = c • Mᴴ

Tactic:
by
  simp

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
j : m ⊕ l
⊢ (fromBlocks A B C D).submatrix f Sum.swap i j = (fromBlocks B A D C).submatrix f id i j

Tactic:
cases j <;> dsimp <;> cases f i

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : m
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (Sum.inr val✝¹) = fromBlocks B A D C (Sum.inl val✝) (Sum.inl val✝¹)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : m
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (Sum.inr val✝¹) = fromBlocks B A D C (Sum.inr val✝) (Sum.inl val✝¹)

case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : l
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (Sum.inl val✝¹) = fromBlocks B A D C (Sum.inl val✝) (Sum.inr val✝¹)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : l
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (Sum.inl val✝¹) = fromBlocks B A D C (Sum.inr val✝) (Sum.inr val✝¹)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: n : ℕ
m' : Type uₘ
α : Type u_1
inst✝ : NonUnitalCommSemiring α
A : m' → Fin n.succ → α
x : α
v : Fin n → α
⊢ of A *ᵥ vecCons x v = x • vecHead ∘ A + of (vecTail ∘ A) *ᵥ v

Tactic:
ext i
  simp [mulVec, mul_comm]

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
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr x) i = 0

Tactic:
exact
    (Submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 <| hϕ (Finsupp.lapply i ∘ₗ ↑b.repr)) _
      ⟨x, hx, rfl⟩

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

Goal state before:
pp: α : Type u
inst✝ : Add α
a₀ a₁ b₀ b₁ : α
⊢ ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁]

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
inst✝ : Add α
a₀ a₁ a₂ b₀ b₁ b₂ : α
⊢ ![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂]

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
R : Type u_1
inst✝ : SMul R α
x : R
a₀ a₁ : α
⊢ x • ![a₀, a₁] = ![x • a₀, x • a₁]

Tactic:
by
  simp

Goal state after: