awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R α)
⊢ Fintype.card α ≤ Fintype.card β

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

Premises used: card_le_of_injective, LinearMap.comp, LinearEquiv.toLinearMap, Function.Injective.comp, 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 : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R α)
⊢ Fintype.card α ≤ Fintype.card β

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

Premises used: card_le_of_injective, LinearMap.comp, LinearEquiv.toLinearMap, Function.Injective.comp, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : RankCondition R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
⊢ Surjective (α := Fin n → R) (β := Fin m → R) (⇑f : (a : Fin n → R) → Fin m → R) → m ≤ n

Tactic:
RankCondition.le_of_fin_surjective f

Premises used: RankCondition.le_of_fin_surjective
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : RankCondition R
α : Type u_1
β : Type u_2
inst_2 : Fintype α
inst_3 : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective (α := α → 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_surjective R
    (Q.symm.toLinearMap ∘ₗ f ∘ₗ P) (Q.symm.surjective.comp (i.comp P.surjective))

Premises used: LinearEquiv.symm, LinearEquiv.surjective, LinearMap.comp, LinearEquiv.toLinearMap, Function.Surjective.comp, le_of_fin_surjective
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : RankCondition R
α : Type u_1
β : Type u_2
inst_2 : Fintype α
inst_3 : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective (α := α → 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_surjective R
    (Q.symm.toLinearMap ∘ₗ f ∘ₗ P) (Q.symm.surjective.comp (i.comp P.surjective))

Premises used: LinearEquiv.symm, LinearEquiv.surjective, LinearMap.comp, LinearEquiv.toLinearMap, Function.Surjective.comp, le_of_fin_surjective
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : RankCondition R
α : Type u_1
β : Type u_2
inst_2 : Fintype α
inst_3 : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective (α := α →₀ R) (β := β →₀ R) (⇑f : (a : α →₀ R) → β →₀ R)
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R α)
⊢ Fintype.card β ≤ Fintype.card α

Tactic:
card_le_of_surjective R (P.toLinearMap ∘ₗ f ∘ₗ Q) (P.surjective.comp (i.comp Q.surjective))

Premises used: LinearEquiv.surjective, LinearMap.comp, LinearEquiv.toLinearMap, Function.Surjective.comp, card_le_of_surjective
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : RankCondition R
α : Type u_1
β : Type u_2
inst_2 : Fintype α
inst_3 : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective (α := α →₀ R) (β := β →₀ R) (⇑f : (a : α →₀ R) → β →₀ R)
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R α)
⊢ Fintype.card β ≤ Fintype.card α

Tactic:
exact card_le_of_surjective R (P.toLinearMap ∘ₗ f ∘ₗ Q) (P.surjective.comp (i.comp Q.surjective))

Premises used: LinearEquiv.surjective, LinearMap.comp, LinearEquiv.toLinearMap, Function.Surjective.comp, card_le_of_surjective
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : RankCondition R
M : Type u_1
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Surjective.{u + 1, u_1 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
g : M →ₗ[R] Fin (n + 1) → R
hg : Surjective.{u_1 + 1, u + 1} (α := M) (β := Fin (n + 1) → R) (⇑g : (a : M) → Fin (n + 1) → R)
⊢ False

Tactic:
simpa using le_of_fin_surjective R (g ∘ₗ f) (hg.comp hf)

Premises used: LinearMap.comp, Function.Surjective.comp, le_of_fin_surjective
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
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)
⊢ StrongRankCondition 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]

