awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
inst_5 : IsPrincipal R M
m : M
hm : Eq (α := Submodule R M) ⊤ (R ∙ m)
y : M₂
h : Membership.mem (γ := Submodule R M₂) ⊤ y
⊢ Membership.mem (γ := Submodule R M₂) (span R (singleton (α := M₂) ((f : (a : M) → M₂) m : M₂))) y
have obtain : ∀ (x : M),
  Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R M₂) ⊤ ((f : (a : M) → M₂) x : M₂) →
    Membership.mem (α := M₂) (γ := Submodule R M₂) (span R (singleton (α := M₂) ((f : (a : M) → M₂) m : M₂)))
      ((f : (a : M) → M₂) x : M₂)
Tactic: obtain ⟨x, rfl⟩ := hf y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
inst_5 : IsPrincipal R M
m : M
hm : Eq (α := Submodule R M) ⊤ (R ∙ m)
x : M
h : Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R M₂) ⊤ ((f : (a : M) → M₂) x : M₂)
⊢ Membership.mem (α := M₂) (γ := Submodule R M₂) (span R (singleton (α := M₂) ((f : (a : M) → M₂) m : M₂)))
    ((f : (a : M) → M₂) x : M₂)
have obtain : ∀ (r : R),
  Membership.mem.{u_5, u_5} (α := M₂) (γ := Submodule R M₂) ⊤ ((f : (a : M) → M₂) (r • m) : M₂) →
    Membership.mem (α := M₂) (γ := Submodule R M₂) (span R (singleton (α := M₂) ((f : (a : M) → M₂) m : M₂)))
      ((f : (a : M) → M₂) (r • m) : M₂)
Tactic: obtain ⟨r, rfl⟩ := mem_span_singleton.mp (hm.le (trivial : x ∈ ⊤))
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
v : ↥(span A (↑p : Set M))
⊢ ∃ (a : TensorProduct.{u_1, u_2, u_3} R A ↥p), (tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M))) a = v
have obtain : ∀ (f : Finsupp.{u_3, u_2} (↑(↑p : Set M) : Type u_3) A)
  (hf :
    (Finsupp.linearCombination A (Subtype.val (p := fun (x : M) ↦ x ∈ (↑p : Set M))) :
          (a : (↑(↑p : Set M) : Type u_3) →₀ A) → M)
        f =
      (↑v : M)),
  ∃ (a : TensorProduct.{u_1, u_2, u_3} R A ↥p), (tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M))) a = v
Tactic: obtain ⟨f, hf⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp v.property
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
v : ↥(span A (↑p : Set M))
f : Finsupp.{u_3, u_2} (↑(↑p : Set M) : Type u_3) A
hf :
  (Finsupp.linearCombination A (Subtype.val (p := fun (x : M) ↦ x ∈ (↑p : Set M))) :
        (a : (↑(↑p : Set M) : Type u_3) →₀ A) → M)
      f =
    (↑v : M)
⊢ ∃ (a : TensorProduct.{u_1, u_2, u_3} R A ↥p), (tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M))) a = v
have h : (tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M)))
    (f.sum fun (x : (↑(↑p : Set M) : Type u_3)) (a : A) ↦ a ⊗ₜ[R] x) =
  v
Tactic: use f.sum fun x a ↦ a ⊗ₜ x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
v : ↥(span A (↑p : Set M))
f : Finsupp.{u_3, u_2} (↑(↑p : Set M) : Type u_3) A
hf :
  (Finsupp.linearCombination A (Subtype.val (p := fun (x : M) ↦ x ∈ (↑p : Set M))) :
        (a : (↑(↑p : Set M) : Type u_3) →₀ A) → M)
      f =
    (↑v : M)
⊢ (tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M)))
      (f.sum fun (x : (↑(↑p : Set M) : Type u_3)) (a : A) ↦ a ⊗ₜ[R] x) =
    v
