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

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

Tactic:
← hzr

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

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
case a.cons.cons.inr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
HL : hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
hs : hd ∈ s
⊢ ∃ z_1 r_1, ∃ (_ : r_1 ∈ Submonoid.closure s), z_1 • r_1 = hd * z • r
Module: Mathlib.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
S : NonUnitalSubalgebra 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)
⊢ ↥(iSup K) →ₙₐ[R] B

Tactic:
exact
      { toFun :=
          Set.iUnionLift (fun i => ↑(K i)) (fun i x => f i x)
            (fun i j x hxi hxj => by
              let ⟨k, hik, hjk⟩ := dir i j
              rw [hf i k hik, hf j k hjk]
              rfl)
            _ (by rw [coe_iSup_of_directed dir])
        map_zero' := by
          dsimp
          exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)
        map_mul' := by
          dsimp
          apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
          all_goals simp
        map_add' := by
          dsimp
          apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
          all_goals simp
        map_smul' := fun r => by
          dsimp
          apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => r • x)
            (fun _ _ => rfl)
          all_goals simp }

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
⊢ comap f (map f S) ≤ S ⊔ adjoin R (⇑f ⁻¹' {0})

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
⊢ S ⊔ adjoin R (⇑f ⁻¹' {0}) ≤ comap f (map f S)

Tactic:
·

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
⊢ comap f (map f S) ≤ S ⊔ adjoin R (⇑f ⁻¹' {0})
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
⊢ S ⊔ adjoin R (⇑f ⁻¹' {0}) ≤ comap f (map f S)

Tactic:
·

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
⊢ S ⊔ adjoin R (⇑f ⁻¹' {0}) ≤ comap f (map f S)
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: case right
R : Type u
inst✝¹⁶ : CommSemiring R
S : Type ?u.6
inst✝¹⁵ : Semiring S
inst✝¹⁴ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝¹³ : DecidableEq ι₁
inst✝¹² : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝¹¹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝¹⁰ : AddCommMonoid M₁'
inst✝⁹ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁸ : AddCommMonoid M₂'
inst✝⁷ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝⁶ : Module R M₁'
inst✝⁵ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁴ : Module R M₂'
inst✝³ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝² : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
⊢ (toModule S (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i ↦
        AlgebraTensorModule.map (lof S ι₁ M₁ i.1) (lof R ι₂ M₂ i.2)) ∘ₗ
      AlgebraTensorModule.lift
        (toModule S ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) fun i₁ ↦
          (toModule R ι₂ (M₁ i₁ →ₗ[S] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) fun i₂ ↦
              (AlgebraTensorModule.curry (lof S (ι₁ × ι₂) (fun i ↦ M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))).flip).flip) =
    LinearMap.id

Tactic:
·

Goal state after:
case right
R : Type u
inst✝¹⁶ : CommSemiring R
S : Type ?u.6
inst✝¹⁵ : Semiring S
inst✝¹⁴ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝¹³ : DecidableEq ι₁
inst✝¹² : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝¹¹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝¹⁰ : AddCommMonoid M₁'
inst✝⁹ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁸ : AddCommMonoid M₂'
inst✝⁷ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝⁶ : Module R M₁'
inst✝⁵ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁴ : Module R M₂'
inst✝³ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝² : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
⊢ (toModule S (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i ↦
        AlgebraTensorModule.map (lof S ι₁ M₁ i.1) (lof R ι₂ M₂ i.2)) ∘ₗ
      AlgebraTensorModule.lift
        (toModule S ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) fun i₁ ↦
          (toModule R ι₂ (M₁ i₁ →ₗ[S] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) fun i₂ ↦
              (AlgebraTensorModule.curry (lof S (ι₁ × ι₂) (fun i ↦ M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))).flip).flip) =
    LinearMap.id
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: case pos
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n✝ : M₂'
i j : ι₁
n : M₁ j
hj : j = i
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n✝ ∘ₗ component S ι₁ M₁ i) ∘ₗ lof S ι₁ M₁ j) n

pp: case neg
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n✝ : M₂'
i j : ι₁
n : M₁ j
hj : ¬j = i
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n✝ ∘ₗ component S ι₁ M₁ i) ∘ₗ lof S ι₁ M₁ j) n

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n✝ : M₂'
i j : ι₁
n : M₁ j
hj : j = i
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n✝ ∘ₗ component S ι₁ M₁ i) ∘ₗ lof S ι₁ M₁ j) n
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: case neg
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n✝ : M₂'
i j : ι₁
n : M₁ j
hj : ¬j = i
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n✝ ∘ₗ component S ι₁ M₁ i) ∘ₗ lof S ι₁ M₁ j) n

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n✝ : M₂'
i j : ι₁
n : M₁ j
hj : ¬j = i
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n✝ ∘ₗ component S ι₁ M₁ i) ∘ₗ lof S ι₁ M₁ j) n
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:
·

Goal state after:
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₀)
Module: Mathlib.Algebra.Module.Projective

Goal state before:
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 ∘ₗ AlgebraTensorModule.map sM LinearMap.id = LinearMap.id

Tactic:
·

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₀)
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: case single.single
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
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n)) (i, k) =
    (Finsupp.single i' m) i ⊗ₜ[R] (Finsupp.single k' n) k

Tactic:
simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]
      split_ifs <;> simp

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

Goal state before:
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
⊢ AlgebraTensorModule.map (linearCombination R id) LinearMap.id ∘ₗ AlgebraTensorModule.map sM LinearMap.id =
    LinearMap.id

Tactic:
·

Goal state after:
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
⊢ AlgebraTensorModule.map (linearCombination R id) LinearMap.id ∘ₗ AlgebraTensorModule.map sM LinearMap.id =
    LinearMap.id
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
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ M ⊗[R₀] N →ₗ[R] M ⊗[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
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] N

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
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ ?s ∘ₗ ?i = LinearMap.id

Tactic:
·

Goal state after:
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
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ M ⊗[R₀] N →ₗ[R] M ⊗[R₀] (N →₀ R₀)
Module: Mathlib.Algebra.Module.Projective

Goal state before:
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
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] N

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
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ ?s ∘ₗ AlgebraTensorModule.map LinearMap.id sN = LinearMap.id

Tactic:
·

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
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] N
Module: Mathlib.Algebra.Module.Projective

Goal state before:
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
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ AlgebraTensorModule.map LinearMap.id (linearCombination R₀ id) ∘ₗ AlgebraTensorModule.map LinearMap.id sN =
    LinearMap.id

Tactic:
·

Goal state after:
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
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ AlgebraTensorModule.map LinearMap.id (linearCombination R₀ id) ∘ₗ AlgebraTensorModule.map LinearMap.id sN =
    LinearMap.id