awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst : Ring R
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R₂ M
x_1 y_1 : M
b_1 : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
span_b :
  N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
c : R
x : M
hx : x ∈ N
hc : c • y + x = 0
⊢ c = 0

Tactic:
exact hli c x hx hc
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst : Ring R
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R₂ M
x_1 y_1 : M
b_1 : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
span_b :
  N = span R (Set.range (ι := Fin n) (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)))
x : M
h : Membership.mem (γ := Submodule R M) ⊤ x
⊢ Membership.mem (γ := Submodule R M)
    (span R
      (Set.range (ι := Fin (n + 1))
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
          (Function.comp (β := ↥N) (⇑N.subtype : (a : ↥N) → M) (⇑b : (a : Fin n) → ↥N)) y)))
    x

Tactic:
simpa [Submodule.mem_span_insert', span_b] using hsp x

Premises used: Submodule.mem_span_insert'
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
N : Submodule R M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
unfold :
  Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → M)
    (⇑(have span_b := ⋯;
        Basis.mk ⋯ ⋯) :
      (a : Fin (n + 1)) → M)
    (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ M)
      (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) (⇑b : (a : Fin n) → ↥N)) y)
⊢ Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → M) (⇑(b.mkFinSnoc y hli hsp) : (a : Fin (n + 1)) → M)
    (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ M)
      (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) (⇑b : (a : Fin n) → ↥N)) y)

Tactic:
unfold mkFinSnoc

Premises used: Module.Basis.mkFinSnoc
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
N : Submodule R M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
⊢ Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → M)
    (⇑(have span_b := ⋯;
        Basis.mk ⋯ ⋯) :
      (a : Fin (n + 1)) → M)
    (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ M)
      (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) (⇑b : (a : Fin n) → ↥N)) y)

Tactic:
coe_mk (v := Fin.snoc (N.subtype ∘ b) y) _ _

Premises used: Module.Basis.coe_mk
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
N : Submodule R M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ (c : R), z + c • y ∈ N
⊢ Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → M)
    (⇑(have span_b := ⋯;
        Basis.mk ⋯ ⋯) :
      (a : Fin (n + 1)) → M)
    (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ M)
      (Function.comp (β := ↥N) (Subtype.val (p := fun (x : M) ↦ x ∈ N)) (⇑b : (a : Fin n) → ↥N)) y)

Tactic:
exact coe_mk (v := Fin.snoc (N.subtype ∘ b) y) _ _

Premises used: Module.Basis.coe_mk
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
R : Type u_3
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
N O : Submodule R M
b : Basis.{0, u_3, u_5} (Fin n) R ↥N
hNO : N ≤ O
y : M
yO : y ∈ O
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ z ∈ O, ∃ (c : R), z + c • y ∈ N
⊢ Eq.{u_5 + 1} (α := (a : Fin (n + 1)) → ↥O) (⇑(b.mkFinSnocOfLE hNO y yO hli hsp) : (a : Fin (n + 1)) → ↥O)
    (Fin.snoc (α := fun (i : Fin (n + 1)) ↦ ↥O)
      (Function.comp (β := ↥N) (⇑(Submodule.inclusion hNO) : (a : ↥N) → ↥O) (⇑b : (a : Fin n) → ↥N))
      (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO))

Tactic:
coe_mkFinSnoc _ _ _ _

Premises used: Module.Basis.coe_mkFinSnoc
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
R : Type u_7
inst : Semiring R
⊢ Eq (α := R × R) ((Basis.finTwoProd R : (a : Fin 2) → R × R) 0 : R × R) ((1, 0) : R × R)

Tactic:
simp [Basis.finTwoProd, LinearEquiv.finTwoArrow]

Premises used: LinearEquiv.finTwoArrow, Module.Basis.finTwoProd
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
R : Type u_7
inst : Semiring R
⊢ Eq (α := R × R) ((Basis.finTwoProd R : (a : Fin 2) → R × R) 1 : R × R) ((0, 1) : R × R)

Tactic:
simp [Basis.finTwoProd, LinearEquiv.finTwoArrow]

Premises used: LinearEquiv.finTwoArrow, Module.Basis.finTwoProd
-- Module: Mathlib.LinearAlgebra.Basis.Fin
Goal:
R : Type u_7
inst : Semiring R
x : R × R
⊢ (⇑((repr (Basis.finTwoProd R) : (a : R × R) → Fin 2 →₀ R) x : Fin 2 →₀ R) : (a : Fin 2) → R) = ![x.1, x.2]

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
⊢ b.flag 0 = ⊥