Premises used: not_iff_not, strongRankCondition_iff_succ
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
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)
⊢ (¬∀ (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

Premises used: Not
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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)
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)
⊢ (∃ (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
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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)

Tactic:
fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩

Premises used: Exists, Exists.intro, Function.Injective, DFunLike.coe, _private.0.strongRankCondition_iff_forall_not_injective.match_1
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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 : (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)
⊢ (∃ (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:
refine fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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)

Tactic:
fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩

Premises used: Exists, _private.0.strongRankCondition_iff_forall_not_injective.match_2, Exists.intro, Function.Injective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
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)
⊢ (∃ (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:
refine fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩
-- 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 : ℕ
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:
f.exists_finsupp_nat_of_fin_fun_injective inj

Premises used: LinearMap.exists_finsupp_nat_of_fin_fun_injective
-- 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 : ℕ
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:
exact f.exists_finsupp_nat_of_fin_fun_injective inj

Premises used: LinearMap.exists_finsupp_nat_of_fin_fun_injective
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
h : ∃ (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)
⊢ Injective (α := Fin (n + 1) → R) (β := ℕ →₀ R)
    (⇑(Finsupp.lmapDomain R R Fin.val ∘ₗ
          (↑(LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R (Fin (n + 1)))) :
            (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) →₀ R)) :
      (a : Fin (n + 1) → R) → ℕ →₀ R)

Tactic:
simpa using Finsupp.mapDomain_injective Fin.val_injective

Premises used: Fin.val_injective, Finsupp.mapDomain_injective
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
h : ∃ (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:
exact ⟨f ∘ₗ Finsupp.lmapDomain R R (↑) ∘ₗ (Finsupp.linearEquivFunOnFinite ..).symm.toLinearMap,
      inj.comp <| by simpa using Finsupp.mapDomain_injective Fin.val_injective⟩
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : InvariantBasisNumber R
n m : ℕ
⊢ ∀ (a : (Fin n → R) ≃ₗ[R] Fin m → R), n = m

Tactic:
InvariantBasisNumber.eq_of_fin_equiv

Premises used: InvariantBasisNumber.eq_of_fin_equiv
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : InvariantBasisNumber R
α : Type u_1
β : Type u_2
inst_2 : Fintype α
inst_3 : Fintype β
f : (α → R) ≃ₗ[R] β → R
⊢ Fintype.card α = Fintype.card β

Tactic:
eq_of_fin_equiv R
    (.funCongrLeft R R (Fintype.equivFin α) ≪≫ₗ f ≪≫ₗ
      .symm (.funCongrLeft R R (Fintype.equivFin β)))

Premises used: eq_of_fin_equiv, LinearEquiv.symm, Fintype.equivFin, LinearEquiv.funCongrLeft, LinearEquiv.trans
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : InvariantBasisNumber R
by_contra! : ∀ (h : Subsingleton R), False
⊢ Nontrivial R

Tactic:
by_contra! h
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : InvariantBasisNumber R
h : Subsingleton R
⊢ False

Tactic:
zero_ne_one (eq_of_fin_equiv R <| .ofSubsingleton ..)

Premises used: eq_of_fin_equiv, zero_ne_one, LinearEquiv.ofSubsingleton
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Semiring R
inst_1 : InvariantBasisNumber R
h : Subsingleton R
⊢ False

Tactic:
exact zero_ne_one (eq_of_fin_equiv R <| .ofSubsingleton ..)

Premises used: eq_of_fin_equiv, zero_ne_one, LinearEquiv.ofSubsingleton
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : IsNoetherianRing R
⊢ StrongRankCondition R

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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 : ι'
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)
⊢ 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

Premises used: Submodule.quotientRel_def
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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 : ι'
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)
⊢ 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 [← map_sub]

Premises used: map_sub
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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.{u, u} (α := (fun (x : ι') ↦ R) h) (γ := Ideal ((fun (x : ι') ↦ R) h)) ((fun (x : ι') ↦ I) h)
    ((e : (a : ι → R) → ι' → R) (a - b) h : R)

Tactic:
Ideal.map_pi _ _ hab e h

Premises used: Ideal.map_pi, Set.Mem
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
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.{u, u} (α := (fun (x : ι') ↦ R) h) (γ := Ideal ((fun (x : ι') ↦ R) h)) ((fun (x : ι') ↦ I) h)
    ((e : (a : ι → R) → ι' → R) (a - b) h : R)

Tactic:
exact Ideal.map_pi _ _ hab e h

Premises used: Ideal.map_pi
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : CommRing R
I_1 : Ideal R
ι : Type v
inst_1 : Fintype ι
ι' : Type w
inst_2 : Fintype ι'
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 : (i : ι) → R
y : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (Ideal.pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
b : (i : ι) → R
⊢ induced_map I (↑e : (ι → R) →ₗ[R] ι' → R)
      (HAdd.hAdd (α :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (Ideal.pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) b)) =
    induced_map I (↑e : (ι → R) →ₗ[R] ι' → R)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a) +
      induced_map I (↑e : (ι → R) →ₗ[R] ι' → R)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) b)

Tactic:
congr_arg _ (map_add ..)

Premises used: Quotient.liftOn', Submodule.Quotient.mk, map_add, Quotient.map₂, congr_arg, _private.0.induced_map
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : CommRing R
I_1 : Ideal R
ι : Type v
inst_1 : Fintype ι
ι' : Type w
inst_2 : Fintype ι'
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 : (i : ι) → R
y : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (Ideal.pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
b : (i : ι) → R
⊢ induced_map I (↑e : (ι → R) →ₗ[R] ι' → R)
      (HAdd.hAdd (α :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (Ideal.pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) b)) =
    induced_map I (↑e : (ι → R) →ₗ[R] ι' → R)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a) +
      induced_map I (↑e : (ι → R) →ₗ[R] ι' → R)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) b)

Tactic:
exact congr_arg _ (map_add ..)

Premises used: map_add, congr_arg
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : CommRing R
I_1 : Ideal R
ι : Type v
inst_1 : Fintype ι
ι' : Type w
inst_2 : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
m : R ⧸ I
a : R
x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (Ideal.pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
b : (i : ι) → R
⊢ induced_map I (↑e : (ι → R) →ₗ[R] ι' → R)
      (HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (Ideal.pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) b)) =
    HSMul.hSMul (α := R ⧸ I)
      ((RingHom.id (R ⧸ I) : (a : R ⧸ I) → R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) : R ⧸ I)
      (induced_map I (↑e : (ι → R) →ₗ[R] ι' → R)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) b))

Tactic:
congr_arg _ (map_smul ..)

Premises used: Quotient.liftOn', Submodule.Quotient.mk, congr_arg, _private.0.induced_map, map_smul, Quotient.liftOn₂'
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : CommRing R
I_1 : Ideal R
ι : Type v
inst_1 : Fintype ι
ι' : Type w
inst_2 : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
m : R ⧸ I
a : R
x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (Ideal.pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
b : (i : ι) → R
⊢ induced_map I (↑e : (ι → R) →ₗ[R] ι' → R)
      (HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (Ideal.pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) b)) =
    HSMul.hSMul (α := R ⧸ I)
      ((RingHom.id (R ⧸ I) : (a : R ⧸ I) → R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) : R ⧸ I)
      (induced_map I (↑e : (ι → R) →ₗ[R] ι' → R)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) b))

Tactic:
exact congr_arg _ (map_smul ..)

Premises used: congr_arg, map_smul
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : CommRing R
I_1 : Ideal R
ι : Type v
inst_1 : Fintype ι
ι' : Type w
inst_2 : Fintype ι'
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 : (i : ι) → R
⊢ induced_map I (↑e.symm : (ι' → R) →ₗ[R] ι → R)
      (induced_map I (↑e : (ι → R) →ₗ[R] ι' → R)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a)) =
    Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a

Tactic:
congr_arg _ (e.left_inv ..)

Premises used: Quotient.liftOn', Submodule.Quotient.mk, LinearEquiv.left_inv, congr_arg, _private.0.induced_map
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : CommRing R
I_1 : Ideal R
ι : Type v
inst_1 : Fintype ι
ι' : Type w
inst_2 : Fintype ι'
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 : (i : ι) → R
⊢ induced_map I (↑e.symm : (ι' → R) →ₗ[R] ι → R)
      (induced_map I (↑e : (ι → R) →ₗ[R] ι' → R)
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a)) =
    Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a

Tactic:
exact congr_arg _ (e.left_inv ..)

Premises used: LinearEquiv.left_inv, congr_arg