awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Goursat (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := submoduleMap (LinearMap.fst R M N) L
Q : ↥L →ₗ[R] ↥N' := submoduleMap (LinearMap.snd R M N) L
L' : Submodule R (Prod.{u_2, u_3} ↥M' ↥N') := (P.prod Q).range
hL₁' :
  Surjective (α := ↥L') (β := ↥M')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.fst (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))
hL₂' :
  Surjective (α := ↥L') (β := ↥N')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.snd (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))
e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥M' ⧸ L'.goursatFst) (↥N' ⧸ L'.goursatSnd)
he :
  (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range =
    (↑e : ↥M' ⧸ L'.goursatFst →ₗ[R] ↥N' ⧸ L'.goursatSnd).graph
m : M
n : N
h :
  (m, n) ∈ L →
    (m, n) ∈
      map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
        (LinearMap.range (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))
⊢ (m, n) ∈ L ↔
    (m, n) ∈
      map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
        (LinearMap.range (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))
have h₁ : (m, n) ∈
    map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
      (LinearMap.range (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L))) →
  (m, n) ∈ L
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Goursat (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := submoduleMap (LinearMap.fst R M N) L
Q : ↥L →ₗ[R] ↥N' := submoduleMap (LinearMap.snd R M N) L
L' : Submodule R (Prod.{u_2, u_3} ↥M' ↥N') := (P.prod Q).range
hL₁' :
  Surjective (α := ↥L') (β := ↥M')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.fst (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))
hL₂' :
  Surjective (α := ↥L') (β := ↥N')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.snd (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))
e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥M' ⧸ L'.goursatFst) (↥N' ⧸ L'.goursatSnd)
he :
  (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range =
    (↑e : ↥M' ⧸ L'.goursatFst →ₗ[R] ↥N' ⧸ L'.goursatSnd).graph
m : M
n : N
⊢ (m, n) ∈ L →
    (m, n) ∈
      map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
        (LinearMap.range (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))
have h : (m, n) ∈ L →
  ∃ (a : M) (_ : ∃ (a_1 : M) (b : N), (a_1, b) ∈ L ∧ a_1 = a) (a_1 : N) (_ : ∃ (a : M) (b : N), (a, b) ∈ L ∧ b = a_1),
    (∃ (a_2 : M) (b : N) (_ : (a_2, b) ∈ L), a_2 = a ∧ b = a_1) ∧ a = m ∧ a_1 = n
Tactic: simp only [mem_map, LinearMap.mem_range, LinearMap.prod_apply, Function.prod_apply,
      Subtype.exists, Prod.exists, LinearMap.prodMap_apply, subtype_apply, Prod.mk.injEq,
      Subtype.ext_iff, submoduleMap_coe_apply, fst_apply, snd_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Goursat (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := submoduleMap (LinearMap.fst R M N) L
Q : ↥L →ₗ[R] ↥N' := submoduleMap (LinearMap.snd R M N) L
L' : Submodule R (Prod.{u_2, u_3} ↥M' ↥N') := (P.prod Q).range
hL₁' :
  Surjective (α := ↥L') (β := ↥M')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.fst (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))
hL₂' :
  Surjective (α := ↥L') (β := ↥N')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.snd (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))
e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥M' ⧸ L'.goursatFst) (↥N' ⧸ L'.goursatSnd)
he :
  (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range =
    (↑e : ↥M' ⧸ L'.goursatFst →ₗ[R] ↥N' ⧸ L'.goursatSnd).graph
m : M
n : N
⊢ (m, n) ∈
      map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
        (LinearMap.range
          (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L))) →
    (m, n) ∈ L
have h : (∃ (a : M) (_ : ∃ (a_1 : M) (b : N), (a_1, b) ∈ L ∧ a_1 = a) (a_1 : N) (_ : ∃ (a : M) (b : N), (a, b) ∈ L ∧ b = a_1),
    (∃ (a_2 : M) (b : N) (_ : (a_2, b) ∈ L), a_2 = a ∧ b = a_1) ∧ a = m ∧ a_1 = n) →
  (m, n) ∈ L
Tactic: simp only [mem_map, LinearMap.mem_range, LinearMap.prod_apply, Function.prod_apply,
      Subtype.exists, Prod.exists, LinearMap.prodMap_apply, subtype_apply, Prod.mk.injEq,
      snd_apply, fst_apply, Subtype.ext_iff, submoduleMap_coe_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Goursat (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := submoduleMap (LinearMap.fst R M N) L
Q : ↥L →ₗ[R] ↥N' := submoduleMap (LinearMap.snd R M N) L
L' : Submodule R (Prod.{u_2, u_3} ↥M' ↥N') := (P.prod Q).range
hL₁' :
  Surjective (α := ↥L') (β := ↥M')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.fst (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))
hL₂' :
  Surjective (α := ↥L') (β := ↥N')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.snd (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))