Tactic:
simp [flag]

Premises used: Module.Basis.flag
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
⊢ b.flag (Fin.last n) = ⊤

Tactic:
simp [flag]

Premises used: Module.Basis.flag
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin (n + 1)
p : Submodule R M
⊢ b.flag k ≤ p ↔ ∀ (i : Fin n), i.castSucc < k → Membership.mem (α := M) p ((b : (a : Fin n) → M) i : M)

Tactic:
span_le.trans forall_mem_image

Premises used: Set.Mem, Iff.trans, Submodule.span_le, Set.forall_mem_image
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
simp :
  Eq (α := Submodule R M) (span R (image (α := Fin n) (⇑b : (a : Fin n) → M) {i : Fin n | i.castSucc < k.succ}))
    (span R (singleton (α := M) ((b : (a : Fin n) → M) k : M)) ⊔
      span R (image (α := Fin n) (⇑b : (a : Fin n) → M) {i : Fin n | i < k}))
⊢ b.flag k.succ = span R (singleton (α := M) ((b : (a : Fin n) → M) k : M)) ⊔ b.flag k.castSucc

Tactic:
simp only [flag, Fin.castSucc_lt_castSucc_iff]

Premises used: Fin.castSucc_lt_castSucc_iff, Module.Basis.flag
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ Eq (α := Submodule R M) (span R (image (α := Fin n) (⇑b : (a : Fin n) → M) {i : Fin n | i.castSucc < k.succ}))
    (span R (singleton (α := M) ((b : (a : Fin n) → M) k : M)) ⊔
      span R (image (α := Fin n) (⇑b : (a : Fin n) → M) {i : Fin n | i < k}))

Tactic:
simp [Fin.castSucc_lt_iff_succ_le, le_iff_eq_or_lt, setOf_or, image_insert_eq, span_insert]

Premises used: le_iff_eq_or_lt, Set.image_insert_eq, Fin.castSucc_lt_iff_succ_le, Submodule.span_insert, Set.setOf_or
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
i : Fin n
k : Fin (n + 1)
h : i.castSucc < k
⊢ Membership.mem (α := M) (b.flag k) ((b : (a : Fin n) → M) i : M)

Tactic:
subset_span <| mem_image_of_mem _ h

Premises used: Set.Mem, Set.mem_image_of_mem, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
inst_3 : Nontrivial R
b : Basis (Fin n) R M
i : Fin n
k : Fin (n + 1)
⊢ Membership.mem (α := M) (b.flag k) ((b : (a : Fin n) → M) i : M) ↔ i.castSucc < k

Tactic:
b.self_mem_span_image

Premises used: Set.Mem, setOf, Module.Basis.self_mem_span_image
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
rw : b.flag k.castSucc ≤ span R (singleton (α := M) ((b : (a : Fin n) → M) k : M)) ⊔ b.flag k.castSucc
⊢ b.flag k.castSucc ≤ b.flag k.succ

Tactic:
rw [flag_succ]

Premises used: Module.Basis.flag_succ
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.castSucc ≤ span R (singleton (α := M) ((b : (a : Fin n) → M) k : M)) ⊔ b.flag k.castSucc

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.castSucc ≤ span R (singleton (α := M) ((b : (a : Fin n) → M) k : M)) ⊔ b.flag k.castSucc

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
⊢ IsChain (fun (x1 x2 : Submodule R M) ↦ x1 ≤ x2) (range b.flag)

Tactic:
b.flag_mono.isChain_range

Premises used: Module.Basis.flag_mono, Monotone.isChain_range
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
inst_3 : Nontrivial R
b : Basis (Fin n) R M
x : Fin n
⊢ b.flag x.castSucc < b.flag x.succ

Tactic:
simp [flag_succ]

Premises used: Module.Basis.flag_succ
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
inst_3 : Nontrivial R
b : Basis (Fin n) R M
k : Fin (n + 1)
l : Fin n
⊢ b.flag k ≤ (b.coord l).ker ↔ k ≤ l.castSucc

Tactic:
simp [flag_le_iff, Finsupp.single_apply_eq_zero, imp_false, imp_not_comm]