have h : (f.sum fun (a : (↑(↑p : Set M) : Type u_3)) (b : A) ↦
    (Submodule.subtype (span A (↑p : Set M)) : (a : ↥(span A (↑p : Set M))) → M)
      ((tensorToSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M))) (b ⊗ₜ[R] a) : ↥(span A (↑p : Set M)))) =
  (↑v : M)
Tactic: rw [map_finsuppSum, Subtype.ext_iff, ← Submodule.subtype_apply, map_finsuppSum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (hypothesis)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
inst_7 : Algebra.IsEpi R A
inst_8 : Module.Flat R A
f : TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) →ₗ[A] ↥(span A (↑p : Set M)) :=
  AlgebraTensorModule.lift
    (restrictScalarsₗ R A (↥(span A (↑p : Set M))) (↥(span A (↑p : Set M))) A ∘ₗ lsmul A ↥(span A (↑p : Set M)))
g : TensorProduct.{u_1, u_2, u_3} R A ↥p →ₗ[R] TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) :=
  lTensor A (inclusionSpan A p)
⊢ Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥p) (β := ↥(span A (↑p : Set M)))
    (⇑(tensorToSpan A p) : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M)))
have hf : Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M))) (β := ↥(span A (↑p : Set M)))
  (⇑f : (a : A ⊗[R] ↥(span A (↑p : Set M))) → ↥(span A (↑p : Set M)))
Tactic: have hf : Injective f := Algebra.injective_lift_lsmul R A _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (hypothesis)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
inst_7 : Algebra.IsEpi R A
inst_8 : Module.Flat R A
f : TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) →ₗ[A] ↥(span A (↑p : Set M)) :=
  AlgebraTensorModule.lift
    (restrictScalarsₗ R A (↥(span A (↑p : Set M))) (↥(span A (↑p : Set M))) A ∘ₗ lsmul A ↥(span A (↑p : Set M)))
g : TensorProduct.{u_1, u_2, u_3} R A ↥p →ₗ[R] TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) :=
  lTensor A (inclusionSpan A p)
hf :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M))) (β := ↥(span A (↑p : Set M)))
    (⇑f : (a : A ⊗[R] ↥(span A (↑p : Set M))) → ↥(span A (↑p : Set M)))
⊢ Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥p) (β := ↥(span A (↑p : Set M)))
    (⇑(tensorToSpan A p) : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M)))
have hg : Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥p) (β := TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)))
  (⇑g : (a : A ⊗[R] ↥p) → A ⊗[R] ↥(span A (↑p : Set M)))
Tactic: have hg : Injective g := lTensor_preserves_injective_linearMap _ (p.injective_inclusionSpan A)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (hypothesis)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
inst_7 : Algebra.IsEpi R A
inst_8 : Module.Flat R A
f : TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) →ₗ[A] ↥(span A (↑p : Set M)) :=
  AlgebraTensorModule.lift
    (restrictScalarsₗ R A (↥(span A (↑p : Set M))) (↥(span A (↑p : Set M))) A ∘ₗ lsmul A ↥(span A (↑p : Set M)))
g : TensorProduct.{u_1, u_2, u_3} R A ↥p →ₗ[R] TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) :=
  lTensor A (inclusionSpan A p)
hf :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M))) (β := ↥(span A (↑p : Set M)))
    (⇑f : (a : A ⊗[R] ↥(span A (↑p : Set M))) → ↥(span A (↑p : Set M)))
hg :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥p) (β := TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)))
    (⇑g : (a : A ⊗[R] ↥p) → A ⊗[R] ↥(span A (↑p : Set M)))
⊢ Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥p) (β := ↥(span A (↑p : Set M)))
    (⇑(tensorToSpan A p) : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M)))
