mathlib-initiative/mathlib-tactics huggingface dataset:
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
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
x y a✝ : N
⊢ (mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm (x + y))))) a✝ =
    (mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm x))) +
        mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm y))))
      a✝

Tactic:
;

Goal state after:
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
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
x y a✝ : N
⊢ (mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm (x + y))))) a✝ =
    (mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm x))) +
        mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm y))))
      a✝
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
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
r : S
v i : N
⊢ (mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm (r • v))))) i =
    ((RingHom.id S) r • mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm v)))) i

Tactic:
;

Goal state after:
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
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
r : S
v i : N
⊢ (mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm (r • v))))) i =
    ((RingHom.id S) r • mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm v)))) i
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : DecidableEq ι
v : ι → M
a✝ : ι
x✝ : S
⊢ (↑R (linearCombination S fun x ↦ 1 ⊗ₜ[R] v x) ∘ₗ lsingle a✝) x✝ =
    ((lTensor S (linearCombination R v) ∘ₗ ↑(finsuppScalarRight R R S ι).symm) ∘ₗ lsingle a✝) x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : DecidableEq ι
v : ι → M
a✝ : ι
x✝ : S
⊢ (↑R (linearCombination S fun x ↦ 1 ⊗ₜ[R] v x) ∘ₗ lsingle a✝) x✝ =
    ((lTensor S (linearCombination R v) ∘ₗ ↑(finsuppScalarRight R R S ι).symm) ∘ₗ lsingle a✝) x✝
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
x✝ : M
a✝ : N
⊢ ((AlgebraTensorModule.curry
            (AlgebraTensorModule.map (linearCombination R id) LinearMap.id ∘ₗ AlgebraTensorModule.map sM LinearMap.id))
          x✝ ∘ₗ
        lsingle a✝)
      1 =
    ((AlgebraTensorModule.curry LinearMap.id) x✝ ∘ₗ lsingle a✝) 1

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
x✝ : M
a✝ : N
⊢ ((AlgebraTensorModule.curry
            (AlgebraTensorModule.map (linearCombination R id) LinearMap.id ∘ₗ AlgebraTensorModule.map sM LinearMap.id))
          x✝ ∘ₗ
        lsingle a✝)
      1 =
    ((AlgebraTensorModule.curry LinearMap.id) x✝ ∘ₗ lsingle a✝) 1
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁷ : CommSemiring R
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₁'
inst✝³ : AddCommMonoid M₂'
inst✝² : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝¹ : Module R M₁'
inst✝ : Module R M₂'
f : M₁' →ₗ[R] M₂'
x✝¹ : M₁'
i✝¹ : ι₁
x✝ : M₁ i✝¹
i✝ : ι₁
⊢ (((AlgebraTensorModule.curry (↑(directSumRight R R M₂' M₁) ∘ₗ rTensor (⨁ (i : ι₁), M₁ i) f)) x✝¹ ∘ₗ lof R ι₁ M₁ i✝¹)
        x✝)
      i✝ =
    (((AlgebraTensorModule.curry ((lmap fun x ↦ rTensor (M₁ x) f) ∘ₗ ↑(directSumRight R R M₁' M₁))) x✝¹ ∘ₗ
          lof R ι₁ M₁ i✝¹)
        x✝)
      i✝

Tactic:
;

Goal state after:
R : Type u
inst✝⁷ : CommSemiring R
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₁'
inst✝³ : AddCommMonoid M₂'
inst✝² : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝¹ : Module R M₁'
inst✝ : Module R M₂'
f : M₁' →ₗ[R] M₂'
x✝¹ : M₁'
i✝¹ : ι₁
x✝ : M₁ i✝¹
i✝ : ι₁
⊢ (((AlgebraTensorModule.curry (↑(directSumRight R R M₂' M₁) ∘ₗ rTensor (⨁ (i : ι₁), M₁ i) f)) x✝¹ ∘ₗ lof R ι₁ M₁ i✝¹)
        x✝)
      i✝ =
    (((AlgebraTensorModule.curry ((lmap fun x ↦ rTensor (M₁ x) f) ∘ₗ ↑(directSumRight R R M₁' M₁))) x✝¹ ∘ₗ
          lof R ι₁ M₁ i✝¹)
        x✝)
      i✝
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₀))
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry
          (AlgebraTensorModule.map LinearMap.id (linearCombination R₀ id) ∘ₗ AlgebraTensorModule.map LinearMap.id sN))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id) x✝¹) x✝

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₀))
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry
          (AlgebraTensorModule.map LinearMap.id (linearCombination R₀ id) ∘ₗ AlgebraTensorModule.map LinearMap.id sN))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id) x✝¹) x✝
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: I : Type u_1
J : Type u_2
R : Type u_5
inst✝³ : DecidableEq I
inst✝² : DecidableEq J
inst✝¹ : Zero R
inst✝ : One R
i✝ j✝ : I × J
⊢ (comp I I J J R) 1 i✝ j✝ = 1 i✝ j✝

Tactic:
;

Goal state after:
I : Type u_1
J : Type u_2
R : Type u_5
inst✝³ : DecidableEq I
inst✝² : DecidableEq J
inst✝¹ : Zero R
inst✝ : One R
i✝ j✝ : I × J
⊢ (comp I I J J R) 1 i✝ j✝ = 1 i✝ j✝
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: I : Type u_1
J : Type u_2
R : Type u_5
inst✝³ : DecidableEq I
inst✝² : DecidableEq J
inst✝¹ : Zero R
inst✝ : One R
i✝ j✝ : I × J
⊢ if i✝ = j✝ then (if i✝.1 = j✝.1 then 1 else 0) i✝.2 j✝.2 = 1 else (if i✝.1 = j✝.1 then 1 else 0) i✝.2 j✝.2 = 0

Tactic:
;

Goal state after:
I : Type u_1
J : Type u_2
R : Type u_5
inst✝³ : DecidableEq I
inst✝² : DecidableEq J
inst✝¹ : Zero R
inst✝ : One R
i✝ j✝ : I × J
⊢ if i✝ = j✝ then (if i✝.1 = j✝.1 then 1 else 0) i✝.2 j✝.2 = 1 else (if i✝.1 = j✝.1 then 1 else 0) i✝.2 j✝.2 = 0
Module: Mathlib.Data.Matrix.Composition

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

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

Tactic:
· rw [single_apply_of_col_ne _ _ hj,
      single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.snd hj)]

Goal state after:
case inr.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
⊢ single k l r k l = single (i, k) (j, l) r (i, k) (j, l)
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✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
m : M₁'
n✝ : ⨁ (i : ι₂), M₂ i
j : ι₂
n : M₂ j
⊢ ((↑R (component S ι₂ (fun i ↦ M₁' ⊗[R] M₂ i) j) ∘ₗ
          ↑R ↑(directSumRight R S M₁' M₂) ∘ₗ (mk R M₁' (⨁ (i : ι₂), M₂ i)) m) ∘ₗ
        lof R ι₂ M₂ j)
      n =
    (((mk R M₁' (M₂ j)) m ∘ₗ component R ι₂ M₂ j) ∘ₗ lof R ι₂ 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✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
m : M₁'
n✝ : ⨁ (i : ι₂), M₂ i
j : ι₂
n : M₂ j
⊢ ((↑R (component S ι₂ (fun i ↦ M₁' ⊗[R] M₂ i) j) ∘ₗ
          ↑R ↑(directSumRight R S M₁' M₂) ∘ₗ (mk R M₁' (⨁ (i : ι₂), M₂ i)) m) ∘ₗ
        lof R ι₂ M₂ j)
      n =
    (((mk R M₁' (M₂ j)) m ∘ₗ component R ι₂ M₂ j) ∘ₗ lof R ι₂ M₂ j) n
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
R' : Type u_6
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype I
inst✝ : Fintype J
x✝¹ x✝ : Matrix I I (Matrix J J R)
i✝ j✝ : I × J
⊢ (compAddEquiv I I J J R).toFun (x✝¹ * x✝) i✝ j✝ =
    ((compAddEquiv I I J J R).toFun x✝¹ * (compAddEquiv I I J J R).toFun x✝) i✝ j✝

Tactic:
;

Goal state after:
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
R' : Type u_6
inst✝³ : AddCommMonoid R
inst✝² : Mul R
inst✝¹ : Fintype I
inst✝ : Fintype J
x✝¹ x✝ : Matrix I I (Matrix J J R)
i✝ j✝ : I × J
⊢ (compAddEquiv I I J J R).toFun (x✝¹ * x✝) i✝ j✝ =
    ((compAddEquiv I I J J R).toFun x✝¹ * (compAddEquiv I I J J R).toFun x✝) i✝ j✝
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: R : Type u
inst✝¹⁵ : CommSemiring R
S : Type u_2
inst✝¹⁴ : Semiring S
inst✝¹³ : Algebra R S
ι₂ : Type v₂
inst✝¹² : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝¹¹ : AddCommMonoid M₁'
inst✝¹⁰ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁹ : Module R M₁'
inst✝⁸ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁷ : Module S M₁'
inst✝⁶ : IsScalarTower R S M₁'
S₀ : Type u_1
inst✝⁵ : CommSemiring S₀
inst✝⁴ : Algebra R S₀
inst✝³ : Algebra S₀ S
inst✝² : Module S₀ M₁'
inst✝¹ : IsScalarTower R S₀ M₁'
inst✝ : IsScalarTower S₀ S M₁'
x✝¹ : M₁'
i✝¹ : ι₂
x✝ : M₂ i✝¹
i✝ : ι₂
⊢ (((AlgebraTensorModule.curry
              ↑(LinearEquiv.restrictScalars R (LinearEquiv.restrictScalars S₀ (directSumRight R S M₁' M₂))))
            x✝¹ ∘ₗ
          lof R ι₂ M₂ i✝¹)
        x✝)
      i✝ =
    (((AlgebraTensorModule.curry ↑(LinearEquiv.restrictScalars R (directSumRight R S₀ M₁' M₂))) x✝¹ ∘ₗ lof R ι₂ M₂ i✝¹)
        x✝)
      i✝

Tactic:
;

Goal state after:
R : Type u
inst✝¹⁵ : CommSemiring R
S : Type u_2
inst✝¹⁴ : Semiring S
inst✝¹³ : Algebra R S
ι₂ : Type v₂
inst✝¹² : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝¹¹ : AddCommMonoid M₁'
inst✝¹⁰ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁹ : Module R M₁'
inst✝⁸ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁷ : Module S M₁'
inst✝⁶ : IsScalarTower R S M₁'
S₀ : Type u_1
inst✝⁵ : CommSemiring S₀
inst✝⁴ : Algebra R S₀
inst✝³ : Algebra S₀ S
inst✝² : Module S₀ M₁'
inst✝¹ : IsScalarTower R S₀ M₁'
inst✝ : IsScalarTower S₀ S M₁'
x✝¹ : M₁'
i✝¹ : ι₂
x✝ : M₂ i✝¹
i✝ : ι₂
⊢ (((AlgebraTensorModule.curry
              ↑(LinearEquiv.restrictScalars R (LinearEquiv.restrictScalars S₀ (directSumRight R S M₁' M₂))))
            x✝¹ ∘ₗ
          lof R ι₂ M₂ i✝¹)
        x✝)
      i✝ =
    (((AlgebraTensorModule.curry ↑(LinearEquiv.restrictScalars R (directSumRight R S₀ M₁' M₂))) x✝¹ ∘ₗ lof R ι₂ M₂ i✝¹)
        x✝)
      i✝
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝² : InvolutiveStar R
inst✝¹ : SetLike S R
inst✝ : StarMemClass S R
s : S
r : R
hr : star r ∈ s
⊢ star (star r) ∈ s

Tactic:
;

Goal state after:
S : Type u_1
R : Type u_2
inst✝² : InvolutiveStar R
inst✝¹ : SetLike S R
inst✝ : StarMemClass S R
s : S
r : R
hr : star r ∈ s
⊢ star (star r) ∈ s
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → MulOneClass (R i)
inst✝ : (i : ι) → StarMul (R i)
i : ι
r : R i
x✝ : ι
⊢ star (mulSingle i r) x✝ = mulSingle i (star r) x✝

Tactic:
;

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → MulOneClass (R i)
inst✝ : (i : ι) → StarMul (R i)
i : ι
r : R i
x✝ : ι
⊢ star (mulSingle i r) x✝ = mulSingle i (star r) x✝
Module: Mathlib.Algebra.Star.Basic

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

Tactic:
;

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddMonoid (R i)
inst✝ : (i : ι) → StarAddMonoid (R i)
i : ι
r : R i
x✝ : ι
⊢ star (single i r) x✝ = single i (star r) x✝
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ star x ≠ 0 ↔ x ≠ 0

Tactic:
simp only [ne_eq, star_eq_zero]

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

Goal state before:
pp: R : Type u
S : Type v
f : R → S
inst✝³ : Star R
inst✝² : Mul R
inst✝¹ : Mul S
inst✝ : StarMul S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
mul : ∀ (x y : R), f (x * y) = f x * f y
x y : R
⊢ f (Star.star (x * y)) = f (Star.star y * Star.star x)

Tactic:
by rw [star, mul, star_mul, mul, star, star]

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

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

Tactic:
;

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

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

Tactic:
;

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ Commute x y ↔ IsSelfAdjoint (x * y)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [isSelfAdjoint_iff, star_mul, hx.star_eq, hy.star_eq, h.eq]
  · simpa only [star_mul, hx.star_eq, hy.star_eq] using! h.symm

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
hz : IsSelfAdjoint z
⊢ IsSelfAdjoint (z * x * star z)

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
hz : IsSelfAdjoint z
⊢ IsSelfAdjoint (z * x * star z)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
n✝ : ℕ
x✝ : ↥(selfAdjoint R)
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
n✝ : ℕ
x✝ : ↥(selfAdjoint R)
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
n✝ : ℤ
x✝ : ↥(selfAdjoint R)
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
n✝ : ℤ
x✝ : ↥(selfAdjoint R)
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ≥0
x : ↥(selfAdjoint R)
⊢ ↑a * ↑x ∈ selfAdjoint R

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ≥0
x : ↥(selfAdjoint R)
⊢ ↑a * ↑x ∈ selfAdjoint R
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ
x : ↥(selfAdjoint R)
⊢ ↑a * ↑x ∈ selfAdjoint R

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ
x : ↥(selfAdjoint R)
⊢ ↑a * ↑x ∈ selfAdjoint R
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
n✝ : ℤ
x✝ : ↥(selfAdjoint R)
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
n✝ : ℤ
x✝ : ↥(selfAdjoint R)
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : Mul α
inst✝ : StarMul α
w : m → α
v : n → α
⊢ (vecMulVec w v).map star = (vecMulVec w v)ᴴᵀ

Tactic:
;

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : Mul α
inst✝ : StarMul α
w : m → α
v : n → α
⊢ (vecMulVec w v).map star = (vecMulVec w v)ᴴᵀ
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ x = ↑(LinearMap.id ⟨x, hx⟩)

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ x = ↑(LinearMap.id ⟨x, hx⟩)
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
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D).map f i j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) i j

Tactic:
;

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D).map f i j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) i j
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ (b.prod b') i = Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i

Tactic:
ext <;> cases i

Goal state after:
case fst.inl
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι
⊢ ((b.prod b') (Sum.inl val✝)).1 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inl val✝)).1

case fst.inr
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι'
⊢ ((b.prod b') (Sum.inr val✝)).1 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inr val✝)).1

case snd.inl
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι
⊢ ((b.prod b') (Sum.inl val✝)).2 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inl val✝)).2

case snd.inr
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
val✝ : ι'
⊢ ((b.prod b') (Sum.inr val✝)).2 =
    (Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') (Sum.inr val✝)).2
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
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (x • fromBlocks A B C D) i j = fromBlocks (x • A) (x • B) (x • C) (x • D) i j

Tactic:
;

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (x • fromBlocks A B C D) i j = fromBlocks (x • A) (x • B) (x • C) (x • D) i j