Premises used: imp_false, Finsupp.single_apply_eq_zero, imp_not_comm, Module.Basis.flag_le_iff
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin (n + 1)
l : Fin n
h : k ≤ l.castSucc
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin (n + 1)
l : Fin n
h : k ≤ l.castSucc
h_1 : Nontrivial R
⊢ b.flag k ≤ (b.coord l).ker

Tactic:
b.flag_le_ker_coord_iff.2 h

Premises used: Iff.mpr, Module.Basis.flag_le_ker_coord_iff
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin (n + 1)
l : Fin n
h : k ≤ l.castSucc
h_1 : Nontrivial R
⊢ b.flag k ≤ (b.coord l).ker

Tactic:
exact b.flag_le_ker_coord_iff.2 h

Premises used: Iff.mpr, Module.Basis.flag_le_ker_coord_iff
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
h : Nontrivial R
rw : b.flag k.castSucc ≤ (b.coord k).ker
rw₁ rw₂ : k.castSucc ≤ k.castSucc
⊢ b.flag k.castSucc ≤ LinearMap.ker (R₂ := R) (M₂ := R) (τ₁₂ := RingHom.id R) ((b.dualBasis : (a : Fin n) → Dual R M) k)

Tactic:
rw [coe_dualBasis, b.flag_le_ker_coord_iff]

Premises used: Module.Basis.coe_dualBasis, Module.Basis.flag_le_ker_coord_iff
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
b : Basis (Fin n) K V
i : Fin n
rw : b.flag i.castSucc ⋖ span K (singleton (α := V) ((b : (a : Fin n) → V) i : V)) ⊔ b.flag i.castSucc
⊢ b.flag i.castSucc ⋖ b.flag i.succ

Tactic:
rw [flag_succ]

Premises used: Module.Basis.flag_succ
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
b : Basis (Fin n) K V
i : Fin n
h : ((b : (a : Fin n) → V) i : V) ∉ b.flag i.castSucc
⊢ b.flag i.castSucc ⋖ span K (singleton (α := V) ((b : (a : Fin n) → V) i : V)) ⊔ b.flag i.castSucc

Tactic:
apply covBy_span_singleton_sup

Premises used: Submodule.covBy_span_singleton_sup
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
b : Basis (Fin n) K V
i : Fin n
⊢ ((b : (a : Fin n) → V) i : V) ∉ b.flag i.castSucc

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
b : Basis (Fin n) K V
i : Fin n
⊢ b.flag i.castSucc ⩿ b.flag i.succ

Tactic:
(b.flag_covBy i).wcovBy

Premises used: Module.Basis.flag_covBy, CovBy.wcovBy
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
b : Basis (Fin n) K V
p : Submodule K V
⊢ p ∈ b.toFlag ↔ ∃ (k : Fin (n + 1)), b.flag k = p

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.LinearAlgebra.Basis.Flag
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
n : ℕ
b : Basis (Fin n) K V
⊢ IsMaxChain (fun (x1 x2 : Submodule K V) ↦ x1 ≤ x2) (range b.flag)

Tactic:
b.toFlag.maxChain

Premises used: setOf, Module.Basis.toFlag, Set.range, Flag.maxChain
-- Module: Mathlib.LinearAlgebra.Basis.MulOpposite
Goal:
R : Type u_1
H : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid H
inst_2 : Module R H
b : Basis ι R H
i : ι
⊢ Eq.{u_2 + 1} (α := Hᵐᵒᵖ) ((b.mulOpposite : (a : ι) → Hᵐᵒᵖ) i : Hᵐᵒᵖ) (op ((b : (a : ι) → H) i) : Hᵐᵒᵖ)

Tactic:
rfl

Premises used: rfl, MulOpposite.op
-- Module: Mathlib.LinearAlgebra.Basis.MulOpposite
Goal:
R : Type u_1
H : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid H
inst_2 : Module R H
b : Basis ι R H
⊢ b.mulOpposite.repr = LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ b.repr

Tactic:
rfl

Premises used: LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.Basis.MulOpposite
Goal:
R : Type u_1
H : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid H
inst_2 : Module R H
b : Basis ι R H
x : Hᵐᵒᵖ
⊢ Eq (α := ι →₀ R) ((b.repr : (a : H) → ι →₀ R) (unop x) : ι →₀ R)
    ((b.mulOpposite.repr : (a : Hᵐᵒᵖ) → ι →₀ R) x : ι →₀ R)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.LinearAlgebra.Basis.MulOpposite