have this : Eq (α := TensorProduct.{u_1, u_2, u_3} R A ↥p →ₗ[R] ↥(span A (↑p : Set M)))
  ((↑R :
      {S : Type u_2} →
        {M : Type (max u_2 u_3)} →
          {M₂ : Type u_3} →
            [inst : Semiring R] →
              [inst_9 : Semiring S] →
                [inst_10 : AddCommMonoid M] →
                  [inst_11 : AddCommMonoid M₂] →
                    [inst_12 : Module R M] →
                      [inst_13 : Module R M₂] →
                        [inst_14 : Module S M] →
                          [inst_15 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (tensorToSpan A p))
  ((↑R :
        {S : Type u_2} →
          {M : Type (max u_2 u_3)} →
            {M₂ : Type u_3} →
              [inst : Semiring R] →
                [inst_9 : Semiring S] →
                  [inst_10 : AddCommMonoid M] →
                    [inst_11 : AddCommMonoid M₂] →
                      [inst_12 : Module R M] →
                        [inst_13 : Module R M₂] →
                          [inst_14 : Module S M] →
                            [inst_15 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      f ∘ₗ
    g)
Tactic: have : p.tensorToSpan A = f.restrictScalars R ∘ₗ g := by ext; simp [tensorToSpan, f, g]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Nontrivial A
inst_3 : Algebra R A
inst_4 : Algebra.IsEpi R A
inst_5 : Flat R A
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : IsScalarTower R A M
p : Submodule R M
inst_10 : Free.{u_1, u_3} R ↥p
inst_11 : Module.Finite.{u_1, u_3} R ↥p
⊢ finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = finrank.{u_1, u_3} R ↥p
have inl : Subsingleton R → finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = finrank.{u_1, u_3} R ↥p
Tactic: rcases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Nontrivial A
inst_3 : Algebra R A
inst_4 : Algebra.IsEpi R A
inst_5 : Flat R A
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : IsScalarTower R A M
p : Submodule R M
inst_10 : Free.{u_1, u_3} R ↥p
inst_11 : Module.Finite.{u_1, u_3} R ↥p
inl : Subsingleton R → finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = finrank.{u_1, u_3} R ↥p
⊢ finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = finrank.{u_1, u_3} R ↥p
have inr : Nontrivial R → finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = finrank.{u_1, u_3} R ↥p
Tactic: rcases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Nontrivial A
inst_3 : Algebra R A
inst_4 : Algebra.IsEpi R A
inst_5 : Flat R A
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : IsScalarTower R A M
p : Submodule R M
inst_10 : Free.{u_1, u_3} R ↥p
inst_11 : Module.Finite.{u_1, u_3} R ↥p
h : Nontrivial R
ι : Type u_3 := Free.ChooseBasisIndex R ↥p
b₁ : Basis ι R ↥p := Free.chooseBasis R ↥p
b₂ : Basis ι A ↥(span A (↑p : Set M)) :=
  Basis.map (M := TensorProduct.{u_1, u_2, u_3} R A ↥p) (Basis.baseChange A b₁) (tensorEquivSpan A p)
⊢ finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = finrank.{u_1, u_3} R ↥p
have inr : finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = Fintype.card ι
Tactic: rw [finrank_eq_card_basis b₁, finrank_eq_card_basis b₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Nontrivial A
inst_3 : Algebra R A
inst_4 : Algebra.IsEpi R A
inst_5 : Flat R A
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : IsScalarTower R A M
p : Submodule R M
inst_10 : Free.{u_1, u_3} R ↥p
inst_11 : Module.Finite.{u_1, u_3} R ↥p
h : Nontrivial R
ι : Type u_3 := Free.ChooseBasisIndex R ↥p
b₁ : Basis ι R ↥p := Free.chooseBasis R ↥p
b₂ : Basis ι A ↥(span A (↑p : Set M)) :=
  Basis.map (M := TensorProduct.{u_1, u_2, u_3} R A ↥p) (Basis.baseChange A b₁) (tensorEquivSpan A p)
inr : finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = Fintype.card ι
⊢ finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = finrank.{u_1, u_3} R ↥p
have inr₁ : Fintype.card ι = Fintype.card ι
Tactic: rw [finrank_eq_card_basis b₁, finrank_eq_card_basis b₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Nontrivial A
inst_3 : Algebra R A
inst_4 : Algebra.IsEpi R A
inst_5 : Flat R A
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : IsScalarTower R A M
inst_10 : IsPrincipalIdealRing R
inst_11 : IsDomain R
inst_12 : IsTorsionFree R M
s : Set M
inst_13 : Module.Finite.{u_1, u_3} R ↥(span R s)
⊢ finrank.{u_2, u_3} A ↥(span A s) = finrank.{u_1, u_3} R ↥(span R s)
have rw : finrank.{u_2, u_3} A ↥(span A (↑(span R s) : Set M)) = finrank.{u_1, u_3} R ↥(span R s)
Tactic: rw [← span_span_of_tower R, finrank_span_eq_finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Nontrivial A
inst_3 : Algebra R A
inst_4 : Algebra.IsEpi R A
inst_5 : Flat R A
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : IsScalarTower R A M
inst_10 : IsPrincipalIdealRing R
inst_11 : IsDomain R
inst_12 : IsTorsionFree R M
s : Set M
inst_13 : Module.Finite.{u_1, u_3} R ↥(span R s)
rw : finrank.{u_2, u_3} A ↥(span A (↑(span R s) : Set M)) = finrank.{u_1, u_3} R ↥(span R s)
⊢ finrank.{u_2, u_3} A ↥(span A s) = finrank.{u_1, u_3} R ↥(span R s)
have rw₁ : finrank.{u_1, u_3} R ↥(span R s) = finrank.{u_1, u_3} R ↥(span R s)
Tactic: rw [← span_span_of_tower R, finrank_span_eq_finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
⊢ u = v
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
h : Nontrivial R
⊢ u = v
have a : ∀ (x : V),
  Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
    ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
h : Nontrivial R
x : V
⊢ Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
    ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
have pos : ∀ (hx : x = 0),
  Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
    ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
h : Nontrivial R
x : V
pos :
  ∀ (hx : x = 0),
    Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
      ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
⊢ Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
    ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
have neg : ∀ (hx : ¬x = 0),
  Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
    ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
h : Nontrivial R
x : V
hx : ¬x = 0
this : ∀ (u : SpecialLinearGroup R V), (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id
⊢ Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
    ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
have this₁ : ∀ (u : SpecialLinearGroup R V) (x : V), ((↑u : V ≃ₗ[R] V) : (a : V) → V) x = x
Tactic: simp only [LinearMap.ext_iff, LinearEquiv.coe_coe, LinearMap.id_coe, id_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
h : Nontrivial R
x : V
hx : ¬x = 0
⊢ Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
    ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
have neg : ∀ (u : SpecialLinearGroup R V), (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id
Tactic: suffices ∀ (u : SpecialLinearGroup R V), (u : V →ₗ[R] V) = LinearMap.id by
      simp only [LinearMap.ext_iff, LinearEquiv.coe_coe, LinearMap.id_coe, id_eq] at this
      simp [this u, this v]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u_1 v : SpecialLinearGroup R V
h : Nontrivial R
x : V
hx : ¬x = 0
u : SpecialLinearGroup R V
⊢ (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id
have neg : ∀ (x : V), Eq (α := V) (((↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V) ((LinearMap.id : (a : V) → V) x : V)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u_1 v : SpecialLinearGroup R V
h : Nontrivial R
x_1 : V
hx : ¬x_1 = 0
u : SpecialLinearGroup R V
x : V
⊢ Eq (α := V) (((↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V) ((LinearMap.id : (a : V) → V) x : V)
have hc : let c : R := ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V);
c = ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
Tactic: set c := (LinearEquiv.smul_id_of_finrank_eq_one d1).symm u with hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u_1 v : SpecialLinearGroup R V
h : Nontrivial R
x_1 : V
hx : ¬x_1 = 0
u : SpecialLinearGroup R V
x : V
c : R := ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
hc : c = ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
⊢ Eq (α := V) (((↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V) ((LinearMap.id : (a : V) → V) x : V)
have hc₁ : (LinearEquiv.smul_id_of_finrank_eq_one d1 : (a : R) → V →ₗ[R] V) c = (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
Tactic: rw [LinearEquiv.eq_symm_apply] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u_1 v : SpecialLinearGroup R V
h : Nontrivial R
x_1 : V
hx : ¬x_1 = 0
u : SpecialLinearGroup R V
x : V
c : R := ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1 : (a : R) → V →ₗ[R] V) c = (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
⊢ Eq (α := V) (((↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V) ((LinearMap.id : (a : V) → V) x : V)
have neg : c = 1
Tactic: suffices c = 1 by
      simp [← hc, LinearEquiv.smul_id_of_finrank_eq_one, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u_1 v : SpecialLinearGroup R V
h : Nontrivial R
x_1 : V
hx : ¬x_1 = 0
u : SpecialLinearGroup R V
x : V
c : R := ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1 : (a : R) → V →ₗ[R] V) c = (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
⊢ c = 1
have hu : Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (↑u : V ≃ₗ[R] V) : Rˣ) (1 : Rˣ)
Tactic: have hu := u.prop
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
A : SpecialLinearGroup R V
⊢ Eq.{u_1 + 1} (α := Rˣ)
    (((LinearEquiv.det (R := R) (M := Module.Dual R V) : (Module.Dual R V ≃ₗ[R] Module.Dual R V) →* Rˣ) :
          (a : Module.Dual R V ≃ₗ[R] Module.Dual R V) → Rˣ)
        (↑A : V ≃ₗ[R] V).dualMap :
      Rˣ)
    (1 : Rˣ)
have simp : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (↑(↑A : V ≃ₗ[R] V) : V →ₗ[R] V) : R) (1 : R)
Tactic: simp only [← Units.val_inj, LinearEquiv.coe_det, Units.val_one,
      LinearEquiv.dualMap, LinearMap.det_dualMap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
u : LinearMap.GeneralLinearGroup R V
⊢ Membership.mem (γ := Set (LinearMap.GeneralLinearGroup R V))
      (Set.range (ι := SpecialLinearGroup R V)
        (⇑toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V))
      u ↔
    Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u.toLinearEquiv : Rˣ) (1 : Rˣ)
have mp : Membership.mem (γ := Set (LinearMap.GeneralLinearGroup R V))
    (Set.range (ι := SpecialLinearGroup R V)
      (⇑toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V))
    u →
  Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u.toLinearEquiv : Rˣ) (1 : Rˣ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.SpecialLinearGroup (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
u : LinearMap.GeneralLinearGroup R V
mp :
  Membership.mem (γ := Set (LinearMap.GeneralLinearGroup R V))
      (Set.range (ι := SpecialLinearGroup R V)
        (⇑toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V))
      u →
    Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u.toLinearEquiv : Rˣ) (1 : Rˣ)
⊢ Membership.mem (γ := Set (LinearMap.GeneralLinearGroup R V))
      (Set.range (ι := SpecialLinearGroup R V)
        (⇑toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V))
      u ↔
    Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u.toLinearEquiv : Rˣ) (1 : Rˣ)
have mpr : Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u.toLinearEquiv : Rˣ) (1 : Rˣ) →
  Membership.mem (γ := Set (LinearMap.GeneralLinearGroup R V))
    (Set.range (ι := SpecialLinearGroup R V)
      (⇑toGeneralLinearGroup : (a : SpecialLinearGroup R V) → LinearMap.GeneralLinearGroup R V))
    u
Tactic: constructor