awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
x : M
rw :
  Eq.{u_7 + 1} (α := M') (sum (((↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) x) fun (a : ι) (m : R) ↦ m • id (f a))
    (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b)
h_zero : ∀ (b : M'), HSMul.hSMul.{u_11, u_7, u_7} (α := R) 0 (id b) = 0
⊢ Eq (α := M') (sum (mapDomain f (((↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) x)) fun (i : M') (a : R) ↦ a • id i)
    (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b)
have h_add : ∀ (b : M') (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b
Tactic: rw [Finsupp.sum_mapDomain_index]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
⊢ Eq (α := Submodule R M')
    (LinearMap.range.{u_11, u_11, u_12, u_7} (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((b.constr S : (a : ι → M') → M →ₗ[R] M') f))
    (span R (range f))
have rw : Eq (α := Submodule R M') (LinearMap.range (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)))
  (span R (range f))
Tactic: rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
    Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←
    Finsupp.span_image_eq_map_linearCombination, Set.image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
rw :
  Eq (α := Submodule R M') (LinearMap.range (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)))
    (span R (range f))
⊢ Eq (α := Submodule R M')
    (LinearMap.range.{u_11, u_11, u_12, u_7} (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((b.constr S : (a : ι → M') → M →ₗ[R] M') f))
    (span R (range f))
have rw₁ : Eq (α := Submodule R M') (map (linearCombination R id) (lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)).range)
  (span R (range f))
Tactic: rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
    Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←
    Finsupp.span_image_eq_map_linearCombination, Set.image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
rw :
  Eq (α := Submodule R M') (LinearMap.range (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)))
    (span R (range f))
rw₁ :
  Eq (α := Submodule R M') (map (linearCombination R id) (lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)).range)
    (span R (range f))
⊢ Eq (α := Submodule R M')
    (LinearMap.range.{u_11, u_11, u_12, u_7} (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((b.constr S : (a : ι → M') → M →ₗ[R] M') f))
    (span R (range f))
have rw₂ : Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (↑b.repr : M →ₗ[R] ι →₀ R).range))
  (span R (range f))
Tactic: rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
    Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←
    Finsupp.span_image_eq_map_linearCombination, Set.image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
rw :
  Eq (α := Submodule R M') (LinearMap.range (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)))
    (span R (range f))
rw₁ :
  Eq (α := Submodule R M') (map (linearCombination R id) (lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)).range)
    (span R (range f))
rw₂ :
  Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (↑b.repr : M →ₗ[R] ι →₀ R).range))
    (span R (range f))
⊢ Eq (α := Submodule R M')
    (LinearMap.range.{u_11, u_11, u_12, u_7} (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((b.constr S : (a : ι → M') → M →ₗ[R] M') f))
    (span R (range f))
have rw₃ : Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) ⊤)) (span R (range f))
Tactic: rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
    Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←
    Finsupp.span_image_eq_map_linearCombination, Set.image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
rw :
  Eq (α := Submodule R M') (LinearMap.range (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)))
    (span R (range f))
rw₁ :
  Eq (α := Submodule R M') (map (linearCombination R id) (lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)).range)
    (span R (range f))
rw₂ :
  Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (↑b.repr : M →ₗ[R] ι →₀ R).range))
    (span R (range f))
rw₃ : Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) ⊤)) (span R (range f))
⊢ Eq (α := Submodule R M')
    (LinearMap.range.{u_11, u_11, u_12, u_7} (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((b.constr S : (a : ι → M') → M →ₗ[R] M') f))
    (span R (range f))
have rw₄ : Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (supported R R univ))) (span R (range f))
Tactic: rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
    Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←
    Finsupp.span_image_eq_map_linearCombination, Set.image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
rw :
  Eq (α := Submodule R M') (LinearMap.range (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)))
    (span R (range f))
rw₁ :
  Eq (α := Submodule R M') (map (linearCombination R id) (lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)).range)
    (span R (range f))
rw₂ :
  Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (↑b.repr : M →ₗ[R] ι →₀ R).range))
    (span R (range f))
rw₃ : Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) ⊤)) (span R (range f))
rw₄ :
  Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (supported R R univ)))
    (span R (range f))
⊢ Eq (α := Submodule R M')
    (LinearMap.range.{u_11, u_11, u_12, u_7} (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((b.constr S : (a : ι → M') → M →ₗ[R] M') f))
    (span R (range f))
have rw₅ : Eq (α := Submodule R M') (map (linearCombination R id) (supported R R (f '' univ))) (span R (range f))
Tactic: rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
    Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←
    Finsupp.span_image_eq_map_linearCombination, Set.image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
rw :
  Eq (α := Submodule R M') (LinearMap.range (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)))
    (span R (range f))
rw₁ :
  Eq (α := Submodule R M') (map (linearCombination R id) (lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)).range)
    (span R (range f))
rw₂ :
  Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (↑b.repr : M →ₗ[R] ι →₀ R).range))
    (span R (range f))
rw₃ : Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) ⊤)) (span R (range f))
rw₄ :
  Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (supported R R univ)))
    (span R (range f))
rw₅ : Eq (α := Submodule R M') (map (linearCombination R id) (supported R R (f '' univ))) (span R (range f))
⊢ Eq (α := Submodule R M')
    (LinearMap.range.{u_11, u_11, u_12, u_7} (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((b.constr S : (a : ι → M') → M →ₗ[R] M') f))
    (span R (range f))
have rw₆ : Eq (α := Submodule R M') (map (linearCombination R id) (supported R R (f '' univ))) (span R (f '' univ))
Tactic: rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
    Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←
    Finsupp.span_image_eq_map_linearCombination, Set.image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
rw :
  Eq (α := Submodule R M') (LinearMap.range (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)))
    (span R (range f))
rw₁ :
  Eq (α := Submodule R M') (map (linearCombination R id) (lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)).range)
    (span R (range f))
rw₂ :
  Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (↑b.repr : M →ₗ[R] ι →₀ R).range))
    (span R (range f))
rw₃ : Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) ⊤)) (span R (range f))
rw₄ :
  Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (supported R R univ)))
    (span R (range f))
rw₅ : Eq (α := Submodule R M') (map (linearCombination R id) (supported R R (f '' univ))) (span R (range f))
rw₆ : Eq (α := Submodule R M') (map (linearCombination R id) (supported R R (f '' univ))) (span R (f '' univ))
⊢ Eq (α := Submodule R M')
    (LinearMap.range.{u_11, u_11, u_12, u_7} (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((b.constr S : (a : ι → M') → M →ₗ[R] M') f))
    (span R (range f))
have rw₇ : Eq (α := Submodule R M') (span R (id '' f '' univ)) (span R (f '' univ))
Tactic: rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
    Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←
    Finsupp.span_image_eq_map_linearCombination, Set.image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
rw :
  Eq (α := Submodule R M') (LinearMap.range (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)))
    (span R (range f))
rw₁ :
  Eq (α := Submodule R M') (map (linearCombination R id) (lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)).range)
    (span R (range f))
rw₂ :
  Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (↑b.repr : M →ₗ[R] ι →₀ R).range))
    (span R (range f))
rw₃ : Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) ⊤)) (span R (range f))
rw₄ :
  Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (supported R R univ)))
    (span R (range f))
rw₅ : Eq (α := Submodule R M') (map (linearCombination R id) (supported R R (f '' univ))) (span R (range f))
rw₆ : Eq (α := Submodule R M') (map (linearCombination R id) (supported R R (f '' univ))) (span R (f '' univ))
rw₇ : Eq (α := Submodule R M') (span R (id '' f '' univ)) (span R (f '' univ))
⊢ Eq (α := Submodule R M')
    (LinearMap.range.{u_11, u_11, u_12, u_7} (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((b.constr S : (a : ι → M') → M →ₗ[R] M') f))
    (span R (range f))
have rw₈ : Eq (α := Submodule R M') (span R (f '' univ)) (span R (f '' univ))
Tactic: rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
    Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←
    Finsupp.span_image_eq_map_linearCombination, Set.image_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι' : Type u_2
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
⊢ b.map (b.equiv b' e) = b'.reindex e.symm
have a : ∀ (i : ι),
  Eq.{u_7 + 1} (α := M') ((b.map (b.equiv b' e) : (a : ι) → M') i : M') ((b'.reindex e.symm : (a : ι) → M') i : M')
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M'_1 : Type u_7
M''_1 : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'_1
inst_4 : Module R_1 M'_1
ι : Type u_10
R_2 : Type u_11
M_2 : Type u_12
inst_5 : Semiring R_2
inst_6 : AddCommMonoid M_2
inst_7 : Module R_2 M_2
b_1 : Basis ι R_2 M_2
inst_8 : Module R_2 M'_1
i_1 : ι
M'' : Type u_13
b'_1 : Basis ι' R_2 M'_1
e : ι ≃ ι'
inst_9 : AddCommMonoid M''
inst_10 : Module R_2 M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst_11 : CommSemiring R
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : AddCommMonoid M'
inst_15 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst_16 : SMulCommClass R R M'
f : M → M'
g : M' → M
hf :
  ∀ (i : ι),
    Membership.mem (γ := Set M') (range.{u_16, u_2 + 1} (ι := ι') (⇑b' : (a : ι') → M')) (f ((b : (a : ι) → M) i))
hg :
  ∀ (i : ι'),
    Membership.mem (γ := Set M) (range.{u_15, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) (g ((b' : (a : ι') → M') i))
hgf : ∀ (i : ι), g (f ((b : (a : ι) → M) i)) = (b : (a : ι) → M) i
hfg : ∀ (i : ι'), f (g ((b' : (a : ι') → M') i)) = (b' : (a : ι') → M') i
i : ι
i' : ι'
hi' : (b' : (a : ι') → M') i' = f ((b : (a : ι) → M) i)
⊢ Eq.{u_15 + 1} (α := M)
    (((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) ∘ₗ
            (b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) :
          (a : M) → M)
        ((b : (a : ι) → M) i : M) :
      M)
    ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
have rw : Eq.{u_15 + 1} (α := M)
  ((((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) : M' →ₗ[R] M) : (a : M') → M)
      ((((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) : M →ₗ[R] M') : (a : M) → M')
          ((b : (a : ι) → M) i : M) :
        M') :
    M)
  ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
Tactic: rw [LinearMap.comp_apply, b.constr_basis, Function.comp_apply, ← hi', b'.constr_basis,
              Function.comp_apply, hi', hgf, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M'_1 : Type u_7
M''_1 : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'_1
inst_4 : Module R_1 M'_1
ι : Type u_10
R_2 : Type u_11
M_2 : Type u_12
inst_5 : Semiring R_2
inst_6 : AddCommMonoid M_2
inst_7 : Module R_2 M_2
b_1 : Basis ι R_2 M_2
inst_8 : Module R_2 M'_1
i_1 : ι
M'' : Type u_13
b'_1 : Basis ι' R_2 M'_1
e : ι ≃ ι'
inst_9 : AddCommMonoid M''
inst_10 : Module R_2 M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst_11 : CommSemiring R
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : AddCommMonoid M'
inst_15 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst_16 : SMulCommClass R R M'
f : M → M'
g : M' → M
hf :
  ∀ (i : ι),
    Membership.mem (γ := Set M') (range.{u_16, u_2 + 1} (ι := ι') (⇑b' : (a : ι') → M')) (f ((b : (a : ι) → M) i))
hg :
  ∀ (i : ι'),
    Membership.mem (γ := Set M) (range.{u_15, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) (g ((b' : (a : ι') → M') i))
hgf : ∀ (i : ι), g (f ((b : (a : ι) → M) i)) = (b : (a : ι) → M) i
hfg : ∀ (i : ι'), f (g ((b' : (a : ι') → M') i)) = (b' : (a : ι') → M') i
i : ι
i' : ι'
hi' : (b' : (a : ι') → M') i' = f ((b : (a : ι) → M) i)
rw :
  Eq.{u_15 + 1} (α := M)
    ((((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) : M' →ₗ[R] M) : (a : M') → M)
        ((((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) : M →ₗ[R] M') : (a : M) → M')
            ((b : (a : ι) → M) i : M) :
          M') :
      M)
    ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
⊢ Eq.{u_15 + 1} (α := M)
    (((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) ∘ₗ
            (b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) :
          (a : M) → M)
        ((b : (a : ι) → M) i : M) :
      M)
    ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
have rw₁ : Eq.{u_15 + 1} (α := M)
  ((((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) : M' →ₗ[R] M) : (a : M') → M)
      ((f ∘ (⇑b : (a : ι) → M)) i) :
    M)
  ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
Tactic: rw [LinearMap.comp_apply, b.constr_basis, Function.comp_apply, ← hi', b'.constr_basis,
              Function.comp_apply, hi', hgf, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M'_1 : Type u_7
M''_1 : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'_1
inst_4 : Module R_1 M'_1
ι : Type u_10
R_2 : Type u_11
M_2 : Type u_12
inst_5 : Semiring R_2
inst_6 : AddCommMonoid M_2
inst_7 : Module R_2 M_2
b_1 : Basis ι R_2 M_2
inst_8 : Module R_2 M'_1
i_1 : ι
M'' : Type u_13
b'_1 : Basis ι' R_2 M'_1
e : ι ≃ ι'
inst_9 : AddCommMonoid M''
inst_10 : Module R_2 M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst_11 : CommSemiring R
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : AddCommMonoid M'
inst_15 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst_16 : SMulCommClass R R M'
f : M → M'
g : M' → M
hf :
  ∀ (i : ι),
    Membership.mem (γ := Set M') (range.{u_16, u_2 + 1} (ι := ι') (⇑b' : (a : ι') → M')) (f ((b : (a : ι) → M) i))
hg :
  ∀ (i : ι'),
    Membership.mem (γ := Set M) (range.{u_15, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) (g ((b' : (a : ι') → M') i))
hgf : ∀ (i : ι), g (f ((b : (a : ι) → M) i)) = (b : (a : ι) → M) i
hfg : ∀ (i : ι'), f (g ((b' : (a : ι') → M') i)) = (b' : (a : ι') → M') i
i : ι
i' : ι'
hi' : (b' : (a : ι') → M') i' = f ((b : (a : ι) → M) i)
rw :
  Eq.{u_15 + 1} (α := M)
    ((((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) : M' →ₗ[R] M) : (a : M') → M)
        ((((b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) : M →ₗ[R] M') : (a : M) → M')
            ((b : (a : ι) → M) i : M) :
          M') :
      M)
    ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
rw₁ :
  Eq.{u_15 + 1} (α := M)
    ((((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) : M' →ₗ[R] M) : (a : M') → M)
        ((f ∘ (⇑b : (a : ι) → M)) i) :
      M)
    ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
⊢ Eq.{u_15 + 1} (α := M)
    (((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) ∘ₗ
            (b.constr R : (a : ι → M') → M →ₗ[R] M') (f ∘ (⇑b : (a : ι) → M)) :
          (a : M) → M)
        ((b : (a : ι) → M) i : M) :
      M)
    ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
have rw₂ : Eq.{u_15 + 1} (α := M)
  ((((b'.constr R : (a : ι' → M) → M' →ₗ[R] M) (g ∘ (⇑b' : (a : ι') → M')) : M' →ₗ[R] M) : (a : M') → M)
      (f ((b : (a : ι) → M) i)) :
    M)
  ((LinearMap.id : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
Tactic: rw [LinearMap.comp_apply, b.constr_basis, Function.comp_apply, ← hi', b'.constr_basis,
              Function.comp_apply, hi', hgf, LinearMap.id_apply]