Goal:
R : Type u_1
H : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid H
inst_2 : Module R H
b : Basis ι R H
x : H
⊢ Eq (α := ι →₀ R) ((b.mulOpposite.repr : (a : Hᵐᵒᵖ) → ι →₀ R) (op x) : ι →₀ R) ((b.repr : (a : H) → ι →₀ R) x : ι →₀ R)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.LinearAlgebra.Basis.MulOpposite
Goal:
R : Type u_1
H : Type u_2
inst : DivisionRing R
inst_1 : AddCommGroup H
inst_2 : Module R H
inst_3 : FiniteDimensional R H
⊢ FiniteDimensional.{u_1, u_2} R Hᵐᵒᵖ

Tactic:
FiniteDimensional.of_finite_basis
  (Basis.ofVectorSpace R H).mulOpposite (Basis.ofVectorSpaceIndex R H).toFinite

Premises used: FiniteDimensional.of_finite_basis, Module.Basis.mulOpposite, Set.toFinite, Module.Basis.ofVectorSpace, Module.Basis.ofVectorSpaceIndex
-- Module: Mathlib.LinearAlgebra.Basis.MulOpposite
Goal:
R : Type u_1
H : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid H
inst_2 : Module R H
inst_3 : Free R H
⊢ Free.{u_1, u_2} R Hᵐᵒᵖ

Tactic:
let ⟨b⟩ := Module.Free.exists_basis (R := R) (M := H)
  Module.Free.of_basis b.2.mulOpposite

Premises used: _private.0.MulOpposite.instFree.match_1, MulOpposite, Module.Basis.mulOpposite, Module.Free, Module.Free.of_basis, Module.Free.exists_basis, Sigma.snd
-- Module: Mathlib.LinearAlgebra.Basis.MulOpposite
Goal:
R : Type u_1
H : Type u_2
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : AddCommMonoid H
inst_3 : Module R H
inst_4 : Free R H
⊢ Module.rank R Hᵐᵒᵖ = Module.rank R H

Tactic:
LinearEquiv.nonempty_equiv_iff_rank_eq.mp ⟨(opLinearEquiv R).symm⟩

Premises used: LinearEquiv.symm, MulOpposite.opLinearEquiv, Nonempty.intro, Iff.mp, LinearEquiv.nonempty_equiv_iff_rank_eq
-- Module: Mathlib.LinearAlgebra.Basis.MulOpposite
Goal:
R : Type u_1
H : Type u_2
inst : DivisionRing R
inst_1 : AddCommGroup H
inst_2 : Module R H
b : Basis (↑(Basis.ofVectorSpaceIndex R H) : Type u_2) R H := Basis.ofVectorSpace R H
rw : Module.finrank.{u_1, u_2} R Hᵐᵒᵖ = Nat.card.{u_2} (↑(Basis.ofVectorSpaceIndex R H) : Type u_2)
rw₁ rw₂ :
  Nat.card.{u_2} (↑(Basis.ofVectorSpaceIndex R H) : Type u_2) =
    Nat.card.{u_2} (↑(Basis.ofVectorSpaceIndex R H) : Type u_2)
⊢ Module.finrank.{u_1, u_2} R Hᵐᵒᵖ = Module.finrank R H

Tactic:
rw [Module.finrank_eq_nat_card_basis b, Module.finrank_eq_nat_card_basis b.mulOpposite]

