mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : F
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
x : R
hx : x ∈ comap f ⊥
⊢ x ∈ ⊥

Tactic:
mem_comap,

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
x : R
hx : f x ∈ ⊥
⊢ x ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
⊢ I = span {x} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I

Tactic:
by
  simp only [le_antisymm_iff, le_span_singleton_mul_iff, span_singleton_mul_le_iff]

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

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

Tactic:
exact normalize_zero

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

Goal state before:
pp: α : 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 * gcd a (b ^ k) ∣ gcd a b * gcd a b ^ k

Tactic:
exact (mul_dvd_mul_iff_left hg).mpr hk

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2
this : WellFounded fun x1 x2 ↦ x1 > x2
⊢ WellFounded DvdNotUnit

Tactic:
convert! InvImage.wf (fun a => ⟨Ideal.span ({ a } : Set α), _, rfl⟩) this

Goal state after:
α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2
this : WellFounded fun x1 x2 ↦ x1 > x2
⊢ DvdNotUnit = InvImage (fun x1 x2 ↦ x1 > x2) fun a ↦ ⟨Ideal.span {a}, ⋯⟩
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
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
a : α
a0 : a = 0
⊢ 0 = 0

pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
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
a : α
a0 : ¬a = 0
⊢ Classical.choose ⋯ = 0

Tactic:
· rfl

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
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
a : α
a0 : ¬a = 0
⊢ Classical.choose ⋯ = 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : 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 : α
a0 : a = 0
⊢ 0 = 0

pp: case neg
α : 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 : α
a0 : ¬a = 0
⊢ normalize (Classical.choose ⋯) = 0

Tactic:
· rfl

Goal state after:
case neg
α : 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 : α
a0 : ¬a = 0
⊢ normalize (Classical.choose ⋯) = 0
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ b ∈ factors a, b ∈ s
hunit : ∀ (c : Rˣ), ↑c ∈ s
⊢ a ∈ s

Tactic:
rcases (factors_spec a ha).2 with ⟨c, hc⟩

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ b ∈ factors a, b ∈ s
hunit : ∀ (c : Rˣ), ↑c ∈ s
c : Rˣ
hc : (factors a).prod * ↑c = a
⊢ a ∈ s
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
⊢ #α ≤ #β

Tactic:
let b : Basis β R (β →₀ R) := ⟨1⟩

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b : Basis β R (β →₀ R) := { repr := 1 }
⊢ #α ≤ #β
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ finrank R M = 0 ↔ Subsingleton M

Tactic:
by
  have := Module.rank_lt_aleph0 R M
  rw [← not_le] at this
  simp [Module.finrank, this, Module.rank_zero_iff_of_free]

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

Goal state before:
pp: case inr.inl.inl
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i : n
⊢ M i i = M i i

pp: case inr.inl.inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j : n
hij : i ≠ j
⊢ M i i = M j j

Tactic:
· rfl

Goal state after:
case inr.inl.inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j : n
hij : i ≠ j
⊢ M i i = M j j
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : LinearOrder M
inst✝¹ : Add M
inst✝ : AddRightMono M
s : Finset ι
a : WithBot M
f : ι → M
⊢ fold max ⊥ (fun i ↦ ↑(f i) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a

Tactic:
classical induction s using Finset.induction_on <;> simp [*, max_add_add_right]

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a a' : α
x✝ : f a' ≠ 0
H : a' ≠ a
⊢ f a' * Multiset.count a {a'} = 0

Tactic:
by simp only [Multiset.count_singleton, if_false, H.symm, mul_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I I' J' : TwoSidedIdeal R
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } I' ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } J' ↔
    I' ≤ J'

