awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
⊢ Injective (α := M') (β := N' →ₗ[S] S)
    (⇑(i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp) : (a : M') → N' →ₗ[S] S)
have rw : (i.restrictScalarsRange₂ j (Algebra.linearMap S R) sorry p hp).ker = ⊥
Tactic: rw [← LinearMap.ker_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp).ker = ⊥
have refine : ∀ (x : M') (hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)), x = 0
Tactic: refine (Submodule.eq_bot_iff _).mpr fun x (hx : f x = 0) ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n : N
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) n : R) (0 : R)
have hn : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) n
Tactic: have hn : n ∈ span R (LinearMap.range j : Set N) := hN ▸ Submodule.mem_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n z : N
hz : z ∈ (↑j.range : Set N)
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) z : R) (0 : R)
have mem : ∀ (n' : N'),
  Eq.{u_1 + 1} (α := R)
    ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n' : N) : R)
    (0 : R)
Tactic: obtain ⟨n', rfl⟩ := hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n x_1 y : N
hx_1 : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) x_1
hy : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) y
h :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R) (0 : R)
h_1 :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) y : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) (x_1 + y) : R)
    (0 : R)
have add : HAdd.hAdd (α := R) (β := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R)
    ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) y : R) =
  0
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n : N
a : R
x_1 : N
hx_1 : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) x_1
h :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) (a • x_1) : R)
    (0 : R)
have smul : HSMul.hSMul (β := R) a ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R) = 0
Tactic: rw [map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n : N
hn : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) n
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) n : R) (0 : R)
have mem : ∀ (z : N) (hz : z ∈ (↑j.range : Set N)),
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) z : R) (0 : R)
Tactic: induction hn using Submodule.span_induction with
    | mem z hz =>
      obtain ⟨n', rfl⟩ := hz
      simpa [f] using LinearMap.congr_fun hx n'
    | zero => simp
    | add => rw [map_add]; aesop
    | smul => rw [map_smul]; aesop
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n : N
hn : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) n
mem :
  ∀ (z : N) (hz : z ∈ (↑j.range : Set N)),
    Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) z : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) n : R) (0 : R)
have zero : Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) 0 : R) (0 : R)
Tactic: induction hn using Submodule.span_induction with
    | mem z hz =>
      obtain ⟨n', rfl⟩ := hz
      simpa [f] using LinearMap.congr_fun hx n'
    | zero => simp
    | add => rw [map_add]; aesop
    | smul => rw [map_smul]; aesop
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n : N
hn : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) n
mem :
  ∀ (z : N) (hz : z ∈ (↑j.range : Set N)),
    Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) z : R) (0 : R)
zero :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) 0 : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) n : R) (0 : R)
have add : ∀ (x_1 y : N),
  Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) x_1 →
    Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) y →
      Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R)
          (0 : R) →
        Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) y : R)
            (0 : R) →
          Eq.{u_1 + 1} (α := R)
            ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) (x_1 + y) : R) (0 : R)
Tactic: induction hn using Submodule.span_induction with
    | mem z hz =>
      obtain ⟨n', rfl⟩ := hz
      simpa [f] using LinearMap.congr_fun hx n'
    | zero => simp
    | add => rw [map_add]; aesop
    | smul => rw [map_smul]; aesop
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx : Eq (α := N' →ₗ[S] S) ((f : (a : M') → N' →ₗ[S] S) x : N' →ₗ[S] S) (0 : N' →ₗ[S] S)
n : N
hn : Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) n
mem :
  ∀ (z : N) (hz : z ∈ (↑j.range : Set N)),
    Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) z : R) (0 : R)
zero :
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) 0 : R) (0 : R)
add :
  ∀ (x_1 y : N),
    Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) x_1 →
      Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) y →
        Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R)
            (0 : R) →
          Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) y : R)
              (0 : R) →
            Eq.{u_1 + 1} (α := R)
              ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) (x_1 + y) : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) n : R) (0 : R)
have smul : ∀ (a : R) (x_1 : N),
  Membership.mem (γ := Submodule R N) (span R (↑j.range : Set N)) x_1 →
    Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) x_1 : R)
        (0 : R) →
      Eq.{u_1 + 1} (α := R)
        ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) (a • x_1) : R) (0 : R)
Tactic: induction hn using Submodule.span_induction with
    | mem z hz =>
      obtain ⟨n', rfl⟩ := hz
      simpa [f] using LinearMap.congr_fun hx n'
    | zero => simp
    | add => rw [map_add]; aesop
    | smul => rw [map_smul]; aesop
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx :
  ∀ (n : N),
    Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) n : R) (0 : R)
⊢ x = 0
have rw : Eq (α := N →ₗ[R] R) ((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) (0 : N →ₗ[R] R)
Tactic: rw [← i.map_eq_zero_iff hi, ← p.map_eq_zero_iff p.toPerfPair.injective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
hi : Injective.{u_5 + 1, u_2 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hN : Eq (α := Submodule R N) (span R (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
f : M' →ₗ[S] N' →ₗ[S] S := i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp
x : M'
hx :
  ∀ (n : N),
    Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) n : R) (0 : R)
⊢ Eq (α := N →ₗ[R] R) ((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) (0 : N →ₗ[R] R)
have h : ∀ (n : N),
  Eq.{u_1 + 1} (α := R) ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) x) : N →ₗ[R] R) : (a : N) → R) n : R)
    ((0 : (a : N) → R) n : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
h :
  ∀ (g : Dual S N'),
    ∃ (m : M'),
      Eq (α := N' →ₗ[S] R)
        ((↑S :
              {S_1 : Type u_1} →
                {M : Type u_3} →
                  {M₂ : Type u_1} →
                    [inst : Semiring S] →
                      [inst_19 : Semiring S_1] →
                        [inst_20 : AddCommMonoid M] →
                          [inst_21 : AddCommMonoid M₂] →
                            [inst_22 : Module S M] →
                              [inst_23 : Module S M₂] →
                                [inst_24 : Module S_1 M] →
                                  [inst_25 : Module S_1 M₂] →
                                    [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (S := R) ((p.toPerfPair : (a : M) → Dual R N) ((i : (a : M') → M) m)) ∘ₗ
          j)
        (Algebra.linearMap S R ∘ₗ g)
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
⊢ Surjective (α := M') (β := N' →ₗ[S] S)
    (⇑(i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp) : (a : M') → N' →ₗ[S] S)
have rw : (i.restrictScalarsRange₂ j (Algebra.linearMap S R) sorry p hp).range = ⊤
Tactic: rw [← LinearMap.range_eq_top]