awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
K : Type u_3
n : ℕ
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
h : x ∘ₗ f = 0
this :
  ∀ (K' : Submodule R K) (hK' : K'.FG),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K' ≤ (a ∘ₗ f).ker
⊢ ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ ⊤ ≤ (a ∘ₗ f).ker

Tactic:
this ⊤ Finite.fg_top

Premises used: Module.Finite.fg_top, Top.top
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
K : Type u_3
n : ℕ
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
h : x ∘ₗ f = 0
this :
  ∀ (K' : Submodule R K) (hK' : K'.FG),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K' ≤ (a ∘ₗ f).ker
h₁ : ∀ (x : ℕ) (x_1 : (Fin n →₀ R) →ₗ[R] Fin x →₀ R) (x_2 : (Fin x →₀ R) →ₗ[R] M), x_1 ∘ₗ f = 0 ↔ ⊤ ≤ (x_1 ∘ₗ f).ker
⊢ ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a ∘ₗ f = 0

Tactic:
convert! this ⊤ Finite.fg_top

Premises used: Module.Finite.fg_top, Top.top
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
K : Type u_3
n : ℕ
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
h : x ∘ₗ f = 0
this :
  ∀ (K' : Submodule R K) (hK' : K'.FG),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K' ≤ (a ∘ₗ f).ker
x_1 : ℕ
x_2 : (Fin n →₀ R) →ₗ[R] Fin x_1 →₀ R
x_3 : (Fin x_1 →₀ R) →ₗ[R] M
⊢ x_2 ∘ₗ f = 0 ↔ ⊤ ≤ (x_2 ∘ₗ f).ker

Tactic:
simp only [top_le_iff, ker_eq_top]

Premises used: LinearMap.ker_eq_top, top_le_iff
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
K : Type u_3
N : Type u_4
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Free R N
inst_10 : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card.{u_4} (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
h₁ :
  ∀ (x_1 : K),
    Eq.{u_2 + 1} (α := M)
      (((x ∘ₗ (↑e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] N)) ∘ₗ
              (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ∘ₗ f :
            (a : K) → M)
          x_1 :
        M)
      ((0 : (a : K) → M) x_1 : M)
⊢ (x ∘ₗ (↑e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] N)) ∘ₗ
      (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ∘ₗ f =
    0

Tactic:
ext
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
K : Type u_3
N : Type u_4
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Free R N
inst_10 : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card.{u_4} (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
x_1 : K
⊢ Eq.{u_2 + 1} (α := M)
    (((x ∘ₗ (↑e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] N)) ∘ₗ
            (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ∘ₗ f :
          (a : K) → M)
        x_1 :
      M)
    ((0 : (a : K) → M) x_1 : M)

Tactic:
simpa [comp_assoc] using congr($h _)

Premises used: LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
K : Type u_3
N : Type u_4
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Free R N
inst_10 : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card.{u_4} (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card.{u_4} (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ (↑e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] N) = y ∘ₗ a
haf : a ∘ₗ (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ∘ₗ f = 0
rwa : x = (y ∘ₗ a) ∘ₗ (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R)
rwa₁ rwa₂ rwa₃ rwa₄ : x ∘ₗ (↑e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] N) = y ∘ₗ a
⊢ x = y ∘ₗ a ∘ₗ (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R)

Tactic:
rwa [← comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]

Premises used: LinearMap.comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
K : Type u_3
N : Type u_4
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Free R N
inst_10 : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card.{u_4} (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card.{u_4} (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ (↑e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] N) = y ∘ₗ a
haf rwa rwa₁ rwa₂ rwa₃ : a ∘ₗ (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ∘ₗ f = 0
⊢ (a ∘ₗ (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R)) ∘ₗ f = 0

Tactic:
rwa [comp_assoc]

Premises used: LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
have :
  ∀ (w : ℕ) (K : Submodule R (Fin w → R)) (ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K) (hK : K.FG),
    ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂
⊢ ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂

Tactic:
have ⟨_, K, ϕ, hK⟩ := FinitePresentation.exists_fin R P
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
⊢ Module.Finite R ↥K

Tactic:
haveI : Module.Finite R K := .of_fg hK
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this : Module.Finite R ↥K
simp_rw : Eq (α := ↥K →ₗ[R] M) (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ ∘ₗ K.subtype) 0
simp_rw₁ : Eq (α := ↥K →ₗ[R] M) (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ 0) 0
⊢ (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0

Tactic:
simp_rw [comp_assoc, (LinearMap.exact_subtype_mkQ K).linearMap_comp_eq_zero, comp_zero]

Premises used: LinearMap.exact_subtype_mkQ, LinearMap.comp_assoc, LinearMap.comp_zero, Function.Exact.linearMap_comp_eq_zero
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this : Module.Finite R ↥K
⊢ (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0

Tactic:
have : (h₁ ∘ₗ ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0 := by
    simp_rw [comp_assoc, (LinearMap.exact_subtype_mkQ K).linearMap_comp_eq_zero, comp_zero]
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this_1 : Module.Finite R ↥K
this : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
obtain :
  ∀ (k : ℕ) (a : (Fin w → R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M)
    (hay : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ = y ∘ₗ a) (ha : a ∘ₗ K.subtype = 0),
    ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂
⊢ ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂

Tactic:
obtain ⟨k, a, y, hay, ha⟩ := exists_factorization_of_comp_eq_zero_of_free this

Premises used: Module.Flat.exists_factorization_of_comp_eq_zero_of_free
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this_1 : Module.Finite R ↥K
this : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
rwa : ∀ (ha : K.subtype.range ≤ a.ker), K ≤ a.ker
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (ha : K ≤ a.ker), K ≤ a.ker
⊢ K ≤ a.ker

Tactic:
rwa [← range_le_ker_iff, Submodule.range_subtype] at ha

Premises used: Submodule.range_subtype, LinearMap.range_le_ker_iff
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this_1 : Module.Finite R ↥K
this : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
h :
  h₁ =
    y ∘ₗ
      Submodule.liftQ.{u_1, u_1, u_1, u_1} (R := R) (M := Fin w → R) K (R₂ := R) (M₂ := Fin k →₀ R) (τ₁₂ :=
          RingHom.id R) a ⋯ ∘ₗ
        (↑ϕ : P →ₗ[R] (Fin w → R) ⧸ K)
⊢ ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂

Tactic:
use k, (K.liftQ a (by rwa [← range_le_ker_iff, Submodule.range_subtype] at ha)) ∘ₗ ϕ, y

Premises used: Submodule.liftQ
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this_1 : Module.Finite R ↥K
this : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
h :
  h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) =
    (y ∘ₗ
        Submodule.liftQ.{u_1, u_1, u_1, u_1} (R := R) (M := Fin w → R) K (R₂ := R) (M₂ := Fin k →₀ R) (τ₁₂ :=
            RingHom.id R) a ⋯ ∘ₗ
          (↑ϕ : P →ₗ[R] (Fin w → R) ⧸ K)) ∘ₗ
      (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P)
⊢ h₁ =
    y ∘ₗ
      Submodule.liftQ.{u_1, u_1, u_1, u_1} (R := R) (M := Fin w → R) K (R₂ := R) (M₂ := Fin k →₀ R) (τ₁₂ :=
          RingHom.id R) a ⋯ ∘ₗ
        (↑ϕ : P →ₗ[R] (Fin w → R) ⧸ K)

Tactic:
apply (cancel_right ϕ.symm.surjective).mp

Premises used: LinearEquiv.symm, LinearEquiv.surjective, LinearMap.cancel_right, Iff.mp
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this_1 : Module.Finite R ↥K
this : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
h :
  (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P)) ∘ₗ K.mkQ =
    ((y ∘ₗ
          Submodule.liftQ.{u_1, u_1, u_1, u_1} (R := R) (M := Fin w → R) K (R₂ := R) (M₂ := Fin k →₀ R) (τ₁₂ :=
              RingHom.id R) a ⋯ ∘ₗ
            (↑ϕ : P →ₗ[R] (Fin w → R) ⧸ K)) ∘ₗ
        (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P)) ∘ₗ
      K.mkQ
⊢ h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) =
    (y ∘ₗ
        Submodule.liftQ.{u_1, u_1, u_1, u_1} (R := R) (M := Fin w → R) K (R₂ := R) (M₂ := Fin k →₀ R) (τ₁₂ :=
            RingHom.id R) a ⋯ ∘ₗ
          (↑ϕ : P →ₗ[R] (Fin w → R) ⧸ K)) ∘ₗ
      (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P)

Tactic:
apply (cancel_right K.mkQ_surjective).mp

Premises used: LinearMap.cancel_right, Iff.mp, Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this_1 : Module.Finite R ↥K
this : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
⊢ (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P)) ∘ₗ K.mkQ =
    ((y ∘ₗ
          Submodule.liftQ.{u_1, u_1, u_1, u_1} (R := R) (M := Fin w → R) K (R₂ := R) (M₂ := Fin k →₀ R) (τ₁₂ :=
              RingHom.id R) a ⋯ ∘ₗ
            (↑ϕ : P →ₗ[R] (Fin w → R) ⧸ K)) ∘ₗ
        (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P)) ∘ₗ
      K.mkQ

Tactic:
simpa [comp_assoc]

Premises used: LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : FinitePresentation R M
⊢ Projective R M

Tactic:
have ⟨_, f, g, eq⟩ := exists_factorization_of_finitePresentation (.id (R := R) (M := M))
  .of_split f g eq.symm

Premises used: LinearMap.id, Module.Projective, Module.Projective.of_split, Eq.symm, _private.0.Module.Flat.projective_of_finitePresentation.match_1, Module.Flat.exists_factorization_of_finitePresentation
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
⊢ FaithfullyFlat A B

Tactic:
⟨fun m hm ↦ ?_⟩

Premises used: Module.FaithfullyFlat.mk
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
refine : ∀ (m : Ideal A) (hm : m.IsMaximal), HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤
⊢ FaithfullyFlat A B

Tactic:
refine ⟨fun m hm ↦ ?_⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
obtain :
  ∀ (m' : PrimeSpectrum B)
    (hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ : PrimeSpectrum A }),
    HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤
⊢ HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤

Tactic:
obtain ⟨m', hm'⟩ := h ⟨m, hm.isPrime⟩

Premises used: PrimeSpectrum.mk, Ideal.IsMaximal.isPrime
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ : PrimeSpectrum A }
rw : m = PrimeSpectrum.asIdeal (PrimeSpectrum.comap (algebraMap A B) m')
rw₁ rw₂ : m = { asIdeal := m, isPrime := ⋯ }.asIdeal
⊢ m = Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal

Tactic:
rw [← PrimeSpectrum.comap_asIdeal (algebraMap A B) m', hm']

Premises used: Algebra.algebraMap, PrimeSpectrum.comap_asIdeal
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ : PrimeSpectrum A }
⊢ m = Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal

Tactic:
have : m = Ideal.comap (algebraMap A B) m'.asIdeal := by
    rw [← PrimeSpectrum.comap_asIdeal (algebraMap A B) m', hm']
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ : PrimeSpectrum A }
this : m = Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal
rw :
  Ne.{u_2 + 1} (α := Submodule A B)
    (Submodule.restrictScalars A
      (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal)))
    ⊤
⊢ HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤

Tactic:
rw [Ideal.smul_top_eq_map, this]

Premises used: Ideal.smul_top_eq_map
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ : PrimeSpectrum A }
this : m = Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal
⊢ Ne.{u_2 + 1} (α := Submodule A B)
    (Submodule.restrictScalars A
      (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal)))
    ⊤

Tactic:
(Submodule.restrictScalars_eq_top_iff _ _ _).ne.mpr
    fun top ↦ m'.isPrime.ne_top <| top_le_iff.mp <| top ▸ Ideal.map_comap_le

Premises used: Iff.mpr, PrimeSpectrum.isPrime, Eq.rec, Iff.ne, top_le_iff, Iff.mp, Submodule.restrictScalars_eq_top_iff, Ideal.map_comap_le, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Flat A B
h : Function.Surjective (α := PrimeSpectrum B) (β := PrimeSpectrum A) (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ : PrimeSpectrum A }
this : m = Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal
⊢ Ne.{u_2 + 1} (α := Submodule A B)
    (Submodule.restrictScalars A
      (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.comap (F := A →+* B) (algebraMap A B) m'.asIdeal)))
    ⊤

Tactic:
exact (Submodule.restrictScalars_eq_top_iff _ _ _).ne.mpr
    fun top ↦ m'.isPrime.ne_top <| top_le_iff.mp <| top ▸ Ideal.map_comap_le

Premises used: Iff.mpr, PrimeSpectrum.isPrime, Eq.rec, Iff.ne, top_le_iff, Iff.mp, Submodule.restrictScalars_eq_top_iff, Ideal.map_comap_le, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsLocalRing A
inst_4 : IsLocalRing B
inst_5 : Flat A B
inst_6 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
⊢ FaithfullyFlat A B

Tactic:
⟨fun m hm ↦ ?_⟩

Premises used: Module.FaithfullyFlat.mk
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsLocalRing A
inst_4 : IsLocalRing B
inst_5 : Flat A B
inst_6 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
refine : ∀ (m : Ideal A) (hm : m.IsMaximal), HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤
⊢ FaithfullyFlat A B

Tactic:
refine ⟨fun m hm ↦ ?_⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsLocalRing A
inst_4 : IsLocalRing B
inst_5 : Flat A B
inst_6 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
rw :
  Ne.{u_2 + 1} (α := Submodule A B)
    (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) (IsLocalRing.maximalIdeal A))) ⊤
⊢ HSMul.hSMul (β := Submodule A B) m ⊤ ≠ ⊤

Tactic:
rw [Ideal.smul_top_eq_map, IsLocalRing.eq_maximalIdeal hm]

Premises used: Ideal.smul_top_eq_map, IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsLocalRing A
inst_4 : IsLocalRing B
inst_5 : Flat A B
inst_6 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
by_contra :
  ∀
    (eqt :
      Eq.{u_2 + 1} (α := Submodule A B)
        (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) (IsLocalRing.maximalIdeal A))) ⊤),
    False
⊢ Ne.{u_2 + 1} (α := Submodule A B)
    (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) (IsLocalRing.maximalIdeal A))) ⊤

Tactic:
by_contra eqt
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsLocalRing A
inst_4 : IsLocalRing B
inst_5 : Flat A B
inst_6 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
m : Ideal A
hm : m.IsMaximal
eqt :
  Eq.{u_2 + 1} (α := Submodule A B)
    (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) (IsLocalRing.maximalIdeal A))) ⊤
⊢ LE.le (α := Submodule A B)
    (Submodule.restrictScalars A (Ideal.map (F := A →+* B) (algebraMap A B) (IsLocalRing.maximalIdeal A)))
    (Submodule.restrictScalars A (IsLocalRing.maximalIdeal B))

Tactic:
have : Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)) ≤
      Submodule.restrictScalars A (IsLocalRing.maximalIdeal B) :=
    ((IsLocalRing.local_hom_TFAE (algebraMap A B)).out 0 2).mp ‹_›