awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (ι → R) →ₗ[R] ι' → R)
      (induced_map I (↑e.symm : (ι' → 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.right_inv ..)

Premises used: LinearEquiv.right_inv, Quotient.liftOn', Submodule.Quotient.mk, 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 : (ι → R) →ₗ[R] ι' → R)
      (induced_map I (↑e.symm : (ι' → 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.right_inv ..)

Premises used: LinearEquiv.right_inv, congr_arg
-- Module: Mathlib.LinearAlgebra.InvariantBasisNumber
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
⊢ InvariantBasisNumber R

Tactic:
⟨fun e =>
    let ⟨I, _hI⟩ := Ideal.exists_maximal R
    eq_of_fin_equiv (R ⧸ I)
      ((Ideal.piQuotEquiv _ _).symm ≪≫ₗ inducedEquiv _ e ≪≫ₗ Ideal.piQuotEquiv _ _)⟩

Premises used: eq_of_fin_equiv, _private.0.invariantBasisNumber_of_nontrivial_of_commRing.match_1, Ideal.exists_maximal, LinearEquiv.symm, InvariantBasisNumber.mk, _private.0.inducedEquiv, HasQuotient.Quotient, Fin, LinearEquiv.trans, Eq, Ideal.piQuotEquiv
-- Module: Mathlib.LinearAlgebra.Isomorphisms
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
x : M
⊢ Eq.{u_3 + 1} (α := M₂) ((↑((f.quotKerEquivRange : (a : M ⧸ f.ker) → ↥f.range) (Submodule.Quotient.mk x)) : M₂) : M₂)
    ((f : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.LinearAlgebra.Isomorphisms
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : M
⊢ Eq.{u_3 + 1} (α := M₂) ((f.quotKerEquivOfSurjective hf : (a : M ⧸ f.ker) → M₂) (Submodule.Quotient.mk x) : M₂)
    ((f : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.LinearAlgebra.Isomorphisms
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
x : M
h : Membership.mem (α := M₂) f.range ((f : (a : M) → M₂) x : M₂)
⊢ Eq.{u_2 + 1} (α := M ⧸ f.ker)
    ((f.quotKerEquivRange.symm : (a : ↥f.range) → M ⧸ f.ker)
        (Subtype.mk (p := fun (x : M₂) ↦ x ∈ f.range) ((f : (a : M) → M₂) x) h) :
      M ⧸ f.ker)
    ((f.ker.mkQ : (a : M) → M ⧸ f.ker) x : M ⧸ f.ker)

Tactic:
f.quotKerEquivRange.symm_apply_apply ((LinearMap.ker f).mkQ x)

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.ker, LinearEquiv.symm_apply_apply, LinearMap.quotKerEquivRange, Submodule.mkQ, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Isomorphisms
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
x : M
⊢ Eq.{u_2 + 1} (α := M ⧸ f.ker)
    (((f.quotKerEquivOfSurjective hf).symm : (a : M₂) → M ⧸ f.ker) ((f : (a : M) → M₂) x) : M ⧸ f.ker)
    (Submodule.Quotient.mk x : M ⧸ f.ker)

Tactic:
simp [LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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
rw : comap p.subtype (p ⊓ p') ≤ comap p.subtype ((p ⊔ p') ⊓ p')
⊢ comap p.subtype (p ⊓ p') ≤ (subToSupQuotient p p').ker

Tactic:
rw [LinearMap.ker_comp, Submodule.inclusion, comap_codRestrict, ker_mkQ, map_comap_subtype]

Premises used: LinearMap.ker_comp, LinearMap.comap_codRestrict, Submodule.inclusion, Submodule.ker_mkQ, Submodule.map_comap_subtype
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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') ≤ comap p.subtype ((p ⊔ p') ⊓ p')

Tactic:
comap_mono (inf_le_inf_right _ le_sup_left)

Premises used: Submodule.comap_mono, le_sup_left, inf_le_inf_right
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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') ≤ comap p.subtype ((p ⊔ p') ⊓ p')

Tactic:
exact comap_mono (inf_le_inf_right _ le_sup_left)

Premises used: Submodule.comap_mono, le_sup_left, inf_le_inf_right
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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
h' : (subToSupQuotient p p').ker ≤ comap p.subtype (p ⊓ p')
⊢ 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')

Tactic:
rw [← ker_eq_bot, quotientInfToSupQuotient, ker_liftQ_eq_bot]

Premises used: LinearMap.ker_eq_bot, Submodule.ker_liftQ_eq_bot, LinearMap.quotientInfToSupQuotient
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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
h' : comap (inclusion ⋯) (comap (p ⊔ p').subtype p') ≤ comap p.subtype (p ⊓ p')
⊢ (subToSupQuotient p p').ker ≤ comap p.subtype (p ⊓ p')

Tactic:
rw [ker_comp, ker_mkQ]

Premises used: LinearMap.ker_comp, Submodule.ker_mkQ
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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 (inclusion ⋯) (comap (p ⊔ p').subtype p') ≤ comap p.subtype (p ⊓ p')

Tactic:
fun ⟨x, hx1⟩ hx2 => ⟨hx1, hx2⟩

Premises used: Membership.mem, Submodule.comap, And.intro, Submodule.subtype, _private.0.LinearMap.quotientInfEquivSupQuotient_injective.match_2, Min.min
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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 (inclusion ⋯) (comap (p ⊔ p').subtype p') ≤ comap p.subtype (p ⊓ p')

Tactic:
exact fun ⟨x, hx1⟩ hx2 => ⟨hx1, hx2⟩
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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
rw : ∀ (x : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'), x ∈ (subToSupQuotient p p').range
⊢ 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')

Tactic:
rw [← range_eq_top, quotientInfToSupQuotient, range_liftQ, eq_top_iff']

Premises used: Submodule.eq_top_iff', LinearMap.range_eq_top, LinearMap.quotientInfToSupQuotient, Submodule.range_liftQ
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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'
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
⊢ 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

Tactic:
rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩

Premises used: Iff.mp, Submodule.mem_sup, rfl
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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'
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))
⊢ 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:
use ⟨y, hy⟩
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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'
h :
  HSub.hSub (α := ↥(p ⊔ p'))
      ((inclusion ⋯ : (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'
⊢ 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:
apply (Submodule.Quotient.eq _).2

Premises used: Submodule.Quotient.eq, Iff.mpr
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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'
⊢ HSub.hSub (α := ↥(p ⊔ p'))
      ((inclusion ⋯ : (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:
simp only [mem_comap, map_sub, coe_subtype, coe_inclusion, sub_add_cancel_left, neg_mem_iff, hz]

Premises used: neg_mem_iff, map_sub, Submodule.mem_comap, Submodule.coe_inclusion, sub_add_cancel_left, Submodule.coe_subtype
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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
⊢ Eq (α := (a : ↥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')
    (⇑(quotientInfEquivSupQuotient p p') :
      (a : ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p') → ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, setOf, Set.inter, Submodule.comap, Set.preimage, Submodule.quotientRel, rfl
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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
⊢ let map : ↥p →ₗ[R] ↥(p ⊔ p') := inclusion ⋯;
  Eq (α := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
    ((quotientInfEquivSupQuotient p p' :
          (a : ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p') → ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
        (Submodule.Quotient.mk x) :
      ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
    (Submodule.Quotient.mk ((map : (a : ↥p) → ↥(p ⊔ p')) x) : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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')
hx : (↑x : M) ∈ p
rw :
  Eq (α := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p') (Submodule.Quotient.mk x)
    (Submodule.Quotient.mk ((inclusion ⋯ : (a : ↥p) → ↥(p ⊔ p')) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) (↑x : M) hx)))
rw₁ rw₂ :
  Eq (α := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p') (Submodule.Quotient.mk x)
    (Submodule.Quotient.mk
      (Subtype.mk (p := fun (x : M) ↦ x ∈ p ⊔ p') (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) (↑x : M) hx) : M) ⋯))
⊢ Eq (α := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p') (Submodule.Quotient.mk x)
    ((quotientInfEquivSupQuotient p p' :
        (a : ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p') → ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
      (Submodule.Quotient.mk (Subtype.mk (p := fun (x : M) ↦ x ∈ p) (↑x : M) hx)))

Tactic:
rw [quotientInfEquivSupQuotient_apply_mk, inclusion_apply]

Premises used: Submodule.inclusion_apply, LinearMap.quotientInfEquivSupQuotient_apply_mk
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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')
⊢ Eq (α := ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p') (Submodule.Quotient.mk x)
      ((quotientInfEquivSupQuotient p p' :
          (a : ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p') → ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p')
        0) ↔
    (↑x : M) ∈ p'

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Isomorphisms
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')
hx : (↑x : M) ∈ p'
⊢ Eq (α := ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p')
    (((quotientInfEquivSupQuotient p p').symm :
          (a : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p') → ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p')
        (Submodule.Quotient.mk x) :
      ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p')
    (0 : ↥p ⧸ comap p.subtype p ⊓ comap p.subtype p')

Tactic:
quotientInfEquivSupQuotient_symm_apply_eq_zero_iff.2 hx

Premises used: LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, Iff.mpr
-- Module: Mathlib.LinearAlgebra.Isomorphisms
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h_1 h : S ≤ T
x : M
hx : x ∈ (↑T : Set M)
⊢ Eq (α := M ⧸ T) (Quotient.mk ((LinearMap.id : (a : M) → M) x) : M ⧸ T) (0 : M ⧸ T)

Tactic:
(Quotient.mk_eq_zero _).mpr hx

Premises used: Iff.mpr, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.Isomorphisms
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h_1 h : S ≤ T
x : M
hx : x ∈ (↑T : Set M)
⊢ Eq (α := M ⧸ T) (Quotient.mk ((LinearMap.id : (a : M) → M) x) : M ⧸ T) (0 : M ⧸ T)

Tactic:
exact (Quotient.mk_eq_zero _).mpr hx

Premises used: Iff.mpr, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.Isomorphisms
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
h : S ≤ T
x : M ⧸ S
⊢ Eq (α := M ⧸ T)
    ((S.quotientQuotientEquivQuotientAux T h : (a : (M ⧸ S) ⧸ map S.mkQ T) → M ⧸ T) (Quotient.mk x) : M ⧸ T)
    ((S.mapQ T LinearMap.id h : (a : M ⧸ S) → M ⧸ T) x : M ⧸ T)

Tactic:
liftQ_apply _ _ _

Premises used: Submodule.liftQ_apply
-- Module: Mathlib.LinearAlgebra.Isomorphisms
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
h : S ≤ T
x : M
⊢ Eq (α := M ⧸ T)
    ((S.quotientQuotientEquivQuotientAux T h : (a : (M ⧸ S) ⧸ map S.mkQ T) → M ⧸ T) (Quotient.mk (Quotient.mk x)) :
      M ⧸ T)
    (Quotient.mk x : M ⧸ T)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.LinearAlgebra.Isomorphisms
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
x_1 : (M ⧸ S) ⧸ map S.mkQ T
x_2 : M ⧸ S
x : M
⊢ Eq (α := (M ⧸ S) ⧸ map S.mkQ T)
    ((T.mapQ (map S.mkQ T) S.mkQ ⋯ : (a : M ⧸ T) → (M ⧸ S) ⧸ map S.mkQ T)
        ((S.quotientQuotientEquivQuotientAux T h : (a : (M ⧸ S) ⧸ map S.mkQ T) → M ⧸ T) (Quotient.mk (Quotient.mk x))) :
      (M ⧸ S) ⧸ map S.mkQ T)
    (Quotient.mk (Quotient.mk x) : (M ⧸ S) ⧸ map S.mkQ T)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Isomorphisms
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
x_1 : M ⧸ T
x : M
⊢ Eq (α := M ⧸ T)
    ((S.quotientQuotientEquivQuotientAux T h : (a : (M ⧸ S) ⧸ map S.mkQ T) → M ⧸ T)
        ((T.mapQ (map S.mkQ T) S.mkQ ⋯ : (a : M ⧸ T) → (M ⧸ S) ⧸ map S.mkQ T) (Quotient.mk x)) :
      M ⧸ T)
    (Quotient.mk x : M ⧸ T)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Isomorphisms
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
rw : map S.mkQ T = map S.mkQ S ⊔ map S.mkQ T
rw₁ : map S.mkQ T = ⊥ ⊔ map S.mkQ T
rw₂ rw₃ : map S.mkQ T = map S.mkQ T
⊢ map S.mkQ T = map S.mkQ (S ⊔ T)

Tactic:
rw [map_sup, mkQ_map_self, bot_sup_eq]

Premises used: Submodule.map_sup, bot_sup_eq, Submodule.mkQ_map_self
-- Module: Mathlib.LinearAlgebra.Isomorphisms
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
hST : T ≤ S
rw :
  Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} (M ⧸ S) =
    Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} ((M ⧸ T) ⧸ map T.mkQ S)
rw₁ rw₂ :
  Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} (M ⧸ S) = Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} (M ⧸ S)
⊢ Nat.card.{u_2} ↥(map T.mkQ S) * Nat.card.{u_2} (M ⧸ S) = Nat.card.{u_2} (M ⧸ T)

Tactic:
rw [Submodule.card_eq_card_quotient_mul_card (map T.mkQ S),
    Nat.card_congr (quotientQuotientEquivQuotient T S hST).toEquiv]

Premises used: Submodule.quotientQuotientEquivQuotient, Nat.card_congr, LinearEquiv.toEquiv, Submodule.mkQ, Submodule.map, Submodule.card_eq_card_quotient_mul_card
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
h : HPow.hPow (α := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f]) k = 0
⊢ IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])

Tactic:
use k
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
h :
  ∀ (q : K[X]) (hq : P ^ k = minpoly K f * q), HPow.hPow (α := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f]) k = 0
⊢ HPow.hPow (α := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f]) k = 0

Tactic:
obtain ⟨q, hq⟩ := nil
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
q : K[X]
hq : P ^ k = minpoly K f * q
h : Eq.{u_2 + 1} (α := End K V) (↑((aeval ff : (a : K[X]) → ↥K[f]) (P ^ k)) : End K V) (↑0 : End K V)
⊢ HPow.hPow (α := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f]) k = 0

Tactic:
rw [← map_pow, Subtype.ext_iff]

Premises used: map_pow, Subtype.ext_iff
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
q : K[X]
hq : P ^ k = minpoly K f * q
⊢ Eq.{u_2 + 1} (α := End K V) (↑((aeval ff : (a : K[X]) → ↥K[f]) (P ^ k)) : End K V) (↑0 : End K V)

Tactic:
simp [ff, hq]
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
⊢ IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])

Tactic:
have nil' : IsNilpotent (aeval ff P) := by
    use k
    obtain ⟨q, hq⟩ := nil
    rw [← map_pow, Subtype.ext_iff]
    simp [ff, hq]
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
⊢ IsCoprime (P ^ k) P'

Tactic:
sep.pow_left

Premises used: IsCoprime.pow_left
-- Module: Mathlib.LinearAlgebra.JordanChevalley
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
P : K[X]
k : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k
ff : ↥K[f] := Subtype.mk (p := fun (x : End K V) ↦ Membership.mem (γ := Subalgebra K (End K V)) K[f] x) f ⋯
P' : K[X] := (derivative : (a : K[X]) → K[X]) P
nil' : IsNilpotent.{u_2} (R := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P : ↥K[f])
obtain :
  ∀ (a b : K[X]) (h : a * P ^ k + b * P' = 1), IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])
⊢ IsUnit.{u_2} (M := ↥K[f]) ((aeval ff : (a : K[X]) → ↥K[f]) P' : ↥K[f])

Tactic:
obtain ⟨a, b, h⟩ : IsCoprime (P ^ k) P' := sep.pow_left

Premises used: IsCoprime.pow_left, HPow.hPow, IsCoprime