e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥M' ⧸ L'.goursatFst) (↥N' ⧸ L'.goursatSnd)
he :
  (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range =
    (↑e : ↥M' ⧸ L'.goursatFst →ₗ[R] ↥N' ⧸ L'.goursatSnd).graph
⊢ ker (M₂ :=
      Prod.{u_2, u_3}
        (HasQuotient.Quotient ↥(map (LinearMap.fst R M N) L) (B := Submodule R ↥(map (LinearMap.fst R M N) L))
          (goursatFst (N := ↥(map (LinearMap.snd R M N) L))
            (LinearMap.range
              (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))))
        (HasQuotient.Quotient ↥(map (LinearMap.snd R M N) L) (B := Submodule R ↥(map (LinearMap.snd R M N) L))
          (goursatSnd (M := ↥(map (LinearMap.fst R M N) L))
            (LinearMap.range
              (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L))))))
      (prodMap
        (mkQ
          (goursatFst (N := ↥(map (LinearMap.snd R M N) L))
            (LinearMap.range
              (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))))
        (mkQ
          (goursatSnd (M := ↥(map (LinearMap.fst R M N) L))
            (LinearMap.range
              (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))))) =
    (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd
have h : ∀ (x : Prod.{u_2, u_3} ↥(map (LinearMap.fst R M N) L) ↥(map (LinearMap.snd R M N) L)),
  Membership.mem (γ := Submodule R (Prod.{u_2, u_3} ↥(map (LinearMap.fst R M N) L) ↥(map (LinearMap.snd R M N) L)))
      (prod
        (goursatFst (N := ↥(map (LinearMap.snd R M N) L))
          (LinearMap.range
            (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L))))
        (goursatSnd (M := ↥(map (LinearMap.fst R M N) L))
          (LinearMap.range
            (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))))
      x ↔
    x ∈ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd
Tactic: simp only [ker_prodMap, ker_mkQ, Submodule.ext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
⊢ StrongRankCondition R ↔
    ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
      ¬Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
have refine_1 : ∀ (h : StrongRankCondition R) (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R)
  (hf : Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)), False
Tactic: refine ⟨fun h n => fun f hf => ?_, fun h => ⟨@fun n m f hf => ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
refine_1 :
  ∀ (h : StrongRankCondition R) (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R)
    (hf : Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)), False
⊢ StrongRankCondition R ↔
    ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
      ¬Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
have refine_2 : ∀
  (h :
    ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
      ¬Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R))
  (n m : ℕ) (f : (Fin n → R) →ₗ[R] Fin m → R)
  (hf : Injective (α := Fin n → R) (β := Fin m → R) (⇑f : (a : Fin n → R) → Fin m → R)), n ≤ m
Tactic: refine ⟨fun h n => fun f hf => ?_, fun h => ⟨@fun n m f hf => ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
h :
  ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
    ¬Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective (α := Fin n → R) (β := Fin m → R) (⇑f : (a : Fin n → R) → Fin m → R)
⊢ n ≤ m
have refine_2 : ∀ (H : ¬n ≤ m), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
inst_2 : OrzechProperty R
⊢ StrongRankCondition R
have refine : ∀ (n : ℕ) (i : (Fin (n + 1) → R) →ₗ[R] Fin n → R)
  (hi : Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑i : (a : Fin (n + 1) → R) → Fin n → R)), False
Tactic: refine (strongRankCondition_iff_succ R).2 fun n i hi ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
inst_2 : OrzechProperty R
n : ℕ
i : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hi : Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑i : (a : Fin (n + 1) → R) → Fin n → R)
⊢ Eq.{u + 1} (α := Fin (n + 1) → R) 0 (update (β := fun (a : Fin (n + 1)) ↦ R) 0 (Fin.last n) 1)
have a : Eq (α := Fin n → R) ((LinearMap.funLeft R R Fin.castSucc : (a : Fin (n + 1) → R) → Fin n → R) 0 : Fin n → R)
  ((LinearMap.funLeft R R Fin.castSucc : (a : Fin (n + 1) → R) → Fin n → R)
      (update (β := fun (a : Fin (n + 1)) ↦ R) 0 (Fin.last n) 1) :
    Fin n → R)
