awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : Module R₁ Mₗ
inst_6 : Module R₂ N
inst_7 : Module R₂ Pₗ
inst_8 : Module R₁ Pₗ
inst_9 : SMulCommClass R₂ R₁ Pₗ
f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
x : Mₗ
x_1 : N
⊢ Eq.{u_9 + 1} (α := Pₗ) ((((f.compl₁₂ id id : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
    ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
have h : Eq.{u_9 + 1} (α := Pₗ)
  ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((id : (a : Mₗ) → Mₗ) x) : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) ((id : (a : N) → N) x_1 : N) :
    Pₗ)
  ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
Tactic: simp_rw [compl₁₂_apply, id_coe, _root_.id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : Module R₁ Mₗ
inst_6 : Module R₂ N
inst_7 : Module R₂ Pₗ
inst_8 : Module R₁ Pₗ
inst_9 : SMulCommClass R₂ R₁ Pₗ
f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
x : Mₗ
x_1 : N
h :
  Eq.{u_9 + 1} (α := Pₗ)
    ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((id : (a : Mₗ) → Mₗ) x) : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ)
        ((id : (a : N) → N) x_1 : N) :
      Pₗ)
    ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
⊢ Eq.{u_9 + 1} (α := Pₗ) ((((f.compl₁₂ id id : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
    ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
have h₁ : Eq.{u_9 + 1} (α := Pₗ)
  ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) (_root_.id x) : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) (_root_.id x_1) : Pₗ)
  ((((f : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) x_1 : Pₗ)
Tactic: simp_rw [compl₁₂_apply, id_coe, _root_.id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂
have mp : f₁.compl₁₂ g g' = f₂.compl₁₂ g g' → f₁ = f₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
mp : f₁.compl₁₂ g g' = f₂.compl₁₂ g g' → f₁ = f₂
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂
have mpr : f₁ = f₂ → f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
⊢ f₁ = f₂
have mp : ∀ (x : Mₗ) (y : N),
  Eq.{u_9 + 1} (α := Pₗ) ((((f₁ : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
    ((((f₂ : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
x : Mₗ
y : N
⊢ Eq.{u_9 + 1} (α := Pₗ) ((((f₁ : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
    ((((f₂ : (a : Mₗ) → N →ₗ[R₂] Pₗ) x : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
have mp : ∀ (x' : Qₗ),
  Eq.{u_9 + 1} (α := Pₗ)
    ((((f₁ : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x') : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
    ((((f₂ : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x') : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
Tactic: obtain ⟨x', rfl⟩ := hₗ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
y : N
x' : Qₗ
⊢ Eq.{u_9 + 1} (α := Pₗ)
    ((((f₁ : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x') : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
    ((((f₂ : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x') : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ) y : Pₗ)
have mp : ∀ (y' : Qₗ'),
  Eq.{u_9 + 1} (α := Pₗ)
    ((((f₁ : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x') : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ)
        ((g' : (a : Qₗ') → N) y' : N) :
      Pₗ)
    ((((f₂ : (a : Mₗ) → N →ₗ[R₂] Pₗ) ((g : (a : Qₗ) → Mₗ) x') : N →ₗ[R₂] Pₗ) : (a : N) → Pₗ)
        ((g' : (a : Qₗ') → N) y' : N) :
      Pₗ)
Tactic: obtain ⟨y', rfl⟩ := hᵣ y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring R₁
inst_1 : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_2 : AddCommMonoid Mₗ
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid Pₗ
inst_5 : AddCommMonoid Qₗ
inst_6 : AddCommMonoid Qₗ'
inst_7 : Module R₁ Mₗ
inst_8 : Module R₂ N
inst_9 : Module R₂ Pₗ
inst_10 : Module R₁ Pₗ
inst_11 : Module R₁ Qₗ
inst_12 : Module R₂ Qₗ'
inst_13 : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective.{u_10 + 1, u_6 + 1} (α := Qₗ) (β := Mₗ) (⇑g : (a : Qₗ) → Mₗ)
hᵣ : Surjective.{u_11 + 1, u_7 + 1} (α := Qₗ') (β := N) (⇑g' : (a : Qₗ') → N)
h : f₁ = f₂
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
have mpr : f₁.compl₁₂ g g' = f₁.compl₁₂ g g'
Tactic: subst h
Cleared hypotheses: f₂, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (hypothesis)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : Module S M
inst_8 : Module S P
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S R P
inst_11 : AddCommMonoid M'
inst_12 : Module S M'
inst_13 : AddCommMonoid P'
inst_14 : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective.{u_6 + 1, u_4 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
f : M →ₗ[R] P
hf : ∀ (m : M'), Membership.mem (α := P) k.range ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
m : M'
⊢ Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
    ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
have this : Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
  ((k ∘ₗ
          codLift
            ((↑S :
                  {S_1 : Type u_1} →
                    {M : Type u_3} →
                      {M₂ : Type u_4} →
                        [inst : Semiring S] →
                          [inst_15 : Semiring S_1] →
                            [inst_16 : AddCommMonoid M] →
                              [inst_17 : AddCommMonoid M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [inst_20 : Module S_1 M] →
                                      [inst_21 : Module S_1 M₂] →
                                        [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                f ∘ₗ
              i)
            k hk hf :
        (a : M') → P)
      m :
    P)
Tactic: have : k (restrictScalarsRange i k hk f hf m) =
      (k ∘ₗ ((f.restrictScalars S).comp i).codLift k hk hf) m :=
    rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : Module S M
inst_8 : Module S P
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S R P
inst_11 : AddCommMonoid M'
inst_12 : Module S M'
inst_13 : AddCommMonoid P'
inst_14 : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective.{u_6 + 1, u_4 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
f : M →ₗ[R] P
hf : ∀ (m : M'), Membership.mem (α := P) k.range ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
m : M'
this :
  Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
    ((k ∘ₗ
            codLift
              ((↑S :
                    {S_1 : Type u_1} →
                      {M : Type u_3} →
                        {M₂ : Type u_4} →
                          [inst : Semiring S] →
                            [inst_15 : Semiring S_1] →
                              [inst_16 : AddCommMonoid M] →
                                [inst_17 : AddCommMonoid M₂] →
                                  [inst_18 : Module S M] →
                                    [inst_19 : Module S M₂] →
                                      [inst_20 : Module S_1 M] →
                                        [inst_21 : Module S_1 M₂] →
                                          [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                  f ∘ₗ
                i)
              k hk hf :
          (a : M') → P)
        m :
      P)
⊢ Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
    ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
have rw : Eq.{u_4 + 1} (α := P)
  ((k ∘ₗ
          codLift
            ((↑S :
                  {S_1 : Type u_1} →
                    {M : Type u_3} →
                      {M₂ : Type u_4} →
                        [inst : Semiring S] →
                          [inst_15 : Semiring S_1] →
                            [inst_16 : AddCommMonoid M] →
                              [inst_17 : AddCommMonoid M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [inst_20 : Module S_1 M] →
                                      [inst_21 : Module S_1 M₂] →
                                        [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                f ∘ₗ
              i)
            k hk hf :
        (a : M') → P)
      m :
    P)
  ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
Tactic: rw [this, comp_codLift, comp_apply, restrictScalars_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : Module S M
inst_8 : Module S P
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S R P
inst_11 : AddCommMonoid M'
inst_12 : Module S M'
inst_13 : AddCommMonoid P'
inst_14 : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective.{u_6 + 1, u_4 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
f : M →ₗ[R] P
hf : ∀ (m : M'), Membership.mem (α := P) k.range ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
m : M'
p : P'
⊢ p = (i.restrictScalarsRange k hk f hf : (a : M') → P') m ↔
    Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) p : P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
have rw : p = (i.restrictScalarsRange k hk f hf : (a : M') → P') m ↔
  Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) p : P)
    ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
Tactic: rw [← restrictScalarsRange_apply i k hk f hf m, hk.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : Module S M
inst_8 : Module S P
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S R P
inst_11 : AddCommMonoid M'
inst_12 : Module S M'
inst_13 : AddCommMonoid P'
inst_14 : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective.{u_6 + 1, u_4 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
f : M →ₗ[R] P
hf : ∀ (m : M'), Membership.mem (α := P) k.range ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
m : M'
p : P'
rw :
  p = (i.restrictScalarsRange k hk f hf : (a : M') → P') m ↔
    Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) p : P)
      ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
⊢ p = (i.restrictScalarsRange k hk f hf : (a : M') → P') m ↔
    Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) p : P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
have rw₁ : p = (i.restrictScalarsRange k hk f hf : (a : M') → P') m ↔ p = (i.restrictScalarsRange k hk f hf : (a : M') → P') m
Tactic: rw [← restrictScalarsRange_apply i k hk f hf m, hk.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : Module S M
inst_8 : Module S P
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S R P
inst_11 : AddCommMonoid M'
inst_12 : Module S M'
inst_13 : AddCommMonoid P'
inst_14 : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective.{u_6 + 1, u_4 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
f : M →ₗ[R] P
hf : ∀ (m : M'), Membership.mem (α := P) k.range ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
m : M'
⊢ Eq.{u_6 + 1} (α := P') ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') (0 : P') ↔
    Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)
have rw : Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
    ((k : (a : P') → P) 0 : P) ↔
  Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)
Tactic: rw [← hk.eq_iff, restrictScalarsRange_apply, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : Module S M
inst_8 : Module S P
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S R P
inst_11 : AddCommMonoid M'
inst_12 : Module S M'
inst_13 : AddCommMonoid P'
inst_14 : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective.{u_6 + 1, u_4 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
f : M →ₗ[R] P
hf : ∀ (m : M'), Membership.mem (α := P) k.range ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
m : M'
rw :
  Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
      ((k : (a : P') → P) 0 : P) ↔
    Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)
⊢ Eq.{u_6 + 1} (α := P') ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') (0 : P') ↔
    Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)
have rw₁ : Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) ((k : (a : P') → P) 0 : P) ↔
  Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)
Tactic: rw [← hk.eq_iff, restrictScalarsRange_apply, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : Module S M
inst_8 : Module S P
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S R P
inst_11 : AddCommMonoid M'
inst_12 : Module S M'
inst_13 : AddCommMonoid P'
inst_14 : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective.{u_6 + 1, u_4 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
f : M →ₗ[R] P
hf : ∀ (m : M'), Membership.mem (α := P) k.range ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
m : M'
rw :
  Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
      ((k : (a : P') → P) 0 : P) ↔
    Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)
rw₁ :
  Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) ((k : (a : P') → P) 0 : P) ↔
    Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)
⊢ Eq.{u_6 + 1} (α := P') ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') (0 : P') ↔
    Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)
have rw₂ : Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P) ↔
  Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P) (0 : P)
Tactic: rw [← hk.eq_iff, restrictScalarsRange_apply, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S M
inst_10 : Module S N
inst_11 : Module S P
inst_12 : IsScalarTower S R M
inst_13 : IsScalarTower S R N
inst_14 : IsScalarTower S R P
inst_15 : AddCommMonoid M'
inst_16 : Module S M'
inst_17 : AddCommMonoid N'
inst_18 : Module S N'
inst_19 : AddCommMonoid P'
inst_20 : Module S P'
inst_21 : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective.{u_8 + 1, u_5 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
B : M →ₗ[R] N →ₗ[R] P
hB :
  ∀ (m : M') (n : N'),
    Membership.mem (α := P) k.range
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
m : M'
n : N'
p : P'
⊢ p = (((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n ↔
    Eq.{u_5 + 1} (α := P) ((k : (a : P') → P) p : P)
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
have rw : p = (((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n ↔
  Eq.{u_5 + 1} (α := P) ((k : (a : P') → P) p : P)
    ((k : (a : P') → P)
        ((((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n : P') :
      P)
Tactic: rw [← restrictScalarsRange₂_apply i j k hk B hB m n, hk.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S M
inst_10 : Module S N
inst_11 : Module S P
inst_12 : IsScalarTower S R M
inst_13 : IsScalarTower S R N
inst_14 : IsScalarTower S R P
inst_15 : AddCommMonoid M'
inst_16 : Module S M'
inst_17 : AddCommMonoid N'
inst_18 : Module S N'
inst_19 : AddCommMonoid P'
inst_20 : Module S P'
inst_21 : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective.{u_8 + 1, u_5 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
B : M →ₗ[R] N →ₗ[R] P
hB :
  ∀ (m : M') (n : N'),
    Membership.mem (α := P) k.range
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
m : M'
n : N'
p : P'
rw :
  p = (((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n ↔
    Eq.{u_5 + 1} (α := P) ((k : (a : P') → P) p : P)
      ((k : (a : P') → P)
          ((((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n : P') :
        P)
⊢ p = (((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n ↔
    Eq.{u_5 + 1} (α := P) ((k : (a : P') → P) p : P)
      ((((B : (a : M) → N →ₗ[R] P) ((i : (a : M') → M) m) : N →ₗ[R] P) : (a : N) → P) ((j : (a : N') → N) n : N) : P)
have rw₁ : p = (((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n ↔
  p = (((i.restrictScalarsRange₂ j k hk B hB : (a : M') → N' →ₗ[S] P') m : N' →ₗ[S] P') : (a : N') → P') n
Tactic: rw [← restrictScalarsRange₂_apply i j k hk B hB m n, hk.eq_iff]