awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Goursat
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)))
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
⊢ (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)))

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Goursat
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 →
    ∃ (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 →
    (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)))

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]

Premises used: LinearMap.prodMap_apply, LinearMap.submoduleMap_coe_apply, Submodule.mem_map, Submodule.subtype_apply, Subtype.exists, Subtype.ext_iff, LinearMap.fst_apply, LinearMap.mem_range, Prod.mk.injEq, Function.prod_apply, LinearMap.prod_apply, Prod.exists, LinearMap.snd_apply
-- Module: Mathlib.LinearAlgebra.Goursat
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 →
    ∃ (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:
grind
-- Module: Mathlib.LinearAlgebra.Goursat
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 :
  (∃ (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
⊢ (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:
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]

Premises used: LinearMap.prodMap_apply, LinearMap.submoduleMap_coe_apply, Submodule.mem_map, Submodule.subtype_apply, Subtype.exists, Subtype.ext_iff, LinearMap.fst_apply, LinearMap.mem_range, Prod.mk.injEq, Function.prod_apply, LinearMap.prod_apply, Prod.exists, LinearMap.snd_apply
-- Module: Mathlib.LinearAlgebra.Goursat
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
⊢ (∃ (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:
grind
-- Module: Mathlib.LinearAlgebra.Goursat
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
⊢ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd ≤ (P.prod Q).range

Tactic:
goursatFst_prod_goursatSnd_le (range <| P.prod Q)

Premises used: LinearMap.range, Submodule.goursatFst_prod_goursatSnd_le, LinearMap.prod
-- Module: Mathlib.LinearAlgebra.Goursat
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
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
⊢ 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

Tactic:
simp only [ker_prodMap, ker_mkQ, Submodule.ext_iff]

Premises used: Submodule.ext_iff, LinearMap.ker_prodMap, Submodule.ker_mkQ
-- Module: Mathlib.LinearAlgebra.Goursat
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
⊢ ∀ (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:
grind
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
⊢ Injective (α := Fin n → R) (β := Fin m → R) (⇑f : (a : Fin n → R) → Fin m → R) → n ≤ m

Tactic:
StrongRankCondition.le_of_fin_injective f

Premises used: StrongRankCondition.le_of_fin_injective
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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)

Tactic:
⟨fun h n => fun f hf => ?_, fun h => ⟨@fun n m f hf => ?_⟩⟩

Premises used: Iff.intro, StrongRankCondition.mk
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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
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
⊢ 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)

Tactic:
refine ⟨fun h n => fun f hf => ?_, fun h => ⟨@fun n m f hf => ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
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:
Nat.not_succ_le_self n (le_of_fin_injective R f hf)

Premises used: le_of_fin_injective, Nat.not_succ_le_self
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
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:
exact Nat.not_succ_le_self n (le_of_fin_injective R f hf)

Premises used: le_of_fin_injective, Nat.not_succ_le_self
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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)
refine_2 : ∀ (H : ¬n ≤ m), False
⊢ n ≤ m

Tactic:
by_contra H
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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)
H : ¬n ≤ m
⊢ False

Tactic:
h m (f.comp (Function.ExtendByZero.linearMap R (Fin.castLE (not_le.1 H))))
        (hf.comp (Function.extend_injective (Fin.strictMono_castLE _).injective _))

Premises used: not_le, Fin.castLE, Function.extend_injective, LinearMap.comp, StrictMono.injective, Function.Injective.comp, Function.ExtendByZero.linearMap, Iff.mp, Fin.strictMono_castLE
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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)
H : ¬n ≤ m
⊢ False

Tactic:
exact
      h m (f.comp (Function.ExtendByZero.linearMap R (Fin.castLE (not_le.1 H))))
        (hf.comp (Function.extend_injective (Fin.strictMono_castLE _).injective _))

Premises used: not_le, Fin.castLE, Function.extend_injective, LinearMap.comp, StrictMono.injective, Function.Injective.comp, Function.ExtendByZero.linearMap, Iff.mp, Fin.strictMono_castLE
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
inst_2 : OrzechProperty R
⊢ StrongRankCondition R

Tactic:
(strongRankCondition_iff_succ R).2 fun n i hi ↦ ?_

Premises used: Iff.mpr, strongRankCondition_iff_succ
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
inst_2 : OrzechProperty R
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
⊢ StrongRankCondition R

Tactic:
refine (strongRankCondition_iff_succ R).2 fun n i hi ↦ ?_

Premises used: Iff.mpr, strongRankCondition_iff_succ
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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)
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)
⊢ Eq.{u + 1} (α := Fin (n + 1) → R) 0 (update (β := fun (a : Fin (n + 1)) ↦ R) 0 (Fin.last n) 1)

Tactic:
apply OrzechProperty.injective_of_surjective_of_injective i (.funLeft ..) hi
      (Fin.castSucc_injective _).surjective_comp_right

Premises used: Function.Injective.surjective_comp_right, Fin.castSucc_injective, OrzechProperty.injective_of_surjective_of_injective, LinearMap.funLeft
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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)
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)
⊢ 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:
ext
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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)
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:
simp
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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)

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
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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)
h : Eq.{u + 1} (α := Fin (n + 1) → R) 0 (update (β := fun (a : Fin (n + 1)) ↦ R) 0 (Fin.last n) 1)
⊢ False

Tactic:
simpa using congr_fun h (Fin.last n)

Premises used: Fin.last, congr_fun
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
α : Type u_1
β : Type u_2
inst_2 : Fintype α
inst_3 : Fintype β
f : (α → R) →ₗ[R] β → R
i : Injective (α := α → R) (β := β → R) (⇑f : (a : α → R) → β → R)
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
Q : (Fin (Fintype.card β) → R) ≃ₗ[R] β → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
le_of_fin_injective R
    (Q.symm.toLinearMap ∘ₗ f ∘ₗ P) (Q.symm.injective.comp (i.comp P.injective))

Premises used: LinearEquiv.symm, LinearMap.comp, LinearEquiv.toLinearMap, Function.Injective.comp, le_of_fin_injective, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
α : Type u_1
β : Type u_2
inst_2 : Fintype α
inst_3 : Fintype β
f : (α → R) →ₗ[R] β → R
i : Injective (α := α → R) (β := β → R) (⇑f : (a : α → R) → β → R)
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
Q : (Fin (Fintype.card β) → R) ≃ₗ[R] β → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
exact le_of_fin_injective R
    (Q.symm.toLinearMap ∘ₗ f ∘ₗ P) (Q.symm.injective.comp (i.comp P.injective))

Premises used: LinearEquiv.symm, LinearMap.comp, LinearEquiv.toLinearMap, Function.Injective.comp, le_of_fin_injective, LinearEquiv.injective