Tactic:
by simpa [ringCon_le_iff] using RingCon.opOrderIso.map_rel_iff

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
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
⊢ x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
intro h; convert! this h; rw [rel_iff, sub_zero, mem_mk']; rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon }.ringCon ≤ J.ringCon

Tactic:
exact inf_le_right

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ x * y ∈ {a | ϕ a = ψ a}

Tactic:
by
    rw [Set.mem_ofPred_eq, map_mul, map_mul, hx, hy]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
e : ι ≃ κ
i : ι
k : κ
hik : i = e.symm k
x : M i
y : M (e.symm k)
hxy : cast ⋯ x = y
⊢ (lequivCongrLeft R e) ((lof R ι M i) x) = (lof R κ (fun i ↦ M (e.symm i)) k) y

Tactic:
subst hik hxy

Goal state after:
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
e : ι ≃ κ
k : κ
x : M (e.symm k)
⊢ (lequivCongrLeft R e) ((lof R ι M (e.symm k)) x) = (lof R κ (fun i ↦ M (e.symm i)) k) (cast ⋯ x)
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
ϕ ψ : A →ₐ[R] B
x y : A
hx : ϕ x = ψ x
hy : ϕ y = ψ y
⊢ x * y ∈ {a | ϕ a = ψ a}

Tactic:
by
    rw [Set.mem_ofPred_eq, map_mul, map_mul, hx, hy]

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

Goal state before:
pp: case a
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
⊢ (adjoin R s).toSubmodule ≤ span R ↑(Subsemigroup.closure s)

pp: case a
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
⊢ span R ↑(Subsemigroup.closure s) ≤ (adjoin R s).toSubmodule

Tactic:
· intro x hx
    induction hx using adjoin_induction with
    | mem x hx => exact subset_span <| Subsemigroup.subset_closure hx
    | add x y _ _ hpx hpy => exact add_mem hpx hpy
    | zero => exact zero_mem _
    | mul x y _ _ hpx hpy =>
      apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy
      case Hs => exact fun x y hx hy ↦ subset_span <| mul_mem hx hy
      case Hadd_l => exact fun x y z _ _ _ hxz hyz ↦ by simpa [add_mul] using add_mem hxz hyz
      case Hadd_r => exact fun x y z _ _ _ hxz hyz ↦ by simpa [mul_add] using add_mem hxz hyz
      case Hsmul_l => exact fun r x y _ _ hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy
      case Hsmul_r => exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy
    | smul r x _ hpx => exact smul_mem _ _ hpx

Goal state after:
case a
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
⊢ span R ↑(Subsemigroup.closure s) ≤ (adjoin R s).toSubmodule
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

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

Tactic:
by
  rw [adjoin_eq_span, span_le]

Goal state after:
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
n : ℤ
s : Set A
⊢ adjoin R (insert (↑n) s) = adjoin R s

Tactic:
by
  simpa using adjoin_insert_algebraMap (n : R) s

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

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x : A
hx : x ∈ comap f (map f S)
⊢ x ∈ S ⊔ adjoin R (⇑f ⁻¹' {0})

Tactic:
mem_comap,

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x : A
hx : f x ∈ map f S
⊢ x ∈ S ⊔ adjoin R (⇑f ⁻¹' {0})
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
p : ι →₀ R
n : N
⊢ (finsuppScalarLeft R N ι) (p ⊗ₜ[R] n) = p.sum fun i m ↦ Finsupp.single i (m • n)

Tactic:
ext i
  rw [finsuppScalarLeft_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]

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

Goal state before:
pp: R : Type u_8
S : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module S N
σ : R →+* S
σ' : S →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst✝ : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
g : N →ₗ[S] N →₀ S :=
  { toFun := fun x ↦ mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯, map_smul' := ⋯ }
x : N
hf : e₂ ((linearCombination R id) (f (e₂.symm x))) = e₂ (e₂.symm x)
⊢ (linearCombination S id) (g x) = x

Tactic:
simpa [linearCombination_apply, sum_mapRange_index, g, map_finsuppSum, e₂.map_smulₛₗ] using! hf

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

Goal state before:
pp: case i
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
⊢ M ⊗[R₀] (N →₀ R₀) →ₗ[R] (M →₀ R) ⊗[R₀] (N →₀ R₀)

pp: case s
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
⊢ (M →₀ R) ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀)

pp: case H
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
⊢ ?s ∘ₗ ?i = LinearMap.id

Tactic:
· exact (AlgebraTensorModule.map sM (LinearMap.id (R := R₀) (M := N →₀ R₀)))

Goal state after:
case s
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
⊢ (M →₀ R) ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] (N →₀ R₀)

case H
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
⊢ ?s ∘ₗ AlgebraTensorModule.map sM LinearMap.id = LinearMap.id
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
⊢ Projective R (M ⊗[R₀] N)

Tactic:
have : Module.Projective R (M ⊗[R₀] (N →₀ R₀)) := by
    fapply Projective.of_split (R := R) (M := ((M →₀ R) ⊗[R₀] (N →₀ R₀)))
    · exact (AlgebraTensorModule.map sM (LinearMap.id (R := R₀) (M := N →₀ R₀)))
    · exact (AlgebraTensorModule.map
        (Finsupp.linearCombination R id) (LinearMap.id (R := R₀) (M := N →₀ R₀)))
    · ext; simp [hsM _]

Goal state after:
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ Projective R (M ⊗[R₀] N)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : ¬i✝.2 = j✝.2
⊢ 0 = 0

Tactic:
· rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
r : α
⊢ single i j r = updateCol 0 j (Pi.single i r)

Tactic:
simpa [← updateCol_transpose] using congr($(single_eq_updateRow_zero j i r)ᵀ)

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

Goal state before:
pp: case refine_1
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ (of (vecCons v A) * B) 0 j = of (vecCons (v ᵥ* B) (of.symm (of A * B))) 0 j

pp: case refine_2
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ ∀ (i : Fin m), (of (vecCons v A) * B) i.succ j = of (vecCons (v ᵥ* B) (of.symm (of A * B))) i.succ j

Tactic:
· rfl

Goal state after:
case refine_2
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ ∀ (i : Fin m), (of (vecCons v A) * B) i.succ j = of (vecCons (v ᵥ* B) (of.symm (of A * B))) i.succ j
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁸ : CommSemiring R
inst✝²⁷ : Semiring A
inst✝²⁶ : Semiring B
inst✝²⁵ : Algebra R A
inst✝²⁴ : Algebra R B
inst✝²³ : AddCommMonoid M
inst✝²² : Module R M
inst✝²¹ : Module A M
inst✝²⁰ : IsScalarTower R A M
inst✝¹⁹ : AddCommMonoid N
inst✝¹⁸ : Module R N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : Module R P
inst✝¹⁵ : Module A P
inst✝¹⁴ : IsScalarTower R A P
inst✝¹³ : AddCommMonoid Q
inst✝¹² : Module R Q
inst✝¹¹ : AddCommMonoid P'
inst✝¹⁰ : Module R P'
inst✝⁹ : Module A P'
inst✝⁸ : Module B P'
inst✝⁷ : IsScalarTower R A P'
inst✝⁶ : IsScalarTower R B P'
inst✝⁵ : SMulCommClass A B P'
inst✝⁴ : AddCommMonoid Q'
inst✝³ : Module R Q'
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
x✝¹ x✝ : M →ₗ[A] N →ₗ[R] P
x : M
y : N
⊢ (lift (x✝¹ + x✝)) (x ⊗ₜ[R] y) = (lift x✝¹ + lift x✝) (x ⊗ₜ[R] y)

Tactic:
simp only [lift_tmul, add_apply]

Goal state after:
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 ⊗ₜ[R] m ∈ comap (LinearMap.baseChange A p.subtype) (span A ↑(map ((TensorProduct.mk R A M) 1) p))

Tactic:
mem_comap,

Goal state after:
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✝¹
⊢ (LinearMap.baseChange A p.subtype) (a ⊗ₜ[R] m) ∈ span A ↑(map ((TensorProduct.mk R A M) 1) p)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ span R (Set.range fun x ↦ { toFun := Pi.single x, map_add' := ⋯ } 1 ᵥ* M) = span R (Set.range M.row)

Tactic:
AddHom.coe_mk,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ span R (Set.range fun x ↦ Pi.single x 1 ᵥ* M) = span R (Set.range M.row)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
i : m
j : n
⊢ (toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i

Tactic:
by
  simp [toMatrix]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (if c i ≠ 0 then c i * snf.a i else 0) = snf.a i * c i

Tactic:
ite_not,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (if c i = 0 then 0 else c i * snf.a i) = snf.a i * c i