Tactic: apply OrzechProperty.injective_of_surjective_of_injective i (.funLeft ..) hi
      (Fin.castSucc_injective _).surjective_comp_right
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
inst_2 : OrzechProperty R
n : ℕ
i : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hi : Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑i : (a : Fin (n + 1) → R) → Fin n → R)
⊢ Eq (α := Fin n → R) ((LinearMap.funLeft R R Fin.castSucc : (a : Fin (n + 1) → R) → Fin n → R) 0 : Fin n → R)
    ((LinearMap.funLeft R R Fin.castSucc : (a : Fin (n + 1) → R) → Fin n → R)
        (update (β := fun (a : Fin (n + 1)) ↦ R) 0 (Fin.last n) 1) :
      Fin n → R)
have a : ∀ (x : Fin n),
  Eq (α := R) ((LinearMap.funLeft R R Fin.castSucc : (a : Fin (n + 1) → R) → Fin n → R) 0 x : R)
    ((LinearMap.funLeft R R Fin.castSucc : (a : Fin (n + 1) → R) → Fin n → R)
        (update (β := fun (a : Fin (n + 1)) ↦ R) 0 (Fin.last n) 1) x :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
inst_2 : OrzechProperty R
n : ℕ
i : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hi : Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑i : (a : Fin (n + 1) → R) → Fin n → R)
⊢ False
have h : Eq.{u + 1} (α := Fin (n + 1) → R) 0 (update (β := fun (a : Fin (n + 1)) ↦ R) 0 (Fin.last n) 1)
Tactic: have h : (0 : Fin (n + 1) → R) = update (0 : Fin (n + 1) → R) (Fin.last n) 1 := by
    apply OrzechProperty.injective_of_surjective_of_injective i (.funLeft ..) hi
      (Fin.castSucc_injective _).surjective_comp_right
    ext; simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
⊢ StrongRankCondition R ↔
    ∀ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), ¬Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)
have rw : (¬∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
      ¬Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) ↔
  ¬∀ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), ¬Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)
Tactic: rw [strongRankCondition_iff_succ, ← not_iff_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
⊢ (¬∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
        ¬Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) ↔
    ¬∀ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), ¬Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)
have push : (∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
    Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) ↔
  ∃ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)
Tactic: push Not
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
⊢ (∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
      Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) ↔
    ∃ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)
have mp : (∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
    Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) →
  ∃ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
mp :
  (∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
      Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) →
    ∃ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)
⊢ (∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
      Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) ↔
    ∃ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)
have mpr : (∃ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)) →
  ∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
    Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
⊢ (∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
      Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) →
    ∃ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)
have mp : (∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
    Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)) →
  ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R)
    (inj : Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)),
    ∃ (f : (ℕ →₀ R) →ₗ[R] Fin n → R), Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)
Tactic: refine fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
⊢ (∃ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)) →
    ∃ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
      Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
have mpr : (∃ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)) →
  ∀ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R)
    (inj : Injective (α := ℕ →₀ R) (β := Fin n → R) (⇑f : (a : ℕ →₀ R) → Fin n → R)),
    ∃ (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R),
      Injective (α := Fin (n + 1) → R) (β := Fin n → R) (⇑f : (a : Fin (n + 1) → R) → Fin n → R)