Premises used: Module.Basis.mulOpposite, Module.finrank_eq_nat_card_basis
-- Module: Mathlib.LinearAlgebra.Basis.Prod
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
x : M × M'
i : ι
⊢ Eq.{u_3 + 1} (α := R)
    (((((b.prod b').repr : (a : M × M') → ι ⊕ ι' →₀ R) x : ι ⊕ ι' →₀ R) : (a : ι ⊕ ι') → R) (Sum.inl i) : R)
    ((((b.repr : (a : M) → ι →₀ R) x.1 : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.LinearAlgebra.Basis.Prod
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
x : M × M'
i : ι'
⊢ Eq.{u_3 + 1} (α := R)
    (((((b.prod b').repr : (a : M × M') → ι ⊕ ι' →₀ R) x : ι ⊕ ι' →₀ R) : (a : ι ⊕ ι') → R) (Sum.inr i) : R)
    ((((b'.repr : (a : M') → ι' →₀ R) x.2 : ι' →₀ R) : (a : ι') → R) i : R)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.LinearAlgebra.Basis.Prod
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
h :
  ∀ (j : ι),
    Eq.{u_3 + 1} (α := R)
      (((b.repr : (a : M) → ι →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl i)).1 : (a : ι) → R) j : R)
      ((((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R) : (a : ι) → R) j : R)
⊢ Eq (α := ι →₀ R) ((b.repr : (a : M) → ι →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl i)).1 : ι →₀ R)
    ((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R)

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Basis.Prod
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i j : ι
h : Eq.{u_3 + 1} (α := R) ((single (Sum.inl i) 1 : (a : ι ⊕ ι') → R) (Sum.inl j) : R) ((single i 1 : (a : ι) → R) j : R)
⊢ Eq.{u_3 + 1} (α := R)
    (((b.repr : (a : M) → ι →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl i)).1 : (a : ι) → R) j : R)
    ((((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R) : (a : ι) → R) j : R)

Tactic:
simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b.repr.apply_symm_apply,
      LinearEquiv.symm_symm, repr_self, Finsupp.fst_sumFinsuppLEquivProdFinsupp]

Premises used: Finsupp.fst_sumFinsuppLEquivProdFinsupp, LinearEquiv.symm_trans_apply, Module.Basis.repr, LinearEquiv.symm_symm, Module.Basis.prod, LinearEquiv.prodCongr_symm, Module.Basis.coe_ofRepr, LinearEquiv.prodCongr_apply, LinearEquiv.apply_symm_apply, Module.Basis.repr_self
-- Module: Mathlib.LinearAlgebra.Basis.Prod
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i j : ι
⊢ Eq.{u_3 + 1} (α := R) ((single (Sum.inl i) 1 : (a : ι ⊕ ι') → R) (Sum.inl j) : R) ((single i 1 : (a : ι) → R) j : R)

Tactic:
apply Finsupp.single_apply_left Sum.inl_injective

Premises used: Sum.inl_injective, Finsupp.single_apply_left
-- Module: Mathlib.LinearAlgebra.Basis.Prod
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι'
h :
  ∀ (i_1 : ι),
    Eq.{u_3 + 1} (α := R)
      (((b.repr : (a : M) → ι →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inr i)).1 : (a : ι) → R) i_1 : R)
      (((b.repr : (a : M) → ι →₀ R) 0 : (a : ι) → R) i_1 : R)
⊢ Eq (α := ι →₀ R) ((b.repr : (a : M) → ι →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inr i)).1)
    ((b.repr : (a : M) → ι →₀ R) 0)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Basis.Prod
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i_1 : ι'
i : ι
h : Eq.{u_3 + 1} (α := R) ((single (Sum.inr i_1) 1 : (a : ι ⊕ ι') → R) (Sum.inl i) : R) (0 : R)
⊢ Eq.{u_3 + 1} (α := R)
    (((b.repr : (a : M) → ι →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inr i_1)).1 : (a : ι) → R) i : R)
    (((b.repr : (a : M) → ι →₀ R) 0 : (a : ι) → R) i : R)

Tactic:
simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b.repr.apply_symm_apply,
      LinearEquiv.symm_symm, Finsupp.fst_sumFinsuppLEquivProdFinsupp,
      map_zero, Finsupp.zero_apply]

Premises used: Finsupp.fst_sumFinsuppLEquivProdFinsupp, map_zero, LinearEquiv.symm_trans_apply, Module.Basis.repr, LinearEquiv.symm_symm, Module.Basis.prod, Finsupp.zero_apply, LinearEquiv.prodCongr_symm, Module.Basis.coe_ofRepr, LinearEquiv.prodCongr_apply, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Basis.Prod
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i_1 : ι'
i : ι
⊢ Eq.{u_3 + 1} (α := R) ((single (Sum.inr i_1) 1 : (a : ι ⊕ ι') → R) (Sum.inl i) : R) (0 : R)

Tactic:
apply Finsupp.single_eq_of_ne Sum.inl_ne_inr

Premises used: Sum.inl_ne_inr, Finsupp.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.Basis.Prod
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
h :
  ∀ (j : ι'),
    Eq.{u_3 + 1} (α := R)
      (((b'.repr : (a : M') → ι' →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl i)).2 : (a : ι') → R) j : R)
      (((b'.repr : (a : M') → ι' →₀ R) 0 : (a : ι') → R) j : R)
⊢ Eq (α := ι' →₀ R) ((b'.repr : (a : M') → ι' →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl i)).2)
    ((b'.repr : (a : M') → ι' →₀ R) 0)

Tactic:
ext j