Tactic: refine fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : InvariantBasisNumber R
⊢ Nontrivial R
have by_contra! : ∀ (h : Subsingleton R), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : CommRing R
I_1 : Ideal R
ι : Type v
inst_1 : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (Ideal.pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
a b : (i : ι) → R
hab : (Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I) : ((i : ι) → R) → ((i : ι) → R) → Prop) a b
h : ι'
⊢ Membership.mem (γ := Ideal ((fun (x : ι') ↦ R) h)) ((fun (x : ι') ↦ I) h)
    (HSub.hSub (α := ι' → R) (β := ι' → R) ((e : (a : ι → R) → ι' → R) a : ι' → R)
      ((e : (a : ι → R) → ι' → R) b : ι' → R) h)
have rw : ∀
  (hab :
    Membership.mem (γ := Submodule ((i : ι) → R) ((i : ι) → R)) (Ideal.pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
      (a - b))
  (h : ι'),
  Membership.mem (γ := Ideal ((fun (x : ι') ↦ R) h)) ((fun (x : ι') ↦ I) h)
    (HSub.hSub (α := ι' → R) (β := ι' → R) ((e : (a : ι → R) → ι' → R) a : ι' → R)
      ((e : (a : ι → R) → ι' → R) b : ι' → R) h)
Tactic: rw [Submodule.quotientRel_def] at hab
Cleared hypotheses: hab, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.InvariantBasisNumber (goal)
Goal:
R : Type u
inst : CommRing R
I_1 : Ideal R
ι : Type v
inst_1 : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (Ideal.pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
a b : (i : ι) → R
hab :
  Membership.mem (γ := Submodule ((i : ι) → R) ((i : ι) → R)) (Ideal.pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I) (a - b)
h : ι'
⊢ Membership.mem (γ := Ideal ((fun (x : ι') ↦ R) h)) ((fun (x : ι') ↦ I) h)
    (HSub.hSub (α := ι' → R) (β := ι' → R) ((e : (a : ι → R) → ι' → R) a : ι' → R)
      ((e : (a : ι → R) → ι' → R) b : ι' → R) h)
have rw : Membership.mem.{u, u} (α := (fun (x : ι') ↦ R) h) (γ := Ideal ((fun (x : ι') ↦ R) h)) ((fun (x : ι') ↦ I) h)
  ((e : (a : ι → R) → ι' → R) (a - b) h : R)
Tactic: rw [← map_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
⊢ comap p.subtype (p ⊓ p') ≤ (subToSupQuotient p p').ker
have rw : comap p.subtype (p ⊓ p') ≤ comap p.subtype ((p ⊔ p') ⊓ p')
Tactic: rw [LinearMap.ker_comp, Submodule.inclusion, comap_codRestrict, ker_mkQ, map_comap_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
⊢ Function.Injective (α := ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p') (β := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
    (⇑(quotientInfToSupQuotient p p') :
      (a : ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p') → ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
have h' : (subToSupQuotient p p').ker ≤ comap p.subtype (p ⊓ p')
Tactic: rw [← ker_eq_bot, quotientInfToSupQuotient, ker_liftQ_eq_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
⊢ (subToSupQuotient p p').ker ≤ comap p.subtype (p ⊓ p')
have h' : comap (inclusion sorry) (comap (p ⊔ p').subtype p') ≤ comap p.subtype (p ⊓ p')
Tactic: rw [ker_comp, ker_mkQ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
⊢ Function.Surjective (α := ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p') (β := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
    (⇑(quotientInfToSupQuotient p p') :
      (a : ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p') → ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
have rw : ∀ (x : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'), x ∈ (subToSupQuotient p p').range
Tactic: rw [← range_eq_top, quotientInfToSupQuotient, range_liftQ, eq_top_iff']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
x_1 : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
x : M
hx : x ∈ p ⊔ p'
⊢ Quot.mk (⇑(comap (p ⊔ p').subtype p').quotientRel : ↥(p ⊔ p') → ↥(p ⊔ p') → Prop)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ p ⊔ p') x hx) ∈
    (subToSupQuotient p p').range
have mk : ∀ (y : M) (hy : y ∈ p) (z : M) (hz : z ∈ p') (hx : y + z ∈ p ⊔ p'),
  Quot.mk (⇑(comap (p ⊔ p').subtype p').quotientRel : ↥(p ⊔ p') → ↥(p ⊔ p') → Prop)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ p ⊔ p') (y + z) hx) ∈
    (subToSupQuotient p p').range
Tactic: rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
x : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ Quot.mk (⇑(comap (p ⊔ p').subtype p').quotientRel : ↥(p ⊔ p') → ↥(p ⊔ p') → Prop)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ p ⊔ p') (y + z) hx) ∈
    (subToSupQuotient p p').range
have h : Eq (α := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
  ((subToSupQuotient p p' : (a : ↥p) → ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
      (Subtype.mk (p := fun (x : M) ↦ x ∈ p) y hy) :
    ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
  (Quot.mk (⇑(comap (p ⊔ p').subtype p').quotientRel : ↥(p ⊔ p') → ↥(p ⊔ p') → Prop)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ p ⊔ p') (y + z) hx) :
    Quot (α := ↥(p ⊔ p')) (⇑(comap (p ⊔ p').subtype p').quotientRel : ↥(p ⊔ p') → ↥(p ⊔ p') → Prop))
Tactic: use ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Isomorphisms (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
x : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ Eq (α := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
    ((subToSupQuotient p p' : (a : ↥p) → ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
        (Subtype.mk (p := fun (x : M) ↦ x ∈ p) y hy) :
      ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
    (Quot.mk (⇑(comap (p ⊔ p').subtype p').quotientRel : ↥(p ⊔ p') → ↥(p ⊔ p') → Prop)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ p ⊔ p') (y + z) hx) :
      Quot (α := ↥(p ⊔ p')) (⇑(comap (p ⊔ p').subtype p').quotientRel : ↥(p ⊔ p') → ↥(p ⊔ p') → Prop))
have h : HSub.hSub (α := ↥(p ⊔ p'))
    ((inclusion sorry : (a : ↥p) → ↥(p ⊔ p')) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) y hy) : ↥(p ⊔ p'))
    (Subtype.mk (p := fun (x : M) ↦ x ∈ p ⊔ p') (y + z) hx) ∈
  comap (p ⊔ p').subtype p'
Tactic: apply (Submodule.Quotient.eq _).2